diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg
index 451a07964..001681149 100644
--- a/src/params/smt_params_helper.pyg
+++ b/src/params/smt_params_helper.pyg
@@ -114,6 +114,7 @@ def_module_params(module_name='smt',
                           ('up.persist_clauses', BOOL, False, 'replay propagated clauses below the levels they are asserted'),
                           ('array.weak', BOOL, False, 'weak array theory'),
                           ('array.extensional', BOOL, True, 'extensional array theory'),
+                          ('finite_set.lattice_refutation', BOOL, True, 'enable lattice refutation for finite set theory'),
                           ('clause_proof', BOOL, False, 'record a clausal proof'),
                           ('dack', UINT, 1, '0 - disable dynamic ackermannization, 1 - expand Leibniz\'s axiom if a congruence is the root of a conflict, 2 - expand Leibniz\'s axiom if a congruence is used during conflict resolution'),
                           ('dack.eq', BOOL, False, 'enable dynamic ackermannization for transitivity of equalities'),
diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp
index 0d572e9d1..c98af1945 100644
--- a/src/smt/theory_finite_set.cpp
+++ b/src/smt/theory_finite_set.cpp
@@ -260,7 +260,8 @@ namespace smt {
             ctx.push_trail(push_back_vector(m_eqs));
             m_find.merge(v1, v2);  // triggers merge_eh, which triggers incremental generation of theory axioms
         }
-        m_lattice_refutation.add_equality(v1, v2);
+        if (ctx.get_fparams().m_finite_set_lattice_refutation)
+            m_lattice_refutation.add_equality(v1, v2);
 
         // Check if Z3 has a boolean variable for it
         TRACE(finite_set, tout << "new_eq_eh_r1: " << n1->get_root() << "r2: "<< n2->get_root() <<"\n";);
@@ -287,7 +288,8 @@ namespace smt {
             ctx.push_trail(push_back_vector(m_diseqs));
             m_axioms.extensionality_axiom(e1, e2);
         }
-        m_lattice_refutation.add_disequality(v1,v2);
+        if (ctx.get_fparams().m_finite_set_lattice_refutation)
+            m_lattice_refutation.add_disequality(v1,v2);
     }
 
     //