diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 0ef563d00..7f4e290c0 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -2048,7 +2048,40 @@ namespace sat {
         return lit;
     }
 
-    ba_solver::constraint* ba_solver::add_xr(literal_vector const& lits, bool learned) {
+    ba_solver::constraint* ba_solver::add_xr(literal_vector const& _lits, bool learned) {
+        struct parity { 
+            bool sign; bool lit; 
+            parity(): sign(false), lit(false) {}
+            // {false, false},  p => {false, true}
+            // {false, false}, !p => {true, true}
+            // {false, true},   p => {true, false}
+            // {false, true},  !p => {true, false}            
+            void add(literal l) {
+                lit = !lit;
+                sign = sign != l.sign();
+            }                
+        };
+        literal_vector lits;
+        u_map<parity> var2parity;
+        for (literal lit : _lits) {
+            var2parity.insert_if_not_there2(lit.var(), parity())->get_data().m_value.add(lit);
+        }       
+        
+        bool polarity = false;
+        for (auto const& kv : var2parity) {
+            bool lit = kv.m_value.lit;
+            bool sign = kv.m_value.sign;
+            if (lit)
+                lits.push_back(literal(kv.m_key, sign));
+            else 
+                polarity = polarity ^ sign;
+        }
+        if (lits.empty()) {
+            throw default_exception("empty xor is TBD");
+        }
+        if (polarity) {
+            lits[0].neg();
+        }
         void * mem = m_allocator.allocate(xr::get_obj_size(lits.size()));
         xr* x = new (mem) xr(next_id(), lits);
         x->set_learned(learned);
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index a78fff1f8..f1ebd2e7c 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -759,8 +759,8 @@ namespace smt {
 
             int_vector zero_v;
             m_graph.compute_zero_succ(v1, zero_v);
-            for (unsigned j = 0; j < zero_v.size(); ++j) {
-                if (zero_v[j] == v2) {
+            for (auto v0 : zero_v) {
+                if (v0 == v2) {
                     zero_v.reset();
                     m_graph.compute_zero_succ(v2, zero_v);
                     break;
@@ -769,13 +769,13 @@ namespace smt {
 
             TRACE("utvpi", 
                   tout << "Disparity: " << v1 << "\n";
-                  for (unsigned j = 0; j < zero_v.size(); ++j) {
-                      tout << "decrement: " << zero_v[j] << "\n";
-                  });
+                  for (auto v : zero_v) {
+                      tout << "decrement: " << v << "\n";
+                  }
+                  display(tout);
+                  );
 
-            for (unsigned j = 0; j < zero_v.size(); ++j) {
-                int v = zero_v[j];
-                
+            for (auto v : zero_v) {                
                 m_graph.inc_assignment(v, numeral(-1));
                 th_var k = from_var(v);
                 if (!is_parity_ok(k)) {