debug loop bound info

a16z · Sep 20, 2024 · 590c6db · 590c6db
1 parent b60f64a
commit 590c6db
Showing 1 changed file with 6 additions and 0 deletions.
diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py
@@ -2364,6 +2364,12 @@ def jumpi(
             follow_false = visited[False] < self.options.loop
             if not (follow_true and follow_false):
                 self.logs.bounded_loops.append(jid)
+                if self.options.debug:
+                    debug(f"\nloop id: {jid}")
+                    debug(f"loop condition: {cond}")
+                    debug(f"calldata: {ex.calldata()}")
+                    debug("path condition:")
+                    debug(ex.path)
         else:
             # for constant-bounded loops
             follow_true = potential_true