symbolic arrayWrite method giving incorrect results

[Stephen Siegel]

Here is an example of incorrect result (from arrayLoop):

Setting array element: D[i][j] <- 0.0
LHS value: &object_D[0,1]
Old array object value: P1_P0_S0_F0_V4<(0, 0), 0.0>
New array object value: P1_P0_S0_F0_V4<(0, 1), 0.0>

Here D is a 2-dimensional array of real. At the beginning of this excerpt, D[0][0]=0.0, and all other elements of D are undefined. The statement executed is D[0][1]=0.0. It is executed by calling arrayWrite:

newValue = valueFactory.arrayWrite(environment.getAssumption(),

oldValue, reference.indices(), value);

which just call arrayWrite in the symbolic package. The result (newValue) has dropped the value of D in position [0,0].

[ywei]

Fixed. The CVC3 will simplify the representation of an array when several entries are on the same row.