diff --git a/regression/smv/modules/self1.desc b/regression/smv/modules/self1.desc
new file mode 100644
index 000000000..de780717d
--- /dev/null
+++ b/regression/smv/modules/self1.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+self1.smv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This does not parse.
diff --git a/regression/smv/modules/self1.smv b/regression/smv/modules/self1.smv
new file mode 100644
index 000000000..1a6a715fe
--- /dev/null
+++ b/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;
diff --git a/regression/smv/modules/use_before_declaration1.desc b/regression/smv/modules/use_before_declaration1.desc
index 4355eca2a..6ca5dc549 100644
--- a/regression/smv/modules/use_before_declaration1.desc
+++ b/regression/smv/modules/use_before_declaration1.desc
@@ -1,5 +1,6 @@
-CORE
+CORE broken-smt-backend
 use_before_declaration1.smv
+
 ^EXIT=0$
 ^SIGNAL=0$
 --