From 14bdc68bf99ce2df6a23a29d088252f5d926250d Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 10 Dec 2025 07:50:59 -0800
Subject: [PATCH] SMV: test for module instance as module argument

This adds a test from the SMV manual, in which a module instance is passed
as argument to another module.
---
 regression/smv/modules/module_argument1.desc |  8 ++++++++
 regression/smv/modules/module_argument1.smv  | 15 +++++++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 regression/smv/modules/module_argument1.desc
 create mode 100644 regression/smv/modules/module_argument1.smv

diff --git a/regression/smv/modules/module_argument1.desc b/regression/smv/modules/module_argument1.desc
new file mode 100644
index 000000000..7e6baa5ac
--- /dev/null
+++ b/regression/smv/modules/module_argument1.desc
@@ -0,0 +1,8 @@
+CORE
+module_argument1.smv
+
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/smv/modules/module_argument1.smv b/regression/smv/modules/module_argument1.smv
new file mode 100644
index 000000000..e046990d9
--- /dev/null
+++ b/regression/smv/modules/module_argument1.smv
@@ -0,0 +1,15 @@
+-- from the NuSMV 2.7 manual
+
+MODULE main
+ VAR
+  a : bar;
+  m : foo(a);
+
+MODULE bar
+ VAR
+  q : boolean;
+  p : boolean;
+
+MODULE foo(c)
+ DEFINE
+  flag := c.q | c.p;