KNOWNBUG tests for LTL BMC

Author: kroening

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.

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)

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.

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)

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.

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