array compare problem in symbolic?

[Stephen Siegel]

In this example I am running compare with a 2-dimensional array and when it comes time to check that the two are equal this query if generated:

CVC3 prover invoked with query: (FORALL (_index0: INT, _index0: INT): (LET cvc_0 = ((_index0 >= 0) AND (_index0 < 1))
IN ((cvc_0 AND cvc_0) => ((simpleArray2Spec_V0 WITH [0] := (simpleArray2Spec_V0[0] WITH [0] := 1))[_index0][_index0] = (simpleArray2Impl_V0 WITH [0] := (simpleArray2Impl_V0[0] WITH [0] := 1))[_index0][_index0])))) under context TRUE 
Valid

Why is _index0 being used for both bound index variables? Shouldn't one be _index0, and the other _index1, or something like that? (Also, what if _index0 is used as a variable in the program?)

[ywei]

The problem is I forgot to increase the suffix of _index. I fixed that so now the theorem prover can generate _index0, _index1...
And for the uniqueness of the bound variable name, I don't have a best solution. I used the underscore as a temporary solution because users don't often use variables names start with underscore. We can add a method to generate random names in the future.

[ywei]

And what example you were running? I have to test the modification on it.

[ywei]

Bug fixed. The example now terminates normally.