Merge pull request #1468 from diffblue/self1

KNOWNBUG test for SMV's `self`

Author: tautschnig

regression/smv/modules/self1.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+self1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This does not parse.

regression/smv/modules/self1.smv

@@ -0,0 +1,18 @@
+-- from the NuSMV 2.7 manual
+
+MODULE container(init_value1, init_value2)
+  VAR c1 : counter(init_value1, self);
+  VAR c2 : counter(init_value2, self);
+
+MODULE counter(init_value, my_container)
+  VAR v: 1..100;
+  ASSIGN
+     init(v) := init_value;
+  DEFINE
+     greatestCounterInContainer := v >= my_container.c1.v &
+                                   v >= my_container.c2.v;
+
+MODULE main
+  VAR c : container(14, 7);
+  SPEC
+    c.c1.greatestCounterInContainer;

regression/smv/modules/use_before_declaration1.desc

@@ -1,5 +1,6 @@
-CORE
+CORE broken-smt-backend
 use_before_declaration1.smv
+
 ^EXIT=0$
 ^SIGNAL=0$
 --