1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
old-is-a-special-case-for-triggers.dfy(15,10): Info: Selected triggers:
{old(f(c))}, {c in sc}
old-is-a-special-case-for-triggers.dfy(20,10): Info: Selected triggers:
{old(f(f(c)))}, {f(c)}, {c in sc}
Rejected triggers: {old(f(c))} (may loop with "old(f(f(c)))")
old-is-a-special-case-for-triggers.dfy(21,10): Info: Selected triggers:
{f(g(c))}, {g(f(c))}, {old(f(g(c)))}, {old(g(f(c)))}, {old(f(f(c)))}, {c in sc}
Rejected triggers:
{g(c)} (may loop with "g(f(c))")
{f(c)} (may loop with "f(g(c))")
{old(g(c))} (may loop with "old(g(f(c)))")
{old(f(c))} (may loop with "old(f(f(c)))", "old(f(g(c)))")
old-is-a-special-case-for-triggers.dfy(25,10): Info: Selected triggers:
{old(f(c))}, {f(c)}, {c in sc}
Rejected triggers: {old(g(f(c)))} (more specific than {old(f(c))})
old-is-a-special-case-for-triggers.dfy(26,10): Info: Selected triggers:
{old(f(c))}, {f(c)}, {c in sc}
Rejected triggers:
{g(f(c))} (more specific than {f(c)})
{old(g(f(c)))} (more specific than {old(f(c))})
Dafny program verifier finished with 5 verified, 0 errors
|
