diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp
index bebb3e384..b097b3462 100644
--- a/src/sat/sat_model_converter.cpp
+++ b/src/sat/sat_model_converter.cpp
@@ -75,7 +75,7 @@ namespace sat {
     void model_converter::operator()(model & m) const {
         vector<entry>::const_iterator begin = m_entries.begin();
         vector<entry>::const_iterator it    = m_entries.end();
-        bool first = true; // false; // true; // false; // true;
+        bool first = false; // true; // false; // // true;
         //SASSERT(!m_solver || m_solver->check_clauses(m));
         while (it != begin) {
             --it;
@@ -101,6 +101,7 @@ namespace sat {
                     if (!sat && it->get_kind() != ATE && v0 != null_bool_var) {     
                         VERIFY(legal_to_flip(v0));                        
                         m[v0] = var_sign ? l_false : l_true;
+                        //IF_VERBOSE(0, verbose_stream() << "assign " << v0 << " "<< m[v0] << "\n");
                     }
                     elim_stack* st = it->m_elim_stack[index];
                     if (st) {
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index ae156cb4b..c048740ac 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1186,7 +1186,8 @@ namespace sat {
            This routine removes literals that were not relevant to establishing it was blocked.
 
            It has a bug: literals that are used to prune tautologies during resolution intersection should be included
-           in the dependencies.
+           in the dependencies. They may get used in some RI prunings and then they have to be included to avoid flipping
+           RI literals.
          */
         void minimize_covered_clause(unsigned idx) {
             // IF_VERBOSE(0, verbose_stream() << "minimize: " << m_covered_clause 
@@ -1211,8 +1212,8 @@ namespace sat {
             }
             for (unsigned i = idx; i > 0; --i) {
                 literal lit = m_covered_clause[i];
-                //s.mark_visited(lit);
-                //continue;
+                s.mark_visited(lit);
+                continue;
                 if (!s.is_marked(lit)) continue;
                 clause_ante const& ante = m_covered_antecedent[i];
                 if (ante.cls()) {
@@ -1630,13 +1631,6 @@ namespace sat {
             for (literal l2 : m_intersection) {
                 watched* w = find_binary_watch(s.get_wlist(~l), ~l2);
                 if (!w) {
-#if 0
-                    IF_VERBOSE(0, verbose_stream() << "bca " << l << " " << ~l2 << "\n"); 
-                    if (l.var() == 10219 && l2.var() == 10202) {
-                        IF_VERBOSE(0, s.s.display(verbose_stream()));
-                        exit(0);
-                    }
-#endif
                     s.s.mk_bin_clause(l, ~l2, true);
                     ++s.m_num_bca;
                 }