From b203ceac65e428296019513779f0ea875e00faef Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 11 Dec 2025 11:53:20 -0800
Subject: [PATCH] SMV: test for next(...) in rhs of ASSIGN next(...)

---
 regression/smv/next/assign_next1.desc |  7 +++++++
 regression/smv/next/assign_next1.smv  | 11 +++++++++++
 2 files changed, 18 insertions(+)
 create mode 100644 regression/smv/next/assign_next1.desc
 create mode 100644 regression/smv/next/assign_next1.smv

diff --git a/regression/smv/next/assign_next1.desc b/regression/smv/next/assign_next1.desc
new file mode 100644
index 000000000..3425a1c5b
--- /dev/null
+++ b/regression/smv/next/assign_next1.desc
@@ -0,0 +1,7 @@
+CORE
+assign_next1.smv
+
+^\[.*\] AG x = y: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/smv/next/assign_next1.smv b/regression/smv/next/assign_next1.smv
new file mode 100644
index 000000000..6df0b75d8
--- /dev/null
+++ b/regression/smv/next/assign_next1.smv
@@ -0,0 +1,11 @@
+MODULE main
+
+VAR x : boolean;
+    y : boolean;
+
+-- The use of next in a 'next' assignment is allowed.
+ASSIGN next(x) := next(y);
+
+ASSIGN init(x) := y;
+
+CTLSPEC AG x = y