diff --git a/examples/SMT-LIB2/finite-sets/cycle.smt2 b/examples/SMT-LIB2/finite-sets/cycle.smt2
new file mode 100644
index 000000000..a0d45b6b2
--- /dev/null
+++ b/examples/SMT-LIB2/finite-sets/cycle.smt2
@@ -0,0 +1,67 @@
+(declare-const s1 (FiniteSet Int))
+(declare-const s2 (FiniteSet Int))
+(declare-const s3 (FiniteSet Int))
+(declare-const s4 (FiniteSet Int))
+(declare-const s5 (FiniteSet Int))
+(declare-const s6 (FiniteSet Int))
+(declare-const s7 (FiniteSet Int))
+(declare-const s8 (FiniteSet Int))
+(declare-const s9 (FiniteSet Int))
+(declare-const s10 (FiniteSet Int))
+
+(declare-const s11 (FiniteSet Int))
+(declare-const s12 (FiniteSet Int))
+(declare-const s13 (FiniteSet Int))
+(declare-const s14 (FiniteSet Int))
+(declare-const s15 (FiniteSet Int))
+(declare-const s16 (FiniteSet Int))
+(declare-const s17 (FiniteSet Int))
+(declare-const s18 (FiniteSet Int))
+(declare-const s19 (FiniteSet Int))
+(declare-const s20 (FiniteSet Int))
+
+(declare-const s21 (FiniteSet Int))
+(declare-const s22 (FiniteSet Int))
+(declare-const s23 (FiniteSet Int))
+(declare-const s24 (FiniteSet Int))
+(declare-const s25 (FiniteSet Int))
+(declare-const s26 (FiniteSet Int))
+(declare-const s27 (FiniteSet Int))
+(declare-const s28 (FiniteSet Int))
+(declare-const s29 (FiniteSet Int))
+(declare-const s30 (FiniteSet Int))
+
+(assert (set.subset s1 s2))
+(assert (set.subset s2 s3))
+(assert (set.subset s3 s4))
+(assert (set.subset s4 s5))
+(assert (set.subset s5 s6))
+(assert (set.subset s6 s7))
+(assert (set.subset s7 s8))
+(assert (set.subset s8 s9))
+(assert (set.subset s9 s10))
+(assert (set.subset s10 s11))
+(assert (set.subset s11 s12))
+(assert (set.subset s12 s13))
+(assert (set.subset s13 s14))
+(assert (set.subset s14 s15))
+(assert (set.subset s15 s16))
+(assert (set.subset s16 s17))
+(assert (set.subset s17 s18))
+(assert (set.subset s18 s19))
+(assert (set.subset s19 s20))
+(assert (set.subset s20 s21))
+(assert (set.subset s21 s22))
+(assert (set.subset s22 s23))
+(assert (set.subset s23 s24))
+(assert (set.subset s24 s25))
+(assert (set.subset s25 s26))
+(assert (set.subset s26 s27))
+(assert (set.subset s27 s28))
+(assert (set.subset s28 s29))
+(assert (set.subset s29 s30))
+(assert (set.subset s30 s1))
+
+(assert (or (not (= s1 s10)) (not (= s1 s11)) (not (= s1 s12)) (not (= s1 s13)) (not (= s1 s14)) (not (= s1 s15))))
+
+(check-sat)
\ No newline at end of file
diff --git a/examples/SMT-LIB2/finite-sets/example-assignment-large.smt2 b/examples/SMT-LIB2/finite-sets/example-assignment-large.smt2
new file mode 100644
index 000000000..11799db70
--- /dev/null
+++ b/examples/SMT-LIB2/finite-sets/example-assignment-large.smt2
@@ -0,0 +1,159 @@
+; example due to nikolaj's project page
+
+
+
+
+(declare-const s1 (FiniteSet Int))
+(declare-const s2 (FiniteSet Int))
+(declare-const s3 (FiniteSet Int))
+(declare-const s4 (FiniteSet Int))
+(declare-const s5 (FiniteSet Int))
+(declare-const s6 (FiniteSet Int))
+(declare-const s7 (FiniteSet Int))
+(declare-const s8 (FiniteSet Int))
+(declare-const s9 (FiniteSet Int))
+
+(declare-const s1prime (FiniteSet Int))
+(declare-const s2prime (FiniteSet Int))
+(declare-const s3prime (FiniteSet Int))
+(declare-const s4prime (FiniteSet Int))
+(declare-const s5prime (FiniteSet Int))
+(declare-const s6prime (FiniteSet Int))
+(declare-const s7prime (FiniteSet Int))
+(declare-const s8prime (FiniteSet Int))
+(declare-const s9prime (FiniteSet Int))
+
+
+(declare-const t1 (FiniteSet Int))
+(declare-const t2 (FiniteSet Int))
+(declare-const t3 (FiniteSet Int))
+(declare-const t4 (FiniteSet Int))
+(declare-const t5 (FiniteSet Int))
+(declare-const t6 (FiniteSet Int))
+(declare-const t7 (FiniteSet Int))
+(declare-const t8 (FiniteSet Int))
+
+(declare-const t1prime (FiniteSet Int))
+(declare-const t2prime (FiniteSet Int))
+(declare-const t3prime (FiniteSet Int))
+(declare-const t4prime (FiniteSet Int))
+(declare-const t5prime (FiniteSet Int))
+(declare-const t6prime (FiniteSet Int))
+(declare-const t7prime (FiniteSet Int))
+(declare-const t8prime (FiniteSet Int))
+
+(declare-const u1 (FiniteSet Int))
+(declare-const u2 (FiniteSet Int))
+(declare-const u3 (FiniteSet Int))
+(declare-const u4 (FiniteSet Int))
+(declare-const u5 (FiniteSet Int))
+(declare-const u6 (FiniteSet Int))
+(declare-const u7 (FiniteSet Int))
+(declare-const u8 (FiniteSet Int))
+
+(declare-const u1prime (FiniteSet Int))
+(declare-const u2prime (FiniteSet Int))
+(declare-const u3prime (FiniteSet Int))
+(declare-const u4prime (FiniteSet Int))
+(declare-const u5prime (FiniteSet Int))
+(declare-const u6prime (FiniteSet Int))
+(declare-const u7prime (FiniteSet Int))
+(declare-const u8prime (FiniteSet Int))
+
+(assert (or (set.subset s1 t1) (set.subset s1 u1)))
+
+(assert (set.subset t1 s2))
+(assert (set.subset u1 s2))
+
+(assert (or (set.subset s2 t2) (set.subset s2 u2)))
+
+(assert (set.subset t2 s3))
+(assert (set.subset u2 s3))
+
+(assert (or (set.subset s3 t3) (set.subset s3 u3)))
+
+(assert (set.subset t3 s4))
+(assert (set.subset u3 s4))
+
+(assert (or (set.subset s4 t4) (set.subset s4 u4)))
+
+(assert (set.subset t4 s5))
+(assert (set.subset u4 s5))
+
+(assert (or (set.subset s5 t5) (set.subset s5 u5)))
+
+(assert (set.subset t5 s6))
+(assert (set.subset u5 s6))
+
+(assert (or (set.subset s6 t6) (set.subset s6 u6)))
+
+(assert (set.subset t6 s7))
+(assert (set.subset u6 s7))
+
+(assert (or (set.subset s7 t7) (set.subset s7 u7)))
+
+(assert (set.subset t7 s8))
+(assert (set.subset u7 s8))
+
+(assert (or (set.subset s8 t8) (set.subset s8 u8)))
+
+(assert (set.subset t8 s9))
+(assert (set.subset u8 s9))
+
+; link
+(assert (set.subset s9 s1prime))
+
+; prime part
+(assert (or (set.subset s1prime t1prime) (set.subset s1prime u1prime)))
+
+(assert (set.subset t1prime s2prime))
+(assert (set.subset u1prime s2prime))
+
+(assert (or (set.subset s2prime t2prime) (set.subset s2prime u2prime)))
+
+(assert (set.subset t2prime s3prime))
+(assert (set.subset u2prime s3prime))
+
+(assert (or (set.subset s3prime t3prime) (set.subset s3prime u3prime)))
+
+(assert (set.subset t3prime s4prime))
+(assert (set.subset u3prime s4prime))
+
+(assert (or (set.subset s4prime t4prime) (set.subset s4prime u4prime)))
+
+(assert (set.subset t4prime s5prime))
+(assert (set.subset u4prime s5prime))
+
+(assert (or (set.subset s5prime t5prime) (set.subset s5prime u5prime)))
+
+(assert (set.subset t5prime s6prime))
+(assert (set.subset u5prime s6prime))
+
+(assert (or (set.subset s6prime t6prime) (set.subset s6prime u6prime)))
+
+(assert (set.subset t6prime s7prime))
+(assert (set.subset u6prime s7prime))
+
+(assert (or (set.subset s7prime t7prime) (set.subset s7prime u7prime)))
+
+(assert (set.subset t7prime s8prime))
+(assert (set.subset u7prime s8prime))
+
+(assert (or (set.subset s8prime t8prime) (set.subset s8prime u8prime)))
+
+(assert (set.subset t8prime s9prime))
+(assert (set.subset u8prime s9prime))
+
+
+
+
+
+
+
+
+
+
+(assert (not (set.subset s1 s9prime)))
+
+
+(check-sat)
\ No newline at end of file
diff --git a/examples/SMT-LIB2/finite-sets/example-assignment.smt2 b/examples/SMT-LIB2/finite-sets/example-assignment.smt2
new file mode 100644
index 000000000..5bbec0405
--- /dev/null
+++ b/examples/SMT-LIB2/finite-sets/example-assignment.smt2
@@ -0,0 +1,78 @@
+; example due to nikolaj's project page
+
+
+
+
+(declare-const s1 (FiniteSet Int))
+(declare-const s2 (FiniteSet Int))
+(declare-const s3 (FiniteSet Int))
+(declare-const s4 (FiniteSet Int))
+(declare-const s5 (FiniteSet Int))
+(declare-const s6 (FiniteSet Int))
+(declare-const s7 (FiniteSet Int))
+(declare-const s8 (FiniteSet Int))
+(declare-const s9 (FiniteSet Int))
+
+(declare-const t1 (FiniteSet Int))
+(declare-const t2 (FiniteSet Int))
+(declare-const t3 (FiniteSet Int))
+(declare-const t4 (FiniteSet Int))
+(declare-const t5 (FiniteSet Int))
+(declare-const t6 (FiniteSet Int))
+(declare-const t7 (FiniteSet Int))
+(declare-const t8 (FiniteSet Int))
+
+(declare-const u1 (FiniteSet Int))
+(declare-const u2 (FiniteSet Int))
+(declare-const u3 (FiniteSet Int))
+(declare-const u4 (FiniteSet Int))
+(declare-const u5 (FiniteSet Int))
+(declare-const u6 (FiniteSet Int))
+(declare-const u7 (FiniteSet Int))
+(declare-const u8 (FiniteSet Int))
+
+(assert (or (set.subset s1 t1) (set.subset s1 u1)))
+
+(assert (set.subset t1 s2))
+(assert (set.subset u1 s2))
+
+(assert (or (set.subset s2 t2) (set.subset s2 u2)))
+
+(assert (set.subset t2 s3))
+(assert (set.subset u2 s3))
+
+(assert (or (set.subset s3 t3) (set.subset s3 u3)))
+
+(assert (set.subset t3 s4))
+(assert (set.subset u3 s4))
+
+(assert (or (set.subset s4 t4) (set.subset s4 u4)))
+
+(assert (set.subset t4 s5))
+(assert (set.subset u4 s5))
+
+(assert (or (set.subset s5 t5) (set.subset s5 u5)))
+
+(assert (set.subset t5 s6))
+(assert (set.subset u5 s6))
+
+(assert (or (set.subset s6 t6) (set.subset s6 u6)))
+
+(assert (set.subset t6 s7))
+(assert (set.subset u6 s7))
+
+(assert (or (set.subset s7 t7) (set.subset s7 u7)))
+
+(assert (set.subset t7 s8))
+(assert (set.subset u7 s8))
+
+(assert (or (set.subset s8 t8) (set.subset s8 u8)))
+
+(assert (set.subset t8 s9))
+(assert (set.subset u8 s9))
+
+
+(assert (not (set.subset s1 s9)))
+
+
+(check-sat)
\ No newline at end of file
diff --git a/examples/SMT-LIB2/finite-sets/example-chain.smt2 b/examples/SMT-LIB2/finite-sets/example-chain.smt2
new file mode 100644
index 000000000..265d51d05
--- /dev/null
+++ b/examples/SMT-LIB2/finite-sets/example-chain.smt2
@@ -0,0 +1,42 @@
+(declare-const s1 (FiniteSet Int))
+(declare-const s2 (FiniteSet Int))
+(declare-const s3 (FiniteSet Int))
+(declare-const s4 (FiniteSet Int))
+(declare-const s5 (FiniteSet Int))
+(declare-const s6 (FiniteSet Int))
+(declare-const s7 (FiniteSet Int))
+(declare-const s8 (FiniteSet Int))
+(declare-const s9 (FiniteSet Int))
+(declare-const s10 (FiniteSet Int))
+(declare-const s11 (FiniteSet Int))
+(declare-const s12 (FiniteSet Int))
+(declare-const s13 (FiniteSet Int))
+(declare-const s14 (FiniteSet Int))
+(declare-const s15 (FiniteSet Int))
+(declare-const s16 (FiniteSet Int))
+(declare-const s17 (FiniteSet Int))
+(declare-const s18 (FiniteSet Int))
+(declare-const s19 (FiniteSet Int))
+
+(assert (set.subset s4 s5))
+(assert (set.subset s5 s6))
+(assert (set.subset s6 s7))
+(assert (set.subset s7 s8))
+(assert (set.subset s8 s9))
+(assert (set.subset s9 s10))
+(assert (set.subset s10 s11))
+
+(assert (set.subset s11 s12))
+(assert (set.subset s12 s13))
+(assert (set.subset s13 s14))
+(assert (set.subset s14 s15))
+(assert (set.subset s15 s16))
+(assert (set.subset s16 s17))
+(assert (set.subset s17 s18))
+(assert (set.subset s18 s19))
+
+(assert (or (set.subset s1 s2) (= s1 s2)))
+(assert (or (set.subset s2 s3) (= s2 s3)))
+(assert (or (set.subset s3 s4) (= s3 s4)))
+(assert (not (set.subset s1 s19)))
+(check-sat)
\ No newline at end of file
diff --git a/examples/SMT-LIB2/finite-sets/example2.smt2 b/examples/SMT-LIB2/finite-sets/example2.smt2
new file mode 100644
index 000000000..fd1296319
--- /dev/null
+++ b/examples/SMT-LIB2/finite-sets/example2.smt2
@@ -0,0 +1,48 @@
+; example due to nikolaj's project page
+
+
+
+
+(declare-const s1 (FiniteSet Int))
+(declare-const s2 (FiniteSet Int))
+(declare-const s3 (FiniteSet Int))
+(declare-const s4 (FiniteSet Int))
+(declare-const s5 (FiniteSet Int))
+(declare-const s6 (FiniteSet Int))
+(declare-const s7 (FiniteSet Int))
+(declare-const s8 (FiniteSet Int))
+(declare-const s9 (FiniteSet Int))
+(declare-const s10 (FiniteSet Int))
+(declare-const s11 (FiniteSet Int))
+(declare-const s12 (FiniteSet Int))
+(declare-const s13 (FiniteSet Int))
+(declare-const s14 (FiniteSet Int))
+(declare-const s15 (FiniteSet Int))
+(declare-const s16 (FiniteSet Int))
+(declare-const s17 (FiniteSet Int))
+(declare-const s18 (FiniteSet Int))
+(declare-const s19 (FiniteSet Int))
+
+
+(assert (set.subset s1 s2))
+(assert (set.subset s2 s3))
+(assert (set.subset s3 s4))
+(assert (set.subset s4 s5))
+(assert (set.subset s5 s6))
+(assert (set.subset s6 s7))
+(assert (set.subset s7 s8))
+(assert (set.subset s8 s9))
+(assert (set.subset s9 s10))
+(assert (set.subset s10 s11))
+(assert (set.subset s11 s12))
+(assert (set.subset s12 s13))
+(assert (set.subset s13 s14))
+(assert (set.subset s14 s15))
+(assert (set.subset s15 s16))
+(assert (set.subset s16 s17))
+(assert (set.subset s17 s18))
+(assert (set.subset s18 s19))
+
+(assert (not (set.subset s1 s19)))
+
+(check-sat)
\ No newline at end of file
diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index a3732f7f6..9eb789889 100644
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@@ -59,6 +59,7 @@ z3_add_component(smt
     theory_dense_diff_logic.cpp
     theory_finite_set.cpp
     theory_finite_set_size.cpp
+    theory_finite_set_lattice_refutation.cpp
     theory_diff_logic.cpp
     theory_dl.cpp
     theory_dummy.cpp
diff --git a/src/smt/theory_finite_set.cpp b/src/smt/theory_finite_set.cpp
index 47898a7b2..0d572e9d1 100644
--- a/src/smt/theory_finite_set.cpp
+++ b/src/smt/theory_finite_set.cpp
@@ -28,7 +28,8 @@ namespace smt {
         theory(ctx, ctx.get_manager().mk_family_id("finite_set")),
         u(m),
         m_axioms(m), m_rw(m), m_find(*this),
-        m_cardinality_solver(*this)
+        m_cardinality_solver(*this),
+        m_lattice_refutation(*this)
     {
         // Setup the add_clause callback for axioms
         std::function<void(theory_axiom *)> add_clause_fn =
@@ -227,8 +228,11 @@ namespace smt {
             e = ctx.mk_enode(term, false, m.is_bool(term), true);        
         
         // Attach theory variable if this is a set
-        if (!is_attached_to_var(e))             
+        if (!is_attached_to_var(e)){            
             ctx.attach_th_var(e, this, mk_var(e));
+            TRACE(finite_set, tout << "create_theory_var: " << e->get_th_var(get_id()) << " enode:" << e->get_expr() << "\n";);
+        }
+
 
         // Assert immediate axioms
         if (!ctx.relevancy())
@@ -256,6 +260,10 @@ 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);
+
+        // 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";);
     }
 
     /**
@@ -279,6 +287,7 @@ namespace smt {
             ctx.push_trail(push_back_vector(m_diseqs));
             m_axioms.extensionality_axiom(e1, e2);
         }
+        m_lattice_refutation.add_disequality(v1,v2);
     }
 
     //
@@ -405,6 +414,8 @@ namespace smt {
     void theory_finite_set::assign_eh(bool_var v, bool is_true) {
         TRACE(finite_set, tout << "assign_eh: v" << v << " is_true: " << is_true << "\n";);
         expr *e = ctx.bool_var2expr(v);
+        TRACE(finite_set, tout << "assign_eh_expr: " << mk_pp(e, m) << "\n";);
+
         // retrieve the watch list for clauses where e appears with opposite polarity
         unsigned idx = 2 * e->get_id() + (is_true ? 1 : 0);
         if (idx >= m_clauses.watch.size())
diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h
index 6ba1cc4c7..3cacd94a8 100644
--- a/src/smt/theory_finite_set.h
+++ b/src/smt/theory_finite_set.h
@@ -87,6 +87,7 @@ the theory solver uses a stand-alone satisfiability checker for Boolean algebras
 #include "util/union_find.h"
 #include "smt/smt_theory.h"
 #include "smt/theory_finite_set_size.h"
+#include "smt/theory_finite_set_lattice_refutation.h"
 #include "model/finite_set_factory.h"
 
 namespace smt {
@@ -96,6 +97,7 @@ namespace smt {
         using th_union_find = union_find<theory_finite_set>;
         friend class theory_finite_set_test;
         friend class theory_finite_set_size;
+        friend class theory_finite_set_lattice_refutation;
         friend struct finite_set_value_proc;
 
         struct var_data {
@@ -139,6 +141,7 @@ namespace smt {
         th_union_find             m_find;
         theory_clauses            m_clauses;
         theory_finite_set_size m_cardinality_solver;
+        theory_finite_set_lattice_refutation m_lattice_refutation;
         finite_set_factory *m_factory = nullptr;
         obj_map<enode, obj_map<enode, bool> *> m_set_members;
         ptr_vector<func_decl> m_set_in_decls;
diff --git a/src/smt/theory_finite_set_lattice_refutation.cpp b/src/smt/theory_finite_set_lattice_refutation.cpp
new file mode 100644
index 000000000..460b09e36
--- /dev/null
+++ b/src/smt/theory_finite_set_lattice_refutation.cpp
@@ -0,0 +1,307 @@
+#include "smt/theory_finite_set_lattice_refutation.h"
+#include "ast/rewriter/finite_set_axioms.h"
+#include "smt/smt_theory.h"
+#include "smt/theory_finite_set.h"
+#include "smt/smt_context.h"
+#include "iostream"
+
+const int NUM_WORDS = 5;
+// some example have shown, the introduction of large conflict clauses can severely slow down refutation
+const int MAX_DECISION_LITERALS=10;
+
+namespace smt {
+    reachability_matrix::reachability_matrix(context& ctx, theory_finite_set_lattice_refutation& t_lattice):
+    reachable(NUM_WORDS*NUM_WORDS*64, 0),
+    links(NUM_WORDS*NUM_WORDS*64*64, {nullptr, nullptr}),
+    link_dls(NUM_WORDS*NUM_WORDS*64*64, 0),
+    non_links(NUM_WORDS*NUM_WORDS*64),
+    non_link_justifications(NUM_WORDS*NUM_WORDS*64*64, {nullptr, nullptr}), largest_var(0), max_size(NUM_WORDS*64), ctx(ctx), t_lattice_refutation(t_lattice) {}
+
+    int reachability_matrix::get_max_var(){
+        return largest_var;
+    }
+
+    inline int reachability_matrix::get_word_index(int row, int col) const{
+        return  (row * NUM_WORDS) + (col / 64);
+    };
+
+    inline uint64_t reachability_matrix::get_bitmask(int col) const{
+        return  1ull << (col%64);
+    };
+
+    bool reachability_matrix::is_reachability_forbidden(theory_var source, theory_var dest){
+        return non_links[get_word_index(source, dest)] & get_bitmask(dest);
+    }
+
+    bool reachability_matrix::in_bounds(theory_var source, theory_var dest){
+        return source >= 0 && dest >= 0 && source < max_size && dest<max_size;
+    }
+
+    bool reachability_matrix::is_reachable(theory_var source, theory_var dest){
+        return reachable[get_word_index(source,dest)] & get_bitmask(dest);
+    }
+
+    bool reachability_matrix::is_linked(theory_var source, theory_var dest){
+        return links[source*max_size+dest].first != nullptr;
+    }
+
+    bool reachability_matrix::bitwise_or_rows(int source_dest, int source){
+        bool changes = false;
+        for (int i = 0; i < NUM_WORDS; i++)
+        {
+            uint64_t old_value = reachable[source_dest*NUM_WORDS+i];
+            uint64_t new_value = reachable[source_dest*NUM_WORDS+i] | reachable[source*NUM_WORDS+i];
+            if(old_value == new_value){
+                continue;
+            }
+            ctx.push_trail(value_trail(reachable[source_dest*NUM_WORDS+i]));
+            reachable[source_dest*NUM_WORDS+i] = new_value;
+            changes = true;
+            check_reachability_conflict_word(source_dest, i);
+        }
+        return changes;
+    }
+
+    bool reachability_matrix::set_reachability(theory_var source, theory_var dest, enode_pair reachability_witness){
+        if (!in_bounds(source, dest) || is_reachable(source, dest)){
+            return false;
+        }
+        ctx.push_trail(value_trail(largest_var));
+        largest_var = std::max({largest_var, source, dest});
+
+        int word_idx = get_word_index(source, dest);
+        ctx.push_trail(value_trail(reachable[word_idx]));
+        reachable[word_idx] |= get_bitmask(dest);
+        ctx.push_trail(value_trail(links[source*max_size + dest]));
+        links[source*max_size+dest] = reachability_witness;
+        ctx.push_trail(value_trail(link_dls[source*max_size+dest]));
+        TRACE(finite_set, tout << "set_reachability(" << source << "," << dest <<"), dl: "<<ctx.get_scope_level());
+        link_dls[source*max_size+dest] = ctx.get_scope_level();
+
+        check_reachability_conflict(source, dest);
+        // update reachability of source
+        bitwise_or_rows(source, dest);
+        
+
+        for (int i = 0; i <= largest_var; i++)
+        { //update reachability of i to the nodes reachable from dest
+            if(!is_reachable(i, source) || i == source){
+                continue;
+            }
+            bitwise_or_rows(i, source);
+        }
+        if(conflict_word>=0 && conflict_row >=0){
+            for (int i = conflict_word*64; i < conflict_word*64+64; i++)
+            {
+                check_reachability_conflict(conflict_row, i);
+            }
+            conflict_word = -1;
+            conflict_row = -1;
+        }
+        return true;
+    }
+
+    bool reachability_matrix::set_non_reachability(theory_var source, theory_var dest, enode_pair non_reachability_witness){
+        if(is_reachability_forbidden(source, dest)){
+            return false;
+        }
+        ctx.push_trail(value_trail(largest_var));
+        largest_var = std::max({largest_var, source, dest});
+        ctx.push_trail(value_trail(non_links[get_word_index(source, dest)]));
+        non_links[get_word_index(source, dest)] |= get_bitmask(dest);
+        ctx.push_trail(value_trail(non_link_justifications[source*max_size+dest]));
+        non_link_justifications[source*max_size+dest] = non_reachability_witness;
+        check_reachability_conflict(source, dest);
+        return true;
+    }
+
+    theory_finite_set_lattice_refutation::theory_finite_set_lattice_refutation(theory_finite_set& th): 
+    m(th.m), ctx(th.ctx), th(th), u(m), bs(m), m_assumption(m), reachability(th.ctx, *this) {}
+
+    // determines if the two enodes capture a subset relation:
+    // checks, whether intersect_expr = intersect(subset, return_value) for some return value
+    // otherwise return null
+    enode* theory_finite_set_lattice_refutation::get_superset(enode* subset, enode* intersect_expr){
+        expr* arg1 = nullptr, *arg2 = nullptr;
+        if(u.is_intersect(intersect_expr->get_expr(), arg1, arg2)){
+            if(arg1 == subset->get_expr()){
+                return ctx.get_enode(arg2);
+            }
+            if(arg2 == subset->get_expr()){
+                return ctx.get_enode(arg1);
+            }
+        }
+        return nullptr;
+    }
+
+    void theory_finite_set_lattice_refutation::add_equality(theory_var v1, theory_var v2){
+        auto n1 = th.get_enode(v1);
+        auto n2 = th.get_enode(v2);
+
+        enode* subset = n1;
+        enode* superset = get_superset(n1, n2);
+        if(superset == nullptr){
+            subset = n2;
+            superset = get_superset(n2, n1);
+        }
+        if(superset == nullptr){
+            add_set_equality(n1, n2);
+            return;
+        }
+        TRACE(finite_set, tout << "new_eq_intersection: " << enode_pp(subset, ctx) << "("<<th.get_th_var(subset)<<")" << "\\subseteq " << enode_pp(superset, ctx)<<"("<<th.get_th_var(superset)<<")");
+        add_subset(subset->get_th_var(th.get_id()), superset->get_th_var(th.get_id()), {n1, n2});
+    };
+
+    void reachability_matrix::get_path(theory_var source, theory_var dest, vector<enode_pair>& path, int& num_decisions){
+        SASSERT(is_reachable(source, dest));
+        vector<bool> visited(max_size, false);
+        if(source != dest){
+            visited[source] = true;
+        }
+        num_decisions = 0;
+        do{
+            bool success = false;
+            // TRACE(finite_set, tout << "get_path:source: "<<source);
+            for (int i = 0; i <= largest_var; i++)
+            {
+                if(!visited[i] && is_linked(source, i) && ((is_reachable(i, dest)) || i == dest)){
+                    path.push_back(links[source*max_size+i]);
+                    if(link_dls[source*max_size+i] != 0){
+                        num_decisions +=1;
+                    }
+
+                    source = i;
+                    visited[source] = true;
+                    success = true;
+                    break;
+                }
+            }
+            SASSERT(success);
+        }while(source != dest);
+        TRACE(finite_set, tout << "get_path_num_decisions: "<<num_decisions);
+    }
+
+    bool reachability_matrix::check_reachability_conflict(theory_var source, theory_var dest){
+        if(is_reachable(source,dest) && is_reachability_forbidden(source, dest)){
+            TRACE(finite_set, tout << "found_conflict1: "<<source<<" -> "<<dest);
+            vector<enode_pair> path;
+            int num_decisions;
+            get_path(source, dest, path, num_decisions);
+            // TRACE(finite_set, tout << "found path: "<<source<<" -> "<<dest<<" length: "<<path.size());
+            if(num_decisions <= MAX_DECISION_LITERALS){
+                TRACE(finite_set, tout << "num_decisions: "<<num_decisions<<" path_length: "<<path.size());
+
+                enode_pair diseq = non_link_justifications[source*max_size+dest];
+                t_lattice_refutation.trigger_conflict(path, diseq);
+            }
+            
+            return true;
+        }
+        return false;
+    }
+
+    bool reachability_matrix::check_reachability_conflict_word(int row, int word){
+        if(reachable[row*NUM_WORDS+word] & non_links[row*NUM_WORDS+word]){
+
+        // somewhere in this word there is a conflict
+        conflict_row = row;
+        conflict_word = word;
+        return true;
+            
+        }
+        return false;
+    }
+
+    void reachability_matrix::print_relations(){
+        TRACE(finite_set, tout << "largest_var: "<<largest_var);
+        for (size_t i = 0; i <  max_size; i++)
+        {
+            for (size_t j = 0; j < max_size; j++)
+            {
+                if((reachable[get_word_index(i,j)]&get_bitmask(j)) || is_reachable(i,j)){
+                    TRACE(finite_set, tout << "reachable: "<<i<<"->"<<j<<"  :"<<is_reachable(i,j));
+                }
+            }
+        }
+    }
+
+    void theory_finite_set_lattice_refutation::trigger_conflict(vector<enode_pair> equalities, enode_pair clashing_disequality){
+        auto eq_expr = m.mk_not(m.mk_eq(clashing_disequality.first->get_expr(), clashing_disequality.second->get_expr()));
+        auto disequality_literal = ctx.get_literal(eq_expr);
+        auto j1 = ext_theory_conflict_justification(th.get_id(), ctx, 1, &disequality_literal, equalities.size(), equalities.data());
+        auto justification = ctx.mk_justification(j1);
+        TRACE(finite_set, tout << "conflict_literal: "<<disequality_literal);
+        
+        TRACE(finite_set, tout << "setting_partial_order_conflict");
+        ctx.set_conflict(justification);
+    }
+
+    void theory_finite_set_lattice_refutation::add_disequality(theory_var v1, theory_var v2){
+        auto n1 = th.get_enode(v1);
+        auto n2 = th.get_enode(v2);
+
+        enode* subset = n1;
+        enode* superset = get_superset(n1, n2);
+        if(superset == nullptr){
+            subset = n2;
+            superset = get_superset(n2, n1);
+        }
+        if(superset == nullptr){
+            return;
+        }
+        TRACE(finite_set, tout << "new_diseq_intersection: " << enode_pp(subset, ctx) << "("<<th.get_th_var(subset)<<")" << "\\not\\subseteq " << enode_pp(superset, ctx)<<"("<<th.get_th_var(superset)<<")");
+        add_not_subset(subset->get_th_var(th.get_id()), superset->get_th_var(th.get_id()), {n1, n2});
+    };
+
+    void theory_finite_set_lattice_refutation::add_subset(theory_var subset_th, theory_var superset_th, enode_pair justifying_equality){
+        if(!reachability.in_bounds(subset_th, superset_th)){
+            return;
+        }
+        if (subset_th == null_theory_var || superset_th == null_theory_var){
+            return;
+        }
+        reachability.set_reachability(subset_th, superset_th, justifying_equality);
+        SASSERT(reachability.is_reachable(subset_th, superset_th));
+        if(reachability.is_reachable(superset_th, subset_th)){
+            TRACE(finite_set, tout << "cycle_detected: " << subset_th << " <--> " << superset_th);
+            vector<enode_pair> path;
+            int num_decisions;
+            reachability.get_path(subset_th, subset_th, path, num_decisions);
+            // we propagate the equality
+            // build justification to be used by all propagated equalities
+            auto j1 = ctx.mk_justification(ext_theory_conflict_justification(th.get_id(), ctx, 0, nullptr, path.size(), path.data()));
+
+            for (size_t i = 0; i < path.size()-1; i++)
+            {
+                auto set1 = path[i].first;
+                auto set2 = path[i+1].first;
+                ctx.add_eq(set1, set2, eq_justification(j1));
+                TRACE(finite_set, tout << "added_equality: " << set1 << " == " << set2);
+            }
+        }
+    };
+
+    void theory_finite_set_lattice_refutation::add_not_subset(theory_var subset_th, theory_var superset_th, enode_pair justifying_disequality){
+        if(!reachability.in_bounds(subset_th, superset_th)){
+            return;
+        }
+        if (subset_th == null_theory_var || superset_th == null_theory_var){
+            return;
+        }
+        reachability.set_non_reachability(subset_th, superset_th, justifying_disequality);
+        SASSERT(reachability.is_reachability_forbidden(subset_th, superset_th));
+    }
+
+    void theory_finite_set_lattice_refutation::add_set_equality(enode* set1, enode* set2){
+        theory_var set1_th = set1->get_th_var(th.get_id());
+        theory_var set2_th = set2->get_th_var(th.get_id());
+        if(!reachability.in_bounds(set1_th, set2_th)){
+            return;
+        }
+        reachability.set_reachability(set1_th, set2_th, {set1, set2});
+        SASSERT(reachability.is_reachable(set1_th, set2_th));
+    
+        reachability.set_reachability(set2_th, set1_th, {set2, set1});
+        SASSERT(reachability.is_reachable(set2_th, set1_th));
+    }
+}
diff --git a/src/smt/theory_finite_set_lattice_refutation.h b/src/smt/theory_finite_set_lattice_refutation.h
new file mode 100644
index 000000000..36e4a1e7d
--- /dev/null
+++ b/src/smt/theory_finite_set_lattice_refutation.h
@@ -0,0 +1,71 @@
+#pragma once
+
+#include "ast/finite_set_decl_plugin.h"
+#include "ast/rewriter/finite_set_axioms.h"
+#include "smt/smt_theory.h"
+
+namespace smt {
+    class context;
+    class theory_finite_set;
+
+    class theory_finite_set_lattice_refutation;
+    class reachability_matrix{
+
+        std::vector<uint64_t> reachable;
+        std::vector<enode_pair> links;
+        std::vector<uint64_t> link_dls;
+        std::vector<uint64_t> non_links;
+        std::vector<enode_pair> non_link_justifications;
+
+        int largest_var;
+
+        int max_size;
+
+        context& ctx;
+        theory_finite_set_lattice_refutation& t_lattice_refutation;
+        int conflict_row = -1;
+        int conflict_word = -1;
+
+        // sets source_dest |= dest, and pushing the changed words to the trail
+        bool bitwise_or_rows(int source_dest, int source);
+        inline int get_word_index(int row, int col) const;
+        inline uint64_t get_bitmask(int col) const;
+        public:
+            void get_path(theory_var source, theory_var dest, vector<enode_pair>& path, int& num_decisions);
+            reachability_matrix(context& ctx, theory_finite_set_lattice_refutation& t_lattice);
+            bool in_bounds(theory_var source, theory_var dest);
+            bool is_reachable(theory_var source, theory_var dest);
+            bool is_reachability_forbidden(theory_var source, theory_var dest);
+            bool is_linked(theory_var source, theory_var dest);
+
+            bool check_reachability_conflict(theory_var source, theory_var dest);
+            bool check_reachability_conflict_word(int row, int word);
+
+            bool set_reachability(theory_var source, theory_var dest, enode_pair reachability_witness);
+            bool set_non_reachability(theory_var source, theory_var dest, enode_pair non_reachability_witness);
+            int get_max_var();
+            void print_relations();
+            
+    };
+
+    class theory_finite_set_lattice_refutation {
+        ast_manager          &m;
+        context             &ctx;
+        theory_finite_set   &th;
+        finite_set_util u;
+        expr_ref_vector bs;
+        expr_ref m_assumption;
+        reachability_matrix reachability;
+
+        enode* get_superset(enode*, enode*);
+        void add_subset(theory_var subset, theory_var superset, enode_pair justifying_equality);
+        void add_not_subset(theory_var subset, theory_var superset, enode_pair justifying_disequality);
+        void propagate_new_subset(theory_var v1, theory_var v2);
+        void add_set_equality(enode* set1, enode* set2);
+        public:
+            void trigger_conflict(vector<enode_pair> equalities, enode_pair clashing_disequality);
+            theory_finite_set_lattice_refutation(theory_finite_set &th);
+            void add_equality(theory_var v1, theory_var v2);
+            void add_disequality(theory_var v1, theory_var v2);
+    };
+}