From 7ed5ca05e353ba6aeb14ab43b877c3294fee2e4c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 18 Jul 2019 08:37:00 -0700 Subject: [PATCH] fix #2408 Signed-off-by: Nikolaj Bjorner --- src/ast/bv_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 545aeb61d..0154b3b58 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -326,7 +326,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned bv_size) { case OP_BXOR: return mk_binary(m_bv_xor, k, "bvxor", bv_size, true); case OP_BNAND: return mk_binary(m_bv_nand, k, "bvnand", bv_size, false); case OP_BNOR: return mk_binary(m_bv_nor, k, "bvnor", bv_size, false); - case OP_BXNOR: return mk_binary(m_bv_xnor, k, "bvxnor", bv_size, false); + case OP_BXNOR: return mk_binary(m_bv_xnor, k, "bvxnor", bv_size, true); case OP_BREDOR: return mk_reduction(m_bv_redor, k, "bvredor", bv_size); case OP_BREDAND: return mk_reduction(m_bv_redand, k, "bvredand", bv_size);