Skip to content

Commit 41ff733

Browse files
committed
Add failing test for unbounded loop
1 parent bc628c0 commit 41ff733

File tree

1 file changed

+15
-0
lines changed

1 file changed

+15
-0
lines changed

tests/for-unbounded-bad.slang

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
method client(n: Int)
2+
requires n >= 0
3+
{
4+
var counter: Int := 0;
5+
for i in 0..n
6+
// @CheckError
7+
invariant counter == i
8+
{
9+
counter := counter + 1;
10+
match {
11+
i == 10 => counter := 0
12+
}
13+
};
14+
assert counter == n
15+
}

0 commit comments

Comments
 (0)