Merge pull request #276 from diffblue/k-induction-bugfix

ebmc: bugfix for k-induction

Author: tautschnig

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

@@ -3,6 +3,6 @@ k-induction3.v
 --module main --bound 9 --k-induction
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.property.p1] .* INCONCLUSIVE$
+^\[main.property.p1] .* REFUTED$
 --
 ^warning: ignoring

regression/ebmc/k-induction/k-induction3.v

@@ -6,6 +6,7 @@ initial a = 0;
 
 always @ (posedge clock) begin
   a = a+1;
+  // expected to be refuted with k >= 9
   assert p1: a!=10;
 end
 

regression/ebmc/k-induction/k-induction5.k-1.desc

@@ -1,11 +1,10 @@
-KNOWNBUG
+CORE
 k-induction5.v
 --module main --bound 1 --k-induction
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.property.property1\] .* PROVED$
-^\[main.property.property2\] .* INCONCLUSIVE$
+^\[main.property.property2\] .* REFUTED$
 --
 ^warning: ignoring
 --
-The result for property2 should be REFUTED.

regression/ebmc/k-induction/k-induction5.k-3.desc

@@ -4,8 +4,7 @@ k-induction5.v
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.property.property1\] .* PROVED$
-^\[main.property.property2\] .* PROVED$
+^\[main.property.property2\] .* REFUTED$
 --
 ^warning: ignoring
 --
-The result for property2 should be REFUTED.

src/ebmc/k_induction.cpp

@@ -173,6 +173,12 @@ int k_inductiont::induction_step()
        p_it.is_failure())
       continue;
 
+    // Do not run the step case for properties that have
+    // failed the base case already. Properties may pass the step
+    // case, but are still false when the base case fails.
+    if(p_it.is_refuted())
+      continue;
+
     auto solver_wrapper = solver_factory(ns, message.get_message_handler());
     auto &solver = solver_wrapper.decision_procedure();