From 281a977b39ec832b5ad4d84027dc98a6e8f99d7c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 18 Oct 2016 10:54:53 +0200 Subject: [PATCH] Ignore L_pi nets in "yosys-smtbmc --cex" --- backends/smt2/smtbmc.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) 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 -- 2.30.2