diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h
index fb244b6c5..293d091df 100644
--- a/src/smt/diff_logic.h
+++ b/src/smt/diff_logic.h
@@ -371,7 +371,9 @@ private:
         SASSERT(m_gamma[target].is_neg());
         acc_assignment(target, gamma);
 
-        TRACE("arith", display(tout << id << "\n"););
+        TRACE("arith", display(tout << id << " " << gamma << "\n");
+              display_edge(tout, last_e);
+              );
 
         dl_var source = target;
         while (true) {
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index 7bc8d4281..74e19112f 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -164,6 +164,8 @@ namespace smt {
         };
         typedef dl_graph<GExt> Graph;
 
+        enum lia_or_lra { not_set, is_lia, is_lra };
+
         smt_params &                   m_params;
         arith_util                     m_util;
         arith_eq_adapter               m_arith_eq_adapter;
@@ -175,7 +177,7 @@ namespace smt {
         ptr_vector<eq_prop_info>       m_eq_prop_infos;
 
         app_ref_vector                 m_terms;
-        bool_vector                  m_signs;
+        bool_vector                    m_signs;
 
         ptr_vector<atom>               m_atoms;
         ptr_vector<atom>               m_asserted_atoms;   // set of asserted atoms
@@ -186,7 +188,7 @@ namespace smt {
         unsigned                       m_num_core_conflicts;
         unsigned                       m_num_propagation_calls;
         double                         m_agility;
-        bool                           m_is_lia;
+        lia_or_lra                     m_lia_or_lra;
         bool                           m_non_diff_logic_exprs;
 
         arith_factory *                m_factory;
@@ -220,6 +222,8 @@ namespace smt {
             return get_family_id() == n->get_family_id();
         }
 
+        void set_sort(expr* n);
+
     public:    
         theory_diff_logic(ast_manager& m, smt_params & params):
             theory(m.mk_family_id("arith")),
@@ -233,7 +237,7 @@ namespace smt {
             m_num_core_conflicts(0),
             m_num_propagation_calls(0),
             m_agility(0.5),
-            m_is_lia(true),
+            m_lia_or_lra(not_set),
             m_non_diff_logic_exprs(false),
             m_factory(nullptr),
             m_nc_functor(*this),
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 73f6981d3..349ad104d 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -252,7 +252,6 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
         k -= numeral(1);
     }
     else {
-        m_is_lia = false;
         k -= this->m_epsilon; 
     }
     edge_id neg = m_graph.add_edge(target, source, k, ~l);
@@ -647,7 +646,7 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
     }
     ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_TH_LEMMA, nullptr);
     if (dump_lemmas()) {
-        symbol logic(m_is_lia ? "QF_LIA" : "QF_LRA");
+        symbol logic(m_lia_or_lra == is_lia ? "QF_LIA" : "QF_LRA");
         ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic);
     }
 
@@ -693,7 +692,7 @@ void theory_diff_logic<Ext>::set_neg_cycle_conflict() {
           );
 
     if (dump_lemmas()) {
-        symbol logic(m_is_lia ? "QF_LIA" : "QF_LRA");
+        symbol logic(m_lia_or_lra == is_lia ? "QF_LIA" : "QF_LRA");
         ctx.display_lemma_as_smt_problem(lits.size(), lits.c_ptr(), false_literal, logic);
     }
 
@@ -743,6 +742,7 @@ theory_var theory_diff_logic<Ext>::mk_term(app* n) {
 
     TRACE("arith", tout << mk_pp(n, get_manager()) << "\n";);
 
+
     rational r;
     if (m_util.is_numeral(n, r)) {
         return mk_num(n, r);
@@ -808,9 +808,26 @@ theory_var theory_diff_logic<Ext>::mk_var(enode* n) {
     TRACE("diff_logic_vars", tout << "mk_var: " << v << "\n";);
     m_graph.init_var(v);
     get_context().attach_th_var(n, this, v);
+    set_sort(n->get_owner());
     return v;
 }
 
+template<typename Ext>
+theory_var theory_diff_logic<Ext>::set_sort(exir* n) {
+    if (m_util.is_int(n->get_owner())) {
+        if (m_lia_or_lra == is_lra) {
+            throw default_exception("difference logic does not work with mixed sorts");
+        }
+        m_lia_or_lra = is_lia;
+    }
+    else {
+        if (m_lia_or_lra == is_lia) {
+            throw default_exception("difference logic does not work with mixed sorts");
+        }
+        m_lia_or_lra = is_lra;
+    }
+}
+
 
 template<typename Ext>
 theory_var theory_diff_logic<Ext>::mk_var(app* n) {
@@ -853,7 +870,7 @@ void theory_diff_logic<Ext>::reset_eh() {
     m_num_core_conflicts    = 0;
     m_num_propagation_calls = 0;
     m_agility               = 0.5;
-    m_is_lia                = true;
+    m_lia_or_lra            = not_set;
     m_non_diff_logic_exprs  = false;
     m_objectives      .reset();
     m_objective_consts.reset();