Merge pull request #8496 from diffblue/fix_update_bit

fix `update_bit` lowering

Author: tautschnig

src/util/bitvector_expr.cpp

@@ -37,6 +37,17 @@ extractbits_exprt::extractbits_exprt(
   add_to_operands(std::move(_src), from_integer(_index, integer_typet()));
 }
 
+update_bit_exprt::update_bit_exprt(
+  exprt _src,
+  const std::size_t _index,
+  exprt _new_value)
+  : update_bit_exprt(
+      std::move(_src),
+      from_integer(_index, integer_typet()),
+      std::move(_new_value))
+{
+}
+
 exprt update_bit_exprt::lower() const
 {
   const auto width = to_bitvector_type(type()).get_width();
@@ -54,7 +65,8 @@ exprt update_bit_exprt::lower() const
     typecast_exprt(src(), src_bv_type), bitnot_exprt(mask_shifted));
 
   // zero-extend the replacement bit to match src
-  auto new_value_casted = zero_extend_exprt{new_value(), src_bv_type};
+  auto new_value_bv = typecast_exprt{new_value(), bv_typet{1}};
+  auto new_value_casted = zero_extend_exprt{new_value_bv, src_bv_type};
 
   // shift the replacement bits
   auto new_value_shifted = shl_exprt(new_value_casted, index());

unit/Makefile

@@ -96,6 +96,7 @@ SRC += analyses/ai/ai.cpp \
        pointer-analysis/value_set.cpp \
        solvers/bdd/miniBDD/miniBDD.cpp \
        solvers/flattening/boolbv.cpp \
+       solvers/flattening/boolbv_update_bit.cpp \
        solvers/floatbv/float_utils.cpp \
        solvers/prop/bdd_expr.cpp \
        solvers/sat/external_sat.cpp \

unit/solvers/flattening/boolbv_update_bit.cpp

@@ -0,0 +1,48 @@
+/*******************************************************************\
+
+Module: Unit tests for boolbvt
+
+Author: Daniel Kroening
+
+\*******************************************************************/
+
+/// \file
+/// Unit tests for boolbvt
+
+#include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
+#include <util/cout_message.h>
+#include <util/namespace.h>
+#include <util/std_expr.h>
+#include <util/symbol_table.h>
+
+#include <solvers/flattening/boolbv.h>
+#include <solvers/sat/satcheck.h>
+#include <testing-utils/use_catch.h>
+
+SCENARIO(
+  "boolbvt_update_bit",
+  "[core][solvers][flattening][boolbvt][update_bit]")
+{
+  console_message_handlert message_handler;
+  message_handler.set_verbosity(0);
+
+  GIVEN("A satisfiable bit-vector formula f with update_bit")
+  {
+    satcheckt satcheck{message_handler};
+    symbol_tablet symbol_table;
+    namespacet ns{symbol_table};
+    boolbvt boolbv{ns, satcheck, message_handler};
+
+    unsignedbv_typet u32{32};
+    boolbv << equal_exprt(
+      symbol_exprt{"x", u32},
+      update_bit_exprt{from_integer(10, u32), 0, true_exprt{}});
+
+    THEN("is indeed satisfiable")
+    {
+      REQUIRE(boolbv() == decision_proceduret::resultt::D_SATISFIABLE);
+    }
+  }
+}