Skip to content

Commit 4e403a8

Browse files
committed
Remove assert false from break tests
1 parent 8c2abc6 commit 4e403a8

File tree

2 files changed

+3
-8
lines changed

2 files changed

+3
-8
lines changed

tests/break-good.slang

Lines changed: 1 addition & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,5 @@ method client()
1212
};
1313
i := i - 1
1414
};
15-
assert i == 15;
16-
// @CheckError
17-
assert false
15+
assert i == 15
1816
}

tests/broke-bad.slang

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -4,19 +4,16 @@ method client()
44
loop
55
invariant i >= 15
66
invariant i <= 30
7-
// CheckError
87
invariant broke ==> i == 10
98
decreases i
109
{
1110
true =>
1211
match {
1312
i == 15 =>
1413
// @CheckError
15-
break
14+
break
1615
};
1716
i := i - 1
1817
};
19-
assert i == 15;
20-
// @CheckError
21-
assert false
18+
assert i == 15
2219
}

0 commit comments

Comments
 (0)