id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
57	nestedLoops: RuntimeException: Undefined value found.	zirkel	ywei	"Running compare on nestedLoopsSpec_2.mmp and nestedLoopsImpl_2.mmp gives the following:

java.lang.RuntimeException: Undefined value found.
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:115)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:164)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:164)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:176)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.valid(CVC3TheoremProver.java:341)
	at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.valid(SymUniverse.java:1552)
	at edu.udel.cis.vsl.minimp.value.impl.ValueFactory.valid(ValueFactory.java:299)
	at edu.udel.cis.vsl.minimp.verify.IF.InnerPredicate.holdsAt(InnerPredicate.java:124)
	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:160)
	at edu.udel.cis.vsl.minimp.test.NestedLoopsTest.testCompare(NestedLoopsTest.java:91)
	at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
	at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:39)
	at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:25)
	at java.lang.reflect.Method.invoke(Method.java:597)
	at org.junit.internal.runners.TestMethodRunner.executeMethodBody(TestMethodRunner.java:99)
	at org.junit.internal.runners.TestMethodRunner.runUnprotected(TestMethodRunner.java:81)
	at org.junit.internal.runners.BeforeAndAfterRunner.runProtected(BeforeAndAfterRunner.java:34)
	at org.junit.internal.runners.TestMethodRunner.runMethod(TestMethodRunner.java:75)
	at org.junit.internal.runners.TestMethodRunner.run(TestMethodRunner.java:45)
	at org.junit.internal.runners.TestClassMethodsRunner.invokeTestMethod(TestClassMethodsRunner.java:66)
	at org.junit.internal.runners.TestClassMethodsRunner.run(TestClassMethodsRunner.java:35)
	at org.junit.internal.runners.TestClassRunner$1.runUnprotected(TestClassRunner.java:42)
	at org.junit.internal.runners.BeforeAndAfterRunner.runProtected(BeforeAndAfterRunner.java:34)
	at org.junit.internal.runners.TestClassRunner.run(TestClassRunner.java:52)
	at org.eclipse.jdt.internal.junit4.runner.JUnit4TestReference.run(JUnit4TestReference.java:45)
	at org.eclipse.jdt.internal.junit.runner.TestExecution.run(TestExecution.java:38)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:460)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:673)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.run(RemoteTestRunner.java:386)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.main(RemoteTestRunner.java:196)"	defect	closed	major		symbolic	1.0	fixed	symbolic, prover, cvc3, CVC3TheoremProver, nestedLoops, example