Ignore L_pi nets in "yosys-smtbmc --cex"

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index fabcdc92d8b89f10119195cfa1deff84e52200af..04c25f91437cd7f2c57cb5234ea5e8f0b533e372 100644 (file)
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -319,12 +319,15 @@ assert topmod in smt.modinfo
 
 if cexfile is not None:
     with open(cexfile, "r") as f:
-        cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?(@\d+)=([01])')
+        cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
         for entry in f.read().split():
             match = cex_regex.match(entry)
             assert match
 
-            name, bit, step, val = match.group(1), match.group(2), match.group(3), match.group(4)
+            name, bit, extra_name, step, val = match.group(1), match.group(2), match.group(3), match.group(4), match.group(5)
+
+            if extra_name != "":
+                continue
 
             if name not in smt.modinfo[topmod].inputs:
                 continue