From d0add7e3d8ed56aa7b5e7ee1fed2fe4e35b45aa0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
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 1c7da4031..fa56c83c9 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -3233,7 +3233,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;