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)); }