Refactor tests with new API

formalsec · Feb 17, 2025 · dbc082c · dbc082c
1 parent 7f9906b
commit dbc082c
Show file tree

Hide file tree

Showing 41 changed files with 891 additions and 910 deletions.
diff --git a/test/bitvector/test_bitvector.ml b/test/bitvector/test_bitvector.ml
@@ -61,8 +61,9 @@ let test_comparisons () =
 
 let test_rotate () =
   let bv = make (z 0b1101) 4 in
-  assert (view (rotate_left bv 1) = z 0b1011);
-  assert (view (rotate_right bv 1) = z 0b1110)
+  let one = make (z 1) 4 in
+  assert (view (rotate_left bv one) = z 0b1011);
+  assert (view (rotate_right bv one) = z 0b1110)
 
 let test_extensions () =
   let bv = make (z 0b1010) 4 in

diff --git a/test/dune b/test/dune
@@ -0,0 +1,4 @@
+(library
+ (name smtml_test)
+ (modules test_harness)
+ (libraries smtml))
diff --git 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
diff --git 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
diff --git a/test/solver/test_bitwuzla.ml b/test/solver/test_bitwuzla.ml
diff --git a/test/solver/test_bv.ml b/test/solver/test_bv.ml
diff --git a/test/solver/test_colibri2.ml b/test/solver/test_colibri2.ml
diff --git a/test/solver/test_cvc5.ml b/test/solver/test_cvc5.ml
diff --git a/test/solver/test_fp.ml b/test/solver/test_fp.ml
diff --git a/test/solver/test_harness.ml b/test/solver/test_harness.ml
diff --git a/test/solver/test_lia.ml b/test/solver/test_lia.ml
diff --git a/test/solver/test_lra.ml b/test/solver/test_lra.ml
diff --git 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