Engine heuristic: fix for assumptions unsupported by k-induction

The k-induction engine now correctly reports unsupported assumptions, and is
then skipped by the engine selection heuristic.

Fixes #921.

Author: kroening

regression/ebmc/engine-heuristic/basic1.desc

@@ -0,0 +1,10 @@
+CORE
+basic1.sv
+
+^\[main\.a0\] always not s_eventually !main\.x: ASSUMED$
+^\[main\.p0\] always main\.x: PROVED up to bound 5$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/engine-heuristic/basic1.sv

@@ -0,0 +1,8 @@
+module main(input clk, input x);
+
+  // not supported by k-induction
+  a0: assume property (not s_eventually !x);
+
+  p0: assert property (x);
+
+endmodule

regression/ebmc/engine-heuristic/basic2.desc

@@ -0,0 +1,11 @@
+CORE
+basic2.sv
+
+^\[main\.a0\] always not s_eventually !main\.y: UNSUPPORTED: unsupported by k-induction$
+^\[main\.a1\] always !main\.x: ASSUMED$
+^\[main\.p0\] always !main\.z: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/engine-heuristic/basic2.sv

@@ -0,0 +1,15 @@
+module main(input clk, input x, input y);
+
+  reg z = 0;
+  always_ff @(posedge clk) z <= z || x;
+
+  // unsupported assumption
+  a0: assume property (not s_eventually !y);
+
+  // supported assumption
+  a1: assume property (!x);
+
+  // inductive property
+  p0: assert property (!z);
+
+endmodule

regression/ebmc/k-induction/k-induction-unsupported2.desc

@@ -3,7 +3,7 @@ k-induction-unsupported2.sv
 --module main --k-induction
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.p0\] always s_eventually main\.x == 10: FAILURE: property unsupported by k-induction$
+^\[main\.p0\] always s_eventually main\.x == 10: UNSUPPORTED: unsupported by k-induction$
 ^\[main\.p1\] always main\.x <= 10: PROVED$
 --
 ^warning: ignoring

regression/ebmc/k-induction/k-induction6.desc

@@ -1,9 +1,10 @@
-KNOWNBUG
+CORE
 k-induction6.sv
-
+--k-induction
+^\[main\.a0\] always not s_eventually !main\.x: UNSUPPORTED: unsupported by k-induction$
+^\[main\.p0\] always main\.x: INCONCLUSIVE$
 ^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The property should hold, but is reported as refuted.

regression/ebmc/k-induction/k-induction7.desc

@@ -0,0 +1,11 @@
+CORE
+k-induction7.sv
+--k-induction
+^\[main\.a0\] always not s_eventually !main\.y: UNSUPPORTED: unsupported by k-induction$
+^\[main\.a1\] always !main\.x: ASSUMED$
+^\[main\.p0\] always !main\.z: PROVED$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/ebmc/k-induction/k-induction7.sv

@@ -0,0 +1,15 @@
+module main(input clk, input x, input y);
+
+  reg z = 0;
+  always_ff @(posedge clk) z <= z || x;
+
+  // unsupported assumption
+  a0: assume property (not s_eventually !y);
+
+  // supported assumption
+  a1: assume property (!x);
+
+  // inductive property
+  p0: assert property (!z);
+
+endmodule

regression/smv/LTL/smv_ltlspec6.desc

@@ -1,7 +1,7 @@
 CORE
 smv_ltlspec6.smv
 
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring

src/ebmc/bdd_engine.cpp

@@ -180,7 +180,7 @@ property_checker_resultt bdd_enginet::operator()()
   try
   {
     // any properties left?
-    if(!properties.has_unknown_property())
+    if(!properties.has_unfinished_property())
       return property_checker_resultt{properties};
 
     // possibly apply liveness-to-safety