aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smtbmc.py
diff options
context:
space:
mode:
authorJannis Harder <me@jix.one>2022-08-08 15:33:47 +0200
committerJannis Harder <me@jix.one>2022-08-16 13:37:30 +0200
commit66f761a8c54b66b8e6b4667cfb54072ad76952e0 (patch)
tree71862630d70845867dcc939bd6c0301418bfd201 /backends/smt2/smtbmc.py
parent927af914f11f895d10475917d5c0b06261703362 (diff)
downloadyosys-66f761a8c54b66b8e6b4667cfb54072ad76952e0.tar.gz
yosys-66f761a8c54b66b8e6b4667cfb54072ad76952e0.tar.bz2
yosys-66f761a8c54b66b8e6b4667cfb54072ad76952e0.zip
smtbmc: Set step range for --yw and dont skip steps for --check-witness
Diffstat (limited to 'backends/smt2/smtbmc.py')
-rw-r--r--backends/smt2/smtbmc.py16
1 files changed, 14 insertions, 2 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 3714e2918..5f05287de 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -482,7 +482,8 @@ if cexfile is not None:
constr_assumes[step].append((cexfile, smtexpr))
if not got_topt:
- skip_steps = max(skip_steps, step)
+ if not check_witness:
+ skip_steps = max(skip_steps, step)
num_steps = max(num_steps, step+1)
if aimfile is not None:
@@ -615,7 +616,8 @@ if aimfile is not None:
constr_assumes[step].append((cexfile, smtexpr))
if not got_topt:
- skip_steps = max(skip_steps, step)
+ if not check_witness:
+ skip_steps = max(skip_steps, step)
# some solvers optimize the properties so that they fail one cycle early,
# thus we check the properties in the cycle the aiger witness ends, and
# if that doesn't work, we check the cycle after that as well.
@@ -623,6 +625,11 @@ if aimfile is not None:
step += 1
if inywfile is not None:
+ if not got_topt:
+ assume_skipped = 0
+ skip_steps = 0
+ num_steps = 0
+
with open(inywfile, "r") as f:
inyw = ReadWitness(f)
@@ -717,6 +724,11 @@ if inywfile is not None:
smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice)
constr_assumes[t].append((inywfile, smt_constr))
+ if not got_topt:
+ if not check_witness:
+ skip_steps = max(skip_steps, t)
+ num_steps = max(num_steps, t+1)
+
if btorwitfile is not None:
with open(btorwitfile, "r") as f:
step = None