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();