Opened 17 years ago

Closed 17 years ago

#3 closed defect (fixed)

Execution exception in InnerPredicate

Reported by: ywei Owned by: Stephen Siegel
Priority: major Milestone:
Component: verify Version: 1.0
Keywords: Cc:

Description (last modified by ywei)

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)

Change History (2)

comment:1 by ywei, 17 years ago

Description: modified (diff)

comment:2 by Stephen Siegel, 17 years ago

Resolution: → fixed
Status: new → closed

Bug fixed in revision 946----input variables were not getting initialized correctly.

Note: See TracTickets for help on using tickets.