From d008dbe50adc47d776b477158b0beb4238562668 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 Dec 2023 09:31:59 -0800
Subject: [PATCH] port Jakob's update to bv_internalize
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/sat/smt/bv_internalize.cpp | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/sat/smt/bv_internalize.cpp b/src/sat/smt/bv_internalize.cpp
index 99d2a34ae..f1e9e8374 100644
--- a/src/sat/smt/bv_internalize.cpp
+++ b/src/sat/smt/bv_internalize.cpp
@@ -191,8 +191,8 @@ namespace bv {
case OP_BAND: internalize_ac(mk_and); break;
case OP_BOR: internalize_ac(mk_or); break;
case OP_BXOR: internalize_ac(mk_xor); break;
- case OP_BNAND: internalize_bin(mk_nand); break;
- case OP_BNOR: internalize_bin(mk_nor); break;
+ case OP_BNAND: if_unary(mk_not); internalize_bin(mk_nand); break;
+ case OP_BNOR: if_unary(mk_not); internalize_bin(mk_nor); break;
case OP_BXNOR: if_unary(mk_not); internalize_bin(mk_xnor); break;
case OP_BCOMP: internalize_bin(mk_comp); break;
case OP_SIGN_EXT: internalize_pun(mk_sign_extend); break;