id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
109	unknown expression type	Stephen Siegel	ywei	"Seems to be problem in symbolic package when converting from CVC expression back to symbolic expression.  The CVC expression printed in the error message below appears to be correct.   

By the way, where does the name {{{_BD1TY0}}} come from?

The command was
{{{
compare -verbose -simplify /Users/siegel/Documents/workspace/MiniMP/examples/simpleArray/simpleArraySpec.mmp -np 1 /Users/siegel/Documents/workspace/MiniMP/examples/simpleArray/simpleArrayImpl.mmp -np 1
}}}

{{{
java.lang.RuntimeException: Unknown or unimplemented expression type: (((_BD1TY0 >= 0) AND (_BD1TY0 < 1)) => ((simpleArraySpec_V0 WITH [0] := 1)[_BD1TY0] = (simpleArrayImpl_V0 WITH [0] := 1)[_BD1TY0]))
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.convertBack(CVC3TheoremProver.java:883)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.convertBack(CVC3TheoremProver.java:863)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.simplify(CVC3TheoremProver.java:655)
	at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.equalsExpression(SymUniverse.java:1300)
	at edu.udel.cis.vsl.minimp.dynamic.impl.DynamicFactory.equals(DynamicFactory.java:204)
	at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:122)
	at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:1)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:100)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:88)
	at edu.udel.cis.vsl.minimp.verify.IF.OuterPredicate.holdsAt(OuterPredicate.java:252)
	at edu.udel.cis.vsl.minimp.verify.IF.OuterPredicate.holdsAt(OuterPredicate.java:1)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:100)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:88)
	at edu.udel.cis.vsl.minimp.verify.Verification.compare(Verification.java:172)
	at edu.udel.cis.vsl.minimp.MiniMP.compareEquivalence(MiniMP.java:476)
	at edu.udel.cis.vsl.minimp.MiniMP.main(MiniMP.java:503)
No violation at this state.
}}}"	defect	closed	major		Administration	1.0	fixed	symbolic CVC3 convert