team-worthwhile/worthwhile — Issue #104: EmptyStackException in prover
Author: jspam
Created: 2012-02-27 14:10:15+00:00
State: open
Labels: prover

When trying to prove `heap.ww` from commit 641ada973eef1235953a87cabeb483bf72b608ea, an `EmptyStackException` is thrown:

```
java.util.EmptyStackException
at java.util.Stack.peek(Stack.java:102)
at java.util.Stack.pop(Stack.java:84)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.pushBinaryOperation(SMTLIBStrategy.java:95)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.visit(SMTLIBStrategy.java:249)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Conjunction.accept(Conjunction.java:47)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.pushBinaryOperation(SMTLIBStrategy.java:92)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.visit(SMTLIBStrategy.java:302)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Implication.accept(Implication.java:47)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.pushQuantifier(SMTLIBStrategy.java:137)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.visit(SMTLIBStrategy.java:279)
at edu.kit.iti.formal.pse.worthwhile.model.ast.ForAllQuantifier.accept(ForAllQuantifier.java:48)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.pushQuantifier(SMTLIBStrategy.java:137)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.visit(SMTLIBStrategy.java:279)
at edu.kit.iti.formal.pse.worthwhile.model.ast.ForAllQuantifier.accept(ForAllQuantifier.java:48)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.pushUnaryOperation(SMTLIBStrategy.java:108)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.visit(SMTLIBStrategy.java:346)
at edu.kit.iti.formal.pse.worthwhile.model.ast.Negation.accept(Negation.java:47)
at edu.kit.iti.formal.pse.worthwhile.prover.SMTLIBStrategy.compileFormula(SMTLIBStrategy.java:60)
at edu.kit.iti.formal.pse.worthwhile.prover.StdProver.checkFormula(StdProver.java:54)
at edu.kit.iti.formal.pse.worthwhile.prover.Z3Prover.checkFormula(Z3Prover.java:1)
at edu.kit.iti.formal.pse.worthwhile.prover.SpecificationChecker.getValidity(SpecificationChecker.java:282)
at edu.kit.iti.formal.pse.worthwhile.prover.SpecificationChecker.checkProgram(SpecificationChecker.java:332)
at edu.kit.iti.formal.pse.worthwhile.ui.proving.WorthwhileProveJob.run(WorthwhileProveJob.java:81)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:54)
```