From e5eaea46aa5b89b3a1e431e26f16d10519b1a098 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 11 Jan 2022 10:41:54 -0800
Subject: [PATCH] ensure m_true is assigned #5753

---
 src/sat/smt/bv_internalize.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index 77115b441..8496717eb 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -371,6 +371,7 @@ namespace bv {
         if (m_true == sat::null_literal) {
             ctx.push(value_trail<sat::literal>(m_true));
             m_true = ctx.internalize(m.mk_true(), false, true, false);
+            s().assign_unit(m_true);
         }
         return m_true;
     }