diff --git a/src/smt/theory_dense_diff_logic.h b/src/smt/theory_dense_diff_logic.h
index 4b08e99d0..941a409fa 100644
--- a/src/smt/theory_dense_diff_logic.h
+++ b/src/smt/theory_dense_diff_logic.h
@@ -162,7 +162,7 @@ namespace smt {
         struct var_value_eq {
             theory_dense_diff_logic & m_th;
             var_value_eq(theory_dense_diff_logic & th):m_th(th) {}
-            bool operator()(theory_var v1, theory_var v2) const { return m_th.m_assignment[v1] == m_th.m_assignment[v2] && m_th.is_int(v1) == m_th.is_int(v2); }
+            bool operator()(theory_var v1, theory_var v2) const { return m_th.m_assignment[v1] == m_th.m_assignment[v2]; }
         };
 
         typedef int_hashtable<var_value_hash, var_value_eq> var_value_table;
diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h
index 08ed144a3..3faff185c 100644
--- a/src/smt/theory_utvpi.h
+++ b/src/smt/theory_utvpi.h
@@ -159,6 +159,25 @@ namespace smt {
         arith_factory *         m_factory;
         rational                m_delta;
         
+        struct var_value_hash;
+        friend struct var_value_hash;
+        struct var_value_hash {
+            theory_utvpi & m_th;
+            var_value_hash(theory_utvpi & th):m_th(th) {}
+            unsigned operator()(theory_var v) const { return m_th.mk_value(v, false).hash(); }
+        };
+
+        struct var_value_eq;
+        friend struct var_value_eq;
+        struct var_value_eq {
+            theory_utvpi & m_th;
+            var_value_eq(theory_utvpi & th):m_th(th) {}
+            bool operator()(theory_var v1, theory_var v2) const { return m_th.mk_value(v1, false) == m_th.mk_value(v2, false) && m_th.is_int(v1) == m_th.is_int(v2); }
+        };
+
+        typedef int_hashtable<var_value_hash, var_value_eq> var_value_table;
+        var_value_table             m_var_value_table;
+
 
         // Set a conflict due to a negative cycle.
         void set_conflict();
@@ -257,6 +276,10 @@ namespace smt {
 
     private:        
 
+        void init_model();
+
+        bool assume_eqs_core();
+
         rational mk_value(theory_var v, bool is_int);
 
         bool is_parity_ok(unsigned v) const;
@@ -271,6 +294,8 @@ namespace smt {
 
         bool check_z_consistency();
 
+        bool has_shared();
+
         virtual void new_eq_eh(th_var v1, th_var v2, justification& j) {
             m_stats.m_num_core2th_eqs++;
             new_eq_or_diseq(true, v1, v2, j);
@@ -299,6 +324,8 @@ namespace smt {
 
         void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just);
         
+        bool is_int(theory_var v) const { return a.is_int(get_enode(v)->get_owner()); }
+
         th_var get_zero(sort* s) { return a.is_int(s) ? m_izero : m_rzero; }
 
         th_var get_zero(expr* e) { return get_zero(get_manager().get_sort(e)); }
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index 9c5d86e0e..0bdc754a2 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -69,6 +69,7 @@ namespace smt {
         m_lia(false),
         m_lra(false),
         m_non_utvpi_exprs(false),
+        m_var_value_table(DEFAULT_HASHTABLE_INITIAL_CAPACITY, var_value_hash(*this), var_value_eq(*this)),
         m_test(m),
         m_factory(nullptr) {
         }            
@@ -203,7 +204,7 @@ namespace smt {
         inc_conflicts();
         literal_vector const& lits = m_nc_functor.get_lits();
         context & ctx = get_context();
-        IF_VERBOSE(2, ctx.display_literals_smt2(verbose_stream() << "conflict:\n", lits));
+        IF_VERBOSE(20, ctx.display_literals_smt2(verbose_stream() << "conflict:\n", lits));
         TRACE("utvpi", ctx.display_literals_smt2(tout << "conflict:\n", lits););
         
         if (m_params.m_arith_dump_lemmas) {
@@ -410,6 +411,9 @@ namespace smt {
         else if (!check_z_consistency()) {
             return FC_CONTINUE;
         }
+        else if (has_shared() && assume_eqs_core()) {
+            return FC_CONTINUE;
+        }
         else if (m_non_utvpi_exprs) {
             return FC_GIVEUP;
         }
@@ -418,6 +422,17 @@ namespace smt {
         }
     }
 
+    template<typename Ext>
+    bool theory_utvpi<Ext>::has_shared() {
+        auto sz = static_cast<theory_var>(get_num_vars());
+        for (theory_var v = 0; v < sz; ++v) {
+            if (is_relevant_and_shared(get_enode(v)))
+                return true;
+        }
+        return false;
+    }
+
+
     template<typename Ext>
     bool theory_utvpi<Ext>::check_z_consistency() {
         int_vector scc_id;
@@ -789,6 +804,11 @@ namespace smt {
     void theory_utvpi<Ext>::init_model(model_generator & m) {            
         m_factory = alloc(arith_factory, get_manager());
         m.register_factory(m_factory);
+        init_model();
+    }
+
+    template<typename Ext>
+    void theory_utvpi<Ext>::init_model() {            
         enforce_parity();
         init_zero();
         dl_var vs[4] = { to_var(m_izero), neg(to_var(m_izero)), to_var(m_rzero), neg(to_var(m_rzero)) };
@@ -797,6 +817,13 @@ namespace smt {
         DEBUG_CODE(model_validate(););
     }
 
+    template<typename Ext>
+    bool theory_utvpi<Ext>::assume_eqs_core() {
+        init_model();
+        return assume_eqs(m_var_value_table);
+    }
+
+
     template<typename Ext>    
     void theory_utvpi<Ext>::model_validate() {
         context& ctx = get_context();