1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
one-message-per-failed-precondition.dfy(13,3): Error BP5002: A precondition for this call might not hold.
one-message-per-failed-precondition.dfy(9,13): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
one-message-per-failed-precondition.dfy(13,3): Error BP5002: A precondition for this call might not hold.
one-message-per-failed-precondition.dfy(8,13): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
one-message-per-failed-precondition.dfy(20,27): Error: possible violation of function precondition
one-message-per-failed-precondition.dfy(18,13): Related location
Execution trace:
(0,0): anon0
(0,0): anon4_Else
one-message-per-failed-precondition.dfy(20,27): Error: possible violation of function precondition
one-message-per-failed-precondition.dfy(17,13): Related location
Execution trace:
(0,0): anon0
(0,0): anon4_Else
Dafny program verifier finished with 4 verified, 4 errors
|
