From 7f1417e8bbf2cf76b25e6f6ed436abeb24cefc28 Mon Sep 17 00:00:00 2001
From: Filipe Marques <filipe.s.marques@tecnico.ulisboa.pt>
Date: Sun, 2 Mar 2025 22:45:49 +0000
Subject: [PATCH] Refactor solver tests

---
 test/regression/dune                          |   4 -
 test/regression/test_pr_77.ml                 |  28 ----
 test/solver/dune                              |  40 ++---
 test/solver/test_altergo.ml                   |  16 --
 test/solver/test_bitwuzla.ml                  |  10 --
 test/solver/test_bv.ml                        |  32 ----
 test/solver/test_colibri2.ml                  |  14 --
 test/solver/test_cvc5.ml                      |  10 --
 test/solver/test_fp.ml                        |  51 ------
 test/solver/test_harness.ml                   |  53 ------
 test/solver/test_lia.ml                       |  14 --
 test/solver/test_lra.ml                       |  18 --
 test/solver/test_optimizer.ml                 |   5 +-
 test/solver/test_solver.ml                    | 154 ++++++++++++++++--
 ....expected => test_solver_altergo.expected} |   0
 test/solver/test_solver_altergo.ml            |  12 ++
 ...expected => test_solver_bitwuzla.expected} |   0
 test/solver/test_solver_bitwuzla.ml           |   9 +
 ...expected => test_solver_colibri2.expected} |   0
 test/solver/test_solver_colibri2.ml           |  12 ++
 ...vc5.expected => test_solver_cvc5.expected} |   0
 test/solver/test_solver_cvc5.ml               |  10 ++
 test/solver/test_solver_params.ml             |  21 ---
 ...st_z3.expected => test_solver_z3.expected} |   0
 test/solver/test_solver_z3.ml                 |  16 ++
 test/solver/test_z3.ml                        |  14 --
 26 files changed, 220 insertions(+), 323 deletions(-)
 delete mode 100644 test/regression/test_pr_77.ml
 delete mode 100644 test/solver/test_altergo.ml
 delete mode 100644 test/solver/test_bitwuzla.ml
 delete mode 100644 test/solver/test_bv.ml
 delete mode 100644 test/solver/test_colibri2.ml
 delete mode 100644 test/solver/test_cvc5.ml
 delete mode 100644 test/solver/test_fp.ml
 delete mode 100644 test/solver/test_harness.ml
 delete mode 100644 test/solver/test_lia.ml
 delete mode 100644 test/solver/test_lra.ml
 rename test/solver/{test_altergo.expected => test_solver_altergo.expected} (100%)
 create mode 100644 test/solver/test_solver_altergo.ml
 rename test/solver/{test_bitwuzla.expected => test_solver_bitwuzla.expected} (100%)
 create mode 100644 test/solver/test_solver_bitwuzla.ml
 rename test/solver/{test_colibri2.expected => test_solver_colibri2.expected} (100%)
 create mode 100644 test/solver/test_solver_colibri2.ml
 rename test/solver/{test_cvc5.expected => test_solver_cvc5.expected} (100%)
 create mode 100644 test/solver/test_solver_cvc5.ml
 delete mode 100644 test/solver/test_solver_params.ml
 rename test/solver/{test_z3.expected => test_solver_z3.expected} (100%)
 create mode 100644 test/solver/test_solver_z3.ml
 delete mode 100644 test/solver/test_z3.ml

diff --git a/test/regression/dune b/test/regression/dune
index a3d1e4bf..640b9765 100644
--- a/test/regression/dune
+++ b/test/regression/dune
@@ -6,7 +6,3 @@
  (applies_to test_issue_183)
  (enabled_if
   (not %{lib-available:colibri2.core})))
