summaryrefslogtreecommitdiff
path: root/Test/triggers/looping-is-hard-to-decide-modulo-equality.dfy
Commit message (Collapse)AuthorAge
* Make `old` a special case for trigger generation.Gravatar Clément Pit--Claudel2015-08-21
Old is particular, because in old(g(f(x))), the triggers are old(g(x)) and old(f(x)). This has a number of implications; see the new tests files for more information.