Merge pull request #940 from diffblue/k-induction-property-checker-result

`k_induction(...)` now returns `property_checker_resultt`

Author: tautschnig

src/ebmc/k_induction.cpp

@@ -94,15 +94,20 @@ Function: k_induction
 
 \*******************************************************************/
 
-void k_induction(
+property_checker_resultt k_induction(
   std::size_t k,
   const transition_systemt &transition_system,
-  ebmc_propertiest &properties,
+  const ebmc_propertiest &properties,
   const ebmc_solver_factoryt &solver_factory,
   message_handlert &message_handler)
 {
+  // copy
+  auto properties_copy = properties;
+
   k_inductiont(
-    k, transition_system, properties, solver_factory, message_handler)();
+    k, transition_system, properties_copy, solver_factory, message_handler)();
+
+  return property_checker_resultt{properties_copy};
 }
 
 /*******************************************************************\
@@ -150,10 +155,8 @@ property_checker_resultt k_induction(
 
   auto solver_factory = ebmc_solver_factory(cmdline);
 
-  k_induction(
+  return k_induction(
     k, transition_system, properties, solver_factory, message_handler);
-
-  return property_checker_resultt{properties};
 }
 
 /*******************************************************************\

src/ebmc/k_induction.h

@@ -18,17 +18,17 @@ Author: Daniel Kroening, [email protected]
 class transition_systemt;
 class ebmc_propertiest;
 
-property_checker_resultt k_induction(
+[[nodiscard]] property_checker_resultt k_induction(
   const cmdlinet &,
   transition_systemt &,
   ebmc_propertiest &,
   message_handlert &);
 
-// Basic k-induction. The result is stored in the ebmc_propertiest argument.
-void k_induction(
+// Basic k-induction, for given k and given solver.
+[[nodiscard]] property_checker_resultt k_induction(
   std::size_t k,
   const transition_systemt &,
-  ebmc_propertiest &,
+  const ebmc_propertiest &,
   const ebmc_solver_factoryt &,
   message_handlert &);
 

src/ebmc/property_checker.cpp

@@ -383,11 +383,13 @@ property_checker_resultt engine_heuristic(
   // First try 1-induction, word-level
   message.status() << "Attempting 1-induction" << messaget::eom;
 
-  k_induction(
+  auto k_induction_result = k_induction(
     1, transition_system, properties, solver_factory, message_handler);
 
+  properties.properties = k_induction_result.properties;
+
   if(!properties.has_unfinished_property())
-    return property_checker_resultt{properties}; // done
+    return k_induction_result; // done
 
   properties.reset_failure();
   properties.reset_inconclusive();