port Jakob's update to bv_internalize

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Dec 18, 2023 · d008dbe · d008dbe
1 parent 085b5e2
commit d008dbe
Showing 1 changed file with 2 additions and 2 deletions.
diff --git 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;