From bdf3689c6e3af9acda353831bfdd645b1b90e886 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 27 Oct 2024 18:53:25 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/smt/theory_intblast.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_intblast.cpp b/src/smt/theory_intblast.cpp index 82feb39bc..a07bf9591 100644 --- a/src/smt/theory_intblast.cpp +++ b/src/smt/theory_intblast.cpp @@ -178,11 +178,13 @@ namespace smt { expr* e = n->get_expr(); SASSERT(bv.is_bv(e)); auto ie = m_translator.translated(e); - expr_ref val(m); rational r; if (bv.is_numeral(e, r)) ; + else if (!ctx.e_internalized(ie)) + ; // it is a compound expression, we don't have to evaluate it. else { + expr_ref val(m); VERIFY(ctx.get_value(ctx.get_enode(ie), val)); VERIFY(a.is_numeral(val, r)); }