From 094fa8cabaafd1cc0ed8e7d485e86cf1651078bf Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 6 Jun 2024 17:35:31 +0200 Subject: [PATCH 1/2] smtbmc: Fix two .yw handling related crashes These came up when using the experimental incremental interface and are also in code that was recently refactored to support that interface. --- backends/smt2/smtbmc.py | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 995a714c9..c3bdcebbe 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -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: @@ -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) From bd28d26021c4bd2c3bcc9d60b0e6e7e93fbebc86 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Fri, 7 Jun 2024 00:17:23 +0000 Subject: [PATCH 2/2] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 9a263c2f2..594e740a9 100644 --- a/Makefile +++ b/Makefile @@ -141,7 +141,7 @@ LIBS += -lrt endif endif -YOSYS_VER := 0.41+126 +YOSYS_VER := 0.41+129 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo