From 168a9aacc7f7900a4f930b639c74d14e443a2653 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 10 Dec 2025 08:19:27 -0800
Subject: [PATCH] KNOWNBUG test for trace of SMV model with module instances

---
 regression/smv/modules/trace1.desc | 21 +++++++++++++++++++++
 regression/smv/modules/trace1.smv  | 12 ++++++++++++
 2 files changed, 33 insertions(+)
 create mode 100644 regression/smv/modules/trace1.desc
 create mode 100644 regression/smv/modules/trace1.smv

diff --git a/regression/smv/modules/trace1.desc b/regression/smv/modules/trace1.desc
new file mode 100644
index 000000000..dc6c74754
--- /dev/null
+++ b/regression/smv/modules/trace1.desc
@@ -0,0 +1,21 @@
+KNOWNBUG
+trace1.smv
+--numbered-trace
+^\[.*\] AG \!a\.c\.d: REFUTED$
+^Counterexample with 2 states:$
+^b\.d@0 = FALSE$
+^a\.c\.d@0 = FALSE$
+^a\.c\.d@1 = TRUE$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+^a@0 = .*$
+^b@0 = .*$
+^a.c@0 = .*$
+^a@1 = .*$
+^b@1 = .*$
+^a.c@1 = .*$
+^b.d@1 = .*$
+--
+The trace contains entries for the module instances.
diff --git a/regression/smv/modules/trace1.smv b/regression/smv/modules/trace1.smv
new file mode 100644
index 000000000..601534f8d
--- /dev/null
+++ b/regression/smv/modules/trace1.smv
@@ -0,0 +1,12 @@
+MODULE main
+  VAR a : foo;
+  VAR b : moo;
+
+SPEC AG !a.c.d
+
+MODULE foo
+  VAR c : moo;
+
+MODULE moo
+  VAR d : boolean;
+  INIT d = FALSE