Add solver argument to testcomp script

bench/testcomp/dune

@@ -3,7 +3,7 @@
 (executable
  (name testcomp)
  (modules testcomp whitelist)
- (libraries bos fpath report tool yaml unix))
+ (libraries bos fpath report tool yaml unix smtml))
 
 (rule
  (deps whitelist.txt)

bench/testcomp/testcomp.ml

@@ -3,7 +3,9 @@ module Unix = struct
   include Bos.OS.U
 end
 
-let tool = Tool.mk_owi ~concolic:false ~workers:24 ~optimisation_level:3
+let tool =
+  Tool.mk_owi ~concolic:false ~workers:24 ~optimisation_level:3
+    ~solver:Smtml.Solver_dispatcher.Z3_solver
 
 let _tool = Tool.mk_klee ()
 

bench/tool/dune

@@ -1,4 +1,4 @@
 (library
  (name tool)
  (modules tool)
- (libraries bos extunix fpath report rusage unix))
+ (libraries bos extunix fpath report rusage unix smtml))

bench/tool/tool.ml

@@ -1,8 +1,11 @@
+module S = Smtml.Solver_dispatcher
+
 type t =
   | Owi of
       { concolic : bool
       ; optimisation_level : int
       ; workers : int
+      ; solver : S.solver_type
       }
   | Klee
 
@@ -11,13 +14,14 @@ let ( let+ ) o f = match o with Ok v -> Ok (f v) | Error _ as e -> e
 let to_short_name = function Owi _ -> "owi" | Klee -> "klee"
 
 let to_reference_name = function
-  | Owi { concolic; workers; optimisation_level } ->
-    Format.sprintf "owi_w%d_O%d%s" workers optimisation_level
+  | Owi { concolic; workers; optimisation_level; solver } ->
+    Format.asprintf "owi_w%d_O%d_s%a%s" workers optimisation_level
+      S.pp_solver_type solver
       (if concolic then "_concolic" else "")
   | Klee -> "klee"
 
-let mk_owi ~concolic ~workers ~optimisation_level =
-  Owi { concolic; workers; optimisation_level }
+let mk_owi ~concolic ~workers ~optimisation_level ~solver =
+  Owi { concolic; workers; optimisation_level; solver }
 
 let mk_klee () = Klee
 
@@ -98,7 +102,7 @@ let execvp ~output_dir tool file timeout =
   let timeout = string_of_int timeout in
   let bin, args =
     match tool with
-    | Owi { workers; optimisation_level; concolic } ->
+    | Owi { workers; optimisation_level; concolic; solver } ->
       ( "owi"
       , [ "owi"; "c" ]
         @ (if concolic then [ "--concolic" ] else [])
@@ -107,6 +111,8 @@ let execvp ~output_dir tool file timeout =
           ; Format.sprintf "-w%d" workers
           ; "-o"
           ; output_dir
+          ; "--solver"
+          ; Format.asprintf "%a" S.pp_solver_type solver
           ; file
           ] )
     | Klee ->

bench/tool/tool.mli

@@ -4,7 +4,12 @@ val to_short_name : t -> string
 
 val to_reference_name : t -> string
 
-val mk_owi : concolic:bool -> workers:int -> optimisation_level:int -> t
+val mk_owi :
+     concolic:bool
+  -> workers:int
+  -> optimisation_level:int
+  -> solver:Smtml.Solver_dispatcher.solver_type
+  -> t
 
 val mk_klee : unit -> t