KNOWNBUG test for SMV's self

Author: kroening

regression/smv/modules/self1.desc

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

regression/smv/modules/self1.smv

@@ -0,0 +1,16 @@
+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;