Promote tests

doc/index.mld

@@ -27,7 +27,7 @@ module Z3 :
     val solver_time : float ref
     val solver_count : int ref
     val pp_statistics : t Smtml_prelude.Fmt.t
-    val create : ?params:Smtml.Params.t -> ?logic:Smtml.Ty.logic -> unit -> t
+    val create : ?params:Smtml.Params.t -> ?logic:Smtml.Logic.t -> unit -> t
     val interrupt : t -> unit
     val clone : t -> t
     val push : t -> unit

test/solver/dune

@@ -21,8 +21,7 @@
  (name test_colibri2)
  (modules test_colibri2)
  (libraries smtml_tests)
- (build_if
-  (and %{lib-available:colibri2} %{lib-available:colibrilib})))
+ (build_if %{lib-available:colibri2.core}))
 
 (test
  (name test_bitwuzla)

test/solver/test_bitwuzla.expected

@@ -1,5 +1,5 @@
 (model
-  (w (i32 4))
-  (x (i32 1))
-  (y (i32 2))
-  (z (i32 3)))
+  (w i32 4)
+  (x i32 1)
+  (y i32 2)
+  (z i32 3))

test/solver/test_colibri2.expected

@@ -1,5 +1,5 @@
 (model
-  (w (i32 4))
-  (x (i32 1))
-  (y (i32 2))
-  (z (i32 3)))
+  (w i32 4)
+  (x i32 1)
+  (y i32 2)
+  (z i32 3))

test/solver/test_cvc5.expected

@@ -1,5 +1,5 @@
 (model
-  (w (i32 4))
-  (x (i32 1))
-  (y (i32 2))
-  (z (i32 3)))
+  (w i32 4)
+  (x i32 1)
+  (y i32 2)
+  (z i32 3))