Add unit tests for conversion of pointer_offset_exprt to SMT

Author: NlightNFotis

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1242,3 +1242,39 @@ TEST_CASE(
     CHECK(converted == expected);
   }
 }
+
+TEST_CASE("pointer_offset_exprt to SMT conversion", "[core][smt2_incremental]")
+{
+  // The config lines are necessary to ensure that pointer width in configured.
+  config.ansi_c.mode = configt::ansi_ct::flavourt::GCC;
+  config.ansi_c.set_arch_spec_x86_64();
+  config.bv_encoding.object_bits = 8;
+
+  const auto pointer_type = pointer_typet(unsigned_int_type(), 64 /* bits */);
+  const pointer_offset_exprt pointer_offset{
+    symbol_exprt{"foo", pointer_type}, pointer_type};
+
+  SECTION("simple pointer_offset_exprt conversion")
+  {
+    const auto converted = convert_expr_to_smt(pointer_offset);
+    const auto expected =
+      smt_bit_vector_theoryt::zero_extend(8)(smt_bit_vector_theoryt::extract(
+        55, 0)(smt_identifier_termt("foo", smt_bit_vector_sortt(64))));
+    CHECK(converted == expected);
+  }
+
+  SECTION("Invariant checks")
+  {
+    const cbmc_invariants_should_throwt invariants_throw;
+    SECTION("pointer_offset_exprt's operand type should be a bitvector type")
+    {
+      auto pointer_offset_copy = pointer_offset;
+      pointer_offset_copy.type() = bool_typet{};
+      REQUIRE_THROWS_MATCHES(
+        convert_expr_to_smt(pointer_offset_copy),
+        invariant_failedt,
+        invariant_failure_containing(
+          "Pointer offset should have a bitvector-based type."));
+    }
+  }
+}