From 872006d9c89819ea3086adb71169bd500b321935 Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Thu, 21 Sep 2023 16:53:51 -0700
Subject: [PATCH 1/2] feat: add --dump-smt-queries option

---
 src/halmos/__main__.py | 11 +++++++++++
 src/halmos/parser.py   |  6 ++++++
 2 files changed, 17 insertions(+)

diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
index 2b91789c..10a84459 100644
--- a/src/halmos/__main__.py
+++ b/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)}"
diff --git a/src/halmos/parser.py b/src/halmos/parser.py
index 4d9a8efd..1a99d97c 100644
--- a/src/halmos/parser.py
+++ b/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")
 

From aa731a4d9ec1530516867491a6d1ac82d16181a6 Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Thu, 21 Sep 2023 17:15:38 -0700
Subject: [PATCH 2/2] feat: add --solver-subprocess-command option

---
 src/halmos/__main__.py | 7 +++----
 src/halmos/parser.py   | 6 ++++++
 2 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
index 10a84459..7a39e3c5 100644
--- a/src/halmos/__main__.py
+++ b/src/halmos/__main__.py
@@ -800,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))`
@@ -809,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)
diff --git a/src/halmos/parser.py b/src/halmos/parser.py
index 1a99d97c..b3720a23 100644
--- a/src/halmos/parser.py
+++ b/src/halmos/parser.py
@@ -215,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",