Another illegal argument exception in AdderTest

[ywei]

Found another illegal argument exception when running AdderTest:

java.lang.IllegalArgumentException: Symbolic constant X1 exists with different type:
REAL[10]
REAL[X0]

at edu.udel.cis.vsl.tass.symbolic.constant.SymbolicConstantFactory.getOrCreateSymbolicConstant(SymbolicConstantFactory.java:34)
at edu.udel.cis.vsl.tass.symbolic.ideal.IdealUniverse.getOrCreateSymbolicConstant(IdealUniverse.java:624)
at edu.udel.cis.vsl.tass.symbolic.ideal.simplify.IdealSimplifier.simplifySymbolicConstant(IdealSimplifier.java:806)
at edu.udel.cis.vsl.tass.symbolic.ideal.simplify.IdealSimplifier.simplifyTree(IdealSimplifier.java:207)
at edu.udel.cis.vsl.tass.symbolic.ideal.simplify.IdealSimplifier.simplify(IdealSimplifier.java:142)
at edu.udel.cis.vsl.tass.symbolic.ideal.simplify.IdealSimplifier.simplify(IdealSimplifier.java:1)
at edu.udel.cis.vsl.tass.simplify.light.LightSymbolicSimplifier.simplify(LightSymbolicSimplifier.java:25)
at edu.udel.cis.vsl.tass.dynamic.impl.DynamicSimplifier.simplify(DynamicSimplifier.java:144)
at edu.udel.cis.vsl.tass.state.impl.ModelStateFactory.simplify(ModelStateFactory.java:61)
at edu.udel.cis.vsl.tass.verify.urgent.StateManager.simplify(StateManager.java:215)
at edu.udel.cis.vsl.tass.verify.urgent.StateManager.nextStateSimple(StateManager.java:109)
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)

[Stephen Siegel]

Fixed: problem was that during simplification type of array variable changed from int[X1] to int[10] and system requested a symbolic constant with same name but different type. Now you are allowed to have two symbolic constants with the same name as long as the types differ.