From 6a49d9941c1441db6217ab7c24d2494000fb9e8b Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 16 Jan 2025 14:21:41 -0800
Subject: [PATCH] BMC: return property_checker_resultt

bmc(...) now returns property_checker_resultt, instead of communicating the
result as a side-effect on the properties data structure.
---
 src/ebmc/bmc.cpp              | 10 +++++++---
 src/ebmc/bmc.h                |  6 +++---
 src/ebmc/k_induction.cpp      |  4 +++-
 src/ebmc/property_checker.cpp | 14 +++++++++-----
 4 files changed, 22 insertions(+), 12 deletions(-)

diff --git a/src/ebmc/bmc.cpp b/src/ebmc/bmc.cpp
index ebaa553a..ac60a981 100644
--- a/src/ebmc/bmc.cpp
+++ b/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)};
 }
diff --git a/src/ebmc/bmc.h b/src/ebmc/bmc.h
index 1cf51025..198a1629 100644
--- a/src/ebmc/bmc.h
+++ b/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 &);
 
diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp
index 756c0db9..43068d01 100644
--- a/src/ebmc/k_induction.cpp
+++ b/src/ebmc/k_induction.cpp
@@ -226,7 +226,7 @@ void k_inductiont::induction_base()
 {
   message.status() << "Induction Base" << messaget::eom;
 
-  bmc(
+  auto result = bmc(
     k,
     false, // convert_only
     false, // bmc_with_assumptions
@@ -234,6 +234,8 @@ void k_inductiont::induction_base()
     properties,
     solver_factory,
     message.get_message_handler());
+
+  properties.properties = std::move(result.properties);
 }
 
 /*******************************************************************\
diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp
index 833392ad..8b6bddae 100644
--- a/src/ebmc/property_checker.cpp
+++ b/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