mirror of https://github.com/YosysHQ/yosys.git
Minor yosys-smtbmc bugfix
This commit is contained in:
parent
583ceee6eb
commit
6523023645
|
@ -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 = re.sub(r'\[([^\]]+)\]', lambda match: smt.net_expr(topmod, "s%d" % state, smt.get_path(topmod, match.group(1))), expr)
|
||||||
expr_list.append(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)
|
return "(and %s)" % " ".join(expr_list)
|
||||||
|
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue