diff --git a/src/autoTune.ml b/src/autoTune.ml
index d532081799..9e3508ccd2 100644
--- a/src/autoTune.ml
+++ b/src/autoTune.ml
@@ -226,6 +226,7 @@ let focusOnSpecification () =
   (* TODO: Finish these two below later *)
   | ValidDeref
   | ValidMemtrack -> ()
+  | MemorySafety -> () (* TODO: This is here for now just to complete the pattern match *)
 
 (*Detect enumerations and enable the "ana.int.enums" option*)
 exception EnumFound
diff --git a/src/witness/svcomp.ml b/src/witness/svcomp.ml
index f1ee18ed72..15d41c0210 100644
--- a/src/witness/svcomp.ml
+++ b/src/witness/svcomp.ml
@@ -55,6 +55,7 @@ struct
         | ValidFree -> "valid-free"
         | ValidDeref -> "valid-deref"
         | ValidMemtrack -> "valid-memtrack"
+        | MemorySafety -> "memory-safety" (* TODO: Currently here only to complete the pattern match *)
       in
       "false(" ^ result_spec ^ ")"
     | Unknown -> "unknown"
diff --git a/src/witness/svcompSpec.ml b/src/witness/svcompSpec.ml
index 8dafb8873c..f066610953 100644
--- a/src/witness/svcompSpec.ml
+++ b/src/witness/svcompSpec.ml
@@ -9,10 +9,11 @@ type t =
   | ValidFree
   | ValidDeref
   | ValidMemtrack
+  | MemorySafety (* Internal property for use in Goblint; serves as a summary for ValidFree, ValidDeref and ValidMemtrack *)
 
 let of_string s =
   let s = String.strip s in
-  let regexp = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )" in
+  let regexp = Str.regexp "CHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )\nCHECK( init(main()), LTL(G \\(.*\\)) )" in
   let regexp_negated = Str.regexp "CHECK( init(main()), LTL(G ! \\(.*\\)) )" in
   if Str.string_match regexp_negated s 0 then
     let global_not = Str.matched_group 1 s in
@@ -28,13 +29,17 @@ let of_string s =
       else
         failwith "Svcomp.Specification.of_string: unknown global not expression"
   else if Str.string_match regexp s 0 then
-    let global = Str.matched_group 1 s in
-    if global = "valid-free" then
+    let global1 = Str.matched_group 1 s in
+    let global2 = Str.matched_group 2 s in
+    let global3 = Str.matched_group 3 s in
+    if global1 = "valid-free" && global2 = "valid-deref" && global3 = "valid-memtrack" then
+      MemorySafety
+      (* if global = "valid-free" then
       ValidFree
     else if global = "valid-deref" then
       ValidDeref
     else if global = "valid-memtrack" then
-      ValidMemtrack
+          ValidMemtrack *)
     else
       failwith "Svcomp.Specification.of_string: unknown global expression"
   else
@@ -65,5 +70,6 @@ let to_string spec =
     | ValidFree -> "valid-free", false
     | ValidDeref -> "valid-deref", false
     | ValidMemtrack -> "valid-memtrack", false
+    | MemorySafety -> "memory-safety", false (* TODO: That's false, it's currently here just to complete the pattern match *)
   in
   print_output spec_str is_neg
diff --git a/src/witness/witness.ml b/src/witness/witness.ml
index 31034a2d9a..437ba187ae 100644
--- a/src/witness/witness.ml
+++ b/src/witness/witness.ml
@@ -505,8 +505,8 @@ struct
         in
         (module TaskResult:WitnessTaskResult)
       )
-    | ValidFree ->
-      let module TrivialArg =
+    | ValidFree (*->*)
+    (* let module TrivialArg =
       struct
         include Arg
         let next _ = []
@@ -534,9 +534,9 @@ struct
         end
         in
         (module TaskResult:WitnessTaskResult)
-      )
-    | ValidDeref ->
-      let module TrivialArg =
+        ) *)
+    | ValidDeref (*->*)
+    (* let module TrivialArg =
       struct
         include Arg
         let next _ = []
@@ -564,9 +564,9 @@ struct
         end
         in
         (module TaskResult:WitnessTaskResult)
-      )
-    | ValidMemtrack ->
-      let module TrivialArg =
+        ) *)
+    | ValidMemtrack (*->*)
+    (* let module TrivialArg =
       struct
         include Arg
         let next _ = []
@@ -583,6 +583,36 @@ struct
         end
         in
         (module TaskResult:WitnessTaskResult)
+        ) else (
+        let module TaskResult =
+        struct
+          module Arg = TrivialArg
+          let result = Result.Unknown
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
+        ) *)
+    | MemorySafety ->
+      let module TrivialArg =
+      struct
+        include Arg
+        let next _ = []
+      end
+      in
+      if not !AnalysisState.svcomp_may_invalid_free || not !AnalysisState.svcomp_may_invalid_deref || not !AnalysisState.svcomp_may_invalid_memtrack then (
+        let module TaskResult =
+        struct
+          module Arg = Arg
+          let result = Result.True
+          let invariant _ = Invariant.none
+          let is_violation _ = false
+          let is_sink _ = false
+        end
+        in
+        (module TaskResult:WitnessTaskResult)
       ) else (
         let module TaskResult =
         struct