mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 04:38:53 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-27 18:53:25 -07:00
parent 98bc3d392d
commit bdf3689c6e
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/theory_intblast.cpp
View file

@ -178,11 +178,13 @@ namespace smt {
expr* e = n->get_expr(); expr* e = n->get_expr();
SASSERT(bv.is_bv(e)); SASSERT(bv.is_bv(e));
auto ie = m_translator.translated(e); auto ie = m_translator.translated(e);
expr_ref val(m);
rational r; rational r;
if (bv.is_numeral(e, 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 { else {
expr_ref val(m);
VERIFY(ctx.get_value(ctx.get_enode(ie), val)); VERIFY(ctx.get_value(ctx.get_enode(ie), val));
VERIFY(a.is_numeral(val, r)); VERIFY(a.is_numeral(val, r));
} }