summaryrefslogtreecommitdiff
path: root/Test/test2/FormulaTerm.bpl.expect
blob: 70fe60b33cd9b3c4d0280576307d97e13b49493d (plain)
1
2
3
4
5
6
FormulaTerm.bpl(12,3): Error BP5003: A postcondition might not hold on this return path.
FormulaTerm.bpl(6,3): Related location: This is the postcondition that might not hold.
Execution trace:
    FormulaTerm.bpl(10,1): start

Boogie program verifier finished with 11 verified, 1 error