-
-(tests
- (names test_pr_77)
- (libraries smtml))
diff --git a/test/regression/test_pr_77.ml b/test/regression/test_pr_77.ml
deleted file mode 100644
index 67b51fef..00000000
--- a/test/regression/test_pr_77.ml
+++ /dev/null
@@ -1,28 +0,0 @@
-open Smtml
-
-let () =
-  let open Num in
-  let nan0 = F32 (Int32.bits_of_float Float.nan) in
-  let nan1 = F32 (Int32.bits_of_float Float.nan) in
-  (* Library functions ensure total order of floats. *)
-  assert (Num.equal nan0 nan1)
-
-let () =
-  let open Expr.Fpa in
-  let nan0 = F32.v Float.nan in
-  let nan1 = F32.v Float.nan in
-  (* Library functions ensure total order of floats. *)
-  assert (Expr.equal nan0 nan1);
-  let assert_ = Expr.relop (Ty_fp 32) Eq nan0 nan1 in
-  (* Evaluation functions do not. *)
-  assert (Expr.equal assert_ (Expr.value False))
-
-let () =
-  let open Expr in
-  let nan0 = value (Real Float.nan) in
-  let nan1 = value (Real Float.nan) in
-  (* Library functions ensure total order of floats. *)
-  assert (Expr.equal nan0 nan1);
-  let assert_ = Expr.relop Ty_real Eq nan0 nan1 in
-  (* Evaluation functions do not. *)
-  assert (Expr.equal assert_ (Expr.value False))
diff --git a/test/solver/dune b/test/solver/dune
index daa3e810..677eb998 100644
--- a/test/solver/dune
+++ b/test/solver/dune
@@ -1,43 +1,37 @@
 (library
- (name smtml_tests)
+ (name smtml_test_solver)
  (modules
-  test_bv
-  test_fp
-  test_harness
-  test_solver_params
   test_solver
-  test_lia
-  test_lra
   test_optimizer)
- (libraries smtml))
+ (libraries smtml smtml_test))
 
 (test
- (name test_z3)
- (modules test_z3)
- (libraries smtml smtml_tests)
+ (name test_solver_z3)
+ (modules test_solver_z3)
+ (libraries smtml smtml_test_solver)
  (build_if %{lib-available:z3}))
 
 (test
- (name test_colibri2)
- (modules test_colibri2)
- (libraries smtml_tests)
+ (name test_solver_colibri2)
+ (modules test_solver_colibri2)
+ (libraries smtml_test smtml_test_solver)
  (build_if %{lib-available:colibri2.core}))
 
 (test
- (name test_bitwuzla)
- (modules test_bitwuzla)
- (libraries smtml_tests)
+ (name test_solver_bitwuzla)
+ (modules test_solver_bitwuzla)
+ (libraries smtml_test smtml_test_solver)
  (build_if %{lib-available:bitwuzla-cxx}))
 
 (test
- (name test_cvc5)
- (modules test_cvc5)
- (libraries smtml_tests)
+ (name test_solver_cvc5)
+ (modules test_solver_cvc5)
+ (libraries smtml_test smtml_test_solver)
  (build_if %{lib-available:cvc5}))
 
 (test
- (name test_altergo)
- (modules test_altergo)
- (libraries smtml_tests)
+ (name test_solver_altergo)
+ (modules test_solver_altergo)
+ (libraries smtml_test smtml_test_solver)
  (build_if
   (and %{lib-available:alt-ergo-lib} %{lib-available:dolmen_model})))
