id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
186	null pointer exception from CVC3 prover	Stephen Siegel	ywei	"Run AdderTest now (TASSv1.0 r1532) and you will get a null pointer exception inside CVC3, which is caused by something in the valid method in CVC3TheoremProver setting the assumption to null, even though the context passed to this method was not null.

{{{
java.lang.NullPointerException
	at cvc3.ValidityChecker.assertFormula(ValidityChecker.java:1289)
	at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.addAssumption(CVC3TheoremProver.java:1014)
	at edu.udel.cis.vsl.tass.prove.cvc.CVC3TheoremProver.valid(CVC3TheoremProver.java:567)
	at edu.udel.cis.vsl.tass.prove.ideal.IdealCVC3HybridProver.valid(IdealCVC3HybridProver.java:49)
	at edu.udel.cis.vsl.tass.dynamic.impl.DynamicFactory.valid(DynamicFactory.java:870)
	at edu.udel.cis.vsl.tass.dynamic.impl.DynamicFactory.isValid(DynamicFactory.java:823)
	at edu.udel.cis.vsl.tass.verify.urgent.Enabler.newPathCondition(Enabler.java:346)
	at edu.udel.cis.vsl.tass.verify.urgent.Enabler.enabledTransitions(Enabler.java:107)
	at edu.udel.cis.vsl.tass.verify.urgent.Enabler.enabledTransitions(Enabler.java:1)
	at edu.udel.cis.vsl.tass.search.DfsSearcher.proceedToNewState(DfsSearcher.java:195)
	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.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:44)
	at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:15)
	at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:41)
	at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:20)
	at org.junit.internal.runners.statements.RunBefores.evaluate(RunBefores.java:28)
	at org.junit.internal.runners.statements.RunAfters.evaluate(RunAfters.java:31)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:73)
	at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:46)
	at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:180)
	at org.junit.runners.ParentRunner.access$000(ParentRunner.java:41)
	at org.junit.runners.ParentRunner$1.evaluate(ParentRunner.java:173)
	at org.junit.internal.runners.statements.RunBefores.evaluate(RunBefores.java:28)
	at org.junit.internal.runners.statements.RunAfters.evaluate(RunAfters.java:31)
	at org.junit.runners.ParentRunner.run(ParentRunner.java:220)
	at org.eclipse.jdt.internal.junit4.runner.JUnit4TestReference.run(JUnit4TestReference.java:46)
	at org.eclipse.jdt.internal.junit.runner.TestExecution.run(TestExecution.java:38)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:467)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.runTests(RemoteTestRunner.java:683)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.run(RemoteTestRunner.java:390)
	at org.eclipse.jdt.internal.junit.runner.RemoteTestRunner.main(RemoteTestRunner.java:197)
}}}"	defect	closed	major	Release 1.0	prove	1.0	fixed	CVC3 theorem prover