fix: check infeasible errors

a16z · Jan 21, 2025 · 11e84e4 · 11e84e4
1 parent edeb7c6
commit 11e84e4
Showing 1 changed file with 5 additions and 3 deletions.
diff --git a/src/halmos/__main__.py b/src/halmos/__main__.py
@@ -724,9 +724,11 @@ 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)}"
+            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: