fix #7292

Z3Prover · Jul 29, 2024 · 68b6ef0 · 68b6ef0
1 parent 25e683e
commit 68b6ef0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/qe/mbp/mbp_basic_tg.cpp b/src/qe/mbp/mbp_basic_tg.cpp
@@ -101,7 +101,7 @@ struct mbp_basic_tg::impl {
                 bool is_or = m.is_or(term);
                 app *c = to_app(term);
                 bool t = is_or ? any_of(*c, is_true) : all_of(*c, is_true);
-                bool f = is_or ? all_of(*c, is_false) : all_of(*c, is_false);
+                bool f = is_or ? all_of(*c, is_false) : any_of(*c, is_false);
                 if (t || f) {
                     mark_seen(term);
                     progress = true;