id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
110	array compare problem in symbolic?	Stephen Siegel	ywei	"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?)
"	defect	closed	major		Administration	1.0	fixed	symbolic array