diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp
index 6b16968c2..637d9a17f 100644
--- a/src/muz_qe/dl_instruction.cpp
+++ b/src/muz_qe/dl_instruction.cpp
@@ -528,9 +528,9 @@ namespace datalog {
 
     class instr_filter_interpreted_and_project : public instruction {
         reg_idx m_src;
-        reg_idx m_res;
         app_ref m_cond;
         unsigned_vector m_cols;
+        reg_idx m_res;
     public:
         instr_filter_interpreted_and_project(reg_idx src, app_ref & condition,
             unsigned col_cnt, const unsigned * removed_cols, reg_idx result)
diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
index 81d631e4e..b8ac520b2 100644
--- a/src/sat/sat_asymm_branch.cpp
+++ b/src/sat/sat_asymm_branch.cpp
@@ -72,11 +72,14 @@ namespace sat {
         int limit  = -static_cast<int>(m_asymm_branch_limit);
         std::stable_sort(s.m_clauses.begin(), s.m_clauses.end(), clause_size_lt());
         m_counter -= s.m_clauses.size();
+        SASSERT(s.m_qhead == s.m_trail.size());
         clause_vector::iterator it  = s.m_clauses.begin();
         clause_vector::iterator it2 = it;
         clause_vector::iterator end = s.m_clauses.end();
         try {
             for (; it != end; ++it) {
+                if (s.inconsistent())
+                    break;
                 SASSERT(s.m_qhead == s.m_trail.size());
                 if (m_counter < limit || s.inconsistent()) {
                     *it2 = *it;
@@ -111,6 +114,7 @@ namespace sat {
     bool asymm_branch::process(clause & c) {
         TRACE("asymm_branch_detail", tout << "processing: " << c << "\n";);
         SASSERT(s.scope_lvl() == 0);
+        SASSERT(s.m_qhead == s.m_trail.size());
 #ifdef Z3DEBUG
         unsigned trail_sz = s.m_trail.size();
 #endif
@@ -143,6 +147,7 @@ namespace sat {
         SASSERT(!s.inconsistent());
         SASSERT(s.scope_lvl() == 0);
         SASSERT(trail_sz == s.m_trail.size());
+        SASSERT(s.m_qhead == s.m_trail.size());
         if (i == sz - 1) {
             // clause size can't be reduced.
             s.attach_clause(c);
@@ -181,15 +186,18 @@ namespace sat {
             s.assign(c[0], justification());
             s.del_clause(c);
             s.propagate_core(false); 
+            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:
             SASSERT(s.value(c[0]) == l_undef && s.value(c[1]) == l_undef);
             s.mk_bin_clause(c[0], c[1], false);
             s.del_clause(c);
+            SASSERT(s.m_qhead == s.m_trail.size());
             return false;
         default:
             c.shrink(new_sz);
             s.attach_clause(c);
+            SASSERT(s.m_qhead == s.m_trail.size());
             return true;
         }
     }
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 51006b2c9..ba0c67235 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -632,7 +632,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";);
@@ -823,7 +824,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) {