id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
12	Execution exception in Evaluator	ywei	ywei	"Revision 952, tile compare example:
Step 4: State 3 -> spec.mmp line 15 proc 0 [main@3->main@4] ""j = j + a[i];""

Predicate does not hold at current state.
CVC3 prover invoked with query: TRUE under context ((0 <= ((X0 * -1) + 3)) AND (0 <= X0)) 
CVC3 prover invoked with query: (0 <= (X0 + -1)) under context ((0 <= ((X0 * -1) + 3)) AND (0 <= X0)) 
edu.udel.cis.vsl.minimp.util.ExecutionException: Execution error encountered at line 15 column 10 through line 15 column 14:
a[i];
Possible array out of bounds error:
  index = 0
  extent = X0
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.referenceValue(Evaluator.java:107)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateSubscript(Evaluator.java:223)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:153)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:133)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:156)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:133)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.executeAssignment(Executor.java:145)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.execute(Executor.java:81)
	at edu.udel.cis.vsl.minimp.verify.std.StateManager.nextState(StateManager.java:74)
	at edu.udel.cis.vsl.minimp.verify.std.StateManager.nextState(StateManager.java:19)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.proceedToNewState(DfsSearcher.java:143)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:104)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:90)
	at edu.udel.cis.vsl.minimp.verify.Verification.compare(Verification.java:136)
	at edu.udel.cis.vsl.minimp.Minimp.compareEquivalence(Minimp.java:356)
	at edu.udel.cis.vsl.minimp.Minimp.main(Minimp.java:375)

"	defect	closed	major		front	1.0	fixed