Merge pull request #901 from diffblue/smv-tests2

SMV: KNOWNBUG tests

Author: tautschnig

regression/smv/define/define1.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+define1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This yields a type error.

regression/smv/define/define1.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+DEFINE a := 1;
+
+VAR b : 1..4;
+ASSIGN next(b) := a + 1;

regression/smv/expressions/smv_if2.desc

@@ -0,0 +1,8 @@
+KNOWNBUG
+smv_if2.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This yields a type error.

regression/smv/expressions/smv_if2.smv

@@ -0,0 +1,8 @@
+MODULE main
+
+VAR input : boolean;
+
+VAR b : 1..4;
+
+ASSIGN init(b) := 1;
+ASSIGN next(b) := (input ? 1 : 3) + 1;

regression/smv/expressions/smv_set2.desc

@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_set2.smv
+--bdd
+^\[spec1\] x in my_set: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The smv_setin operator is not implemented.

regression/smv/expressions/smv_set2.smv

@@ -0,0 +1,9 @@
+MODULE main
+
+DEFINE my_set := {1, 2};
+
+VAR x : 1..3;
+ASSIGN init(x) := {1, 2, 3};
+       next(x) := x;
+
+SPEC x in my_set;