diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 623c73758..47c4b6150 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -625,7 +625,8 @@ namespace sat {
         case 1:
             TRACE("elim_lit", tout << "clause became unit: " << c[0] << "\n";);
             propagate_unit(c[0]);
-            remove_clause(c);
+            // propagate_unit will delete c.
+            // remove_clause(c);
             return;
         case 2:
             TRACE("elim_lit", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
@@ -816,7 +817,8 @@ namespace sat {
                 }
                 if (sz == 1) {
                     propagate_unit(c[0]);
-                    remove_clause(c);
+                    // propagate_unit will delete c.
+                    // remove_clause(c);
                     continue;
                 }
                 if (sz == 2) {