id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
80	simplify fails on dividing by plus expressions	Stephen Siegel	ywei	"frederic:diffusion siegel$ tass verify -simplify diffusion1_seq.mmp 
+----------------------------------------------------------------------+
|           TASS: Toolkit for Accurate Scientific Software             |
|  version 1.0.r1080 (2009-09-07)        http://vsl.cis.udel.edu/tass  |
+----------------------------------------------------------------------+
                   command            : verify
                   model              : diffusion1_seq.mmp(np=1)
                   Deadlock detection : absolute
                   Reduction          : standard
                   verbose:           : No
                   simplify:          : Yes
                   bufferBound        : 10
                   use loop technique : false

cvc3.Cvc3Exception: Arithmetic error: Divide by a PLUS expression not handled in(1 / (-1 + X0))
	at cvc3.ValidityChecker.jniSimplify(Native Method)
	at cvc3.ValidityChecker.simplify(ValidityChecker.java:1304)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.simplify(CVC3TheoremProver.java:639)
	at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.divideExpression(SymUniverse.java:574)
	at edu.udel.cis.vsl.minimp.value.impl.ValueFactory.divide(ValueFactory.java:216)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateDivide(Evaluator.java:303)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:206)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:151)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.initializeVariable(Executor.java:432)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.initialize(Executor.java:478)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.initialize(Executor.java:489)
	at edu.udel.cis.vsl.minimp.verify.std.StateManager.initialState(StateManager.java:49)
	at edu.udel.cis.vsl.minimp.verify.Verification.verify(Verification.java:76)
	at edu.udel.cis.vsl.minimp.Minimp.verify(Minimp.java:431)
	at edu.udel.cis.vsl.minimp.Minimp.main(Minimp.java:525)
Exception in thread ""main"" java.lang.NullPointerException
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.convertBack(CVC3TheoremProver.java:662)
	at edu.udel.cis.vsl.minimp.symbolic.prover.CVC3TheoremProver.simplify(CVC3TheoremProver.java:649)
	at edu.udel.cis.vsl.minimp.symbolic.SymUniverse.divideExpression(SymUniverse.java:574)
	at edu.udel.cis.vsl.minimp.value.impl.ValueFactory.divide(ValueFactory.java:216)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateDivide(Evaluator.java:303)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluateBinary(Evaluator.java:206)
	at edu.udel.cis.vsl.minimp.semantics.impl.Evaluator.evaluate(Evaluator.java:151)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.initializeVariable(Executor.java:432)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.initialize(Executor.java:478)
	at edu.udel.cis.vsl.minimp.semantics.impl.Executor.initialize(Executor.java:489)
	at edu.udel.cis.vsl.minimp.verify.std.StateManager.initialState(StateManager.java:49)
	at edu.udel.cis.vsl.minimp.verify.Verification.verify(Verification.java:76)
	at edu.udel.cis.vsl.minimp.Minimp.verify(Minimp.java:431)
	at edu.udel.cis.vsl.minimp.Minimp.main(Minimp.java:525)
frederic:diffusion siegel$ 
"	defect	closed	major		symbolic	1.0	fixed	symbolic, division, quotient