From c7ec2afedb80181c275d17c440d4f94e3bacc574 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 1 Nov 2024 15:38:30 -0700
Subject: [PATCH] fixes to model construction

---
 src/smt/theory_intblast.cpp | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

diff --git a/src/smt/theory_intblast.cpp b/src/smt/theory_intblast.cpp
index 85e8bf433..0e8b937d7 100644
--- a/src/smt/theory_intblast.cpp
+++ b/src/smt/theory_intblast.cpp
@@ -180,11 +180,8 @@ namespace smt {
         if (!bv.is_numeral(e, r)) {
             for (enode* sib : *n) {
                 ie = m_translator.translated(sib->get_expr());
-                if (ctx.e_internalized(ie)) {
-                    ctx.get_value(ctx.get_enode(ie), val);
-                    VERIFY(a.is_numeral(val, r));
+                if (ctx.e_internalized(ie) && ctx.get_value(ctx.get_enode(ie), val) && a.is_numeral(val, r))
                     break;
-                }
             }
         }
         return alloc(expr_wrapper_proc, m_factory->mk_num_value(r, bv.get_bv_size(e)));