Skip to content

Commit f457b5e

Browse files
authored
Merge pull request #892 from diffblue/range_type7
SMV: two tests for range types
2 parents 35fdabf + e89a6ed commit f457b5e

File tree

4 files changed

+45
-0
lines changed

4 files changed

+45
-0
lines changed
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE broken-smt-backend
2+
range_type7.smv
3+
--bound 5
4+
^\[spec1\] G x != 1: REFUTED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
--
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) := 6;
6+
7+
next(x) :=
8+
case
9+
x!=1 : x - 1;
10+
TRUE: 1;
11+
esac;
12+
13+
-- should fail
14+
LTLSPEC G x!=1
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG broken-smt-backend
2+
range_type8.smv
3+
--bound 5
4+
^\[spec1\] G x != 1: REFUTED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
--
9+
We do not have type checking for unary minus.
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) := 6;
6+
7+
next(x) :=
8+
case
9+
x!=1 : x + -1; -- unary minus
10+
TRUE: 1;
11+
esac;
12+
13+
-- should fail
14+
LTLSPEC G x!=1

0 commit comments

Comments
 (0)