SMV: test for next(...) in rhs of ASSIGN next(...)

Author: kroening

regression/smv/next/assign_next1.desc

@@ -0,0 +1,7 @@
+CORE
+assign_next1.smv
+
+^\[.*\] AG x = y: PROVED .*$
+^EXIT=0$
+^SIGNAL=0$
+--

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