From a61e9d6b49c405d94a184fc073858aab3da63f99 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 May 2021 10:33:43 -0700 Subject: [PATCH] #5260 --- src/ast/rewriter/bool_rewriter.cpp | 2 +- src/sat/tactic/goal2sat.cpp | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) 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);