mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-08-16 09:55:30 +00:00
Code Activity

Don't use induction step for depth

Browse source
This commit is contained in:
Krystine Sherwin 2025-07-08 15:47:33 +12:00
parent 4fc23bebec
commit 488d25b625
No known key found for this signature in database
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
sbysrc/sby_engine_smtbmc.py
View file

@ -216,6 +216,8 @@ def run(mode, task, engine_idx, engine):
if match: if match:
last_prop = [] last_prop = []
recorded_last = False recorded_last = False
if mode == "prove_induction":
return line
last_step = current_step last_step = current_step
current_step = int(match[1]) current_step = int(match[1])
if current_step != last_step and last_step is not None: if current_step != last_step and last_step is not None: