From 028d726f0a6a5f8ec55cd8dce3f79e17be8d2965 Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Tue, 21 Jan 2025 17:13:44 -0800
Subject: [PATCH] fix: check infeasible errors (#445)

---
 .github/workflows/test-external.yml | 8 ++++----
 src/halmos/__main__.py              | 9 ++++++---
 2 files changed, 10 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/test-external.yml b/.github/workflows/test-external.yml
index f9f41449..bfdf7ff3 100644
--- 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
index eee58413..b6daa409 100644
--- 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: