Add a test for making sure we hit the invariant in case we subtract a pointer from a constant

Author: NlightNFotis

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -586,6 +586,22 @@ TEST_CASE(
         smt_term_four_32bit));
   }
 
+  SECTION("Subtraction of pointer from integer")
+  {
+    // 2 - (*int32_t)a -- Semantically void expression, need to make sure
+    // we throw in this case.
+    const cbmc_invariants_should_throwt invariants_throw;
+    
+    const auto pointer_arith_expr = minus_exprt{two_bvint, pointer_a};
+    
+    REQUIRE_THROWS_MATCHES(
+      test.convert(pointer_arith_expr),
+      invariant_failedt,
+      invariant_failure_containing(
+        "minus expressions of pointer and integer expect lhs to be the pointer"));
+  }
+
+
   SECTION("Subtraction of two pointer arguments")
   {
     // (int32_t *)a - (int32_t *)b