diff --git a/src/ast/sls/sat_ddfw.cpp b/src/ast/sls/sat_ddfw.cpp
index e30e62399..ef68a7dd5 100644
--- a/src/ast/sls/sat_ddfw.cpp
+++ b/src/ast/sls/sat_ddfw.cpp
@@ -432,19 +432,26 @@ namespace sat {
         }
 #endif
 
-        m_num_models.reserve(m_unsat.size() + 1);
         if (m_unsat.size() < m_min_sz) 
             m_models.reset();        
         
         m_min_sz = m_unsat.size();
-        m_num_models.reserve(m_min_sz + 1);
-        m_num_models[m_min_sz]++;
 
-        if (m_num_models[m_min_sz] >= 10) {
-            if (m_num_models[m_min_sz] >= 200)
+#if 0
+        m_num_models.reserve(m_min_sz + 1);
+        unsigned nm = m_num_models[m_min_sz]++;
+        
+
+        if (nm >= 10) {
+            if (nm >= 200)
                 m_num_models[m_min_sz] = 10, m_restart_next = m_flips;
+            if (nm % 1 == 0) {
+                for (unsigned v = 0; v < num_vars(); ++v)
+                    bias(v) += value(v) ? 1 : -1;
+            }
             return;
         }
+#endif
 
         unsigned h = value_hash();
         unsigned occs = 0;
diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp
index 7bca0f3c8..fb721e168 100644
--- a/src/ast/sls/sls_euf_plugin.cpp
+++ b/src/ast/sls/sls_euf_plugin.cpp
@@ -137,8 +137,10 @@ namespace sls {
         while (slit != flit);
         // flip the last literal on the replay stack
         IF_VERBOSE(10, verbose_stream() << "sls.euf - flip " << flit << "\n");
+        ctx.add_clause(lits);
         ctx.flip(flit.var());        
         m_replay_stack.back().neg();
+
     }
 
     void euf_plugin::replay() {
@@ -342,7 +344,7 @@ namespace sls {
                     m_values.insert(t);
             }
         }
-        //validate_model();
+        // validate_model();
         return true;
     }
 
@@ -483,7 +485,7 @@ namespace sls {
     }
 
     void euf_plugin::collect_statistics(statistics& st) const {
-        st.update("sls.euf-conflict", m_stats.m_num_conflicts);
+        st.update("sls-euf-conflict", m_stats.m_num_conflicts);
     }
 
     void euf_plugin::reset_statistics() {