Add unit tests for conversion of pointer_offset_exprt to SMT

Author: NlightNFotis

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -1241,3 +1241,35 @@ TEST_CASE(
     CHECK(converted == expected);
   }
 }
+
+TEST_CASE("pointer_offset_exprt to SMT conversion", "[core][smt2_incremental]")
+{
+  const symbol_exprt foo{"foo", pointer_typet(unsigned_int_type(), 64)};
+
+  SECTION("simple pointer_offset_exprt conversion")
+  {
+    const pointer_offset_exprt pointer_offset_exp =
+      *expr_try_dynamic_cast<pointer_offset_exprt>(pointer_offset(foo));
+    const auto converted = convert_expr_to_smt(pointer_offset_exp);
+    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")
+    {
+      pointer_offset_exprt pointer_offset_exp =
+        *expr_try_dynamic_cast<pointer_offset_exprt>(pointer_offset(foo));
+      pointer_offset_exp.type() = bool_typet{};
+      REQUIRE_THROWS_MATCHES(
+        convert_expr_to_smt(pointer_offset_exp),
+        invariant_failedt,
+        invariant_failure_containing(
+          "Pointer offset should have a bitvector-based type."));
+    }
+  }
+}