Merge pull request #1263 from diffblue/k_induction_liveness_to_safety

k-induction: remove redundant call to liveness_to_safety

Author: tautschnig

src/ebmc/k_induction.cpp

@@ -140,7 +140,7 @@ Function: k_induction
 
 property_checker_resultt k_induction(
   const cmdlinet &cmdline,
-  transition_systemt &transition_system,
+  const transition_systemt &transition_system,
   ebmc_propertiest &properties,
   message_handlert &message_handler)
 {
@@ -158,10 +158,6 @@ property_checker_resultt k_induction(
   if(properties.properties.empty())
     throw ebmc_errort() << "no properties";
 
-  // liveness to safety translation, if requested
-  if(cmdline.isset("liveness-to-safety"))
-    liveness_to_safety(transition_system, properties);
-
   // Are there any properties suitable for k-induction?
   // Fail early if not.
   if(!k_inductiont::have_supported_property(properties.properties))

src/ebmc/k_induction.h

@@ -20,7 +20,7 @@ class ebmc_propertiest;
 
 [[nodiscard]] property_checker_resultt k_induction(
   const cmdlinet &,
-  transition_systemt &,
+  const transition_systemt &,
   ebmc_propertiest &,
   message_handlert &);