id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
16	symbolic exception: arrayloop_2	Stephen Siegel	ywei	"frederic:arrayloop siegel$ tass compare arrayloopSpec_2.mmp arrayloopImpl_2.mmp 
MiniMP version 1.0
URL: http://vsl.cis.udel.edu

Minimp initialized with 1 process
Program runs in compare mode.
Program parsed succesfully.
IR generated succesfully.
java.lang.RuntimeException: Unknown symbolic expression: Undefined
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:170)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.processWriteExpr(CVC3TheoremProver.java:252)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:166)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.processWriteExpr(CVC3TheoremProver.java:252)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:166)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.processWriteExpr(CVC3TheoremProver.java:252)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:166)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.processWriteExpr(CVC3TheoremProver.java:252)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:166)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.processSubscriptExpr(CVC3TheoremProver.java:239)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:162)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.processSubscriptExpr(CVC3TheoremProver.java:239)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:162)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.parseSymExpr(CVC3TheoremProver.java:142)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.simplify(CVC3TheoremProver.java:420)
	at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.plusExpression(SymUniverse.java:244)
	at edu.udel.cis.vsl.minimp.value.impl.ValueFactory.add(ValueFactory.java:174)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateAdd(Evaluator.java:237)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:166)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:130)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.executeAssignment(Executor.java:139)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.execute(Executor.java:67)
	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:1)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.proceedToNewState(DfsSearcher.java:141)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:102)
	at edu.udel.cis.vsl.minimp.search.DfsSearcher.search(DfsSearcher.java:88)
	at edu.udel.cis.vsl.minimp.verify.Verification.compare(Verification.java:138)
	at edu.udel.cis.vsl.minimp.Minimp.compareEquivalence(Minimp.java:356)
	at edu.udel.cis.vsl.minimp.Minimp.main(Minimp.java:375)
Trace from P1:
P1 Trace summary:

Step 1: State 0 -> arrayloopSpec_2.mmp line 11 proc 0 [main@0->main@1] ""i = 0;"" -> State 1
Step 2: State 1 -> arrayloopSpec_2.mmp line 12 proc 0 [main@1->main@2] ""j = 0;"" -> State 2
.
.
.
"	defect	closed	major		symbolic	1.0	fixed		ywei@…