diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
index 8a761ea3a..782713d5c 100644
--- a/src/sat/sat_asymm_branch.cpp
+++ b/src/sat/sat_asymm_branch.cpp
@@ -188,8 +188,8 @@ namespace sat {
         case 1:
             TRACE("asymm_branch", tout << "produced unit clause: " << c[0] << "\n";);
             s.assign(c[0], justification());
-            s.del_clause(c);
             s.propagate_core(false); 
+            s.del_clause(c);
             SASSERT(s.inconsistent() || s.m_qhead == s.m_trail.size());
             return false; // check_missed_propagation() may fail, since m_clauses is not in a consistent state.
         case 2:
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index bd975115b..e744bc007 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -279,7 +279,10 @@ namespace sat {
             unsigned sz = c.size();
             if (sz == 0) {
                 s.set_conflict(justification());
-                return;
+                for (; it != end; ++it, ++it2) {
+                    *it2 = *it;
+                }
+                break;
             }
             if (sz == 1) {
                 s.assign(c[0], justification());