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