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

fix #7510

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-15 13:12:20 -08:00
parent a84130e844
commit 5365952796
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_model_checker.cpp
View file

@ -520,6 +520,8 @@ namespace smt {
m_context->is_relevant(q) && m_context->is_relevant(q) &&
m_context->get_assignment(q) == l_true && m_context->get_assignment(q) == l_true &&
(!m_context->get_fparams().m_ematching || !m.is_lambda_def(q)))) { (!m_context->get_fparams().m_ematching || !m.is_lambda_def(q)))) {
if (!m_qm->mbqi_enabled(q))
++num_failures;
continue; continue;
} }
@ -528,7 +530,7 @@ namespace smt {
tout << m_context->get_assignment(q) << "\n";); tout << m_context->get_assignment(q) << "\n";);
if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) { if (m_params.m_mbqi_trace && q->get_qid() != symbol::null) {
verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n"; IF_VERBOSE(1, verbose_stream() << "(smt.mbqi :checking " << q->get_qid() << ")\n");
} }
found_relevant = true; found_relevant = true;
if (!check(q)) { if (!check(q)) {