id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
3	Execution exception in InnerPredicate	ywei	Stephen Siegel	"Revision 945, tile example:

CVC3 prover invoked with query: (LET cvc_0 = (X1[1] + X1[0])
IN (cvc_0 = (X1[2] + cvc_0))) under context (((1 < X0) AND ((0 < X0) AND ((X0 < 4) AND NOT (X0 < 0)))) AND NOT (2 < X0)) 
edu.udel.cis.vsl.minimp.util.ExecutionException: Execution error encountered at line 3 column 0 through line 3 column 23:
output real s is impl.s;
Expected value: X1[2]+X1[1]+X1[0]
Actual value: X1[1]+X1[0]
edu.udel.cis.vsl.minimp.util.ExecutionException: Execution error encountered at line 3 column 0 through line 3 column 23:
output real s is impl.s;
Expected value: X1[2]+X1[1]+X1[0]
Actual value: X1[1]+X1[0]
	at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:113)
	at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:1)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:90)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:78)
	at edu.udel.cis.vsl.minimp.verify.IF.OuterPredicate.holdsAt(OuterPredicate.java:154)
	at edu.udel.cis.vsl.minimp.verify.IF.OuterPredicate.holdsAt(OuterPredicate.java:1)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:90)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:78)
	at edu.udel.cis.vsl.minimp.verify.Verification.compare(Verification.java:132)
	at edu.udel.cis.vsl.minimp.Minimp.compareEquivalence(Minimp.java:241)
	at edu.udel.cis.vsl.minimp.Minimp.main(Minimp.java:260)
"	defect	closed	major		verify	1.0	fixed