From ddecc8524347a0769ae425bb8738518f5b76025b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 3 Aug 2023 15:49:17 +0300
Subject: [PATCH] Move options from unassume bench to yaml confs

---
 conf/bench-yaml-validate.json  |  8 --------
 conf/bench-yaml.json           | 14 --------------
 conf/svcomp-yaml-validate.json | 13 +++++--------
 conf/svcomp-yaml.json          | 10 +++++++++-
 4 files changed, 14 insertions(+), 31 deletions(-)

diff --git a/conf/bench-yaml-validate.json b/conf/bench-yaml-validate.json
index ca830be08a..7b18371bd1 100644
--- a/conf/bench-yaml-validate.json
+++ b/conf/bench-yaml-validate.json
@@ -52,14 +52,6 @@
       "tokens": true
     }
   },
-  "witness": {
-    "enabled": false,
-    "invariant": {
-      "loop-head": true,
-      "after-lock": true,
-      "other": false
-    }
-  },
   "sem": {
     "unknown_function": {
       "invalidate": {
diff --git a/conf/bench-yaml.json b/conf/bench-yaml.json
index a24035fc9b..fd97b2c08c 100644
--- a/conf/bench-yaml.json
+++ b/conf/bench-yaml.json
@@ -48,20 +48,6 @@
       ]
     }
   },
-  "witness": {
-    "enabled": false,
-    "yaml": {
-      "enabled": true
-    },
-    "invariant": {
-      "exact": false,
-      "exclude-vars": [
-        "tmp\\(___[0-9]+\\)?",
-        "cond",
-        "RETURN"
-      ]
-    }
-  },
   "sem": {
     "unknown_function": {
       "invalidate": {
diff --git a/conf/svcomp-yaml-validate.json b/conf/svcomp-yaml-validate.json
index fc2ada7143..1934a56932 100644
--- a/conf/svcomp-yaml-validate.json
+++ b/conf/svcomp-yaml-validate.json
@@ -12,6 +12,10 @@
     "float": {
       "interval": true
     },
+    "apron": {
+      "domain": "polyhedra",
+      "strengthening": true
+    },
     "activated": [
       "base",
       "threadid",
@@ -31,6 +35,7 @@
       "region",
       "thread",
       "threadJoins",
+      "apron",
       "unassume"
     ],
     "context": {
@@ -74,14 +79,6 @@
   "exp": {
     "region-offsets": true
   },
-  "witness": {
-    "enabled": false,
-    "invariant": {
-      "loop-head": true,
-      "after-lock": false,
-      "other": true
-    }
-  },
   "solver": "td3",
   "sem": {
     "unknown_function": {
diff --git a/conf/svcomp-yaml.json b/conf/svcomp-yaml.json
index 6e3d0e4767..e09d1c80d7 100644
--- a/conf/svcomp-yaml.json
+++ b/conf/svcomp-yaml.json
@@ -12,6 +12,10 @@
     "float": {
       "interval": true
     },
+    "apron": {
+      "domain": "polyhedra",
+      "strengthening": true
+    },
     "activated": [
       "base",
       "threadid",
@@ -30,7 +34,8 @@
       "symb_locks",
       "region",
       "thread",
-      "threadJoins"
+      "threadJoins",
+      "apron"
     ],
     "context": {
       "widen": false
@@ -76,6 +81,9 @@
       "enabled": true
     },
     "invariant": {
+      "loop-head": true,
+      "other": false,
+      "accessed": false,
       "exact": false,
       "exclude-vars": [
         "tmp\\(___[0-9]+\\)?",