BMC: return property_checker_resultt

src/ebmc/bmc.cpp

@@ -191,17 +191,19 @@ void bmc_with_iterative_constraint_strengthening(
   }
 }
 
-void bmc(
+property_checker_resultt bmc(
   std::size_t bound,
   bool convert_only,
   bool bmc_with_assumptions,
   const transition_systemt &transition_system,
-  ebmc_propertiest &properties,
+  const ebmc_propertiest &properties_in,
   const ebmc_solver_factoryt &solver_factory,
   message_handlert &message_handler)
 {
-  messaget message(message_handler);
+  // copy
+  ebmc_propertiest properties = properties_in;
 
+  messaget message(message_handler);
   message.status() << "Generating Decision Problem" << messaget::eom;
 
   // convert the transition system
@@ -299,4 +301,6 @@ void bmc(
       << std::chrono::duration<double>(sat_stop_time - sat_start_time).count()
       << messaget::eom;
   }
+
+  return property_checker_resultt{std::move(properties)};
 }

src/ebmc/bmc.h

@@ -12,19 +12,19 @@ Author: Daniel Kroening, dkr@amazon.com
 #ifndef EBMC_BMC_H
 #define EBMC_BMC_H
 
-#include "ebmc_properties.h"
 #include "ebmc_solver_factory.h"
+#include "property_checker.h"
 
 class exprt;
 class transition_systemt;
 
 /// This is word-level BMC.
-void bmc(
+[[nodiscard]] property_checker_resultt bmc(
   std::size_t bound,
   bool convert_only,
   bool bmc_with_assumptions,
   const transition_systemt &,
-  ebmc_propertiest &,
+  const ebmc_propertiest &,
   const ebmc_solver_factoryt &,
   message_handlert &);
 

src/ebmc/k_induction.cpp

@@ -226,14 +226,16 @@ void k_inductiont::induction_base()
 {
   message.status() << "Induction Base" << messaget::eom;
 
-  bmc(
+  auto result = bmc(
     k,
     false, // convert_only
     false, // bmc_with_assumptions
     transition_system,
     properties,
     solver_factory,
     message.get_message_handler());
+
+  properties.properties = std::move(result.properties);
 }
 
 /*******************************************************************\

src/ebmc/property_checker.cpp

@@ -31,7 +31,7 @@ Author: Daniel Kroening, dkr@amazon.com
 property_checker_resultt word_level_bmc(
   const cmdlinet &cmdline,
   const transition_systemt &transition_system,
-  ebmc_propertiest &properties,
+  const ebmc_propertiest &properties,
   message_handlert &message_handler)
 {
   auto solver_factory = ebmc_solver_factory(cmdline);
@@ -61,6 +61,8 @@ property_checker_resultt word_level_bmc(
         result=finish_word_level_bmc(solver);
 #endif
       }
+
+      return property_checker_resultt{properties};
     }
     else
     {
@@ -83,7 +85,7 @@ property_checker_resultt word_level_bmc(
 
       bool bmc_with_assumptions = cmdline.isset("bmc-with-assumptions");
 
-      bmc(
+      auto result = bmc(
         bound,
         convert_only,
         bmc_with_assumptions,
@@ -94,6 +96,8 @@ property_checker_resultt word_level_bmc(
 
       if(convert_only)
         return property_checker_resultt::success();
+
+      return result;
     }
   }
 
@@ -115,8 +119,6 @@ property_checker_resultt word_level_bmc(
   {
     return property_checker_resultt::error();
   }
-
-  return property_checker_resultt{properties};
 }
 
 property_checker_resultt finish_bit_level_bmc(
@@ -394,7 +396,7 @@ property_checker_resultt engine_heuristic(
   // Now try BMC with bound 5, word-level
   message.status() << "Attempting BMC with bound 5" << messaget::eom;
 
-  bmc(
+  auto bmc_result = bmc(
     5,     // bound
     false, // convert_only
     cmdline.isset("bmc-with-assumptions"),
@@ -403,6 +405,8 @@ property_checker_resultt engine_heuristic(
     solver_factory,
     message_handler);
 
+  properties.properties = std::move(bmc_result.properties);
+
   if(!properties.has_unfinished_property())
     return property_checker_resultt{properties}; // done