SMT2 backend: convert pointer minus scalar

This adds the missing conversion for "pointer - scalar" to the SMT2 backend.
It's not used by CBMC, which rewrites these to p+(-s) in the simplifier.

Author: kroening

src/solvers/smt2/smt2_conv.cpp

@@ -3587,7 +3587,19 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
   }
   else if(expr.type().id()==ID_pointer)
   {
-    SMT2_TODO("pointer subtraction");
+    if(
+      expr.op0().type().id() == ID_pointer &&
+      (expr.op1().type().id() == ID_unsignedbv ||
+       expr.op1().type().id() == ID_signedbv))
+    {
+      // rewrite p-o to p+(-o)
+      return convert_plus(
+        plus_exprt(expr.op0(), unary_minus_exprt(expr.op1())));
+    }
+    else
+      UNEXPECTEDCASE(
+        "unsupported operand types for -: " + expr.op0().type().id_string() +
+        " and " + expr.op1().type().id_string());
   }
   else if(expr.type().id()==ID_vector)
   {