From 895541d047b6ddd882a7f22fd6989b15afb238de Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 10 Dec 2025 07:56:40 -0800
Subject: [PATCH] KNOWNBUG test for SMV's self

Also fix pattern misuse in use_before_declaration1.desc.
---
 regression/smv/modules/self1.desc              |  9 +++++++++
 regression/smv/modules/self1.smv               | 18 ++++++++++++++++++
 .../smv/modules/use_before_declaration1.desc   |  3 ++-
 3 files changed, 29 insertions(+), 1 deletion(-)
 create mode 100644 regression/smv/modules/self1.desc
 create mode 100644 regression/smv/modules/self1.smv

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$
 --