From 289f8360f2875138132187496a407a238ac56dd7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 Oct 2024 23:39:39 -0700 Subject: [PATCH] fix non-termination Signed-off-by: Nikolaj Bjorner --- src/ast/simplifiers/elim_unconstrained.cpp | 6 ++++-- src/sat/smt/intblast_solver.cpp | 2 -- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp index 5d563aabf..478eb0028 100644 --- a/src/ast/simplifiers/elim_unconstrained.cpp +++ b/src/ast/simplifiers/elim_unconstrained.cpp @@ -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(); diff --git a/src/sat/smt/intblast_solver.cpp b/src/sat/smt/intblast_solver.cpp index cef918a95..caca1e48c 100644 --- a/src/sat/smt/intblast_solver.cpp +++ b/src/sat/smt/intblast_solver.cpp @@ -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");