diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 1e258498..4ec81a22 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -41,3 +41,6 @@ jobs:
 
       - name: Build
         run: opam exec -- dune build @install
+
+      - name: Test
+        run: opam exec -- dune runtest
diff --git a/example/dune b/example/dune
index bd271219..91da71b3 100644
--- a/example/dune
+++ b/example/dune
@@ -3,6 +3,7 @@
  (libraries smtml))
 
 (cram
+ (enabled_if %{lib-available:z3})
  (deps
   ./product_mix.exe
   (source_tree test)))
diff --git a/lib/optimizer.mli b/lib/optimizer.mli
index ee669738..ac7670a6 100644
--- a/lib/optimizer.mli
+++ b/lib/optimizer.mli
@@ -16,4 +16,5 @@
 (* along with this program.  If not, see <https://www.gnu.org/licenses/>.  *)
 (***************************************************************************)
 
-include Optimizer_intf.Intf (** @inline *)
+(** @inline *)
+include Optimizer_intf.Intf
diff --git a/test/dune b/test/dune
index 5c3b1fe6..20812e82 100644
--- a/test/dune
+++ b/test/dune
@@ -6,13 +6,16 @@
   test_harness
   test_solver_params
   test_solver
-  test_lia)
+  test_lia
+  test_lra
+  test_optimizer)
  (libraries smtml))
 
 (test
  (name test_z3)
  (modules test_z3)
- (libraries smtml smtml_tests))
+ (libraries smtml smtml_tests)
+ (build_if %{lib-available:z3}))
 
 (test
  (name test_colibri2)
diff --git a/test/parser/dune b/test/parser/dune
index aaaa8b1f..25fb1e17 100644
--- a/test/parser/dune
+++ b/test/parser/dune
@@ -1,4 +1,5 @@
 (cram
+ (enabled_if %{lib-available:z3})
  (deps
   %{bin:smtml}
   test_core.smtml
diff --git a/test/regression/dune b/test/regression/dune
index 4e55867e..849f7fae 100644
--- a/test/regression/dune
+++ b/test/regression/dune
@@ -1,4 +1,5 @@
 (cram
+ (enabled_if %{lib-available:z3})
  (deps %{bin:smtml} test_pr_71.smtml))
 
 (tests
diff --git a/test/test_lra.ml b/test/test_lra.ml
new file mode 100644
index 00000000..ea9168b3
--- /dev/null
+++ b/test/test_lra.ml
@@ -0,0 +1,18 @@
+open Smtml
+
+module Make (M : Mappings_intf.S) = struct
+  module Solver = Solver.Batch (M)
+
+  let () =
+    let solver = Solver.create () in
+    assert (
+      let x = Expr.mk_symbol Symbol.("x" @: Ty_real) in
+      let y = Expr.mk_symbol Symbol.("y" @: Ty_real) in
+      let c0 = Expr.relop Ty_bool Eq x y in
+      let c1 =
+        Expr.relop Ty_bool Eq
+          (Expr.cvtop Ty_real ToString x)
+          (Expr.cvtop Ty_real ToString y)
+      in
+      `Sat = Solver.check solver [ c0; c1 ] )
+end
diff --git a/test/test_optimizer.ml b/test/test_optimizer.ml
new file mode 100644
index 00000000..417cc988
--- /dev/null
+++ b/test/test_optimizer.ml
@@ -0,0 +1,15 @@
+open Smtml
+
+module Make (M : Mappings_intf.S) = struct
+  open Test_harness
+  module Optimizer = Optimizer.Make (M)
+
+  let () =
+    let open Infix in
+    let opt = Optimizer.create () in
+    let x = symbol "x" Ty_int in
+    Optimizer.add opt Int.[ x >= int 0; x < int 5 ];
+    Optimizer.protect opt (fun () ->
+        assert (Stdlib.(Some (Value.Int 0) = Optimizer.minimize opt x)) );
+    assert (Stdlib.(Some (Value.Int 4) = Optimizer.maximize opt x))
+end
diff --git a/test/test_z3.ml b/test/test_z3.ml
index 80f8e741..4de68842 100644
--- a/test/test_z3.ml
+++ b/test/test_z3.ml
@@ -5,6 +5,8 @@ let () = assert Z3_mappings.is_available
 
 module Test_solver_params = Test_solver_params.Make (Z3_mappings.Fresh.Make ())
 module Test_solver = Test_solver.Make (Z3_mappings.Fresh.Make ())
+module Test_optimizer = Test_optimizer.Make (Z3_mappings.Fresh.Make ())
 module Test_bv = Test_bv.Make (Z3_mappings.Fresh.Make ())
 module Test_fp = Test_fp.Make (Z3_mappings.Fresh.Make ())
 module Test_lia = Test_lia.Make (Z3_mappings.Fresh.Make ())
+module Test_lra = Test_lra.Make (Z3_mappings.Fresh.Make ())
diff --git a/test/unit/dune b/test/unit/dune
index 2557140d..60e56fdb 100644
--- a/test/unit/dune
+++ b/test/unit/dune
@@ -1,8 +1,6 @@
 (tests
  (names
   test_expr_hc
-  test_optimizer
-  test_real
   test_simplify
   test_unop
   test_binop
diff --git a/test/unit/test_optimizer.ml b/test/unit/test_optimizer.ml
deleted file mode 100644
index 020a35f8..00000000
--- a/test/unit/test_optimizer.ml
+++ /dev/null
@@ -1,19 +0,0 @@
-open Smtml
-open Ty
-open Expr
-module Optimizer = Optimizer.Z3
-
-let v i = value (Int i)
-
-let ( >= ) i1 i2 = relop Ty_int Ge i1 i2
-
-let ( < ) i1 i2 = relop Ty_int Lt i1 i2
-
-let () =
-  let opt = Optimizer.create () in
-  let x = mk_symbol Symbol.("x" @: Ty_int) in
-  Optimizer.add opt [ x >= v 0; x < v 5 ];
-  Optimizer.push opt;
-  assert (Some (Value.Int 0) = Optimizer.minimize opt x);
-  Optimizer.pop opt;
-  assert (Some (Value.Int 4) = Optimizer.maximize opt x)
diff --git a/test/unit/test_real.ml b/test/unit/test_real.ml
deleted file mode 100644
index f812d712..00000000
--- a/test/unit/test_real.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-open Smtml
-module Solver = Solver.Z3_batch
-
-let solver = Solver.create ()
-
-let () =
-  assert (
-    let x = Expr.mk_symbol Symbol.("x" @: Ty_real) in
-    let y = Expr.mk_symbol Symbol.("y" @: Ty_real) in
-    let c0 = Expr.relop Ty_bool Eq x y in
-    let c1 =
-      Expr.relop Ty_bool Eq
-        (Expr.cvtop Ty_real ToString x)
-        (Expr.cvtop Ty_real ToString y)
-    in
-    `Sat = Solver.check solver [ c0; c1 ] )