Skip to content

Commit baccf87

Browse files
authored
Merge pull request #4431 from jix/smtbmc-fixes
smtbmc: Fix two .yw handling related crashes
2 parents 855ac28 + 094fa8c commit baccf87

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

Diff for: backends/smt2/smtbmc.py

+5
Original file line numberDiff line numberDiff line change
@@ -719,6 +719,8 @@ def smt_extract_mask(smt_expr, mask):
719719
return combined_chunks, ''.join(mask_index_order[start:end] for start, end in chunks)[::-1]
720720

721721
def smt_concat(exprs):
722+
if not isinstance(exprs, (tuple, list)):
723+
exprs = tuple(exprs)
722724
if not exprs:
723725
return ""
724726
if len(exprs) == 1:
@@ -818,6 +820,9 @@ def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False):
818820
if not bits_re.match(bits):
819821
raise ValueError("unsupported bit value in Yosys witness file")
820822

823+
if bits.count('?') == len(bits):
824+
continue
825+
821826
smt_expr = ywfile_signal(sig, map_steps.get(t, t))
822827

823828
smt_expr, bits = smt_extract_mask(smt_expr, bits)

0 commit comments

Comments
 (0)