diff options
| author | Clifford Wolf <clifford@clifford.at> | 2016-08-22 17:45:01 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2016-08-22 17:45:01 +0200 |
| commit | 6523023645bd2227cac68f46364dff3867d9641a (patch) | |
| tree | 8a4b97b68a3451c98f32c5ba71dcad7ddb3d1718 | |
| parent | 583ceee6eb69fb8093f7d184d737ea93e2744c5b (diff) | |
| download | yosys-6523023645bd2227cac68f46364dff3867d9641a.tar.gz yosys-6523023645bd2227cac68f46364dff3867d9641a.tar.bz2 yosys-6523023645bd2227cac68f46364dff3867d9641a.zip | |
Minor yosys-smtbmc bugfix
| -rw-r--r-- | backends/smt2/smtbmc.py | 6 |
1 files changed, 6 insertions, 0 deletions
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) |