From 488d25b6250398e6b21c21cd30ad85cb03618063 Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Tue, 8 Jul 2025 15:47:33 +1200
Subject: [PATCH] Don't use induction step for depth

---
 sbysrc/sby_engine_smtbmc.py | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 52f0459..cdd579a 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -216,6 +216,8 @@ def run(mode, task, engine_idx, engine):
         if match:
             last_prop = []
             recorded_last = False
+            if mode == "prove_induction":
+                return line
             last_step = current_step
             current_step = int(match[1])
             if current_step != last_step and last_step is not None: