Avoid invalid shift caused by excessive object bits

The unit test presented an invalid system configuration that would
provide zero offset bits. Also, guard against such set-ups by an
additional INVARIANT.

Author: tautschnig

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -877,6 +877,9 @@ static smt_termt convert_expr_to_smt(
     "Objects should be tracked before converting their address to SMT terms");
   const std::size_t object_id = object->second.unique_id;
   const std::size_t object_bits = config.bv_encoding.object_bits;
+  INVARIANT(
+    object_bits < sizeof(std::size_t) * CHAR_BITS,
+    "Object bits must too large for this platform");
   const std::size_t max_objects = std::size_t(1) << object_bits;
   if(object_id >= max_objects)
   {

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1550,7 +1550,7 @@ TEST_CASE(
     }
     SECTION("Pointer should be wide enough to encode offset")
     {
-      config.bv_encoding.object_bits = 64;
+      config.bv_encoding.object_bits = 63;
       const address_of_exprt address_of_foo{foo};
       track_expression_objects(address_of_foo, ns, test.object_map);
       test.object_map.at(foo).unique_id = 256;