From 6131273c1c95bf762749aa7a6a857fec09603def Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 31 Oct 2023 16:10:14 +0200
Subject: [PATCH] Separate memsafetySpecification autotuner and enable in
 svcomp conf

Normal specification autotuner does other things we didn't want in SV-COMP.
---
 conf/svcomp.json                    | 3 ++-
 src/common/util/options.schema.json | 2 +-
 src/maingoblint.ml                  | 2 +-
 3 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/conf/svcomp.json b/conf/svcomp.json
index 913d43784b..342ac6f298 100644
--- a/conf/svcomp.json
+++ b/conf/svcomp.json
@@ -70,7 +70,8 @@
         "congruence",
         "octagon",
         "wideningThresholds",
-        "loopUnrollHeuristic"
+        "loopUnrollHeuristic",
+        "memsafetySpecification"
       ]
     }
   },
diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
index 400dde06dc..4d1b012701 100644
--- a/src/common/util/options.schema.json
+++ b/src/common/util/options.schema.json
@@ -544,7 +544,7 @@
               "type": "array",
               "items": { "type": "string" },
               "default": [
-                "congruence", "singleThreaded", "specification", "mallocWrappers", "noRecursiveIntervals", "enums", "loopUnrollHeuristic", "arrayDomain", "octagon", "wideningThresholds"
+                "congruence", "singleThreaded", "specification", "mallocWrappers", "noRecursiveIntervals", "enums", "loopUnrollHeuristic", "arrayDomain", "octagon", "wideningThresholds", "memsafetySpecification"
               ]
             }
           },
diff --git a/src/maingoblint.ml b/src/maingoblint.ml
index b5998df2d1..9e0b41fe3c 100644
--- a/src/maingoblint.ml
+++ b/src/maingoblint.ml
@@ -186,7 +186,7 @@ let handle_options () =
   check_arguments ();
   AfterConfig.run ();
   Sys.set_signal (GobSys.signal_of_string (get_string "dbg.solver-signal")) Signal_ignore; (* Ignore solver-signal before solving (e.g. MyCFG), otherwise exceptions self-signal the default, which crashes instead of printing backtrace. *)
-  if AutoTune.isActivated "specification" && get_string "ana.specification" <> "" then
+  if AutoTune.isActivated "memsafetySpecification" && get_string "ana.specification" <> "" then
     AutoTune.focusOnMemSafetySpecification ();
   Cilfacade.init_options ();
   handle_flags ()