From 24eae3f6e0ad81c843d2de242b85002a8fe9314c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 15 Jan 2017 12:06:56 -0800 Subject: [PATCH] fix crash with unary xor #870 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bool_rewriter.cpp | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) 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; }