diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 3b9b81448..e5dd057bb 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1389,7 +1389,7 @@ namespace sat {
                         }
                     }
                 }
-                else {
+                else if (lvl(lit) < m_conflict_lvl) {
                     slack -= std::abs(coeff);
                     m_lemma.push_back(~lit);
                 }
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index e384a944d..84a875d55 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -2536,8 +2536,13 @@ namespace sat {
         }
         num = i;
         // reset m_diff_levels.
-        for (i = 0; i < num; i++)
-            m_diff_levels[lvl(lits[i])] = false;
+        for (i = 0; i < num; i++) {
+            literal lit = lits[i];
+            if (value(lit) == l_false) {
+                VERIFY(lvl(lit) < m_diff_levels.size());
+                m_diff_levels[lvl(lit)] = false;
+            }
+        }
         return glue < max_glue;        
     }