From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 18 Oct 2016 08:54:53 +0000 (+0200)
Subject: Ignore L_pi nets in "yosys-smtbmc --cex"
X-Git-Tag: yosys-0.7~16
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=281a977b39ec832b5ad4d84027dc98a6e8f99d7c;p=yosys.git

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

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index fabcdc92d..04c25f914 100644
--- 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