Skip to content

Commit 94fa46a

Browse files
authored
Merge pull request #1536 from diffblue/assign_set2
KNOWNBUG test for nondeterministic definition of variable
2 parents 81220a2 + 6c8cc5a commit 94fa46a

File tree

2 files changed

+17
-0
lines changed

2 files changed

+17
-0
lines changed
Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
KNOWNBUG
2+
assign_set2.smv
3+
--bdd
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
--
8+
This does not type check.
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
MODULE main
2+
3+
VAR x : 0..6;
4+
5+
-- this is a nondeterministic choice
6+
ASSIGN x := { 1, 4 };
7+
8+
SPEC AG x != 2
9+
SPEC EX x = 1

0 commit comments

Comments
 (0)