diff --git a/src/smt/diff_logic.h b/src/smt/diff_logic.h
index 9d79e3e52ba..167e1f2a971 100644
--- a/src/smt/diff_logic.h
+++ b/src/smt/diff_logic.h
@@ -263,7 +263,7 @@ class dl_graph {
 
 public:
     // An assignment is feasible if all edges are feasible.
-    bool is_feasible() const {
+    bool is_feasible_dbg() const {
         for (unsigned i = 0; i < m_edges.size(); ++i) {
             if (!is_feasible(m_edges[i])) {
                 return false;
@@ -422,7 +422,7 @@ class dl_graph {
             }
 
             if (m_heap.empty()) {
-                SASSERT(is_feasible());
+                SASSERT(is_feasible_dbg());
                 reset_marks();
                 m_assignment_stack.reset();
                 return true;
@@ -498,7 +498,7 @@ class dl_graph {
 
     // Add an new weighted edge "source --weight--> target" with explanation ex.
     edge_id add_edge(dl_var source, dl_var target, const numeral & weight, const explanation & ex) {
-        // SASSERT(is_feasible());
+        // SASSERT(is_feasible_dbg());
         edge_id new_id = m_edges.size();
         m_edges.push_back(edge(source, target, weight, m_timestamp, ex));
         m_activity.push_back(0);
@@ -513,7 +513,7 @@ class dl_graph {
     // The method assumes the graph is feasible before the invocation.
     bool enable_edge(edge_id id) {
         edge& e = m_edges[id];
-        SASSERT(is_feasible());
+        SASSERT(is_feasible_dbg());
         bool r = true;
         if (!e.is_enabled()) {
             e.enable(m_timestamp);
@@ -523,7 +523,7 @@ class dl_graph {
                 r = make_feasible(id);
             }
             SASSERT(check_invariant());
-            SASSERT(!r || is_feasible()); 
+            SASSERT(!r || is_feasible_dbg()); 
             m_enabled_edges.push_back(id);
         }
         return r;
@@ -862,7 +862,7 @@ class dl_graph {
     // Create a new scope.
     // That is, save the number of edges in the graph.
     void push() {
-        // SASSERT(is_feasible()); <<< I relaxed this condition
+        // SASSERT(is_feasible_dbg()); <<< I relaxed this condition
         m_trail_stack.push_back(scope(m_edges.size(), m_enabled_edges.size(), m_timestamp));
     }
     
@@ -896,20 +896,20 @@ class dl_graph {
         }
         m_trail_stack.shrink(new_lvl);
         SASSERT(check_invariant()); 
-        // SASSERT(is_feasible()); <<< I relaxed the condition in push(), so this assertion is not valid anymore.
+        // SASSERT(is_feasible_dbg()); <<< I relaxed the condition in push(), so this assertion is not valid anymore.
     }
 
     // Make m_assignment[v] == zero
     // The whole assignment is adjusted in a way feasibility is preserved.
     // This method should only be invoked if the current assignment if feasible.
     void set_to_zero(dl_var v) {
-        SASSERT(is_feasible());
+        SASSERT(is_feasible_dbg());
         if (!m_assignment[v].is_zero()) {
             numeral k = m_assignment[v];
             for (auto& a : m_assignment) {
                 a -= k;
             }
-            SASSERT(is_feasible());
+            SASSERT(is_feasible_dbg());
         }
     }
 
@@ -929,7 +929,7 @@ class dl_graph {
                     if (!m_assignment[w].is_zero()) {
                         enable_edge(add_edge(v, w, numeral(0), explanation()));
                         enable_edge(add_edge(w, v, numeral(0), explanation()));
-                        SASSERT(is_feasible());                        
+                        SASSERT(is_feasible_dbg());                        
                     }
                 }
                 return;
@@ -947,7 +947,7 @@ class dl_graph {
         if (!m_assignment[v].is_zero() || !m_assignment[w].is_zero()) {
             enable_edge(add_edge(v, w, numeral(0), explanation()));
             enable_edge(add_edge(w, v, numeral(0), explanation()));
-            SASSERT(is_feasible());
+            SASSERT(is_feasible_dbg());
         }
     }
 
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index 74e19112fa3..b47215ff068 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -171,6 +171,7 @@ namespace smt {
         arith_eq_adapter               m_arith_eq_adapter;
         theory_diff_logic_statistics   m_stats;
         Graph                          m_graph;
+        bool                           m_consistent;
         theory_var                     m_izero, m_rzero; // cache the variable representing the zero variable.
         int_vector                     m_scc_id;                  // Cheap equality propagation
         eq_prop_info_set               m_eq_prop_info_set;        // set of existing equality prop infos
@@ -230,6 +231,7 @@ namespace smt {
             m_params(params),
             m_util(m),
             m_arith_eq_adapter(*this, params, m_util),
+            m_consistent(true),
             m_izero(null_theory_var),
             m_rzero(null_theory_var),
             m_terms(m),
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index 6ffea438011..31ec2bce110 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -72,6 +72,8 @@ void theory_diff_logic<Ext>::init(context * ctx) {
 
 template<typename Ext>
 bool theory_diff_logic<Ext>::internalize_term(app * term) {
+    if (!m_consistent)
+        return false;
     bool result = null_theory_var != mk_term(term);
     CTRACE("arith", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";);
     if (!result) {
@@ -161,6 +163,8 @@ void theory_diff_logic<Ext>::found_non_diff_logic_expr(expr * n) {
 
 template<typename Ext>
 bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
+    if (!m_consistent)
+        return false;
     context & ctx = get_context();
     if (!m_util.is_le(n) && !m_util.is_ge(n)) {
         found_non_diff_logic_expr(n);
@@ -341,7 +345,7 @@ void theory_diff_logic<Ext>::pop_scope_eh(unsigned num_scopes) {
     m_scopes.shrink(new_lvl);
     unsigned num_edges = m_graph.get_num_edges();
     m_graph.pop(num_scopes);
-    CTRACE("arith", !m_graph.is_feasible(), m_graph.display(tout););
+    CTRACE("arith", !m_graph.is_feasible_dbg(), m_graph.display(tout););
     if (num_edges != m_graph.get_num_edges() && m_num_simplex_edges > 0) {
         m_S.reset();
         m_num_simplex_edges = 0;
@@ -540,11 +544,13 @@ void theory_diff_logic<Ext>::propagate() {
 
 template<typename Ext>
 void theory_diff_logic<Ext>::inc_conflicts() {
-     m_stats.m_num_conflicts++;   
-     if (m_params.m_arith_adaptive) {
-         double g = m_params.m_arith_adaptive_propagation_threshold;
-         m_agility = m_agility*g + 1 - g;
-     }
+    get_context().push_trail(value_trail<context, bool>(m_consistent));
+    m_consistent = false;
+    m_stats.m_num_conflicts++;   
+    if (m_params.m_arith_adaptive) {
+        double g = m_params.m_arith_adaptive_propagation_threshold;
+        m_agility = m_agility*g + 1 - g;
+    }
 }
 
 template<typename Ext>
@@ -568,6 +574,7 @@ bool theory_diff_logic<Ext>::propagate_atom(atom* a) {
     if (!m_graph.enable_edge(edge_id)) {
         TRACE("arith", display(tout););
         set_neg_cycle_conflict();
+        
         return false;
     }
     return true;
@@ -741,7 +748,6 @@ 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);
@@ -944,10 +950,10 @@ void theory_diff_logic<Ext>::display(std::ostream & out) const {
 }
 
 template<typename Ext>
-bool theory_diff_logic<Ext>::is_consistent() const {
+bool theory_diff_logic<Ext>::is_consistent() const {    
     DEBUG_CODE(
         context& ctx = get_context();
-        for (unsigned i = 0; m_graph.is_feasible() && i < m_atoms.size(); ++i) {
+        for (unsigned i = 0; m_graph.is_feasible_dbg() && i < m_atoms.size(); ++i) {
             atom* a = m_atoms[i];
             bool_var bv = a->get_bool_var();
             lbool asgn = ctx.get_assignment(bv);        
@@ -958,7 +964,7 @@ bool theory_diff_logic<Ext>::is_consistent() const {
                 SASSERT(m_graph.is_feasible(edge_id));
             }
         });
-    return m_graph.is_feasible();
+    return m_consistent;
 }
 
 
@@ -1230,8 +1236,8 @@ theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shar
     Simplex& S = m_S;
     ast_manager& m = get_manager();
 
-    CTRACE("arith",!m_graph.is_feasible(), m_graph.display(tout););
-    SASSERT(m_graph.is_feasible());
+    CTRACE("arith",!m_graph.is_feasible_dbg(), m_graph.display(tout););
+    SASSERT(m_graph.is_feasible_dbg());
 
     update_simplex(S);
 
@@ -1294,8 +1300,8 @@ theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shar
             rational r = rational(val.first);
             m_graph.set_assignment(i, numeral(r));
         }
-        CTRACE("arith",!m_graph.is_feasible(), m_graph.display(tout););
-        SASSERT(m_graph.is_feasible());
+        CTRACE("arith",!m_graph.is_feasible_dbg(), m_graph.display(tout););
+        SASSERT(m_graph.is_feasible_dbg());
         inf_eps r1(rational(0), r);
         blocker = mk_gt(v, r1);
         return inf_eps(rational(0), r + m_objective_consts[v]);
diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h
index 3faff185c20..e7570637681 100644
--- a/src/smt/theory_utvpi.h
+++ b/src/smt/theory_utvpi.h
@@ -138,6 +138,7 @@ namespace smt {
         smt_params              m_params;
         arith_util              a;
         arith_eq_adapter        m_arith_eq_adapter;
+        bool                    m_consistent;
         th_var                  m_izero, m_rzero; //cache the variable representing the zero variable.
 
         dl_graph<GExt>          m_graph;
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index 0276ae3a51d..05367b87723 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -61,6 +61,7 @@ namespace smt {
         theory(m.mk_family_id("arith")),
         a(m),
         m_arith_eq_adapter(*this, m_params, a),
+        m_consistent(true),
         m_izero(null_theory_var),
         m_rzero(null_theory_var),
         m_nc_functor(*this),
@@ -192,6 +193,8 @@ namespace smt {
 
     template<typename Ext>
     void theory_utvpi<Ext>::inc_conflicts() {
+        get_context().push_trail(value_trail<context, bool>(m_consistent));
+        m_consistent = false;
         m_stats.m_num_conflicts++;   
         if (m_params.m_arith_adaptive) {
             double g = m_params.m_arith_adaptive_propagation_threshold;
@@ -312,6 +315,8 @@ namespace smt {
 
     template<typename Ext>
     bool theory_utvpi<Ext>::internalize_atom(app * n, bool) {
+        if (!m_consistent)
+            return false;
         context & ctx = get_context();
         if (!a.is_le(n) && !a.is_ge(n) && !a.is_lt(n) && !a.is_gt(n)) {
             found_non_utvpi_expr(n);
@@ -362,6 +367,8 @@ namespace smt {
 
     template<typename Ext>
     bool theory_utvpi<Ext>::internalize_term(app * term) {
+        if (!m_consistent)
+            return false;
         bool result = !get_context().inconsistent() && null_theory_var != mk_term(term);
         CTRACE("utvpi", !result, tout << "Did not internalize " << mk_pp(term, get_manager()) << "\n";);
         return result;
@@ -698,8 +705,8 @@ namespace smt {
     }
 
     template<typename Ext>
-    bool theory_utvpi<Ext>::is_consistent() const {
-        return m_graph.is_feasible();
+    bool theory_utvpi<Ext>::is_consistent() const {        
+        return m_consistent;
     }
 
 
@@ -743,7 +750,7 @@ namespace smt {
      */
     template<typename Ext>
     void theory_utvpi<Ext>::enforce_parity() {
-        SASSERT(m_graph.is_feasible());
+        SASSERT(m_graph.is_feasible_dbg());
         unsigned_vector todo;        
         unsigned sz = get_num_vars();
         for (unsigned i = 0; i < sz; ++i) {
@@ -788,7 +795,7 @@ namespace smt {
                 }
             }    
             TRACE("utvpi", display(tout););
-            SASSERT(m_graph.is_feasible());     
+            SASSERT(m_graph.is_feasible_dbg());     
         }
         DEBUG_CODE(
             for (unsigned i = 0; i < sz; ++i) {
@@ -798,7 +805,7 @@ namespace smt {
                     UNREACHABLE();
                 }            
             });
-        SASSERT(m_graph.is_feasible());
+        SASSERT(m_graph.is_feasible_dbg());
     }