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

Due to some previous Z3 bug, this will only work for versions newer
than the as yet unpublished 4.13.4.

Even than, this flag does not currently work correctly due to some
change in the z3-produced SMT models.

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")
      };