diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 34d63547b..40e9e6570 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2007,12 +2007,38 @@ namespace smt {
        Reduce the size of v to old_size.
     */
     void context::del_clauses(clause_vector & v, unsigned old_size) {
-        SASSERT(old_size <= v.size());
+        unsigned num_collect = v.size() - old_size;
+        if (num_collect == 0)
+            return;
+        
         clause_vector::iterator begin = v.begin() + old_size;
         clause_vector::iterator it    = v.end();
-        while (it != begin) {
-            --it;
-            del_clause(false, *it);
+        if (num_collect > 1000) {
+            uint_set watches;
+            while (it != begin) {
+                --it;
+                clause* c = *it;
+                remove_lit_occs(*c, get_num_bool_vars());
+                if (!c->deleted()) {
+                    c->mark_as_deleted(m);                    
+                }
+                watches.insert((~c->get_literal(0)).index());
+                watches.insert((~c->get_literal(1)).index());
+            }
+            for (auto w: watches) {
+                m_watches[w].remove_deleted();
+            }
+            for (it = v.end(); it != begin; ) {
+                --it;
+                (*it)->deallocate(m);
+            }
+            m_stats.m_num_del_clause += (v.size() - old_size);
+        }
+        else {
+            while (it != begin) {
+                --it;
+                del_clause(false, *it);
+            }
         }
         v.shrink(old_size);
     }
diff --git a/src/smt/watch_list.cpp b/src/smt/watch_list.cpp
index f95e1c571..5cb28a312 100644
--- a/src/smt/watch_list.cpp
+++ b/src/smt/watch_list.cpp
@@ -94,6 +94,20 @@ namespace smt {
         }
         end_cls_core() -= sizeof(clause *);
     }
+
+    void watch_list::remove_deleted() {
+        clause_iterator end = end_clause();
+        clause_iterator it = begin_clause();
+        clause_iterator prev = it;
+        unsigned num_deleted = 0;
+        for (; it != end; ++it) {
+            if ((*it)->deleted())
+                ++num_deleted;
+            else 
+                *prev++ = *it;
+        }
+        end_cls_core() -= num_deleted * sizeof(clause *);
+    }
     
     void watch_list::remove_literal(literal l) {
         literal * begin = begin_literals();
diff --git a/src/smt/watch_list.h b/src/smt/watch_list.h
index 0b49f0cca..0344ad74d 100644
--- a/src/smt/watch_list.h
+++ b/src/smt/watch_list.h
@@ -171,6 +171,8 @@ namespace smt {
         }
         
         void remove_clause(clause * c);
+
+        void remove_deleted();
         
         void remove_literal(literal l);