diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index 64a9816c9ba..ba80cb7911c 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -111,6 +111,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr) return convert_update(to_update_expr(expr)); else if(expr.id() == ID_update_bit) return convert_update_bit(to_update_bit_expr(expr)); + else if(expr.id() == ID_update_bits) + return convert_update_bits(to_update_bits_expr(expr)); else if(expr.id()==ID_case) return convert_case(expr); else if(expr.id()==ID_cond) diff --git a/src/util/bitvector_expr.cpp b/src/util/bitvector_expr.cpp index c62a50e594c..d8d6ff02e9e 100644 --- a/src/util/bitvector_expr.cpp +++ b/src/util/bitvector_expr.cpp @@ -77,17 +77,17 @@ exprt update_bits_exprt::lower() const to_bitvector_type(new_value().type()).get_width(); auto src_bv_type = bv_typet(width); - // build a mask 1...1 0...0 + // build a mask 0...0 1...1 auto mask_bv = make_bvrep(width, [new_value_width](std::size_t index) { - return index >= new_value_width; + return index < new_value_width; }); auto mask_expr = constant_exprt(mask_bv, src_bv_type); // shift the mask by the index auto mask_shifted = shl_exprt(mask_expr, index()); - auto src_masked = - bitand_exprt(typecast_exprt(src(), src_bv_type), mask_shifted); + auto src_masked = bitand_exprt( + typecast_exprt(src(), src_bv_type), bitnot_exprt(mask_shifted)); // zero-extend or shrink the replacement bits to match src auto new_value_casted = typecast_exprt(new_value(), src_bv_type);