diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 566623eed..65a81d2e1 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3226,7 +3226,9 @@ namespace smt { return true; if (!is_app(a)) return false; - if (m.is_true(a) || m.is_false(a)) + if (m.is_false(a)) + return false; + if (m.is_true(a)) return true; if (is_app(a) && to_app(a)->get_family_id() == m.get_basic_family_id()) return false;