mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-28 11:25:53 +00:00
Merge pull request #3514 from jix/smtbmc-kind-witness-fix
smtbmc: Fix witness handling for k-induction failures
This commit is contained in:
commit
f4ede15d68
1 changed files with 1 additions and 1 deletions
|
@ -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
|
||||
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue