From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 3 Dec 2016 11:37:20 +0000 (+0100)
Subject: Improved yosys-smtbmc default -t/--assume-skipped for --cex and --aig
X-Git-Tag: yosys-0.8~564
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=37760541bd4298677f208f2740e721c1be95bbd7;p=yosys.git

Improved yosys-smtbmc default -t/--assume-skipped for --cex and --aig
---

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