From 5f9973d8c4b1cbd86dadb58da8425d5e2acfc1a2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 7 Jun 2020 16:28:53 -0700
Subject: [PATCH] fix #4508

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/ba_solver.cpp | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 2905d334c..ee74e90a2 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -330,7 +330,7 @@ namespace sat {
         m_stats.m_num_conflicts++;
         TRACE("ba", display(tout, c, true); );
         if (!validate_conflict(c)) {
-            display(std::cout, c, true);
+            IF_VERBOSE(0, display(verbose_stream(), c, true));
             UNREACHABLE();
         }
         SASSERT(validate_conflict(c));
@@ -2941,6 +2941,8 @@ namespace sat {
 
     void ba_solver::pre_simplify() {
         VERIFY(s().at_base_lvl());
+        if (s().inconsistent())
+            return;
         m_constraint_removed = false;
         xor_finder xf(s());
         for (unsigned sz = m_constraints.size(), i = 0; i < sz; ++i) pre_simplify(xf, *m_constraints[i]);
@@ -2983,6 +2985,8 @@ namespace sat {
 
     void ba_solver::simplify() {        
         if (!s().at_base_lvl()) s().pop_to_base_level();
+        if (s().inconsistent())
+            return;
         unsigned trail_sz, count = 0;
         do {
             trail_sz = s().init_trail_size();