From 8838b1eaa474ea116be8f9bfacc03ffb37bef248 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Tue, 18 Oct 2022 19:51:36 +0200
Subject: [PATCH] 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.
---
 backends/smt2/smtio.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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