diff options
| author | Jannis Harder <me@jix.one> | 2022-10-19 11:28:12 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-10-19 11:28:12 +0200 |
| commit | f4ede15d6857c02576a32f94043af866fde607aa (patch) | |
| tree | 6eb79201fa45f0f99d2c5d0c1d01d166936fb0b3 | |
| parent | d02ae8f2fc78f43e870e2d67d472b3e7039e2bbe (diff) | |
| parent | 8838b1eaa474ea116be8f9bfacc03ffb37bef248 (diff) | |
| download | yosys-f4ede15d6857c02576a32f94043af866fde607aa.tar.gz yosys-f4ede15d6857c02576a32f94043af866fde607aa.tar.bz2 yosys-f4ede15d6857c02576a32f94043af866fde607aa.zip | |
Merge pull request #3514 from jix/smtbmc-kind-witness-fix
smtbmc: Fix witness handling for k-induction failures
| -rw-r--r-- | backends/smt2/smtio.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index f5cfe436d..a73745896 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -701,7 +701,7 @@ class SmtIo: if witness["type"] == "mem": if allregs and not witness["rom"]: width, size = witness["width"], witness["size"] - witness = {**witness, "uninitialized": {"width": width * size, "offset": 0}} + witness = {**witness, "uninitialized": [{"width": width * size, "offset": 0}]} if not witness["uninitialized"]: continue |