summaryrefslogtreecommitdiff
path: root/Test/triggers
ModeNameSize
-rw-r--r--auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy979logplain
-rw-r--r--auto-triggers-fix-an-issue-listed-in-the-ironclad-notebook.dfy.expect213logplain
-rw-r--r--constructors-cause-matching-loops.dfy351logplain
-rw-r--r--constructors-cause-matching-loops.dfy.expect251logplain
-rw-r--r--function-applications-are-triggers.dfy583logplain
-rw-r--r--function-applications-are-triggers.dfy.expect687logplain
-rw-r--r--large-quantifiers-dont-break-dafny.dfy2074logplain
-rw-r--r--large-quantifiers-dont-break-dafny.dfy.expect627logplain
-rw-r--r--loop-detection-is-not-too-strict.dfy1834logplain
-rw-r--r--loop-detection-is-not-too-strict.dfy.expect1116logplain
-rw-r--r--loop-detection-looks-at-ranges-too.dfy524logplain
-rw-r--r--loop-detection-looks-at-ranges-too.dfy.expect421logplain
-rw-r--r--loop-detection-messages--unit-tests.dfy1254logplain
-rw-r--r--loop-detection-messages--unit-tests.dfy.expect3014logplain
-rw-r--r--looping-is-hard-to-decide-modulo-equality.dfy1246logplain
-rw-r--r--looping-is-hard-to-decide-modulo-equality.dfy.expect571logplain
-rw-r--r--matrix-accesses-are-triggers.dfy372logplain
-rw-r--r--matrix-accesses-are-triggers.dfy.expect496logplain
-rw-r--r--nested-quantifiers-all-get-triggers.dfy374logplain
-rw-r--r--nested-quantifiers-all-get-triggers.dfy.expect225logplain
-rw-r--r--old-is-a-special-case-for-triggers.dfy1489logplain
-rw-r--r--old-is-a-special-case-for-triggers.dfy.expect1098logplain
-rw-r--r--redundancy-detection-is-bidirectional.dfy1133logplain
-rw-r--r--redundancy-detection-is-bidirectional.dfy.expect795logplain
-rw-r--r--regression-tests.dfy716logplain
-rw-r--r--regression-tests.dfy.expect133logplain
-rw-r--r--set-construction-is-a-good-trigger.dfy657logplain
-rw-r--r--set-construction-is-a-good-trigger.dfy.expect304logplain
-rw-r--r--some-proofs-only-work-without-autoTriggers.dfy2007logplain
-rw-r--r--some-proofs-only-work-without-autoTriggers.dfy.expect1276logplain
-rw-r--r--some-terms-do-not-look-like-the-triggers-they-match.dfy809logplain
-rw-r--r--some-terms-do-not-look-like-the-triggers-they-match.dfy.expect750logplain
-rw-r--r--splitting-picks-the-right-tokens.dfy745logplain
-rw-r--r--splitting-picks-the-right-tokens.dfy.expect2084logplain
-rw-r--r--splitting-triggers-recovers-expressivity.dfy1778logplain
-rw-r--r--splitting-triggers-recovers-expressivity.dfy.expect2253logplain
-rw-r--r--splitting-triggers-yields-better-precondition-related-errors.dfy505logplain
-rw-r--r--splitting-triggers-yields-better-precondition-related-errors.dfy.expect2159logplain
-rw-r--r--suppressing-warnings-behaves-properly.dfy808logplain
-rw-r--r--suppressing-warnings-behaves-properly.dfy.expect1509logplain
-rw-r--r--triggers-prevent-some-inlining.dfy1079logplain
-rw-r--r--triggers-prevent-some-inlining.dfy.expect765logplain
-rw-r--r--useless-triggers-are-removed.dfy930logplain
-rw-r--r--useless-triggers-are-removed.dfy.expect858logplain
-rw-r--r--wf-checks-use-the-original-quantifier.dfy1309logplain
-rw-r--r--wf-checks-use-the-original-quantifier.dfy.expect945logplain