diff options
author | Jannis Harder <me@jix.one> | 2022-08-08 15:33:47 +0200 |
---|---|---|
committer | Jannis Harder <me@jix.one> | 2022-08-16 13:37:30 +0200 |
commit | 66f761a8c54b66b8e6b4667cfb54072ad76952e0 (patch) | |
tree | 71862630d70845867dcc939bd6c0301418bfd201 /backends | |
parent | 927af914f11f895d10475917d5c0b06261703362 (diff) | |
download | yosys-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')
-rw-r--r-- | backends/smt2/smtbmc.py | 16 |
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 |