Skip to content

Commit f97f227

Browse files
committed
Add KNOWNBUG test for SMV ranges
1 parent 5aa449b commit f97f227

File tree

2 files changed

+22
-0
lines changed

2 files changed

+22
-0
lines changed
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
range_type6.smv
3+
--bound 10
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
--
8+
The result does not match the expected result.
Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
MODULE main
2+
VAR x:1..6;
3+
4+
ASSIGN
5+
init(x) := 1;
6+
7+
next(x) :=
8+
case
9+
x=1 : x+1;
10+
TRUE: 4;
11+
esac;
12+
13+
-- should fail
14+
LTLSPEC G x!=4

0 commit comments

Comments
 (0)