From e7658c5e85aa4b21d6611e74c18999bc649201b7 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 17 Jan 2025 10:21:00 -0800
Subject: [PATCH] k-induction(...) now returns property_checker_resultt

The k-induction(...) function now returns property_checker_resultt, instead
of using a side-effect on an argument passed by reference.
---
 src/ebmc/k_induction.cpp      | 15 +++++++++------
 src/ebmc/k_induction.h        |  8 ++++----
 src/ebmc/property_checker.cpp |  6 ++++--
 3 files changed, 17 insertions(+), 12 deletions(-)

diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp
index 43068d011..5720f4f16 100644
--- a/src/ebmc/k_induction.cpp
+++ b/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};
 }
 
 /*******************************************************************\
diff --git a/src/ebmc/k_induction.h b/src/ebmc/k_induction.h
index ffbec0043..528528ccb 100644
--- a/src/ebmc/k_induction.h
+++ b/src/ebmc/k_induction.h
@@ -18,17 +18,17 @@ Author: Daniel Kroening, kroening@kroening.com
 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 &);
 
diff --git a/src/ebmc/property_checker.cpp b/src/ebmc/property_checker.cpp
index c748f81ba..4f046e365 100644
--- a/src/ebmc/property_checker.cpp
+++ b/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();