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