Skip to content

Commit 495dc93

Browse files
committed
Add bad test for early return
1 parent 2f4c299 commit 495dc93

File tree

1 file changed

+11
-0
lines changed

1 file changed

+11
-0
lines changed

tests/early-return-bad.slang

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
method M(n: Int) : Int
2+
ensures n == 1 ==> result == 2
3+
ensures n != 1 ==> result == 3
4+
{
5+
match {
6+
n == 1 =>
7+
// @CheckError
8+
return 9
9+
};
10+
return 3
11+
}

0 commit comments

Comments
 (0)