diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smtbmc.py | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 56c7bccc1..dc89b795d 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -337,6 +337,11 @@ assert topmod is not None assert topmod in smt.modinfo if cexfile is not None: + if not got_topt: + assume_skipped = 0 + skip_steps = 0 + num_steps = 0 + with open(cexfile, "r") as f: cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])') for entry in f.read().split(): @@ -368,11 +373,20 @@ if cexfile is not None: # print("cex@%d: %s" % (step, smtexpr)) constr_assumes[step].append((cexfile, smtexpr)) + if not got_topt: + skip_steps = max(skip_steps, step) + num_steps = max(num_steps, step+1) + if aigprefix is not None: input_map = dict() init_map = dict() latch_map = dict() + if not got_topt: + assume_skipped = 0 + skip_steps = 0 + num_steps = 0 + with open(aigprefix + ".aim", "r") as f: for entry in f.read().splitlines(): entry = entry.split() @@ -473,8 +487,7 @@ if aigprefix is not None: constr_assumes[step].append((cexfile, smtexpr)) if not got_topt: - skip_steps = step - assume_skipped = 0 + skip_steps = max(skip_steps, step) num_steps = max(num_steps, step+1) step += 1 |