diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp
index b55e9fadd..97de59283 100644
--- a/src/ast/sls/sls_euf_plugin.cpp
+++ b/src/ast/sls/sls_euf_plugin.cpp
@@ -86,6 +86,7 @@ namespace sls {
         if (!g.inconsistent())
             return;
 
+        ++m_stats.m_num_conflicts;
         unsigned n = 1;
         sat::literal_vector lits;
         sat::literal flit = sat::null_literal, slit;
@@ -111,7 +112,7 @@ namespace sls {
         }
         while (slit != flit);
         // flip the last literal on the replay stack
-        IF_VERBOSE(2, verbose_stream() << "sls.euf - flip " << flit << "\n");
+        IF_VERBOSE(10, verbose_stream() << "sls.euf - flip " << flit << "\n");
         ctx.flip(flit.var());
         m_replay_stack.back().neg();
     }
@@ -142,6 +143,7 @@ namespace sls {
             auto a = g.find(x);
             auto b = g.find(y);
             g.merge(a, b, to_ptr(lit));
+            g.merge(g.find(e), g.find(m.mk_true()), to_ptr(lit));
         }
         else if (!lit.sign() && m.is_distinct(e)) {
             auto n = to_app(e)->get_num_args();
@@ -206,6 +208,7 @@ namespace sls {
                     flit = l;
             }
             ctx.add_clause(lits);
+            ++m_stats.m_num_conflicts;
             if (flit != sat::null_literal)
                 ctx.flip(flit.var());
         };   
@@ -406,4 +409,12 @@ namespace sls {
             }
         }
     }
+
+    void euf_plugin::collect_statistics(statistics& st) const {
+        st.update("sls.euf-conflict", m_stats.m_num_conflicts);
+    }
+
+    void euf_plugin::reset_statistics() {
+        m_stats.reset();
+    }
 }
diff --git a/src/ast/sls/sls_euf_plugin.h b/src/ast/sls/sls_euf_plugin.h
index 406243ea4..ce0afa529 100644
--- a/src/ast/sls/sls_euf_plugin.h
+++ b/src/ast/sls/sls_euf_plugin.h
@@ -23,6 +23,10 @@ Author:
 namespace sls {
     
     class euf_plugin : public plugin {
+        struct stats {
+            unsigned m_num_conflicts = 0;
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
         obj_map<func_decl, ptr_vector<app>> m_app;
         struct value_hash {
             euf_plugin& cc;
@@ -36,7 +40,10 @@ namespace sls {
         };
         hashtable<app*, value_hash, value_eq> m_values;
 
+
+
         bool m_incremental = false;
+        stats m_stats;
 
         scoped_ptr<euf::egraph> m_g;
         scoped_ptr<obj_map<sort, unsigned>> m_num_elems;
@@ -75,8 +82,8 @@ namespace sls {
         bool repair_down(app* e) override { return false; }
         void repair_literal(sat::literal lit) override {}
 
-        void collect_statistics(statistics& st) const override {}
-        void reset_statistics() override {}
+        void collect_statistics(statistics& st) const override;
+        void reset_statistics() override;
     };
     
 }