simplify fails on dividing by plus expressions

[Stephen Siegel]

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$

[ywei]

Can not reproduce the bug. The program terminated normally and all properties hold. Need more tests.