BMC: reconsider encoding of F

Author: kroening

regression/smv/LTL/smv_ltlspec_FG1.bmc.desc

@@ -1,7 +1,7 @@
 KNOWNBUG
 smv_ltlspec_FG1.smv
---bound 2
-^\[spec1\] F G x!=1: PROVED$
+--bound 3
+^\[spec1\] F G x != 1: PROVED up to bound 3$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/smv/LTL/smv_ltlspec_FG1.smv

@@ -10,4 +10,8 @@ TRANS x=1 -> next(x)=2
 
 TRANS x=2 -> next(x)=2
 
+-- This should pass.
+-- There are traces of two kinds:
+-- 0, 0, 0, ...
+-- 0, ..., 0, 1, 2, 2, ...
 LTLSPEC F G x!=1

regression/smv/LTL/smv_ltlspec_or1.desc

@@ -1,8 +1,10 @@
-CORE
+KNOWNBUG
 smv_ltlspec_or1.smv
 --bound 10
 ^\[spec1\] F !x \| G x: PROVED up to bound 10$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
+--
+The BMC engine gives the wrong answer.