diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index cd7f23576..edf1c82a2 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -2294,8 +2294,8 @@ namespace sat {
             // literal is no longer watched.
             return l_undef;
         }
-        SASSERT(index <= bound);
-        SASSERT(c[index] == alit);
+        VERIFY(index <= bound);
+        VERIFY(c[index] == alit);
         
         // find a literal to swap with:
         for (unsigned i = bound + 1; i < sz; ++i) {
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index 6b8d4cba7..a8eb09278 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -181,8 +181,9 @@ namespace sat {
         for (bool_var v : to_elim) {
             literal  l(v, false);
             literal r  = roots[v];
-            SASSERT(v != r.var());
-            if (m_solver.is_external(v) || !m_solver.set_root(l, r)) {
+            SASSERT(v != r.var());            
+            if (m_solver.is_external(v)) {
+                m_solver.set_root(l, r);
                 // cannot really eliminate v, since we have to notify extension of future assignments
                 m_solver.mk_bin_clause(~l, r, false);
                 m_solver.mk_bin_clause(l, ~r, false);