From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 13 Sep 2016 11:23:06 +0000 (+0200)
Subject: Work-around for boolector bug
X-Git-Tag: yosys-0.7~62
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d39db41df87113792c383fc2f127a3d42ae6dd0e;p=yosys.git

Work-around for boolector bug
---

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 3cfbbaf93..fa4966089 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -478,14 +478,14 @@ def write_trace(steps_start, steps_stop, index):
 def print_failed_asserts_worker(mod, state, path):
     assert mod in smt.modinfo
 
-    if smt.get("(|%s_a| %s)" % (mod, state)) == "true":
+    if smt.get("(|%s_a| %s)" % (mod, state)) in ["true", "#b1"]:
         return
 
     for cellname, celltype in smt.modinfo[mod].cells.items():
         print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
 
     for assertfun, assertinfo in smt.modinfo[mod].asserts.items():
-        if smt.get("(|%s| %s)" % (assertfun, state)) == "false":
+        if smt.get("(|%s| %s)" % (assertfun, state)) in ["false", "#b0"]:
             print_msg("Assert failed in %s: %s" % (path, assertinfo))