aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
authorJannis Harder <me@jix.one>2022-10-18 19:51:36 +0200
committerJannis Harder <me@jix.one>2022-10-18 19:51:36 +0200
commit8838b1eaa474ea116be8f9bfacc03ffb37bef248 (patch)
tree4efcb3488947eecc59163c25893a90eebc1ae459 /backends
parent2e837956dc055bc517d5bd5cd75b72bf0eb62272 (diff)
downloadyosys-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.py2
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