diff --git a/regression/smv/next/next1.desc b/regression/smv/next/next1.desc
new file mode 100644
index 000000000..2ec6d6a88
--- /dev/null
+++ b/regression/smv/next/next1.desc
@@ -0,0 +1,8 @@
+CORE
+next1.smv
+--bdd
+^\[.*\] !x: PROVED$
+^\[.*\] AX x: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/smv/next/next1.smv b/regression/smv/next/next1.smv
new file mode 100644
index 000000000..9dc12ffe1
--- /dev/null
+++ b/regression/smv/next/next1.smv
@@ -0,0 +1,9 @@
+MODULE main
+
+VAR x : boolean;
+
+INIT !x
+TRANS next(x)
+
+CTLSPEC !x
+CTLSPEC AX x
diff --git a/regression/smv/next/next2.desc b/regression/smv/next/next2.desc
new file mode 100644
index 000000000..2234cbe02
--- /dev/null
+++ b/regression/smv/next/next2.desc
@@ -0,0 +1,7 @@
+CORE
+next2.smv
+--bdd
+^\[.*\] AX x <-> !x: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/smv/next/next2.smv b/regression/smv/next/next2.smv
new file mode 100644
index 000000000..8a8478e74
--- /dev/null
+++ b/regression/smv/next/next2.smv
@@ -0,0 +1,7 @@
+MODULE main
+
+VAR x : boolean;
+
+TRANS next(x)=!x
+
+CTLSPEC (AX x) <-> !x
diff --git a/regression/smv/next/next3.desc b/regression/smv/next/next3.desc
new file mode 100644
index 000000000..1411cf908
--- /dev/null
+++ b/regression/smv/next/next3.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+next3.smv
+--bdd
+^\[.*\] AX x <-> !x: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The BDD engine gives the wrong answer.
diff --git a/regression/smv/next/next3.smv b/regression/smv/next/next3.smv
new file mode 100644
index 000000000..d71b4f3a1
--- /dev/null
+++ b/regression/smv/next/next3.smv
@@ -0,0 +1,7 @@
+MODULE main
+
+VAR x : boolean;
+
+TRANS next(!x)=x
+
+CTLSPEC (AX x) <-> !x