diff --git a/src/sat/sat_aig_cuts.cpp b/src/sat/sat_aig_cuts.cpp
index 63e643c45..e91fe5929 100644
--- a/src/sat/sat_aig_cuts.cpp
+++ b/src/sat/sat_aig_cuts.cpp
@@ -632,7 +632,7 @@ namespace sat {
             }
             unsigned num_comp = (1 << n.size());
             for (unsigned i = 0; i < num_comp; ++i) {
-                unsigned parity = 0;
+                bool parity = false;
                 m_clause.reset();
                 for (unsigned j = 0; j < n.size(); ++j) {
                     literal lit = m_literals[n.offset() + j];
@@ -640,11 +640,11 @@ namespace sat {
                         lit.neg();
                     }
                     else {
-                        ++parity;
+                        parity ^= true;
                     }
                     m_clause.push_back(lit);
                 }
-                m_clause.push_back(1 == (parity % 2) ? r : ~r);
+                m_clause.push_back(parity ? r : ~r);
                 on_clause(m_clause);
             }
             return;
diff --git a/src/sat/sat_aig_simplifier.cpp b/src/sat/sat_aig_simplifier.cpp
index 66005a0f7..4d3f78145 100644
--- a/src/sat/sat_aig_simplifier.cpp
+++ b/src/sat/sat_aig_simplifier.cpp
@@ -215,7 +215,9 @@ namespace sat {
             // <=> 
             // ~head = t1 + t2 + ..
             literal head = ~xors[index];
+            TRACE("aig_simplifier", tout << xors << "\n";);
             unsigned sz = xors.size() - 1;
+            m_lits.reset();
             for (unsigned i = xors.size(); i-- > 0; ) {
                 if (i != index) 
                     m_lits.push_back(xors[i]);
diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index bf8c51658..54eb008ca 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -469,6 +469,7 @@ namespace sat {
             std::string line;
             std::getline(std::cin, line);                
             SASSERT(false);
+            INVOKE_DEBUGGER();
             exit(0);
             UNREACHABLE();
             //display(std::cout);
diff --git a/src/sat/sat_xor_finder.cpp b/src/sat/sat_xor_finder.cpp
index 39e1e1588..8504eae01 100644
--- a/src/sat/sat_xor_finder.cpp
+++ b/src/sat/sat_xor_finder.cpp
@@ -61,9 +61,10 @@ namespace sat {
         for (literal l : c) {
             m_var_position[l.var()] = i;
             s.mark_visited(l.var());
-            parity ^= l.sign();
+            parity ^= !l.sign();
             mask |= (l.sign() << (i++)); 
         }
+        // parity is number of true literals in clause.
         m_clauses_to_remove.reset();
         m_clauses_to_remove.push_back(&c);
         m_clause.resize(c.size());
@@ -108,7 +109,7 @@ namespace sat {
             lits.push_back(literal(l.var(), false));
             s.set_external(l.var());
         }
-        if (parity) lits[0].neg();
+        if (parity == (lits.size() % 2 == 0)) lits[0].neg();
         m_on_xor(lits);
     }