diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index b60310476..f21b2c554 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/src/ast/rewriter/bool_rewriter.cpp
@@ -62,7 +62,7 @@ br_status bool_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * co
         return BR_DONE;
     case OP_XOR:
         switch (num_args) {
-        case 0: return BR_FAILED;
+        case 0: result = m().mk_false(); return BR_DONE;
         case 1: result = args[0]; return BR_DONE;
         case 2: mk_xor(args[0], args[1], result); return BR_DONE;
         default: UNREACHABLE(); return BR_FAILED;
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index d11ff60a9..9cb21c769 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -577,6 +577,8 @@ struct goal2sat::imp : public sat::sat_internalizer {
     }
 
     void convert_iff2(app * t, bool root, bool sign) {
+        if (t->get_num_args() != 2)
+            throw default_exception("unexpected number of arguments to xor");
         SASSERT(t->get_num_args() == 2);
         unsigned sz = m_result_stack.size();
         SASSERT(sz >= 2);