Mode | Name | Size | |
---|---|---|---|
-rw-r--r-- | function-applications-are-triggers.dfy | 569 | logplain |
-rw-r--r-- | function-applications-are-triggers.dfy.expect | 61 | logplain |
-rw-r--r-- | large-quantifiers-dont-break-dafny.dfy | 2059 | logplain |
-rw-r--r-- | large-quantifiers-dont-break-dafny.dfy.expect | 62 | logplain |
-rw-r--r-- | loop-detection-is-not-too-strict.dfy | 891 | logplain |
-rw-r--r-- | loop-detection-is-not-too-strict.dfy.expect | 242 | logplain |
-rw-r--r-- | nested-quantifiers-all-get-triggers.dfy | 359 | logplain |
-rw-r--r-- | nested-quantifiers-all-get-triggers.dfy.expect | 61 | logplain |
-rw-r--r-- | some-terms-do-not-look-like-the-triggers-they-match.dfy | 794 | logplain |
-rw-r--r-- | some-terms-do-not-look-like-the-triggers-they-match.dfy.expect | 742 | logplain |
-rw-r--r-- | splitting-triggers-yields-better-precondition-related-errors.dfy | 490 | logplain |
-rw-r--r-- | splitting-triggers-yields-better-precondition-related-errors.dfy.expect | 2159 | logplain |
-rw-r--r-- | triggers-prevent-some-inlining.dfy | 1064 | logplain |
-rw-r--r-- | triggers-prevent-some-inlining.dfy.expect | 61 | logplain |