From f9c5f6fac07b7bc5297aa8e570d9df598176b662 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 14 Sep 2025 21:03:31 -0700 Subject: [PATCH] k-induction: remove reduntant call to liveness_to_safety liveness_to_safety is already done in ebmc_parse_options, hence, there's no need to call it again in k_induction. --- src/ebmc/k_induction.cpp | 6 +----- src/ebmc/k_induction.h | 2 +- 2 files changed, 2 insertions(+), 6 deletions(-) diff --git a/src/ebmc/k_induction.cpp b/src/ebmc/k_induction.cpp index 9a3849336..a371d3e4e 100644 --- a/src/ebmc/k_induction.cpp +++ b/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)) diff --git a/src/ebmc/k_induction.h b/src/ebmc/k_induction.h index 528528ccb..2fabf6d58 100644 --- a/src/ebmc/k_induction.h +++ b/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 &);