diff --git a/regression/cbmc-java/VarLengthArrayTrace1/Container.class b/regression/cbmc-java/VarLengthArrayTrace1/Container.class
new file mode 100644
index 00000000000..fd0aca0d247
Binary files /dev/null and b/regression/cbmc-java/VarLengthArrayTrace1/Container.class differ
diff --git a/regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.class b/regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.class
new file mode 100644
index 00000000000..3ec80acb986
Binary files /dev/null and b/regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.class differ
diff --git a/regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.java b/regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.java
new file mode 100644
index 00000000000..b014a545c7a
--- /dev/null
+++ b/regression/cbmc-java/VarLengthArrayTrace1/VarLengthArrayTrace1.java
@@ -0,0 +1,21 @@
+public class VarLengthArrayTrace1 {
+
+  public static void main(int unknown, int arg2) {
+
+    Container c = new Container(unknown);
+    if(c.val != 2) return;
+    int[] arr = new int[c.val];
+    arr[1] = arg2;
+    int test = arr[1];
+    assert(test != 10);
+
+  }
+
+}
+
+class Container {
+
+  public Container(int v) { val = v; }
+  int val;
+
+}
diff --git a/regression/cbmc-java/VarLengthArrayTrace1/test.desc b/regression/cbmc-java/VarLengthArrayTrace1/test.desc
new file mode 100644
index 00000000000..74403444d22
--- /dev/null
+++ b/regression/cbmc-java/VarLengthArrayTrace1/test.desc
@@ -0,0 +1,10 @@
+CORE
+VarLengthArrayTrace1.class
+--trace
+^EXIT=10$
+^SIGNAL=0$
+dynamic_3_array\[1l\]=10
+--
+^warning: ignoring
+assignment removed
+irep("(\\"nil\\")")
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index ed9c6262ee4..19cfe1f7e5c 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/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();