BMC: reconsider lasso-shaped encodings

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

regression/smv/LTL/smv_ltlspec_U3.smv

@@ -0,0 +1,6 @@
+MODULE main
+
+VAR x : boolean;
+
+-- should pass
+LTLSPEC (TRUE U x) -> F x

regression/smv/LTL/smv_ltlspec_or1.desc

@@ -6,3 +6,4 @@ smv_ltlspec_or1.smv
 ^SIGNAL=0$
 --
 ^warning: ignoring
+--

regression/smv/LTL/smv_ltlspec_or2.desc

@@ -0,0 +1,9 @@
+CORE
+smv_ltlspec_or2.smv
+--bound 10
+^\[spec1\] F z \| z V x: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/smv/LTL/smv_ltlspec_or2.smv

@@ -0,0 +1,11 @@
+MODULE main
+
+VAR x : boolean;
+
+VAR z : boolean;
+
+ASSIGN init(z) := FALSE;
+       next(z) := FALSE;
+
+-- should fail
+LTLSPEC (F z) | (z V x)

regression/verilog/SVA/sva_or1.bmc.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+sva_or1.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Wrong answer on ##[*]

regression/verilog/SVA/sva_or1.sv

@@ -0,0 +1,7 @@
+module main(input a);
+
+  initial p0: assert property ((s_eventually a) or (always !a));
+  initial p1: assert property ((s_eventually a) or not ##[*] a);
+  initial p2: assert property ((##[*] a) or (always !a));
+
+endmodule

src/smvlang/smv_typecheck.cpp

@@ -1940,9 +1940,13 @@ void smv_typecheckt::create_var_symbols(
       else
         symbol.pretty_name = strip_smv_prefix(symbol.name);
 
-      symbol.value = nil_exprt{};
-      symbol.is_input = true;
+      if(symbol.type.id() == "submodule")
+        symbol.is_input = false;
+      else
+        symbol.is_input = true;
+
       symbol.is_state_var = false;
+      symbol.value = nil_exprt{};
       symbol.location = item.expr.source_location();
 
       symbol_table.insert(std::move(symbol));