k-induction does not support $past

k-induction requires instrumentation of $past.  This adds a removal step,
and a precondition that $past has been removed.

Author: kroening

CHANGELOG

@@ -11,6 +11,7 @@
 * SMV: abs, bool, count, max, min, toint, word1
 * BMC: new encoding for F, avoiding spurious traces
 * EBMC: verification results now have "result" verbosity level
+* Soundness fix for combination of $past and k-induction
 
 # EBMC 5.6
 

src/ebmc/instrument_past.cpp

@@ -30,12 +30,14 @@ void collect_past(const exprt &expr, past_sett &past_set)
   }
 }
 
-void collect_past(transition_systemt &transition_system, past_sett &past_set)
+void collect_past(
+  const transition_systemt &transition_system,
+  past_sett &past_set)
 {
   collect_past(transition_system.trans_expr, past_set);
 }
 
-void collect_past(ebmc_propertiest &properties, past_sett &past_set)
+void collect_past(const ebmc_propertiest &properties, past_sett &past_set)
 {
   for(auto &property : properties.properties)
   {
@@ -199,3 +201,14 @@ void instrument_past(
   instrument_past_model(past_map, transition_system);
   instrument_past_model(past_map, properties);
 }
+
+bool has_past(
+  const transition_systemt &transition_system,
+  const ebmc_propertiest &properties)
+{
+  past_sett past_set;
+  collect_past(transition_system, past_set);
+  collect_past(properties, past_set);
+
+  return !past_set.empty();
+}

src/ebmc/instrument_past.h

@@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
 #include "ebmc_properties.h"
 #include "transition_system.h"
 
+bool has_past(const transition_systemt &, const ebmc_propertiest &);
+
 void instrument_past(transition_systemt &, ebmc_propertiest &);
 
 #endif // EBMC_INSTRUMENT_PAST_H

src/ebmc/k_induction.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include "bmc.h"
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
+#include "instrument_past.h"
 #include "liveness_to_safety.h"
 
 #include <fstream>
@@ -185,6 +186,9 @@ Function: k_inductiont::operator()
 
 void k_inductiont::operator()()
 {
+  // check that $past is not present
+  PRECONDITION(!has_past(transition_system, properties));
+
   // Unsupported assumption? Mark as such.
   bool assumption_unsupported = false;
   for(auto &property : properties.properties)

src/ebmc/property_checker.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include "ebmc_error.h"
 #include "ebmc_solver_factory.h"
 #include "ic3_engine.h"
+#include "instrument_past.h"
 #include "k_induction.h"
 #include "netlist.h"
 #include "output_file.h"
@@ -461,6 +462,12 @@ property_checker_resultt property_checker(
                               !cmdline.isset("k-induction") &&
                               !cmdline.isset("ic3") && !cmdline.isset("bound");
 
+  if(cmdline.isset("k-induction") || use_heuristic_engine)
+  {
+    // The step case of k-induction can't do $past
+    instrument_past(transition_system, properties);
+  }
+
   auto result = [&]() -> property_checker_resultt
   {
     if(cmdline.isset("bdd") || cmdline.isset("show-bdds"))