Skip to content

Commit f078be6

Browse files
committed
Add test for complex break paths
1 parent 495dc93 commit f078be6

File tree

1 file changed

+36
-0
lines changed

1 file changed

+36
-0
lines changed

tests/break-paths-complex.slang

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
method client(n: Int)
2+
{
3+
var i: Int := 30;
4+
var j: Int := i;
5+
loop
6+
invariant i >= 15
7+
invariant i <= 30
8+
decreases i
9+
{
10+
i == 15 =>
11+
match {
12+
n % 2 == 0 =>
13+
j := -1;
14+
break,
15+
n % 2 == 1 =>
16+
j := -2;
17+
break
18+
};
19+
i := i - 1,
20+
true =>
21+
i := i - 1
22+
};
23+
24+
match {
25+
n % 2 == 0 =>
26+
assert j == -1,
27+
n % 2 == 1 =>
28+
// This fails because j is actually -2
29+
// @CheckError
30+
assert j == -3,
31+
};
32+
33+
// this is reachable so should also fail
34+
// @CheckError
35+
assert false
36+
}

0 commit comments

Comments
 (0)