diff --git a/regression/smv/LTL/smv_ltlspec_F4.desc b/regression/smv/LTL/smv_ltlspec_F4.desc
new file mode 100644
index 000000000..33154fd01
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_F4.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_ltlspec_F4.smv
+--bound 3
+^\[spec1\] F \(some_input <-> X some_input\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BMC engine gives the wrong answer.
diff --git a/regression/smv/LTL/smv_ltlspec_F4.smv b/regression/smv/LTL/smv_ltlspec_F4.smv
new file mode 100644
index 000000000..7f16b5c60
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_F4.smv
@@ -0,0 +1,6 @@
+MODULE main
+
+VAR some_input : boolean;
+
+-- Expected to fail. The input can alternate infinitely often.
+LTLSPEC F (some_input <-> X some_input)
diff --git a/regression/smv/LTL/smv_ltlspec_F5.desc b/regression/smv/LTL/smv_ltlspec_F5.desc
new file mode 100644
index 000000000..952a884b6
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_F5.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_ltlspec_F5.smv
+--bound 3 --numbered-trace
+^\[spec1\] F \(!some_input \& X !some_input\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BMC engine gives the wrong answer.
diff --git a/regression/smv/LTL/smv_ltlspec_F5.smv b/regression/smv/LTL/smv_ltlspec_F5.smv
new file mode 100644
index 000000000..dd929f90a
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_F5.smv
@@ -0,0 +1,7 @@
+MODULE main
+
+VAR some_input : boolean;
+
+-- Expected to fail
+-- The shortest loop is FALSE, FALSE
+LTLSPEC F (!some_input & X !some_input)
diff --git a/regression/smv/LTL/smv_ltlspec_F6.desc b/regression/smv/LTL/smv_ltlspec_F6.desc
new file mode 100644
index 000000000..be862b8bc
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_F6.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+smv_ltlspec_F6.smv
+--bound 3 --numbered-trace
+^\[spec1\] F X some_input: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+The BMC engine gives the wrong answer.
diff --git a/regression/smv/LTL/smv_ltlspec_F6.smv b/regression/smv/LTL/smv_ltlspec_F6.smv
new file mode 100644
index 000000000..9ddd851eb
--- /dev/null
+++ b/regression/smv/LTL/smv_ltlspec_F6.smv
@@ -0,0 +1,6 @@
+MODULE main
+
+VAR some_input : boolean;
+
+-- Expected to fail
+LTLSPEC F X some_input