From 1d3ee70af4d5d800d92143315b84e37a5c6a5cfd Mon Sep 17 00:00:00 2001 From: Jamey Sharp Date: Sun, 8 Aug 2021 15:52:54 -0700 Subject: [PATCH] support bit-blasting bvand (#5458) --- src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index 1f220d639..a846795e1 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -285,6 +285,7 @@ void OP(unsigned num_args, expr * const * args, expr_ref & result) { \ MK_BIN_AC_REDUCE(reduce_add, reduce_bin_add, mk_adder); MK_BIN_AC_REDUCE(reduce_mul, reduce_bin_mul, mk_multiplier); + MK_BIN_AC_REDUCE(reduce_and, reduce_bin_and, mk_and); MK_BIN_AC_REDUCE(reduce_or, reduce_bin_or, mk_or); MK_BIN_AC_REDUCE(reduce_xor, reduce_bin_xor, mk_xor); @@ -472,6 +473,9 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); SASSERT(num == 2); reduce_sle(args[0], args[1], result); return BR_DONE; + case OP_BAND: + reduce_and(num, args, result); + return BR_DONE; case OP_BOR: reduce_or(num, args, result); return BR_DONE;