mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 14:49:01 +00:00
Code Activity

fix non-termination

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-10-29 23:39:39 -07:00
parent 0a404f94be
commit 289f8360f2
2 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/ast/simplifiers/elim_unconstrained.cpp
View file

@ -175,7 +175,7 @@ void elim_unconstrained::eliminate() {
if (!inverted)
continue;
IF_VERBOSE(1, verbose_stream() << "replace " << mk_bounded_pp(t, m) << " / " << mk_bounded_pp(rr, m) << " -> " << mk_bounded_pp(r, m) << "\n");
IF_VERBOSE(4, verbose_stream() << "replace " << mk_bounded_pp(t, m) << " / " << mk_bounded_pp(rr, m) << " -> " << mk_bounded_pp(r, m) << "\n");
TRACE("elim_unconstrained", tout << mk_bounded_pp(t, m) << " / " << mk_bounded_pp(rr, m) << " -> " << mk_bounded_pp(r, m) << "\n");
@ -309,8 +309,10 @@ expr* elim_unconstrained::reconstruct_term(node& n) {
expr_ref new_t(m);
while (!todo.empty()) {
node* np = todo.back();
if (!np->is_dirty())
if (!np->is_dirty()) {
todo.pop_back();
continue;
}
SASSERT(np->is_root());
auto t = np->term();
unsigned sz0 = todo.size();

2
src/sat/smt/intblast_solver.cpp
View file

@ -492,14 +492,12 @@ namespace intblast {
else {
expr_ref bv2int(bv.mk_bv2int(n->get_expr()), m);
euf::enode* b2i = ctx.get_enode(bv2int);
if (!b2i) verbose_stream() << bv2int << "\n";
SASSERT(b2i);
VERIFY(b2i);
arith::arith_value av(ctx);
rational r;
VERIFY(av.get_value(b2i->get_expr(), r));
value = bv.mk_numeral(r, bv.get_bv_size(n->get_expr()));
verbose_stream() << ctx.bpp(n) << " := " << value << "\n";
}
values.set(n->get_root_id(), value);
TRACE("model", tout << "add_value " << ctx.bpp(n) << " := " << value << "\n");