blob: 1ebc0bce80981732941cd7b56282ce437a7da5c4 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
loop-detection-messages--unit-tests.dfy(12,9): Warning: Selected triggers: {f(i)} (loops with {f(i + 1)})
(!) Suppressing loops would leave this expression without triggers.
loop-detection-messages--unit-tests.dfy(16,9): Warning: For expression {false ==> f(i) == f(i + 1)}:
Selected triggers: {f(i)} (loops with {f(i + 1)})
(!) Suppressing loops would leave this expression without triggers.
loop-detection-messages--unit-tests.dfy(20,9): Warning: (!) No terms found to trigger on.
loop-detection-messages--unit-tests.dfy(24,9): Warning: (!) No trigger covering all quantified variables found.
loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression {false ==> f(i) == f(i)}:
(!) No trigger covering all quantified variables found.
loop-detection-messages--unit-tests.dfy(26,9): Warning: For expression {false ==> g(j + 1) == 0}:
(!) No trigger covering all quantified variables found.
Dafny program verifier finished with 4 verified, 0 errors
|
