Skip to content

Commit ff4b7fd

Browse files
committed
Add tests to make sure different preconditions affect each other
1 parent 306ebd3 commit ff4b7fd

File tree

2 files changed

+23
-0
lines changed

2 files changed

+23
-0
lines changed
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
method a(n: Int)
2+
requires n >= 0
3+
{
4+
assert true
5+
}
6+
7+
method b(n: Int)
8+
requires n < 0
9+
{
10+
// @CheckError
11+
assert false
12+
}
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
method a(n: Int)
2+
requires n >= 0
3+
{
4+
assert true
5+
}
6+
7+
method b(n: Int)
8+
requires n < 0
9+
{
10+
assert true
11+
}

0 commit comments

Comments
 (0)