From 8c00181815369de87b45bbe015b5606ec7b9b5f2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 19 Oct 2023 10:41:24 -0700
Subject: [PATCH] fix #6955

---
 src/qe/qsat.cpp | 26 +++++++++++---------------
 1 file changed, 11 insertions(+), 15 deletions(-)

diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index fe4c4945c..6472a83c2 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -568,25 +568,21 @@ namespace qe {
             m_solver = nullptr;
         }
 
-      void assert_expr(expr *e) {
-        if (!m.is_true(e)) 
-          m_solver->assert_expr(e);
-      }
+        void assert_expr(expr* e) {
+            if (!m.is_true(e))
+                m_solver->assert_expr(e);
+        }
         void assert_blocking_fml(expr* e) {
-          if (m.is_true(e)) return;
-          if (m_last_assert) {
-            if (e == m_last_assert) {
-              verbose_stream() << "Asserting this expression twice in a row:\n " << m_last_assert << "\n";
-              SASSERT(false);
-              std::exit(3);
+            if (m.is_true(e))
+                return;
+            if (m_last_assert && e == m_last_assert && !m.is_false(e)) {
+                IF_VERBOSE(0, verbose_stream() << "Asserting this expression twice in a row:\n " << m_last_assert << "\n");
+                UNREACHABLE();
             }
-            
-          }
-          m_last_assert = e;
-
+            m_last_assert = e;
             m_solver->assert_expr(e);
         }
-        
+
         void get_core(expr_ref_vector& core) {
             core.reset();
             m_solver->get_unsat_core(core);