diff options
author | Jannis Harder <me@jix.one> | 2022-10-18 19:51:36 +0200 |
---|---|---|
committer | Jannis Harder <me@jix.one> | 2022-10-18 19:51:36 +0200 |
commit | 8838b1eaa474ea116be8f9bfacc03ffb37bef248 (patch) | |
tree | 4efcb3488947eecc59163c25893a90eebc1ae459 /backends | |
parent | 2e837956dc055bc517d5bd5cd75b72bf0eb62272 (diff) | |
download | yosys-8838b1eaa474ea116be8f9bfacc03ffb37bef248.tar.gz yosys-8838b1eaa474ea116be8f9bfacc03ffb37bef248.tar.bz2 yosys-8838b1eaa474ea116be8f9bfacc03ffb37bef248.zip |
smtbmc: Fix witness handling for k-induction failures
The "uninitialized" value is a _list_ of chunks that are part of the
initial state for the witness trace.
Diffstat (limited to 'backends')
-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 |