diff --git a/src/sat/sat_mus.cpp b/src/sat/sat_mus.cpp
index 7717fe795..db1e90b39 100644
--- a/src/sat/sat_mus.cpp
+++ b/src/sat/sat_mus.cpp
@@ -37,7 +37,6 @@ namespace sat {
         m_core.append(m_mus);                
         s.m_core.reset();
         s.m_core.append(m_core);
-        m_model.reset();
     }
 
     lbool mus::operator()() {
@@ -47,8 +46,7 @@ namespace sat {
         reset();
         literal_vector& core = m_core;
         literal_vector& mus = m_mus;
-        core.append(s.get_core());
-        
+        core.append(s.get_core());        
 
         while (!core.empty()) {
             TRACE("sat", 
@@ -74,14 +72,9 @@ namespace sat {
             case l_true: {
                 SASSERT(value_at(lit, s.get_model()) == l_false);
                 mus.push_back(lit);
-                if (core.empty()) {
-                    break;
+                if (!core.empty()) {
+                    // mr(); // TBD: measure
                 }
-                // sz = core.size();
-                // measure_mr();
-                // core.append(mus);
-                // rmr();
-                // core.resize(sz);
                 break;
             }
             case l_false:
@@ -105,141 +98,27 @@ namespace sat {
         return l_true;
     }
 
-    void mus::measure_mr() {
-        model const& m2 = s.get_model();
-        if (!m_model.empty()) {
-            unsigned n = 0;
-            for (unsigned i = 0; i < m_model.size(); ++i) {
-                if (m2[i] != m_model[i]) ++n;
-            }
-            std::cout << "model diff: " << n << " out of " << m_model.size() << "\n";
-        }
-        m_model.reset();
-        m_model.append(m2); 
-
+    void mus::mr() {
         sls sls(s);
         literal_vector tabu;
         tabu.append(m_mus);
         tabu.append(m_core);
+        bool reuse_model = false;
         for (unsigned i = m_mus.size(); i < tabu.size(); ++i) {
             tabu[i] = ~tabu[i];
-            lbool is_sat = sls(tabu.size(), tabu.c_ptr()); 
+            lbool is_sat = sls(tabu.size(), tabu.c_ptr(), reuse_model); 
             tabu[i] = ~tabu[i];
-            switch (is_sat) {
-            case l_true:
-                //m_mus.push_back(tabu[i]);
-                //m_core.erase(tabu[i]);
-                std::cout << "in core " << tabu[i] << "\n";
-                break;
-            default:
-                break;
+            if (is_sat == l_true) {
+                m_mus.push_back(tabu[i]);
+                m_core.erase(tabu[i]);
+                IF_VERBOSE(2, verbose_stream() << "in core " << tabu[i] << "\n";);
+                reuse_model = true;
+            }
+            else {
+                IF_VERBOSE(2, verbose_stream() << "NOT in core " << tabu[i] << "\n";);
+                reuse_model = false;
             }
         }
     }
-
-    // 
-    // TBD: eager model rotation allows rotating the same clause 
-    // several times with respect to different models.
-    // 
-    void mus::rmr() {
-        return;
-#if 0
-        model& model = s.m_model;
-        literal lit = m_mus.back();
-        literal assumption_lit;
-        SASSERT(value_at(lit, model) == l_false); 
-        // literal is false in current model.
-        unsigned sz = m_toswap.size();
-        find_swappable(lit);
-        unsigned sz1 = m_toswap.size();
-        for (unsigned i = sz; i < sz1; ++i) {
-            lit = m_toswap[i];
-            SASSERT(value_at(lit, model) == l_false);  
-            model[lit.var()] = ~model[lit.var()];    // swap assignment
-            if (has_single_unsat(assumption_lit) && !m_mus.contains(assumption_lit)) {
-                m_mus.push_back(assumption_lit);
-                rmr();
-            }
-            model[lit.var()] = ~model[lit.var()];    // swap assignment back            
-        }
-        m_toswap.resize(sz);
-#endif
-    }
-
-    bool mus::has_single_unsat(literal& assumption_lit) {
-        model const& model = s.get_model();
-        return false;
-    }
-
-    //
-    // lit is false in model.
-    // find clauses where ~lit occurs, and all other literals
-    // are false in model.
-    // for each of the probed literals, determine if swapping the
-    // assignment falsifies a hard clause, if not, add to m_toswap.
-    // 
-
-    void mus::find_swappable(literal lit) {
-        IF_VERBOSE(3, verbose_stream() << "(sat.mus swap " << lit << ")\n";);
-        unsigned sz = m_toswap.size();
-        literal lit2, lit3;
-        model const& model = s.get_model();
-        SASSERT(value_at(lit, model) == l_false);  
-        watch_list const& wlist = s.get_wlist(lit);
-        watch_list::const_iterator it  = wlist.begin();
-        watch_list::const_iterator end = wlist.end();
-        unsigned num_cand = 0;
-        for (; it != end && num_cand <= 1; ++it) {
-            switch (it->get_kind()) {
-            case watched::BINARY:
-                if (it->is_learned()) {
-                    break;
-                }
-                lit2 = it->get_literal();
-                if (value_at(lit2, model) == l_true) {
-                    break;
-                }
-                IF_VERBOSE(1, verbose_stream() << "(" << ~lit << " " << lit2 << ") ";);
-                TRACE("sat", tout << ~lit << " " << lit2 << "\n";);
-                ++num_cand;
-                break;
-            case watched::TERNARY:
-                lit2 = it->get_literal1();
-                lit3 = it->get_literal2();
-                if (value_at(lit2, model) == l_true) {
-                    break;
-                }
-                if (value_at(lit3, model) == l_true) {
-                    break;
-                }
-
-                IF_VERBOSE(1, verbose_stream() << "(" << ~lit << " " << lit2 << " " << lit3 << ") ";);
-                ++num_cand;
-                break;
-            case watched::CLAUSE: {
-                clause_offset cls_off = it->get_clause_offset();
-                clause& c = *(s.m_cls_allocator.get_clause(cls_off));
-                if (c.is_learned()) {
-                    break;
-                }
-                ++num_cand;
-                IF_VERBOSE(1, verbose_stream() << c << " ";);
-                TRACE("sat", tout << c << "\n";);
-                break;
-            }
-            case watched::EXT_CONSTRAINT:
-                TRACE("sat", tout << "external constraint - should avoid rmr\n";);
-                return;
-            }
-        }
-        if (num_cand > 1) {
-            m_toswap.resize(sz);
-        }
-        else {
-            IF_VERBOSE(1, verbose_stream() << "wlist size: " << num_cand << " " << m_core.size() << "\n";);
-        }
-
-    }
-
 }
 
diff --git a/src/sat/sat_mus.h b/src/sat/sat_mus.h
index 964bddfe5..c91464394 100644
--- a/src/sat/sat_mus.h
+++ b/src/sat/sat_mus.h
@@ -23,8 +23,6 @@ namespace sat {
     class mus {
         literal_vector m_core;
         literal_vector m_mus;
-        literal_vector m_toswap;        
-        model m_model;
 
         solver& s;
     public:
@@ -33,10 +31,7 @@ namespace sat {
         lbool operator()();
     private:
         lbool mus2();
-        void rmr();
-        void measure_mr();
-        bool has_single_unsat(literal& assumption_lit);
-        void find_swappable(literal lit);
+        void mr();
         void reset();
         void set_core();
     };
diff --git a/src/sat/sat_sls.cpp b/src/sat/sat_sls.cpp
index 615cd7e2c..04c8d0605 100644
--- a/src/sat/sat_sls.cpp
+++ b/src/sat/sat_sls.cpp
@@ -53,6 +53,7 @@ namespace sat {
     sls::sls(solver& s): s(s) {
         m_max_tries = 10000;
         m_prob_choose_min_var = 43;
+        m_clause_generation = 0;
     }
 
     sls::~sls() {
@@ -61,12 +62,13 @@ namespace sat {
         }
     }
 
-    lbool sls::operator()(unsigned sz, literal const* tabu) {
-        init(sz, tabu);
-        
-        for (unsigned i = 0; !m_false.empty() && i < m_max_tries; ++i) {
+    lbool sls::operator()(unsigned sz, literal const* tabu, bool reuse_model) {
+        init(sz, tabu, reuse_model);
+        unsigned i;
+        for (i = 0; !m_false.empty() && i < m_max_tries; ++i) {
             flip();
         }
+        IF_VERBOSE(2, verbose_stream() << "tries " << i << "\n";);
         if (m_false.empty()) {
             SASSERT(s.check_model(m_model));
             return l_true;
@@ -74,10 +76,18 @@ namespace sat {
         return l_undef;
     }
 
-    void sls::init(unsigned sz, literal const* tabu) {
-        init_clauses();
-        init_model(sz, tabu);
-        init_use();            
+    void sls::init(unsigned sz, literal const* tabu, bool reuse_model) {
+        bool same_generation = (m_clause_generation == s.m_stats.m_non_learned_generation);
+        if (!same_generation) {
+            init_clauses();
+            init_use();          
+            IF_VERBOSE(0, verbose_stream() << s.m_stats.m_non_learned_generation << " " << m_clause_generation << "\n";);  
+        }
+        if (!reuse_model) {
+            init_model();
+        }
+        init_tabu(sz, tabu);
+        m_clause_generation = s.m_stats.m_non_learned_generation;
     }
 
     void sls::init_clauses() {
@@ -97,22 +107,17 @@ namespace sat {
         for (unsigned i = 0; i < bincs.size(); ++i) {
             lits[0] = bincs[i].first;
             lits[1] = bincs[i].second;
-            m_clauses.push_back(m_alloc.mk_clause(2, lits, false));
+            clause* cl = m_alloc.mk_clause(2, lits, false);
+            m_clauses.push_back(cl);
+            m_bin_clauses.push_back(cl);
         }
     }
 
-    void sls::init_model(unsigned sz, literal const* tabu) {
+    void sls::init_model() {
         m_num_true.reset();
         m_model.reset();
         m_model.append(s.get_model());
-        m_tabu.reset();
-        m_tabu.resize(s.num_vars(), false);
-        for (unsigned i = 0; i < sz; ++i) {
-            m_model[tabu[i].var()] = tabu[i].sign()?l_false:l_true;
-            SASSERT(value_at(tabu[i], m_model) == l_true);
-        }
-
-        sz = m_clauses.size();
+        unsigned sz = m_clauses.size();
         for (unsigned i = 0; i < sz; ++i) {
             clause const& c = *m_clauses[i];
             unsigned n = 0;
@@ -136,7 +141,32 @@ namespace sat {
             if (n == 0) {
                 m_false.insert(i);
             }
-        }        
+        } 
+    }
+
+    void sls::init_tabu(unsigned sz, literal const* tabu) {        
+        // our main use is where m_model satisfies all the hard constraints.
+        // SASSERT(s.check_model(m_model));
+        // SASSERT(m_false.empty());
+        // ASSERT: m_num_true is correct count.       
+        m_tabu.reset();
+        m_tabu.resize(s.num_vars(), false);
+        for (unsigned i = 0; i < sz; ++i) {
+            literal lit = tabu[i];
+            if (s.m_level[lit.var()] == 0) continue;
+            if (value_at(lit, m_model) == l_false) {
+                flip(lit);                
+            }
+            m_tabu[lit.var()] = true;
+        }
+        for (unsigned i = 0; i < s.m_trail.size(); ++i) {
+            literal lit = s.m_trail[i];
+            if (s.m_level[lit.var()] > 0) break;
+            if (value_at(lit, m_model) != l_true) {
+                flip(lit);
+            }           
+            m_tabu[lit.var()] = true;
+        }    
     }
 
     void sls::init_use() {
@@ -191,7 +221,7 @@ namespace sat {
                 m_min_vars.push_back(lit);
             }
         }
-        if (min_break == 0 || (m_min_vars.empty() && m_rand(100) >= m_prob_choose_min_var)) {
+        if (min_break == 0 || (!m_min_vars.empty() && m_rand(100) >= m_prob_choose_min_var)) {
             lit = m_min_vars[m_rand(m_min_vars.size())];
             return true;
         }
@@ -206,8 +236,15 @@ namespace sat {
 
     void sls::flip() {
         literal lit;
-        if (!pick_flip(lit)) return;
+        if (pick_flip(lit)) {
+            flip(lit);
+        }
+    }
+
+    void sls::flip(literal lit) {
+        // IF_VERBOSE(0, verbose_stream() << lit << " ";);
         SASSERT(value_at(lit, m_model) == l_false);
+        SASSERT(!m_tabu[lit.var()]);
         m_model[lit.var()] = lit.sign()?l_false:l_true;
         SASSERT(value_at(lit, m_model) == l_true);
         unsigned_vector const& use1 = get_use(lit);
diff --git a/src/sat/sat_sls.h b/src/sat/sat_sls.h
index f651b3123..6237c5b13 100644
--- a/src/sat/sat_sls.h
+++ b/src/sat/sat_sls.h
@@ -42,6 +42,7 @@ namespace sat {
         random_gen m_rand;
         unsigned   m_max_tries;
         unsigned   m_prob_choose_min_var;      // number between 0 and 99.
+        unsigned   m_clause_generation;
         ptr_vector<clause const>    m_clauses; // vector of all clauses.
         index_set        m_false;              // clauses currently false
         vector<unsigned_vector>  m_use_list;   // use lists for literals
@@ -54,15 +55,17 @@ namespace sat {
     public:
         sls(solver& s);
         ~sls();        
-        lbool operator()(unsigned sz, literal const* tabu);
+        lbool operator()(unsigned sz, literal const* tabu, bool reuse_model);
     private:
         bool local_search();
-        void init(unsigned sz, literal const* tabu);
-        void init_model(unsigned sz, literal const* tabu);
+        void init(unsigned sz, literal const* tabu, bool reuse_model);
+        void init_tabu(unsigned sz, literal const* tabu);
+        void init_model();
         void init_use();
         void init_clauses();
         bool pick_flip(literal& lit);
         void flip();
+        void flip(literal lit);
         unsigned get_break_count(literal lit, unsigned min_break);
         unsigned_vector const& get_use(literal lit);        
     };
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 25ad62361..c100f15b1 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -61,6 +61,7 @@ namespace sat {
         for (clause * const * it = begin; it != end; ++it) {
             m_cls_allocator.del_clause(*it);
         }
+        ++m_stats.m_non_learned_generation;
     }
 
     void solver::copy(solver const & src) {
@@ -165,6 +166,12 @@ namespace sat {
         mk_clause(3, ls);
     }
 
+    void solver::del_clause(clause& c) {
+        m_cls_allocator.del_clause(&c); 
+        m_stats.m_del_clause++; 
+        if (!c.is_learned()) m_stats.m_non_learned_generation++;
+    }
+
     clause * solver::mk_clause_core(unsigned num_lits, literal * lits, bool learned) {
         TRACE("sat", tout << "mk_clause: " << mk_lits_pp(num_lits, lits) << "\n";);
         if (!learned) {
@@ -173,7 +180,8 @@ namespace sat {
             if (!keep) {
                 return 0; // clause is equivalent to true.
             }
-        }
+            ++m_stats.m_non_learned_generation;
+        }        
 
         switch (num_lits) {
         case 0:
@@ -2690,6 +2698,7 @@ namespace sat {
         m_del_clause = 0;
         m_minimized_lits = 0;
         m_dyn_sub_res = 0;
+        m_non_learned_generation = 0;
     }
 
     void mk_stat::display(std::ostream & out) const {
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 804bea5ce..33e88f64e 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -58,6 +58,7 @@ namespace sat {
         unsigned m_del_clause;
         unsigned m_minimized_lits;
         unsigned m_dyn_sub_res;
+        unsigned m_non_learned_generation;
         stats() { reset(); }
         void reset();
         void collect_statistics(statistics & st) const;
@@ -173,7 +174,7 @@ namespace sat {
         void mk_clause(literal l1, literal l2, literal l3);
 
     protected:
-        void del_clause(clause & c) { m_cls_allocator.del_clause(&c); m_stats.m_del_clause++; }
+        void del_clause(clause & c);
         clause * mk_clause_core(unsigned num_lits, literal * lits, bool learned);
         void mk_bin_clause(literal l1, literal l2, bool learned);
         bool propagate_bin_clause(literal l1, literal l2);