From 590c6db84496862b5216e92073cc95a2741a47d4 Mon Sep 17 00:00:00 2001
From: Daejun Park <daejunpark@gmail.com>
Date: Fri, 20 Sep 2024 14:26:24 -0700
Subject: [PATCH] debug loop bound info

---
 src/halmos/sevm.py | 6 ++++++
 1 file changed, 6 insertions(+)

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