mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

debugging #3511

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-29 17:34:24 -07:00
parent f74079de01
commit ba4765f16f
4 changed files with 20 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_context.cpp
View file

@ -3368,9 +3368,9 @@ namespace smt {
} }
if (r == l_true && gparams::get_value("model_validate") == "true") { if (r == l_true && gparams::get_value("model_validate") == "true") {
recfun::util u(m); recfun::util u(m);
model_ref mdl;
get_model(mdl);
if (u.get_rec_funs().empty()) { if (u.get_rec_funs().empty()) {
model_ref mdl;
get_model(mdl);
if (mdl.get()) { if (mdl.get()) {
for (theory* t : m_theory_set) { for (theory* t : m_theory_set) {
t->validate_model(*mdl); t->validate_model(*mdl);
@ -3384,7 +3384,7 @@ namespace smt {
if (lit.sign() ? m_model->is_true(v) : m_model->is_false(v)) { if (lit.sign() ? m_model->is_true(v) : m_model->is_false(v)) {
IF_VERBOSE(10, verbose_stream() IF_VERBOSE(10, verbose_stream()
<< "invalid assignment " << (lit.sign() ? "true" : "false") << "invalid assignment " << (lit.sign() ? "true" : "false")
<< " to #" << v->get_id() << " := " << mk_bounded_pp(v, m, 2) << "\n"); << " to #" << v->get_id() << " := " << mk_bounded_pp(v, m, 3) << "\n");
} }
} }
for (clause* cls : m_aux_clauses) { for (clause* cls : m_aux_clauses) {

10
src/smt/smt_context_inv.cpp
View file

@ -374,15 +374,17 @@ namespace smt {
case l_undef: case l_undef:
break; break;
case l_true: case l_true:
if (!m_proto_model->eval(n, res, false)) return true; if (!m_proto_model->eval(n, res, false))
CTRACE("mbqi_bug", !m.is_true(res), tout << n << " evaluates to " << res << "\n";); return true;
CTRACE("model", !m.is_true(res), tout << n << " evaluates to " << res << "\n";);
if (m.is_false(res)) { if (m.is_false(res)) {
return false; return false;
} }
break; break;
case l_false: case l_false:
if (!m_proto_model->eval(n, res, false)) return true; if (!m_proto_model->eval(n, res, false))
CTRACE("mbqi_bug", !m.is_false(res), tout << n << " evaluates to " << res << "\n";); return true;
CTRACE("model", !m.is_false(res), tout << n << " evaluates to " << res << "\n";);
if (m.is_true(res)) { if (m.is_true(res)) {
return false; return false;
} }

14
src/smt/tactic/ctx_solver_simplify_tactic.cpp
View file

@ -98,13 +98,14 @@ protected:
return; return;
SASSERT(m_solver.get_scope_level() == 0); SASSERT(m_solver.get_scope_level() == 0);
TRACE("ctx_solver_simplify_tactic", TRACE("ctx_solver_simplify_tactic",
for (unsigned i = 0; i < fmls.size(); ++i) { for (expr* f : fmls) {
tout << mk_pp(fmls[i], m) << "\n"; tout << mk_pp(f, m) << "\n";
} }
tout << "=>\n"; tout << "=>\n";
tout << mk_pp(fml, m) << "\n";); tout << fml << "\n";);
DEBUG_CODE( DEBUG_CODE(
{ {
// enable_trace("after_search");
m_solver.push(); m_solver.push();
expr_ref fml1(m); expr_ref fml1(m);
fml1 = mk_and(m, fmls.size(), fmls.c_ptr()); fml1 = mk_and(m, fmls.size(), fmls.c_ptr());
@ -114,9 +115,14 @@ protected:
lbool is_sat = m_solver.check(); lbool is_sat = m_solver.check();
TRACE("ctx_solver_simplify_tactic", tout << "is non-equivalence sat?: " << is_sat << "\n";); TRACE("ctx_solver_simplify_tactic", tout << "is non-equivalence sat?: " << is_sat << "\n";);
if (is_sat == l_true) { if (is_sat == l_true) {
model_ref mdl;
m_solver.get_model(mdl);
TRACE("ctx_solver_simplify_tactic", TRACE("ctx_solver_simplify_tactic",
tout << "result is not equivalent to input\n"; tout << "result is not equivalent to input\n";
tout << mk_pp(fml1, m) << "\n";); tout << mk_pp(fml1, m) << "\n";
tout << "evaluates to: " << (*mdl)(fml1) << "\n";
m_solver.display(tout) << "\n";
);
UNREACHABLE(); UNREACHABLE();
} }
m_solver.pop(1); m_solver.pop(1);

1
src/smt/theory_lra.cpp
View file

@ -1659,6 +1659,7 @@ public:
} }
final_check_status final_check_eh() { final_check_status final_check_eh() {
reset_variable_values();
IF_VERBOSE(12, verbose_stream() << "final-check " << m_solver->get_status() << "\n"); IF_VERBOSE(12, verbose_stream() << "final-check " << m_solver->get_status() << "\n");
m_use_nra_model = false; m_use_nra_model = false;
lbool is_sat = l_true; lbool is_sat = l_true;