From ec4246463fd58fb5185f05e7c8674af12ab584cd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 28 Dec 2025 10:41:27 -0800 Subject: [PATCH] fix #8045 --- src/smt/smt_context.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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;