fix: check infeasible errors (#445)

a16z · Jan 22, 2025 · 028d726 · 028d726
1 parent 6163a6c
commit 028d726
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 7 deletions.
diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml
@@ -54,22 +54,22 @@ jobs:
             dir: "snekmate"
             cmd: "--config test/halmos.toml --contract ERC20TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
             branch: ""
-            profile: "halmos"
+            profile: "halmos-venom"
           - repo: "pcaversaccio/snekmate"
             dir: "snekmate"
             cmd: "--config test/halmos.toml --contract ERC721TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
             branch: ""
-            profile: "halmos"
+            profile: "halmos-venom"
           - repo: "pcaversaccio/snekmate"
             dir: "snekmate"
             cmd: "--config test/halmos.toml --contract ERC1155TestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
             branch: ""
-            profile: "halmos"
+            profile: "halmos-venom"
           - repo: "pcaversaccio/snekmate"
             dir: "snekmate"
             cmd: "--config test/halmos.toml --contract MathTestHalmos --solver-command 'jsi --model --sequence yices,bitwuzla-abstraction' --solver-threads 1"
             branch: ""
-            profile: "halmos"
+            profile: "halmos-venom"
 
     steps:
       - name: Checkout halmos

diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
@@ -724,9 +724,12 @@ def future_callback(future_model):
             future_models.append(future_model)
 
         elif ex.context.is_stuck():
-            stuck.append((idx, ex, ex.context.get_stuck_reason()))
-            if args.print_blocked_states:
-                traces[idx] = f"{hexify(ex.path)}\n{rendered_trace(ex.context)}"
+            debug(f"Potential error path (id: {idx+1})")
+            res, _, _ = solve(ex.path.to_smt2(args), args)
+            if res != unsat:
+                stuck.append((idx, ex, ex.context.get_stuck_reason()))
+                if args.print_blocked_states:
+                    traces[idx] = f"{hexify(ex.path)}\n{rendered_trace(ex.context)}"
 
         elif not error_output:
             if args.print_success_states: