From 1ef83351cb8dd39898f4530f5618e681ac079c5f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 9 Feb 2020 12:32:11 -0800 Subject: [PATCH] fix #2963 Signed-off-by: Nikolaj Bjorner --- src/qe/qe_sat_tactic.cpp | 4 ++-- src/smt/theory_bv.cpp | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/qe/qe_sat_tactic.cpp b/src/qe/qe_sat_tactic.cpp index d9858b3c1..6eb697880 100644 --- a/src/qe/qe_sat_tactic.cpp +++ b/src/qe/qe_sat_tactic.cpp @@ -672,9 +672,9 @@ namespace qe { lbool r = solver.check(); m_assignments.reset(); solver.get_assignments(m_assignments); + if(r == l_true && i == 0) solver.get_model(model); solver.pop(1); - check_success(r != l_undef); - if (r == l_true && i == 0) solver.get_model(model); + check_success(r != l_undef); return r == l_true; } diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 3442cd369..b8034b19d 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -529,6 +529,7 @@ namespace smt { bool theory_bv::get_fixed_value(app* x, numeral & result) const { context& ctx = get_context(); + CTRACE("bv", !ctx.e_internalized(x), tout << "not internalized " << mk_pp(x, get_manager()) << "\n";); if (!ctx.e_internalized(x)) return false; enode * e = ctx.get_enode(x); theory_var v = e->get_th_var(get_id());