diff --git a/src/smt/theory_utvpi.cpp b/src/smt/theory_utvpi.cpp
index 1f56b748b..3a9f10c30 100644
--- a/src/smt/theory_utvpi.cpp
+++ b/src/smt/theory_utvpi.cpp
@@ -138,14 +138,12 @@ namespace smt {
                 m_coeff_map.insert_if_not_there2(e, rational(0))->get_data().m_value += mul;
             }
         }
-        obj_map<expr, rational>::iterator it  = m_coeff_map.begin();
-        obj_map<expr, rational>::iterator end = m_coeff_map.end();
-        for (; it != end; ++it) {
-            rational r = it->m_value;
+        for (auto const& kv : m_coeff_map) {
+            rational r = kv.m_value;
             if (r.is_zero()) {
                 continue;
             }
-            m_terms.push_back(std::make_pair(it->m_key, r));
+            m_terms.push_back(std::make_pair(kv.m_key, r));
             if (m_terms.size() > 2) {
                 return false;
             }
diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h
index 6f12c50e6..f85158e05 100644
--- a/src/smt/theory_utvpi.h
+++ b/src/smt/theory_utvpi.h
@@ -138,7 +138,7 @@ namespace smt {
         smt_params              m_params;
         arith_util              a;
         arith_eq_adapter        m_arith_eq_adapter;
-        th_var                  m_zero; //cache the variable representing the zero variable.
+        th_var                  m_izero, m_rzero; //cache the variable representing the zero variable.
 
         dl_graph<GExt>          m_graph;
         nc_functor              m_nc_functor;
@@ -299,7 +299,7 @@ namespace smt {
 
         void new_eq_or_diseq(bool is_eq, th_var v1, th_var v2, justification& eq_just);
         
-        th_var get_zero(sort* s) { init_zero(); return m_zero; }
+        th_var get_zero(sort* s) { init_zero(); 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 3b46bae29..5d2e23163 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -62,7 +62,8 @@ namespace smt {
             theory(m.mk_family_id("arith")),
             a(m),
             m_arith_eq_adapter(*this, m_params, a),
-            m_zero(null_theory_var),
+            m_izero(null_theory_var),
+            m_rzero(null_theory_var),
             m_nc_functor(*this),
             m_asserted_qhead(0),
             m_agility(0.5),
@@ -133,7 +134,8 @@ namespace smt {
     template<typename Ext>
     void theory_utvpi<Ext>::reset_eh() {
         m_graph            .reset();
-        m_zero              = null_theory_var;
+        m_izero              = null_theory_var;
+        m_rzero              = null_theory_var;
         m_atoms            .reset();
         m_asserted_atoms   .reset();
         m_stats            .reset();
@@ -259,13 +261,13 @@ namespace smt {
     template<typename Ext>
     void theory_utvpi<Ext>::init(context* ctx) {
         theory::init(ctx);
-        m_zero = null_theory_var;
     }
 
     template<typename Ext>
     void theory_utvpi<Ext>::init_zero() {
-        if (m_zero == null_theory_var) {
-            m_zero  = mk_var(get_context().mk_enode(a.mk_numeral(rational(0), true), false, false, true));
+        if (m_izero == null_theory_var) {
+            m_izero  = mk_var(get_context().mk_enode(a.mk_numeral(rational(0), true), false, false, true));
+            m_rzero  = mk_var(get_context().mk_enode(a.mk_numeral(rational(0), false), false, false, true));
         }
     }
 
@@ -783,7 +785,8 @@ namespace smt {
         m.register_factory(m_factory);
         enforce_parity();
         init_zero();
-        m_graph.set_to_zero(to_var(m_zero), neg(to_var(m_zero)));
+        m_graph.set_to_zero(to_var(m_izero), neg(to_var(m_izero)));
+        m_graph.set_to_zero(to_var(m_rzero), neg(to_var(m_rzero)));
         compute_delta();   
         DEBUG_CODE(model_validate(););
     }