summaryrefslogtreecommitdiff
path: root/Test/triggers/loop-detection-is-not-too-strict.dfy
Commit message (Collapse)AuthorAge
* Further relax the loop detection conditionsGravatar Clément Pit--Claudel2015-08-27
| | | | | Mismatches are now allowed up to expressions not involving any of the bound variables of the quantifier under inspection.
* Add /printTooltips to trigger testsGravatar Clément Pit--Claudel2015-08-21
|
* Add tests for quantifier splitting and trigger generationGravatar Clément Pit--Claudel2015-08-19