Execution exception in Evaluator

[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)

[Stephen Siegel]

I think this is a result of incorrect computations in symbolic package. The "and" of two symbolic expressions is not computed correctly. This means the path condition does not updated correctly when control enters the loop: the expression "X0>=1" should be added to the path condition, but it is not because the symbolic package is not returning the "and" correctly. See my other bug report tickets.

[ywei]

Fixed by correcting other bugs.