FormulaTerm2.bpl(41,5): Error BP5001: This assertion might not hold.
Execution trace:
    FormulaTerm2.bpl(38,3): start
FormulaTerm2.bpl(49,5): Error BP5001: This assertion might not hold.
Execution trace:
    FormulaTerm2.bpl(47,3): start

Boogie program verifier finished with 2 verified, 2 errors