summaryrefslogtreecommitdiff
path: root/Test/triggers
Commit message (Expand)AuthorAge
* Renamed identifiers for increased geopolitical appealGravatar Rustan Leino2016-02-08
* In method and iterator specifications, inline top-level predicates (exceptGravatar leino2015-10-24
* Implement {:nowarn}, clarify some messages, and add a few testsGravatar Clément Pit--Claudel2015-08-28
* Add a small test from the IronClad notebookGravatar Clément Pit--Claudel2015-08-27
* Further relax the loop detection conditionsGravatar Clément Pit--Claudel2015-08-27
* Small fix: there is no loop in (forall x :: Q(x) && Q(0))Gravatar Clément Pit--Claudel2015-08-27
* Improve the redundancy detection algorithm used while constructing sets of termsGravatar Clément Pit--Claudel2015-08-26
* s/loops with/may loop with/Gravatar Clément Pit--Claudel2015-08-23
* Make quantifier splitting a two step processGravatar Clément Pit--Claudel2015-08-23
* Improve error reporting for split quantifiersGravatar Clément Pit--Claudel2015-08-23
* Allow MultiSelectExpr as quantifier headsGravatar Clément Pit--Claudel2015-08-23
* Look at the full quantifier to find loops, not just the term.Gravatar Clément Pit--Claudel2015-08-22
* Make `old` a special case for trigger generation.Gravatar Clément Pit--Claudel2015-08-21
* Rephrase the message about triggers being rejected because they are too strongGravatar Clément Pit--Claudel2015-08-21
* Adjust WF checks to use unsplit quantifiers.Gravatar Clément Pit--Claudel2015-08-21
* Add tests for display expressions used as triggersGravatar Clément Pit--Claudel2015-08-21
* Add /printTooltips to trigger testsGravatar Clément Pit--Claudel2015-08-21
* Fix a typoGravatar Clément Pit--Claudel2015-08-20
* Implement the SelectTrigger method, removing redundant triggers.Gravatar Clément Pit--Claudel2015-08-20
* Add unit tests for trigger-related error messagesGravatar Clément Pit--Claudel2015-08-20
* Simplify error reporting in the trigger generator to get cleaner messagesGravatar Clément Pit--Claudel2015-08-20
* Add a test to show how trigger splitting balances the downsides of loop detec...Gravatar Clément Pit--Claudel2015-08-20
* Add tests for quantifier splitting and trigger generationGravatar Clément Pit--Claudel2015-08-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 20:38:31 +0000