aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
authorJannis Harder <me@jix.one>2022-10-20 13:44:45 +0200
committerJannis Harder <me@jix.one>2022-10-20 13:49:47 +0200
commit96029400cbf661fb5303572923df3f0dc17164ee (patch)
treee4cd774dbc532aa6968e13818cc692806d2f7385 /backends
parent6781746872087d8c1eb3f5560fe338a693a40d7c (diff)
downloadyosys-96029400cbf661fb5303572923df3f0dc17164ee.tar.gz
yosys-96029400cbf661fb5303572923df3f0dc17164ee.tar.bz2
yosys-96029400cbf661fb5303572923df3f0dc17164ee.zip
smtbmc: Do not assume skipped assertions when loading a witness trace
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.
Diffstat (limited to 'backends')
-rw-r--r--backends/smt2/smtbmc.py3
1 files changed, 0 insertions, 3 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 4c1f07229..cb21eb3aa 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -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