From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 22 Aug 2016 15:45:01 +0000 (+0200)
Subject: Minor yosys-smtbmc bugfix
X-Git-Tag: yosys-0.7~108
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6523023645bd2227cac68f46364dff3867d9641a;p=yosys.git

Minor yosys-smtbmc bugfix
---

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index a11fed2d5..498621612 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -171,6 +171,12 @@ def get_constr_expr(db, state):
         expr = re.sub(r'\[([^\]]+)\]', lambda match: smt.net_expr(topmod, "s%d" % state, smt.get_path(topmod, match.group(1))), expr)
         expr_list.append(expr)
 
+    if len(expr_list) == 0:
+        return "true"
+
+    if len(expr_list) == 1:
+        return expr_list[0]
+
     return "(and %s)" % " ".join(expr_list)