diff --git a/src/halmos/sevm.py b/src/halmos/sevm.py index e3c1d236..8c86756a 100644 --- 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