Recanonicalize with_exprt when renaming old member

It may happen that during renaming the `old` subexpression of a `with_exprt`
expression is propagated with a value that has an array type with a size that
is a symbol with an L2 index that is different. In this case the type of the
`with_exprt` will not match with the type of the `old` subexpression
anymore.
To address this issue we re-canonicalize the `with_exprt` by propagating
the type of the `old` subexpression to the type of the `with_exprt`.

Author: peterschrammel

src/goto-symex/goto_symex_state.cpp

@@ -263,6 +263,22 @@ goto_symex_statet::rename(exprt expr, const namespacet &ns)
       *it = rename<level>(std::move(*it), ns).get();
 
     const exprt &c_expr = as_const(expr);
+
+    // It may happen that the `old` subexpression of a `with_exprt` expression
+    // is propagated with a value that has an array type with a size that is a
+    // symbol with an L2 index that is different. In this case the type of the
+    // `with_exprt` will not match with the type of the `old` subexpression
+    // anymore.
+    // To address this issue we re-canonicalize the `with_exprt` by propagating
+    // the type of the `old` subexpression to the type of the `with_exprt`.
+    const auto *c_with_expr = expr_try_dynamic_cast<with_exprt>(c_expr);
+    if(
+      c_with_expr && can_cast_type<array_typet>(c_with_expr->type()) &&
+      can_cast_type<array_typet>(c_with_expr->old().type()) &&
+      c_with_expr->type() != c_with_expr->old().type())
+    {
+      expr.type() = to_with_expr(expr).old().type();
+    }
     INVARIANT_WITH_DIAGNOSTICS(
       (expr.id() != ID_with ||
        c_expr.type() == to_with_expr(c_expr).old().type()) &&