mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-12 02:04:43 +00:00
Code Activity

fixes to model construction

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-11-01 15:38:30 -07:00
parent 040c29a152
commit c7ec2afedb
1 changed files with 1 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/smt/theory_intblast.cpp
View file

@ -180,11 +180,8 @@ namespace smt {
if (!bv.is_numeral(e, r)) {
for (enode* sib : *n) {
ie = m_translator.translated(sib->get_expr());
if (ctx.e_internalized(ie)) {
ctx.get_value(ctx.get_enode(ie), val);
VERIFY(a.is_numeral(val, r));
if (ctx.e_internalized(ie) && ctx.get_value(ctx.get_enode(ie), val) && a.is_numeral(val, r))
break;
}
}
}
return alloc(expr_wrapper_proc, m_factory->mk_num_value(r, bv.get_bv_size(e)));