diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 05f47ada7..f6597fbc5 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -59,9 +59,12 @@ br_status bool_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * co mk_implies(args[0], args[1], result); return BR_DONE; case OP_XOR: - SASSERT(num_args == 2); - mk_xor(args[0], args[1], result); - return BR_DONE; + switch (num_args) { + case 0: return BR_FAILED; + 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; + } default: return BR_FAILED; }