feat: add custom solver options (#197)

src/halmos/__main__.py

@@ -453,6 +453,17 @@ def run(
         else:
             stuck.append((opcode, idx, ex))
 
+    if len(execs_to_model) > 0 and args.dump_smt_queries:
+        dirname = f"/tmp/{funname}.{uuid.uuid4().hex}"
+        os.makedirs(dirname)
+        print(f"Generating SMT queries in {dirname}")
+        for idx, ex in execs_to_model:
+            fname = f"{dirname}/{idx+1}.smt2"
+            query = ex.solver.to_smt2()
+            with open(fname, "w") as f:
+                f.write("(set-logic QF_AUFBV)\n")
+                f.write(query)
+
     if len(execs_to_model) > 0 and args.verbose >= 1:
         print(
             f"# of potential paths involving assertion violations: {len(execs_to_model)} / {len(exs)}"
@@ -789,7 +800,7 @@ def gen_model(args: Namespace, idx: int, ex: Exec) -> ModelWithContext:
             print(f"  Checking again in an external process")
         fname = f"/tmp/{uuid.uuid4().hex}.smt2"
         if args.verbose >= 1:
-            print(f"    z3 -model {fname} >{fname}.out")
+            print(f"    {args.solver_subprocess_command} {fname} >{fname}.out")
         query = ex.solver.to_smt2()
         # replace uninterpreted abstraction with actual symbols for assertion solving
         # TODO: replace `(evm_bvudiv x y)` with `(ite (= y (_ bv0 256)) (_ bv0 256) (bvudiv x y))`
@@ -798,9 +809,8 @@ def gen_model(args: Namespace, idx: int, ex: Exec) -> ModelWithContext:
         with open(fname, "w") as f:
             f.write("(set-logic QF_AUFBV)\n")
             f.write(query)
-        res_str = subprocess.run(
-            ["z3", "-model", fname], capture_output=True, text=True
-        ).stdout.strip()
+        cmd = args.solver_subprocess_command.split() + [fname]
+        res_str = subprocess.run(cmd, capture_output=True, text=True).stdout.strip()
         res_str_head = res_str.split("\n", 1)[0]
         with open(f"{fname}.out", "w") as f:
             f.write(res_str)

src/halmos/parser.py

@@ -147,6 +147,12 @@ def mk_arg_parser() -> argparse.ArgumentParser:
         help="turn unknown counterexample warnings to errors",
     )
 
+    group_debug.add_argument(
+        "--dump-smt-queries",
+        action="store_true",
+        help="dump SMT queries for assertion violations",
+    )
+
     # build options
     group_build = parser.add_argument_group("Build options")
 
@@ -209,6 +215,12 @@ def mk_arg_parser() -> argparse.ArgumentParser:
         action="store_true",
         help="run an extra solver in subprocess for unknown",
     )
+    group_solver.add_argument(
+        "--solver-subprocess-command",
+        metavar="COMMAND",
+        default="z3 -model",
+        help="use the given command for the subprocess solver (requires --solver-subprocess) (default: %(default)s)",
+    )
     group_solver.add_argument(
         "--solver-parallel",
         action="store_true",