From aad465cf1803bc9ee0d10373e90397e4f0809321 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 10 Nov 2023 19:33:35 +0100
Subject: [PATCH] Autotune for Termination

---
 src/autoTune.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/autoTune.ml b/src/autoTune.ml
index 8300241bac..c756b17eb2 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -243,7 +243,14 @@ let focusOnSpecification (spec: Svcomp.Specification.t) =
   | NoDataRace -> (*enable all thread analyses*)
     print_endline @@ "Specification: NoDataRace -> enabling thread analyses \"" ^ (String.concat ", " notNeccessaryThreadAnalyses) ^ "\"";
     enableAnalyses notNeccessaryThreadAnalyses;
-  | Termination -> ()
+  | Termination -> 
+    let terminationAnas = ["termination"; "isEverMultiThreaded"; "apron"] in
+    print_endline @@ "Specification: Termination -> enabling termination analyses \"" ^ (String.concat ", " terminationAnas) ^ "\"";
+    enableAnalyses terminationAnas;
+    set_string "sem.int.signed_overflow" "assume_none";
+    set_bool "ana.int.interval" true;
+    set_string "ana.apron.domain" "polyhedra"; (* TODO: Needed? *)
+    ()
   | NoOverflow -> (*We focus on integer analysis*)
     set_bool "ana.int.def_exc" true;
     set_bool "ana.int.interval" true