id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
188	Illegal argument exception in AdderTest	ywei	Stephen Siegel	"Got an illegal argument exception in AdderTest:

java.lang.IllegalArgumentException: Real expression not instanceof RationalExpression: X1[0]
	at edu.udel.cis.vsl.tass.symbolic.ideal.IdealUniverse.ideal(IdealUniverse.java:656)
	at edu.udel.cis.vsl.tass.symbolic.ideal.IdealUniverse.arrayRead(IdealUniverse.java:364)
	at edu.udel.cis.vsl.tass.symbolic.ideal.IdealUniverse.arrayRead(IdealUniverse.java:1)
	at edu.udel.cis.vsl.tass.dynamic.impl.DynamicFactory.arrayRead(DynamicFactory.java:212)
	at edu.udel.cis.vsl.tass.semantics.impl.Evaluator.dereference(Evaluator.java:503)
	at edu.udel.cis.vsl.tass.semantics.impl.Evaluator.evaluateSubscript(Evaluator.java:519)
	at edu.udel.cis.vsl.tass.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:312)
	at edu.udel.cis.vsl.tass.semantics.impl.Evaluator.evaluate(Evaluator.java:248)
	at edu.udel.cis.vsl.tass.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:323)
	at edu.udel.cis.vsl.tass.semantics.impl.Evaluator.evaluate(Evaluator.java:248)
	at edu.udel.cis.vsl.tass.semantics.impl.Executor.executeAssignment(Executor.java:251)
	at edu.udel.cis.vsl.tass.semantics.impl.Executor.execute(Executor.java:101)
	at edu.udel.cis.vsl.tass.verify.urgent.StateManager.nextStateSimple(StateManager.java:105)
	at edu.udel.cis.vsl.tass.verify.urgent.StateManager.nextState(StateManager.java:92)
	at edu.udel.cis.vsl.tass.verify.urgent.StateManager.nextState(StateManager.java:24)
	at edu.udel.cis.vsl.tass.search.DfsSearcher.proceedToNewState(DfsSearcher.java:183)
	at edu.udel.cis.vsl.tass.search.DfsSearcher.search(DfsSearcher.java:141)
	at edu.udel.cis.vsl.tass.search.DfsSearcher.search(DfsSearcher.java:122)
	at edu.udel.cis.vsl.tass.verify.Comparison.compare(Comparison.java:84)
	at adder.AdderTest.testCompare(AdderTest.java:55)
	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	Release 1.0	symbolic	1.0	fixed