Clean variable-length array size expressions. Fixes verification-engine-utils#192

This enables trace construction to reduce variable-length array
references down to constants, populating the full_lhs_value trace
member where previously it would have been a non-constant expression
such as `nil[0]` due to simplify_expr failing to evaluate the array
base expression.

Author: smowton

src/goto-symex/symex_builtin_functions.cpp

@@ -478,7 +478,9 @@ void goto_symext::symex_cpp_new(
   {
     symbol.type=array_typet();
     symbol.type.subtype()=code.type().subtype();
-    symbol.type.set(ID_size, code.find(ID_size));
+    exprt size_arg=static_cast<const exprt&>(code.find(ID_size));
+    clean_expr(size_arg, state, false);
+    symbol.type.set(ID_size, size_arg);
   }
   else
     symbol.type=code.type().subtype();