mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 18:36:16 +00:00
Code Activity

fix crash with unary xor #870

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-01-15 12:06:56 -08:00
parent dd0d3d4510
commit 24eae3f6e0
1 changed files with 6 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/rewriter/bool_rewriter.cpp
View file

@ -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); mk_implies(args[0], args[1], result);
return BR_DONE; return BR_DONE;
case OP_XOR: case OP_XOR:
SASSERT(num_args == 2); switch (num_args) {
mk_xor(args[0], args[1], result); case 0: return BR_FAILED;
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;
}
default: default:
return BR_FAILED; return BR_FAILED;
} }