diff --git a/test/solver/test_altergo.ml b/test/solver/test_altergo.ml
deleted file mode 100644
index a54dfd0a..00000000
--- a/test/solver/test_altergo.ml
+++ /dev/null
@@ -1,16 +0,0 @@
-open Smtml
-open Smtml_tests
-
-let () =
-  Printexc.record_backtrace true;
-  assert Altergo_mappings.is_available;
-  let module Test_solver_params =
-    Test_solver_params.Make (Altergo_mappings.Fresh.Make ()) in
-  let module Test_solver = Test_solver.Make (Altergo_mappings.Fresh.Make ()) in
-  (* let module Test_optimizer =
-     Test_optimizer.Make (Altergo_mappings.Fresh.Make ()) in *)
-  let module Test_bv = Test_bv.Make (Altergo_mappings.Fresh.Make ()) in
-  (* let module Test_fp = Test_fp.Make (Altergo_mappings.Fresh.Make ()) in *)
-  let module Test_lia = Test_lia.Make (Altergo_mappings.Fresh.Make ()) in
-  (* let module Test_lra = Test_lra.Make (Altergo_mappings.Fresh.Make ()) in *)
-  ()
diff --git a/test/solver/test_bitwuzla.ml b/test/solver/test_bitwuzla.ml
deleted file mode 100644
index 7b01fecb..00000000
--- a/test/solver/test_bitwuzla.ml
+++ /dev/null
@@ -1,10 +0,0 @@
-open Smtml
-open Smtml_tests
-
-let () =
-  assert Bitwuzla_mappings.is_available;
-  let module Test_solver_params =
-    Test_solver_params.Make (Bitwuzla_mappings.Fresh.Make ()) in
-  let module Test_bv = Test_bv.Make (Bitwuzla_mappings) in
-  let module Test_fp = Test_fp.Make (Bitwuzla_mappings) in
-  ()
diff --git a/test/solver/test_bv.ml b/test/solver/test_bv.ml
deleted file mode 100644
index ed098888..00000000
--- a/test/solver/test_bv.ml
+++ /dev/null
@@ -1,32 +0,0 @@
-open Smtml
-open Test_harness
-
-module Make (M : Mappings_intf.S) = struct
-  open Test_harness.Infix
-  module I8 = Expr.Bitv.I8
-  module I32 = Expr.Bitv.I32
-  module Solver = Solver.Incremental (M)
-
-  let params = Params.default ()
-
-  let () =
-    let solver = Solver.create ~params ~logic:QF_BVFP () in
-    let x = Expr.symbol @@ Symbol.make (Ty_bitv 8) "h" in
-    Solver.add solver I8.[ x > v 0; x < v 2 ];
-    assert_sat (Solver.check solver []);
-    let val_x = Solver.get_value solver x in
-    assert (Expr.equal val_x (I8.v 1))
-
-  let () =
-    let solver = Solver.create ~params ~logic:QF_BVFP () in
-    let x = Expr.symbol @@ Symbol.make (Ty_bitv 32) "x" in
-    let y = Expr.symbol @@ Symbol.make (Ty_bitv 32) "y" in
-    let z = Expr.symbol @@ Symbol.make (Ty_bitv 32) "z" in
-    let w = Expr.symbol @@ Symbol.make (Ty_bitv 32) "w" in
-    Solver.add solver I32.[ x > v 0l && w < v 5l ];
-    Solver.add solver I32.[ x < y && y < z && z < w ];
-    assert_sat (Solver.check solver []);
-    match Solver.model solver with
-    | None -> assert false
-    | Some m -> Model.pp Format.std_formatter ~no_values:false m
-end
diff --git a/test/solver/test_colibri2.ml b/test/solver/test_colibri2.ml
deleted file mode 100644
index e55a27c9..00000000
--- a/test/solver/test_colibri2.ml
+++ /dev/null
@@ -1,14 +0,0 @@
-open Smtml
-open Smtml_tests
-
-let () =
-  assert Colibri2_mappings.is_available;
-  let module Test_solver_params = Test_solver_params.Make (Colibri2_mappings) in
-  let module Test_solver = Test_solver.Make (Colibri2_mappings) in
-  (* let module Test_optimizer =
-     Test_optimizer.Make (Altergo_mappings.Fresh.Make ()) in *)
-  let module Test_bv = Test_bv.Make (Colibri2_mappings) in
-  let module Test_fp = Test_fp.Make (Colibri2_mappings) in
-  let module Test_lia = Test_lia.Make (Colibri2_mappings) in
-  (* let module Test_lra = Test_lra.Make (Altergo_mappings.Fresh.Make ()) in *)
-  ()
diff --git a/test/solver/test_cvc5.ml b/test/solver/test_cvc5.ml
deleted file mode 100644
index c7284fb4..00000000
--- a/test/solver/test_cvc5.ml
+++ /dev/null
@@ -1,10 +0,0 @@
-open Smtml
-open Smtml_tests
-
-let () =
-  assert Cvc5_mappings.is_available;
-  let module Test_solver_params =
-    Test_solver_params.Make (Cvc5_mappings.Fresh.Make ()) in
-  let module Test_bv = Test_bv.Make (Cvc5_mappings) in
-  (* let module Test_fp = Test_fp.Make (Cvc5_mappings) in *)
-  ()
diff --git a/test/solver/test_fp.ml b/test/solver/test_fp.ml
deleted file mode 100644
index ab9ff72c..00000000
--- a/test/solver/test_fp.ml
+++ /dev/null
@@ -1,51 +0,0 @@
-open Smtml
-open Test_harness
-
-module Make (M : Mappings_intf.S) = struct
-  module Solver = Solver.Incremental (M)
-  module F32 = Expr.Fpa.F32
-  module F64 = Expr.Fpa.F64
-
-  (* Regression for get value *)
-  let () =
-    let solver = Solver.create ~logic:QF_BVFP () in
-    let x = F32.sym "x" in
-    let const = F32.v 50.0 in
-    Solver.add solver F32.[ x = const ];
-    assert_sat (Solver.check solver []);
-    assert (Expr.equal (Solver.get_value solver x) const)
-
-  let () =
-    let solver = Solver.create ~logic:QF_BVFP () in
-    let x = F64.sym "x" in
-    let const = F64.v 50.0 in
-    Solver.add solver F64.[ x = const ];
-    assert_sat (Solver.check solver []);
-    assert (Expr.equal (Solver.get_value solver x) const)
-
-  (* Sqrt *)
-  let () =
-    let solver = Solver.create ~logic:QF_BVFP () in
-    let x = F32.sym "x" in
-    Solver.add solver F32.[ x = F32.v 4.0 ];
-    Solver.add solver F32.[ Expr.unop (Ty_fp 32) Sqrt x = F32.v 2.0 ];
-    assert_sat (Solver.check solver []);
-    assert (Expr.equal (Solver.get_value solver x) (F32.v 4.0))
-
-  (* Copysign *)
-  let () =
-    let solver = Solver.create ~logic:QF_BVFP () in
-    let x = F32.sym "x" in
-    let y = F32.sym "y" in
-    Solver.add solver F32.[ x > v 0.0; y < v 0.0 ];
-    Solver.add solver F32.[ Expr.binop (Ty_fp 32) Copysign x y < v 0.0 ];
-    assert_sat (Solver.check solver [])
-
-  let () =
-    let solver = Solver.create ~logic:QF_BVFP () in
-    let x = F64.sym "x" in
-    let y = F64.sym "y" in
-    Solver.add solver F64.[ x > v 0.0; y < v 0.0 ];
-    Solver.add solver F64.[ Expr.binop (Ty_fp 64) Copysign x y < v 0.0 ];
-    assert_sat (Solver.check solver [])
-end
diff --git a/test/solver/test_harness.ml b/test/solver/test_harness.ml
deleted file mode 100644
index cab1487f..00000000
--- a/test/solver/test_harness.ml
+++ /dev/null
@@ -1,53 +0,0 @@
-open Smtml
-open Expr
-
-let assert_sat result =
-  assert (
-    match result with
-    | `Sat -> true
-    | `Unsat -> false
-    | `Unknown -> failwith "Solver returned unknown" )
-
-module Infix = struct
-  let int i = value (Int i)
-
-  let symbol name ty = symbol (Symbol.make ty name)
-
-  let ( = ) i1 i2 = relop Ty_bool Eq i1 i2
-
-  let ( <> ) i1 i2 = relop Ty_bool Ne i1 i2
-
-  let ( && ) b1 b2 = binop Ty_bool And b1 b2
-
-  let ( || ) b1 b2 = binop Ty_bool Or b1 b2
-
-  let ( => ) b1 b2 =
-    let left = unop Ty_bool Not b1 in
-    binop Ty_bool Or left b2
-
-  module Int = struct
-    let ( ~- ) i = unop Ty_int Neg i
-
-    let ( + ) i1 i2 = binop Ty_int Add i1 i2
-
-    let ( - ) i1 i2 = binop Ty_int Sub i1 i2
-
-    let ( * ) i1 i2 = binop Ty_int Mul i1 i2
-
-    let ( / ) i1 i2 = binop Ty_int Div i1 i2
-
-    let ( % ) i1 i2 = binop Ty_int Rem i1 i2
-
-    let ( ** ) i1 i2 = binop Ty_int Pow i1 i2
-
-    let ( < ) i1 i2 = relop Ty_int Lt i1 i2
-
-    let ( > ) i1 i2 = relop Ty_int Gt i1 i2
-
-    let ( <= ) i1 i2 = relop Ty_int Le i1 i2
-
-    let ( >= ) i1 i2 = relop Ty_int Ge i1 i2
-
-    let to_real i = cvtop Ty_real Reinterpret_int i
-  end
-end
diff --git a/test/solver/test_lia.ml b/test/solver/test_lia.ml
deleted file mode 100644
index 5c035879..00000000
--- a/test/solver/test_lia.ml
+++ /dev/null
@@ -1,14 +0,0 @@
-open Smtml
-open Test_harness
-open Infix
-open Infix.Int
-
-module Make (M : Mappings_intf.S) = struct
-  module Solver = Solver.Incremental (M)
-
-  let () =
-    let solver = Solver.create ~logic:QF_LIA () in
-    let a = symbol "a" Ty_int in
-    Solver.add solver [ a + int 1 = int 2 => ((a * int 2) + int 2 = int 4) ];
-    assert_sat (Solver.check solver [])
-end
diff --git a/test/solver/test_lra.ml b/test/solver/test_lra.ml
deleted file mode 100644
index 4ad123f0..00000000
--- a/test/solver/test_lra.ml
+++ /dev/null
@@ -1,18 +0,0 @@
-open Smtml
-
-module Make (M : Mappings_intf.S) = struct
-  module Solver = Solver.Batch (M)
-
-  let () =
-    let solver = Solver.create () in
-    assert (
-      let x = Expr.symbol Symbol.("x" @: Ty_real) in
-      let y = Expr.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/solver/test_optimizer.ml b/test/solver/test_optimizer.ml
index 31fa63cf..1c08b856 100644
--- a/test/solver/test_optimizer.ml
+++ b/test/solver/test_optimizer.ml
@@ -1,10 +1,11 @@
 open Smtml
 
+(* TODO: Move this some place else? *)
 module Make (M : Mappings_intf.S) = struct
-  open Test_harness
+  open Smtml_test.Test_harness
   module Optimizer = Optimizer.Make (M)
 
-  let () =
+  let test () =
     let open Infix in
     let opt = Optimizer.create () in
     let x = symbol "x" Ty_int in
diff --git a/test/solver/test_solver.ml b/test/solver/test_solver.ml
index 124100fb..b2e44bfd 100644
--- a/test/solver/test_solver.ml
+++ b/test/solver/test_solver.ml
@@ -1,11 +1,31 @@
 open Smtml
 
 module Make (M : Mappings_intf.S) = struct
-  open Test_harness
+  open Smtml_test.Test_harness
   module Cached = Solver.Cached (M)
   module Solver = Solver.Incremental (M)
 
-  let () =
+  let test_default_params () =
+    assert (Params.default_value Timeout = Int32.(to_int max_int));
+    assert (Params.default_value Model = true);
+    assert (Params.default_value Unsat_core = false);
+    assert (Params.default_value Ematching = true)
+
+  let test_solver_params () =
+    let params =
+      Params.(
+        default () $ (Timeout, 900) $ (Model, false) $ (Unsat_core, true)
+        $ (Ematching, false) $ (Parallel, true) $ (Num_threads, 1) )
+    in
+    assert (Params.get params Unsat_core);
+    let _ : Solver.t = Solver.create ~params () in
+    ()
+
+  let test_params () =
+    test_default_params ();
+    test_solver_params ()
+
+  let test_cached_solver () =
     let solver = Cached.create ~logic:LIA () in
     let x = Infix.symbol "x" Ty_int in
     let c = Infix.(Int.(x >= int 0)) in
@@ -16,32 +36,28 @@ module Make (M : Mappings_intf.S) = struct
     assert (Cached.cache_misses () = 1);
     assert (Cached.cache_hits () = 2)
 
-  let () =
+  let test () =
     let open Infix in
     let solver = Solver.create ~logic:LIA () in
     let symbol_x = Symbol.("x" @: Ty_int) in
     let x = Expr.symbol symbol_x in
-    assert_sat (Solver.check solver []);
+    assert_sat ~f:"test" (Solver.check solver []);
 
     Solver.push solver;
     Solver.add solver Int.[ x >= int 0 ];
     assert_sat (Solver.check solver []);
-    assert (
-      let v = Solver.get_value solver x in
-      Expr.equal v (int 0) );
+    assert_equal (Solver.get_value solver x) (int 0);
     Solver.pop solver 1;
 
     Solver.push solver;
     Solver.add solver [ x = int 3 ];
-    assert_sat (Solver.check solver []);
-    assert (
-      let v = Solver.get_value solver Int.(x * x) in
-      Expr.equal v (int 9) );
+    assert_sat ~f:"test" (Solver.check solver []);
+    assert_equal (Solver.get_value solver Int.(x * x)) (int 9);
     Solver.pop solver 1;
 
     Solver.push solver;
     Solver.add solver Int.[ x >= int 0 || x < int 0 ];
-    assert_sat (Solver.check solver []);
+    assert_sat ~f:"test" (Solver.check solver []);
     (* necessary, otherwise the solver doesn't know x and can't produce a model
        for it *)
     let model = Solver.model ~symbols:[ symbol_x ] solver in
@@ -53,5 +69,117 @@ module Make (M : Mappings_intf.S) = struct
     assert_sat (Solver.check solver []);
     let model = Solver.model solver in
     let val_x = Option.bind model (fun m -> Model.evaluate m symbol_x) in
-    assert (Stdlib.(Some (Value.Int 5) = val_x))
+    assert (match val_x with Some v -> Value.equal v (Int 5) | None -> false)
+
+  let test_lia () =
+    let open Infix in
+    let solver = Solver.create ~logic:QF_LIA () in
+    let a = symbol "a" Ty_int in
+    Solver.add solver Int.[ a + int 1 = int 2 => ((a * int 2) + int 2 = int 4) ];
+    assert_sat ~f:"test_lia" (Solver.check solver [])
+
+  let test_lra () =
+    let solver = Solver.create () in
+    assert_sat ~f:"test_lra"
+      (let x = Expr.symbol Symbol.("x" @: Ty_real) in
+       let y = Expr.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
+       Solver.check solver [ c0; c1 ] )
+
+  let test_bv_8 () =
+    let open Infix in
+    let solver = Solver.create ~params:(Params.default ()) ~logic:QF_BVFP () in
+    let ty = Ty.Ty_bitv 8 in
+    let x = symbol "h" ty in
+    Solver.add solver
+      [ Expr.relop ty Gt x (int8 0); Expr.relop ty Lt x (int8 2) ];
+    assert_sat ~f:"test_bv_8" (Solver.check solver []);
+    assert_equal (Solver.get_value solver x) (int8 1)
+
+  let test_bv_32 () =
+    let open Infix in
+    let solver = Solver.create ~params:(Params.default ()) ~logic:QF_BVFP () in
+    let ty = Ty.Ty_bitv 32 in
+    let x = symbol "x" ty in
+    let y = symbol "y" ty in
+    let z = symbol "z" ty in
+    let w = symbol "w" ty in
+    Solver.add solver
+      [ Expr.relop ty Gt x (int32 0l) && Expr.relop ty Lt w (int32 5l)
+      ; Expr.relop ty Lt x y && Expr.relop ty Lt y z && Expr.relop ty Lt z w
+      ];
+    assert_sat ~f:"test_bv_32" (Solver.check solver []);
+    match Solver.model solver with
+    | None -> assert false
+    | Some m -> Model.pp Format.std_formatter ~no_values:false m
+
+  let test_bv () =
+    test_bv_8 ();
+    test_bv_32 ()
+
+  let test_fp_get_value32 () =
+    let open Infix in
+    let solver = Solver.create ~logic:QF_BVFP () in
+    let ty = Ty.Ty_fp 32 in
+    let x = symbol "x" ty in
+    let const = float32 50.0 in
+    Solver.add solver [ Expr.relop ty Eq x const ];
+    assert_sat ~f:"test_fp_get_value32" (Solver.check solver []);
+    assert_equal (Solver.get_value solver x) const
+
+  let test_fp_get_value64 () =
+    let open Infix in
+    let solver = Solver.create ~logic:QF_BVFP () in
+    let ty = Ty.Ty_fp 64 in
+    let x = symbol "x" ty in
+    let const = float64 50.0 in
+    Solver.add solver [ Expr.relop ty Eq x const ];
+    assert_sat ~f:"test_fp_get_value64" (Solver.check solver []);
+    assert_equal (Solver.get_value solver x) const
+
+  let test_fp_sqrt () =
+    let open Infix in
+    let solver = Solver.create ~logic:QF_BVFP () in
+    let ty = Ty.Ty_fp 32 in
+    let x = symbol "x" ty in
+    Solver.add solver [ Expr.relop ty Eq x (float32 4.0) ];
+    Solver.add solver [ Expr.relop ty Eq (Expr.unop ty Sqrt x) (float32 2.0) ];
+    assert_sat ~f:"test_fp_sqrt" (Solver.check solver []);
+    assert_equal (Solver.get_value solver x) (float32 4.0)
+
+  let test_fp_copysign32 () =
+    let open Infix in
+    let solver = Solver.create ~logic:QF_BVFP () in
+    let ty = Ty.Ty_fp 32 in
+    let x = symbol "x" ty in
+    let y = symbol "y" ty in
+    Solver.add solver
+      [ Expr.relop ty Gt x (float32 0.0) && Expr.relop ty Lt y (float32 0.0)
+      ; Expr.relop ty Lt (Expr.binop ty Copysign x y) (float32 0.0)
+      ];
+    assert_sat ~f:"test_copysign32" (Solver.check solver [])
+
+  let test_fp_copysign64 () =
+    let open Infix in
+    let solver = Solver.create ~logic:QF_BVFP () in
+    let ty = Ty.Ty_fp 64 in
+    let x = symbol "x" ty in
+    let y = symbol "y" ty in
+    Solver.add solver
+      [ Expr.relop ty Gt x (float64 0.0) && Expr.relop ty Lt y (float64 0.0)
+      ; Expr.relop ty Lt (Expr.binop ty Copysign x y) (float64 0.0)
+      ];
+    assert_sat ~f:"test_copysign64" (Solver.check solver [])
+
+  let test_fp () =
+    test_fp_get_value32 ();
+    test_fp_get_value64 ();
+    test_fp_sqrt ();
+    test_fp_copysign32 ();
+    test_fp_copysign64 ()
 end
diff --git a/test/solver/test_altergo.expected b/test/solver/test_solver_altergo.expected
similarity index 100%
rename from test/solver/test_altergo.expected
rename to test/solver/test_solver_altergo.expected
diff --git a/test/solver/test_solver_altergo.ml b/test/solver/test_solver_altergo.ml
new file mode 100644
index 00000000..4d5909a1
--- /dev/null
+++ b/test/solver/test_solver_altergo.ml
@@ -0,0 +1,12 @@
+open Smtml
+open Smtml_test_solver
+
+let () =
+  Printexc.record_backtrace true;
+  assert Altergo_mappings.is_available;
+  let module Alt_ergo = Test_solver.Make (Altergo_mappings.Fresh.Make ()) in
+  Alt_ergo.test_params ();
+  Alt_ergo.test_cached_solver ();
+  Alt_ergo.test ();
+  Alt_ergo.test_bv ();
+  Alt_ergo.test_lia ()
diff --git a/test/solver/test_bitwuzla.expected b/test/solver/test_solver_bitwuzla.expected
similarity index 100%
rename from test/solver/test_bitwuzla.expected
rename to test/solver/test_solver_bitwuzla.expected
diff --git a/test/solver/test_solver_bitwuzla.ml b/test/solver/test_solver_bitwuzla.ml
new file mode 100644
index 00000000..04f1ae06
--- /dev/null
+++ b/test/solver/test_solver_bitwuzla.ml
@@ -0,0 +1,9 @@
+open Smtml
+open Smtml_test_solver
+
+let () =
+  assert Bitwuzla_mappings.is_available;
+  let module Bitwuzla = Test_solver.Make (Bitwuzla_mappings.Fresh.Make ()) in
+  Bitwuzla.test_params ();
+  Bitwuzla.test_bv ();
+  Bitwuzla.test_fp ()
diff --git a/test/solver/test_colibri2.expected b/test/solver/test_solver_colibri2.expected
similarity index 100%
rename from test/solver/test_colibri2.expected
rename to test/solver/test_solver_colibri2.expected
diff --git a/test/solver/test_solver_colibri2.ml b/test/solver/test_solver_colibri2.ml
new file mode 100644
index 00000000..bf56c119
--- /dev/null
+++ b/test/solver/test_solver_colibri2.ml
@@ -0,0 +1,12 @@
+open Smtml
+open Smtml_test_solver
+
+let () =
+  assert Colibri2_mappings.is_available;
+  let module C2 = Test_solver.Make (Colibri2_mappings) in
+  C2.test_params ();
+  C2.test_cached_solver ();
+  C2.test ();
+  C2.test_bv ();
+  C2.test_fp ();
+  C2.test_lia ()
diff --git a/test/solver/test_cvc5.expected b/test/solver/test_solver_cvc5.expected
similarity index 100%
rename from test/solver/test_cvc5.expected
rename to test/solver/test_solver_cvc5.expected
diff --git a/test/solver/test_solver_cvc5.ml b/test/solver/test_solver_cvc5.ml
new file mode 100644
index 00000000..dfe5a803
--- /dev/null
+++ b/test/solver/test_solver_cvc5.ml
@@ -0,0 +1,10 @@
+open Smtml
+open Smtml_test_solver
+
+let () =
+  assert Cvc5_mappings.is_available;
+  let module Cvc5 = Test_solver.Make (Cvc5_mappings.Fresh.Make ()) in
+  Cvc5.test_params ();
+  Cvc5.test_cached_solver ();
+  Cvc5.test ();
+  Cvc5.test_bv ()
diff --git a/test/solver/test_solver_params.ml b/test/solver/test_solver_params.ml
deleted file mode 100644
index 668de040..00000000
--- a/test/solver/test_solver_params.ml
+++ /dev/null
@@ -1,21 +0,0 @@
-open Smtml
-
-module Make (M : Mappings_intf.S) = struct
-  open Params
-  module Solver = Solver.Incremental (M)
-
-  let () =
-    assert (default_value Timeout = Int32.(to_int max_int));
-    assert (default_value Model = true);
-    assert (default_value Unsat_core = false);
-    assert (default_value Ematching = true)
-
-  let () =
-    let params =
-      default () $ (Timeout, 900) $ (Model, false) $ (Unsat_core, true)
-      $ (Ematching, false) $ (Parallel, true) $ (Num_threads, 1)
-    in
-    assert (Params.get params Unsat_core);
-    let _ : Solver.t = Solver.create ~params () in
-    ()
-end
diff --git a/test/solver/test_z3.expected b/test/solver/test_solver_z3.expected
similarity index 100%
rename from test/solver/test_z3.expected
rename to test/solver/test_solver_z3.expected
diff --git a/test/solver/test_solver_z3.ml b/test/solver/test_solver_z3.ml
new file mode 100644
index 00000000..f77f009e
--- /dev/null
+++ b/test/solver/test_solver_z3.ml
@@ -0,0 +1,16 @@
+open Smtml
+open Smtml_test_solver
+
+let () =
+  assert Z3_mappings.is_available;
+  let module Z3_mappings = Z3_mappings.Fresh.Make () in
+  let module Z3_opt = Test_optimizer.Make (Z3_mappings) in
+  Z3_opt.test ();
+  let module Z3 = Test_solver.Make (Z3_mappings) in
+  Z3.test_params ();
+  Z3.test_cached_solver ();
+  Z3.test ();
+  Z3.test_lia ();
+  Z3.test_lra ();
+  Z3.test_bv ();
+  Z3.test_fp ()
diff --git a/test/solver/test_z3.ml b/test/solver/test_z3.ml
deleted file mode 100644
index 8b03ba26..00000000
--- a/test/solver/test_z3.ml
+++ /dev/null
@@ -1,14 +0,0 @@
-open Smtml
-open Smtml_tests
-
-let () =
-  assert Z3_mappings.is_available;
-  let module Test_solver_params =
-    Test_solver_params.Make (Z3_mappings.Fresh.Make ()) in
-  let module Test_solver = Test_solver.Make (Z3_mappings.Fresh.Make ()) in
-  let module Test_optimizer = Test_optimizer.Make (Z3_mappings.Fresh.Make ()) in
-  let module Test_bv = Test_bv.Make (Z3_mappings.Fresh.Make ()) in
-  let module Test_fp = Test_fp.Make (Z3_mappings.Fresh.Make ()) in
-  let module Test_lia = Test_lia.Make (Z3_mappings.Fresh.Make ()) in
-  let module Test_lra = Test_lra.Make (Z3_mappings.Fresh.Make ()) in
-  ()