From 5c3c88e4601882d61d7365ff2939229198feda9b Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 10 Nov 2025 15:59:17 -0800
Subject: [PATCH] SMV: KNOWNBUG test for module type checking

NuSMV defers module type checking until the module is instantiated.  Hence,
errors are tolerated if the module is not instantiated.
---
 regression/smv/modules/parameters2.desc | 9 +++++++++
 regression/smv/modules/parameters2.smv  | 9 +++++++++
 2 files changed, 18 insertions(+)
 create mode 100644 regression/smv/modules/parameters2.desc
 create mode 100644 regression/smv/modules/parameters2.smv

diff --git a/regression/smv/modules/parameters2.desc b/regression/smv/modules/parameters2.desc
new file mode 100644
index 000000000..18158a51a
--- /dev/null
+++ b/regression/smv/modules/parameters2.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+parameters2.smv
+
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This yields a type-checking error.
diff --git a/regression/smv/modules/parameters2.smv b/regression/smv/modules/parameters2.smv
new file mode 100644
index 000000000..c024deb9b
--- /dev/null
+++ b/regression/smv/modules/parameters2.smv
@@ -0,0 +1,9 @@
+MODULE main
+
+MODULE my-module(x)
+
+-- this is tolerated when the module is not instantiated
+CTLSPEC x + 1
+
+-- this, too
+CTLSPEC something_not_known_at_all