luke/yosys
1
0
Fork 0
mirror of https://github.com/YosysHQ/yosys.git synced 2026-08-22 14:17:27 +02:00
Code Issues Packages Projects Releases Wiki Activity

smtbmc: Do not assume skipped assertions when loading a witness trace

Browse Source 
This is not valid when the prefix of a trace already violates
assertions. This can happen when the trace generating solver doesn't
look for a minimal length counterexample.
This commit is contained in:
Jannis Harder
2022-10-20 13:49:47 +02:00
parent 6781746872
commit 96029400cb
1 changed files with 0 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
backends/smt2/smtbmc.py
-3
View File
@@ -453,7 +453,6 @@ assert topmod in smt.modinfo
if cexfile is not None:
if not got_topt:
assume_skipped = 0
skip_steps = 0
num_steps = 0
@@ -499,7 +498,6 @@ if aimfile is not None:
latch_map = dict()
if not got_topt:
assume_skipped = 0
skip_steps = 0
num_steps = 0
@@ -633,7 +631,6 @@ if aimfile is not None:
if inywfile is not None:
if not got_topt:
assume_skipped = 0
skip_steps = 0
num_steps = 0