mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-29 09:28:45 +00:00
Code Activity

mk_value needs to accept more cases where integer expression doesn't evalate

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-27 19:03:20 -07:00
parent bdf3689c6e
commit 5e2cefea9f
1 changed files with 2 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_intblast.cpp
View file

@ -179,13 +179,12 @@ namespace smt {
SASSERT(bv.is_bv(e)); SASSERT(bv.is_bv(e));
auto ie = m_translator.translated(e); auto ie = m_translator.translated(e);
rational r; rational r;
expr_ref val(m);
if (bv.is_numeral(e, r)) if (bv.is_numeral(e, r))
; ;
else if (!ctx.e_internalized(ie)) else if (!ctx.e_internalized(ie))
; // it is a compound expression, we don't have to evaluate it. ; // it is a compound expression, we don't have to evaluate it.
else { else if (ctx.get_value(ctx.get_enode(ie), val)) {
expr_ref val(m);
VERIFY(ctx.get_value(ctx.get_enode(ie), val));
VERIFY(a.is_numeral(val, r)); VERIFY(a.is_numeral(val, r));
} }
return alloc(expr_wrapper_proc, m_factory->mk_num_value(r, bv.get_bv_size(e))); return alloc(expr_wrapper_proc, m_factory->mk_num_value(r, bv.get_bv_size(e)));