mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-25 15:23:41 +00:00
Code Activity

update model generation to fix model bug

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-11-01 14:41:15 -07:00
parent 55b64e1f29
commit 040c29a152
1 changed files with 10 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/smt/theory_intblast.cpp
View file

@ -174,15 +174,18 @@ namespace smt {
model_value_proc* theory_intblast::mk_value(enode* n, model_generator& mg) { model_value_proc* theory_intblast::mk_value(enode* n, model_generator& mg) {
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);
rational r; rational r;
expr* ie = nullptr;
expr_ref val(m); expr_ref val(m);
if (bv.is_numeral(e, r)) if (!bv.is_numeral(e, r)) {
; for (enode* sib : *n) {
else if (!ctx.e_internalized(ie)) ie = m_translator.translated(sib->get_expr());
; // it is a compound expression, we don't have to evaluate it. if (ctx.e_internalized(ie)) {
else if (ctx.get_value(ctx.get_enode(ie), val)) { ctx.get_value(ctx.get_enode(ie), val);
VERIFY(a.is_numeral(val, r)); VERIFY(a.is_numeral(val, r));
break;
}
}
} }
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)));
} }