mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-05 08:30:50 +00:00
Code Activity

fix condition that skipped mbqi

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-06-01 19:56:54 -07:00
parent eaf7562a1d
commit 2dbe233f6a
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_model_checker.cpp
View file

@ -512,8 +512,7 @@ namespace smt {
for (quantifier * q : *m_qm) {
if (!(m_qm->mbqi_enabled(q) &&
m_context->is_relevant(q) &&
m_context->get_assignment(q) == l_true &&
(!m_context->get_fparams().m_ematching))) {
m_context->get_assignment(q) == l_true)) {
if (!m_qm->mbqi_enabled(q))
++num_failures;
continue;