The MJI implementation of Object.clone incorrectly handles arrays with elements of size 2 (i.e. longs and doubles). The following code demonstrates the problem:
long[] a1 = new long[] {1l, 2l, 3l, 4l, 5l};
long[] a2 = a1.clone();
for(long l : a2) { System.out.println(l); }
The problem seems to start at line 48 in JPF_java_lang_Object.java. The order of the operands in the ternary operator are backwards. Currently, if the component type is a primitive getType is called. getType returns and L-slash type instead of the actual primitive type. Then when this L-slahs type is passed to DynamicArea.newArray the size of the component type is always 1 since the L-slash type starts with L and L has a size of 1.
Long story short, to fix the problem switch the order of the operands for the ternary operator at line 48 in JPF_java_lang_Object.java.