Test/triggers/splitting-triggers-recovers-expressivity.dfy.expect


1
2
3
4
5
6
7
8
9
10

splitting-triggers-recovers-expressivity.dfy(12,63): Error BP5003: A postcondition might not hold on this return path.
splitting-triggers-recovers-expressivity.dfy(12,10): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0
splitting-triggers-recovers-expressivity.dfy(19,15): Error BP5003: A postcondition might not hold on this return path.
splitting-triggers-recovers-expressivity.dfy(19,10): Related location: This is the postcondition that might not hold.
Execution trace:
    (0,0): anon0

Dafny program verifier finished with 14 verified, 2 errors