Fix unit tests to work for pointer subtraction

Author: NlightNFotis

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -479,10 +479,20 @@ TEST_CASE(
   SECTION("Subtraction of two pointer arguments")
   {
     // (int32_t *)a - (int32_t *)b
-    const auto constructed_term =
-      test.convert(minus_exprt{pointer_b, pointer_a});
-    const auto expected_term =
-      smt_bit_vector_theoryt::subtract(smt_term_b, smt_term_a);
+    const auto pointer_subtraction = minus_exprt{pointer_b, pointer_a};
+    const symbol_tablet symbol_table;
+    const namespacet ns{symbol_table};
+    track_expression_objects(pointer_subtraction, ns, test.object_map);
+    associate_pointer_sizes(
+      pointer_subtraction,
+      ns,
+      test.pointer_sizes,
+      test.object_map,
+      test.object_size_function.make_application);
+    const auto constructed_term = test.convert(pointer_subtraction);
+    const auto expected_term = smt_bit_vector_theoryt::unsigned_divide(
+      smt_bit_vector_theoryt::subtract(smt_term_b, smt_term_a),
+      smt_term_four_32bit);
     CHECK(constructed_term == expected_term);
   }