diff --git a/regression/smv/CTL/smv_ctlspec_AFAG1.bdd.desc b/regression/smv/CTL/smv_ctlspec_AFAG1.bdd.desc
new file mode 100644
index 000000000..99a34b550
--- /dev/null
+++ b/regression/smv/CTL/smv_ctlspec_AFAG1.bdd.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_ltlspec_AFAG1.smv
+--bdd
+^\[spec1\] AF AG !buechi_state: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BDD engine returns the wrong answer.
diff --git a/regression/smv/CTL/smv_ctlspec_AFAG1.bmc.desc b/regression/smv/CTL/smv_ctlspec_AFAG1.bmc.desc
new file mode 100644
index 000000000..c9fb26586
--- /dev/null
+++ b/regression/smv/CTL/smv_ctlspec_AFAG1.bmc.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_ltlspec_AFAG1.smv
+--bound 3
+^\[spec1\] AF AG !buechi_state: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BMC engine returns the wrong answer.
diff --git a/regression/smv/CTL/smv_ctlspec_AFAG1.smv b/regression/smv/CTL/smv_ctlspec_AFAG1.smv
new file mode 100644
index 000000000..6a5a43efb
--- /dev/null
+++ b/regression/smv/CTL/smv_ctlspec_AFAG1.smv
@@ -0,0 +1,12 @@
+MODULE main
+
+VAR flag : boolean;
+VAR buechi_state : boolean;
+
+TRANS next(flag) = !flag
+
+TRANS !buechi_state & !next(buechi_state)
+    | !buechi_state & !flag & next(buechi_state)
+    | buechi_state  & flag  & next(buechi_state)
+
+CTLSPEC AF AG !buechi_state
diff --git a/regression/smv/LTL/smv_ltlspec_FG1.bdd.desc b/regression/smv/LTL/smv_ltlspec_FG1.bdd.desc
new file mode 100644
index 000000000..bff760c31
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_FG1.bdd.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_ltlspec_FG1.smv
+--bdd
+^\[spec1\] F G x!=1: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BDD engine returns the wrong answer.
diff --git a/regression/smv/LTL/smv_ltlspec_FG1.bmc.desc b/regression/smv/LTL/smv_ltlspec_FG1.bmc.desc
new file mode 100644
index 000000000..be44f81a8
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_FG1.bmc.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_ltlspec_FG1.smv
+--bound 2
+^\[spec1\] F G x!=1: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BMC engine returns the wrong answer.
diff --git a/regression/smv/LTL/smv_ltlspec_FG1.smv b/regression/smv/LTL/smv_ltlspec_FG1.smv
new file mode 100644
index 000000000..15da57962
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_FG1.smv
@@ -0,0 +1,13 @@
+MODULE main
+
+VAR x : 0..2;
+
+ASSIGN init(x) := 0;
+
+TRANS x=0 -> (next(x)=0 | next(x)=1)
+
+TRANS x=1 -> next(x)=2
+
+TRANS x=2 -> next(x)=2
+
+LTLSPEC F G x!=1