diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 6f3d0da2f..f1f32eef5 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1387,7 +1387,6 @@ namespace sat {
             IF_VERBOSE(20, verbose_stream() << "(sat.card slack: " << slack << " skipped: " << num_skipped << ")\n";);
             return false;
         }
-
         
         if (m_lemma[0] == null_literal) {
             if (m_lemma.size() == 1) {
diff --git a/src/sat/sat_elim_eqs.cpp b/src/sat/sat_elim_eqs.cpp
index 7580ebba5..d10bea7bb 100644
--- a/src/sat/sat_elim_eqs.cpp
+++ b/src/sat/sat_elim_eqs.cpp
@@ -229,7 +229,6 @@ namespace sat {
         cleanup_clauses(roots, m_solver.m_learned);
         if (m_solver.inconsistent()) return;
         save_elim(roots, to_elim);
-        VERIFY(check_clauses(roots));
         m_solver.propagate(false);
         SASSERT(check_clauses(roots));
     }
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 8011837dd..cc79e75ff 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -372,9 +372,6 @@ namespace sat {
 
     clause * solver::mk_nary_clause(unsigned num_lits, literal * lits, bool learned) {
         m_stats.m_mk_clause++;
-        for (unsigned i = 0; i + 1 < num_lits; ++i) {
-            VERIFY (lits[i] != ~lits[i + 1]);
-        }
         clause * r = m_cls_allocator.mk_clause(num_lits, lits, learned);
         SASSERT(!learned || r->is_learned());
         bool reinit = attach_nary_clause(*r);