Rewriting of (T)(x OP y) must not introduce overflow

Distributing signed-to-unsigned type casts over addition can result in
an unsigned overflow where previously there was no overflow.

Author: tautschnig

regression/goto-instrument/simplify-overflow/main.c

@@ -0,0 +1,7 @@
+int main()
+{
+  int x;
+  int y;
+  __CPROVER_assume(x > 0 && -x == y);
+  unsigned result = x + y;
+}

regression/goto-instrument/simplify-overflow/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--constant-propagator --signed-overflow-check --unsigned-overflow-check
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This use of "--constant-propagator" is just to exercise expression
+simplification. In this example, distributing the type cast from signed to
+unsigned int over "x+y" would result in an unsigned integer overflow. The
+original program, which does not have such a type cast on each of the operands,
+does not have any (unsigned) overflow.

src/util/simplify_expr.cpp

@@ -918,7 +918,9 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       to_bitvector_type(expr_type).get_width()>
       to_bitvector_type(op_type).get_width();
 
-    if(!enlarge)
+    if(
+      !enlarge &&
+      (expr_type.id() != ID_unsignedbv || op_type.id() == ID_unsignedbv))
     {
       irep_idt op_id = expr.op().id();