KNOWNBUG test 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)