riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

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.
This commit is contained in:
Jannis Harder 2022-10-18 19:51:36 +02:00
parent 2e837956dc
commit 8838b1eaa4
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
backends/smt2/smtio.py
View File

@ -701,7 +701,7 @@ class SmtIo:
if witness["type"] == "mem": if witness["type"] == "mem":
if allregs and not witness["rom"]: if allregs and not witness["rom"]:
width, size = witness["width"], witness["size"] 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"]: if not witness["uninitialized"]:
continue continue