diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index cfc4d9c13..896f4b9aa 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -2024,13 +2024,24 @@ br_status bv_rewriter::mk_bv_nand(unsigned num, expr * const * args, expr_ref &
     return BR_REWRITE2;
 }
 
-br_status bv_rewriter::mk_bv_nor(unsigned num, expr * const * args, expr_ref & result) {
-    result = m_util.mk_bv_not(m_util.mk_bv_or(num, args));
+br_status bv_rewriter::mk_bv_nor(unsigned num_args, expr * const * args, expr_ref & result) {
+    result = m_util.mk_bv_not(m_util.mk_bv_or(num_args, args));
     return BR_REWRITE2;
 }
 
 br_status bv_rewriter::mk_bv_xnor(unsigned num_args, expr * const * args, expr_ref & result) {
-    result = m_util.mk_bv_not(m_util.mk_bv_xor(num_args, args));
+    switch (num_args) {
+    case 0: result = m().mk_true(); break;
+    case 1: result = m_util.mk_bv_not(args[0]); break;
+    case 2: result = m_util.mk_bv_not(m_util.mk_bv_xor(num_args, args)); break;
+    default:
+        mk_bv_xnor(2, args, result);
+        for (unsigned i = 2; i < num_args; ++i) {
+            expr* _args[2] = { result, args[i] };
+            mk_bv_xnor(2, _args, result);
+        }
+        return BR_REWRITE_FULL;
+    }
     return BR_REWRITE2;
 }