Skip to content

Commit

Permalink
smtbmc: Fix two .yw handling related crashes
Browse files Browse the repository at this point in the history
These came up when using the experimental incremental interface and are
also in code that was recently refactored to support that interface.
  • Loading branch information
jix committed Jun 6, 2024
1 parent 855ac28 commit 094fa8c
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions backends/smt2/smtbmc.py
Original file line number Diff line number Diff line change
Expand Up @@ -719,6 +719,8 @@ def smt_extract_mask(smt_expr, mask):
return combined_chunks, ''.join(mask_index_order[start:end] for start, end in chunks)[::-1]

def smt_concat(exprs):
if not isinstance(exprs, (tuple, list)):
exprs = tuple(exprs)
if not exprs:
return ""
if len(exprs) == 1:
Expand Down Expand Up @@ -818,6 +820,9 @@ def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False):
if not bits_re.match(bits):
raise ValueError("unsupported bit value in Yosys witness file")

if bits.count('?') == len(bits):
continue

smt_expr = ywfile_signal(sig, map_steps.get(t, t))

smt_expr, bits = smt_extract_mask(smt_expr, bits)
Expand Down

0 comments on commit 094fa8c

Please sign in to comment.