From f6e282b8f4cd941a87b81f19e692da71cad58a57 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 1 Nov 2025 14:58:18 -0700
Subject: [PATCH] SMV: test for complex identifiers

---
 regression/smv/identifiers/complex_identifier1.desc |  7 +++++++
 regression/smv/identifiers/complex_identifier1.smv  | 12 ++++++++++++
 2 files changed, 19 insertions(+)
 create mode 100644 regression/smv/identifiers/complex_identifier1.desc
 create mode 100644 regression/smv/identifiers/complex_identifier1.smv

diff --git a/regression/smv/identifiers/complex_identifier1.desc b/regression/smv/identifiers/complex_identifier1.desc
new file mode 100644
index 000000000..3d072e2a3
--- /dev/null
+++ b/regression/smv/identifiers/complex_identifier1.desc
@@ -0,0 +1,7 @@
+CORE
+complex_identifier1.smv
+
+^EXIT=10$
+^SIGNAL=0$
+--
+--
diff --git a/regression/smv/identifiers/complex_identifier1.smv b/regression/smv/identifiers/complex_identifier1.smv
new file mode 100644
index 000000000..348ca30f6
--- /dev/null
+++ b/regression/smv/identifiers/complex_identifier1.smv
@@ -0,0 +1,12 @@
+MODULE main
+
+-- complex identifiers can use '[...]' and '.'
+VAR some_var : boolean;
+VAR some_var[3] : boolean;
+VAR some_var[4].whatnot : boolean;
+VAR some_var[5][2].whatnot : boolean;
+
+INIT some_var[5][2].whatnot
+
+-- spaces are ok
+INIT some_var [4] . whatnot