diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp
index cd0be62b5..b3b69f640 100644
--- a/src/tactic/aig/aig.cpp
+++ b/src/tactic/aig/aig.cpp
@@ -546,14 +546,34 @@ struct aig_manager::imp {
         }
 
         void mk_iff(unsigned spos) {
+            if (spos + 2 != m_result_stack.size())
+                throw default_exception("aig conversion assumes expressions have been simplified");
             SASSERT(spos + 2 == m_result_stack.size());
             aig_lit r = m.mk_iff(m_result_stack[spos], m_result_stack[spos+1]);
             save_node_result(spos, r);
         }
         
         void mk_xor(unsigned spos) {
-            SASSERT(spos + 2 == m_result_stack.size());
-            aig_lit r = m.mk_xor(m_result_stack[spos], m_result_stack[spos+1]);
+            SASSERT(spos <= m_result_stack.size());
+            unsigned num = m_result_stack.size() - spos;
+            aig_lit r;
+            switch (num) {
+            case 0:
+                r = m.m_true;
+                break;
+            case 1:
+                r = m_result_stack[spos];
+                break;
+            case 2:
+                r = m.mk_xor(m_result_stack[spos], m_result_stack[spos+1]);                
+                break;
+            default:
+                r = m.mk_xor(m_result_stack[spos], m_result_stack[spos+1]);
+                for (unsigned i = 2; i < num; ++i) {
+                    r = m.mk_xor(r, m_result_stack[spos + i]);
+                }
+                break;
+            }
             save_node_result(spos, r);
         }