Fix return of wrong value in pointer subtraction.

When subtracting pointers, such as in the expression (&a - &b), both
a and b need to be of the same type, and the return value is the number
of "steps" (as in, pointer increments for the underlying type) for the
two types.

Author: NlightNFotis

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -657,11 +657,23 @@ static smt_termt convert_expr_to_smt(
   // into an if-else branch that gives proper error handling information.
   const bool one_operand_pointer = lhs_is_pointer || rhs_is_pointer;
 
-  if(both_operands_bitvector || both_operands_pointers)
+  if(both_operands_bitvector)
   {
     return smt_bit_vector_theoryt::subtract(
       converted.at(minus.lhs()), converted.at(minus.rhs()));
   }
+  else if(both_operands_pointers)
+  {
+    const auto lhs_base_type = to_pointer_type(minus.lhs().type()).base_type();
+    const auto rhs_base_type = to_pointer_type(minus.rhs().type()).base_type();
+    INVARIANT(
+      lhs_base_type == rhs_base_type,
+      "only pointers of the same object type can be subtracted.");
+    return smt_bit_vector_theoryt::unsigned_divide(
+      smt_bit_vector_theoryt::subtract(
+        converted.at(minus.lhs()), converted.at(minus.rhs())),
+      pointer_sizes.at(lhs_base_type));
+  }
   else if(one_operand_pointer)
   {
     UNIMPLEMENTED_FEATURE(