From 9d8629dc30b557e319838070e260508d4def8cf5 Mon Sep 17 00:00:00 2001
From: Julian Erhard <julian.erhard@tum.de>
Date: Sun, 19 Nov 2023 16:57:56 +0100
Subject: [PATCH] Use autotune.activated termination as separate switch whether
 termination analysis should be activated (instead of using specification).

---
 conf/svcomp.json | 3 +--
 src/autoTune.ml  | 3 +++
 src/goblint.ml   | 2 +-
 3 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/conf/svcomp.json b/conf/svcomp.json
index cc6d1e303a..107c59994c 100644
--- a/conf/svcomp.json
+++ b/conf/svcomp.json
@@ -72,8 +72,7 @@
         "wideningThresholds",
         "loopUnrollHeuristic",
         "memsafetySpecification",
-        "termination",
-        "specification"
+        "termination"
       ]
     }
   },
diff --git a/src/autoTune.ml b/src/autoTune.ml
index 70f61d5172..346e9d7b6f 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -506,6 +506,9 @@ let isTerminationTask () = List.mem Svcomp.Specification.Termination (Svcomp.Spe
 let specificationIsActivated () =
   isActivated "specification" && get_string "ana.specification" <> ""
 
+let specificationTerminationIsActivated () =
+  isActivated "termination"
+
 let chooseConfig file =
   let factors = collectFactors visitCilFileSameGlobals file in
   let fileCompplexity = estimateComplexity factors file in
diff --git a/src/goblint.ml b/src/goblint.ml
index 9b95c95da4..25e809f9e9 100644
--- a/src/goblint.ml
+++ b/src/goblint.ml
@@ -39,7 +39,7 @@ let main () =
       print_endline GobSys.command_line;
     );
     (* When analyzing a termination specification, activate the termination analysis before pre-processing. *)
-    if get_bool "ana.autotune.enabled" && AutoTune.specificationIsActivated () then AutoTune.focusOnTermination ();
+    if get_bool "ana.autotune.enabled" && AutoTune.specificationTerminationIsActivated () then AutoTune.focusOnTermination ();
     let file = lazy (Fun.protect ~finally:GoblintDir.finalize preprocess_parse_merge) in
     if get_bool "server.enabled" then (
       let file =