Skip to content

Commit 926049e

Browse files
committed
Tests only: more tests with constraints and loops
1 parent 1ca0db5 commit 926049e

File tree

2 files changed

+53
-0
lines changed

2 files changed

+53
-0
lines changed
Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
// xfail-stage0
2+
// error-pattern: Unsatisfied precondition constraint (for example, even(y
3+
4+
fn print_even(int y) : even(y) {
5+
log y;
6+
}
7+
8+
pred even(int y) -> bool {
9+
true
10+
}
11+
12+
fn main() {
13+
14+
let int y = 42;
15+
check even(y);
16+
do {
17+
print_even(y);
18+
do {
19+
do {
20+
do {
21+
y += 1;
22+
} while (true);
23+
} while (true);
24+
} while (true);
25+
} while (true);
26+
}
Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
// xfail-stage0
2+
// error-pattern: Unsatisfied precondition constraint (for example, even(y
3+
4+
fn print_even(int y) : even(y) {
5+
log y;
6+
}
7+
8+
pred even(int y) -> bool {
9+
true
10+
}
11+
12+
fn main() {
13+
14+
let int y = 42;
15+
let int x = 1;
16+
check even(y);
17+
while (true) {
18+
print_even(y);
19+
while (true) {
20+
while (true) {
21+
while (true) {
22+
y += x;
23+
}
24+
}
25+
}
26+
}
27+
}

0 commit comments

Comments
 (0)