BMC: reconsider encoding of F

Author: kroening

CHANGELOG

@@ -7,6 +7,7 @@
 * SystemVerilog: fix for |-> and |=> for empty matches
 * LTL/SVA to Buechi with --buechi
 * SMV: abs, bool, count, max, min, toint, word1
+* BMC: new encoding for F, avoiding spurious traces
 
 # EBMC 5.6
 

regression/smv/CTL/smv_ctlspec_AFAG1.bmc.desc

@@ -1,10 +1,9 @@
-KNOWNBUG
-smv_ltlspec_AFAG1.smv
---bound 3
-^\[spec1\] AF AG !buechi_state: PROVED$
+CORE
+smv_ctlspec_AFAG1.smv
+--bound 10
+^\[spec1\] AF AG !buechi_state: PROVED up to bound 10$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The BMC engine returns the wrong answer.

regression/smv/LTL/smv_ltlspec_F4.desc

@@ -1,10 +1,9 @@
-KNOWNBUG
+CORE
 smv_ltlspec_F4.smv
---bound 3
+--bound 2
 ^\[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_F6.desc

@@ -1,10 +1,11 @@
-KNOWNBUG
+CORE
 smv_ltlspec_F6.smv
---bound 3 --numbered-trace
+--bound 1 --numbered-trace
 ^\[spec1\] F X some_input: REFUTED$
+^some_input@0 = FALSE$
+^some_input@1 = FALSE$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The BMC engine gives the wrong answer.

regression/smv/LTL/smv_ltlspec_FG1.bmc.desc

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

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_FX1.bdd.desc

@@ -0,0 +1,9 @@
+CORE
+smv_ltlspec_FX1.smv
+--bdd
+^\[spec1\] F X X p: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/smv/LTL/smv_ltlspec_FX1.bmc.desc

@@ -0,0 +1,9 @@
+CORE
+smv_ltlspec_FX1.smv
+--bound 1
+^\[spec1\] F X X p: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/smv/LTL/smv_ltlspec_FX1.smv

@@ -0,0 +1,7 @@
+MODULE main
+
+VAR p : boolean;
+
+-- This should fail for any bound >= 1.
+-- The shortest lasso is FALSE, FALSE, ...
+LTLSPEC F X X p

regression/smv/LTL/smv_ltlspec_U3.desc

@@ -0,0 +1,9 @@
+CORE
+smv_ltlspec_U3.smv
+--bound 5
+^\[.*\] TRUE U x -> F x: PROVED up to bound 5$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--