blob: 7a99ea2dbd315d3801a789e491a5a7e90462f550 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// This file checks that loops between the range and the term of a quantifier
// are properly detected.
predicate P(x: int)
method M(x: int) {
// This will be flagged as a loop even without looking at the range
assert true || forall x: int | P(x) :: P(x+1);
// This requires checking the range for looping terms
assert true || forall x: int | P(x+1) :: P(x);
}
|