BMC: reconsider lasso-shaped encodings

This replaces the lasso-shaped encodings in the word-level BMC property
encoding.  The lasso and straigth-line encodings are now built as separate
obligations.  In the lasso encoding, all operators follow the same lasso
shape.  This avoids spurious traces where the eventually operator follows
the lasso but a safety part of the property does not.

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
+--