From a566c7307df5c8d28cac2681e1746eefd5cb5fd9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 3 Sep 2021 12:33:04 -0700
Subject: [PATCH] #5532

---
 src/sat/smt/bv_internalize.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index 8c16d6052..439764515 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -244,8 +244,9 @@ namespace bv {
             expr_ref b2b(bv.mk_bit2bool(e, i), m);
             m_bits[v].push_back(sat::null_literal);
             sat::literal lit = ctx.internalize(b2b, false, false, m_is_redundant);
-            (void)lit;
             TRACE("bv", tout << "add-bit: " << lit << " " << literal2expr(lit) << "\n";);
+            if (m_bits[v].back() == sat::null_literal)
+                m_bits[v].back() = lit;
             SASSERT(m_bits[v].back() == lit);
         }
     }