Skip to content

Commit 8c2abc6

Browse files
committed
Add test for bad method variant
1 parent 5ae04b0 commit 8c2abc6

File tree

1 file changed

+17
-0
lines changed

1 file changed

+17
-0
lines changed

tests/method-variant-bad.slang

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
method sumn(n: Int): Int
2+
requires n >= 0
3+
ensures result == n * (n + 1)/2
4+
decreases n
5+
{
6+
var ret: Int;
7+
match {
8+
n == 0 =>
9+
ret := 0,
10+
true =>
11+
var res: Int;
12+
// @CheckError
13+
res := sumn(n + 1);
14+
ret := res + n
15+
};
16+
return ret
17+
}

0 commit comments

Comments
 (0)