Add z3new as solver type command line flag, which sets sat.smt=true.

backend/cn/bin/main.ml

@@ -727,7 +727,7 @@ module Verify_flags = struct
     let doc = "Specify the SMT solver interface" in
     Arg.(
       value
-      & opt (some (enum [ ("z3", Simple_smt.Z3); ("cvc5", Simple_smt.CVC5) ])) None
+      & opt (some (enum [ ("z3", Simple_smt.Z3); ("z3new", Simple_smt.Z3new); ("cvc5", Simple_smt.CVC5) ])) None
       & info [ "solver-type" ] ~docv:"z3|cvc5" ~doc)
 
 

backend/cn/lib/simple_smt.ml

@@ -320,6 +320,7 @@ let arr_store arr i v = app_ "store" [ arr; i; v ]
     to decide how to generate terms for those cases. *)
 type solver_extensions =
   | Z3
+  | Z3new
   | CVC5
   | Other
 
@@ -545,7 +546,7 @@ let get_model s =
   match s.config.exts with
   | CVC5 -> ans
   | Other -> ans
-  | Z3 ->
+  | (Z3 | Z3new) ->
     (* Workaround for https://github.com/Z3Prover/z3/issues/7270:
        remove `as-array` *)
     let rec drop_as_array x =
@@ -903,3 +904,8 @@ let z3 : solver_config =
   (* let params = [ ("sat.smt", "true") ] in *)
   let params = [] in
   { exe = "z3"; opts = [ "-in"; "-smt2" ]; params; exts = Z3; log = quiet_log }
+
+
+let z3new : solver_config =
+  let params = [ ("sat.smt", "true"); ("model.completion", "true"); ] in
+  { exe = "z3"; opts = [ "-in"; "-smt2" ]; params; exts = Z3new; log = quiet_log }

backend/cn/lib/solver.ml

@@ -1260,6 +1260,7 @@ let make globals =
        | Some t ->
          (match t with
           | SMT.Z3 -> SMT.z3
+          | SMT.Z3new -> SMT.z3new
           | SMT.CVC5 -> SMT.cvc5
           | SMT.Other -> failwith "Unsupported solver.")
        | None ->
@@ -1279,6 +1280,7 @@ let make globals =
          Logger.make
            (match !cfg.exts with
             | SMT.Z3 -> "z3"
+            | SMT.Z3new -> "z3new"
             | SMT.CVC5 -> "cvc5"
             | SMT.Other -> "other")
      };