From 11ab583232c52d71a30311c3b7836beedb442835 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 19 Oct 2023 10:34:31 -0700
Subject: [PATCH] fix #6956

---
 src/smt/smt_consequences.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index cac8d40b1..fe2bd7149 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -274,6 +274,12 @@ namespace smt {
                                     expr_ref_vector& conseq, 
                                     expr_ref_vector& unfixed) {
 
+        for (expr* a : assumptions0)
+            if (!m.is_bool(a)) {
+                std::string msg = std::string("assumption ") + mk_pp(a, m) + std::string(" is not Boolean");
+                warning_msg(msg.c_str());
+                throw default_exception(msg.c_str());
+            }
         m_antecedents.reset();
         m_antecedents.insert(true_literal.var(), index_set());
         pop_to_base_lvl();