diff --git a/conf/malloc.json b/conf/malloc.json
new file mode 100644
index 00000000000..fad7c6258c1
--- /dev/null
+++ b/conf/malloc.json
@@ -0,0 +1,150 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true
+    },
+    "apron": {
+      "domain": "polyhedra"
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "memOutOfBounds"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+        "ldv_malloc",
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc",
+        "ldv_kzalloc"
+      ]
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": true,
+      "activated": [
+        "singleThreaded",
+        "mallocWrappers",
+        "noRecursiveIntervals",
+        "enums",
+        "congruence",
+        "octagon",
+        "wideningThresholds",
+        "loopUnrollHeuristic",
+        "memsafetySpecification",
+        "termination",
+        "tmpSpecialAnalysis"
+      ]
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true,
+      "exclude-vars": [
+        "tmp\\(___[0-9]+\\)?",
+        "cond",
+        "RETURN",
+        "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
+        ".*____CPAchecker_TMP_[0-9]+",
+        "__VERIFIER_assert__cond",
+        "__ksymtab_.*",
+        "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
+      ]
+    }
+  },
+  "pre": {
+    "enabled": false
+  },
+  "warn": {
+    "integer": false
+  }
+}
\ No newline at end of file
diff --git a/conf/relational-malloc-pointer_tracking b/conf/relational-malloc-pointer_tracking
new file mode 100644
index 00000000000..ae603f8856e
--- /dev/null
+++ b/conf/relational-malloc-pointer_tracking
@@ -0,0 +1,140 @@
+{
+    "ana": {
+        "sv-comp": {
+            "enabled": true,
+            "functions": true
+        },
+        "int": {
+            "def_exc": true,
+            "enums": false,
+            "interval": true
+        },
+        "float": {
+            "interval": true
+        },
+        "apron": {
+            "domain": "polyhedra",
+            "pointer_tracking": true
+        },
+        "activated": [
+            "base",
+            "threadid",
+            "threadflag",
+            "threadreturn",
+            "mallocWrapper",
+            "mutexEvents",
+            "mutex",
+            "access",
+            "race",
+            "escape",
+            "expRelation",
+            "mhp",
+            "assert",
+            "var_eq",
+            "symb_locks",
+            "region",
+            "thread",
+            "threadJoins",
+            "memOutOfBounds",
+            "taintPartialContexts",
+            "apron"
+        ],
+        "path_sens": [
+            "mutex",
+            "malloc_null",
+            "uninit",
+            "expsplit",
+            "activeSetjmp",
+            "memLeak",
+            "threadflag"
+        ],
+        "context": {
+            "widen": false
+        },
+        "malloc": {
+            "wrappers": [
+                "kmalloc",
+                "__kmalloc",
+                "usb_alloc_urb",
+                "__builtin_alloca",
+                "kzalloc",
+                "ldv_malloc",
+                "kzalloc_node",
+                "ldv_zalloc",
+                "kmalloc_array",
+                "kcalloc",
+                "ldv_xmalloc",
+                "ldv_xzalloc",
+                "ldv_calloc",
+                "ldv_kzalloc"
+            ]
+        },
+        "base": {
+            "arrays": {
+                "domain": "partitioned"
+            }
+        },
+        "race": {
+            "free": false,
+            "call": false
+        },
+        "autotune": {
+            "enabled": false
+        }
+    },
+    "exp": {
+        "region-offsets": true
+    },
+    "solver": "td3",
+    "sem": {
+        "unknown_function": {
+            "spawn": false
+        },
+        "int": {
+            "signed_overflow": "assume_none"
+        },
+        "null-pointer": {
+            "dereference": "assume_none"
+        }
+    },
+    "witness": {
+        "graphml": {
+            "enabled": true,
+            "id": "enumerate",
+            "unknown": false
+        },
+        "yaml": {
+            "enabled": true,
+            "format-version": "2.0",
+            "entry-types": [
+                "invariant_set"
+            ],
+            "invariant-types": [
+                "loop_invariant"
+            ]
+        },
+        "invariant": {
+            "loop-head": true,
+            "after-lock": false,
+            "other": false,
+            "accessed": false,
+            "exact": true,
+            "exclude-vars": [
+                "tmp\\(___[0-9]+\\)?",
+                "cond",
+                "RETURN",
+                "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
+                ".*____CPAchecker_TMP_[0-9]+",
+                "__VERIFIER_assert__cond",
+                "__ksymtab_.*",
+                "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
+            ]
+        }
+    },
+    "pre": {
+        "enabled": false
+    },
+    "warn": {
+        "integer": false
+    }
+}
\ No newline at end of file
diff --git a/conf/relational-malloc.json b/conf/relational-malloc.json
new file mode 100644
index 00000000000..6f0dda978fe
--- /dev/null
+++ b/conf/relational-malloc.json
@@ -0,0 +1,139 @@
+{
+  "ana": {
+    "sv-comp": {
+      "enabled": true,
+      "functions": true
+    },
+    "int": {
+      "def_exc": true,
+      "enums": false,
+      "interval": true
+    },
+    "float": {
+      "interval": true
+    },
+    "apron": {
+      "domain": "polyhedra"
+    },
+    "activated": [
+      "base",
+      "threadid",
+      "threadflag",
+      "threadreturn",
+      "mallocWrapper",
+      "mutexEvents",
+      "mutex",
+      "access",
+      "race",
+      "escape",
+      "expRelation",
+      "mhp",
+      "assert",
+      "var_eq",
+      "symb_locks",
+      "region",
+      "thread",
+      "threadJoins",
+      "memOutOfBounds",
+      "taintPartialContexts",
+      "apron"
+    ],
+    "path_sens": [
+      "mutex",
+      "malloc_null",
+      "uninit",
+      "expsplit",
+      "activeSetjmp",
+      "memLeak",
+      "threadflag"
+    ],
+    "context": {
+      "widen": false
+    },
+    "malloc": {
+      "wrappers": [
+        "kmalloc",
+        "__kmalloc",
+        "usb_alloc_urb",
+        "__builtin_alloca",
+        "kzalloc",
+        "ldv_malloc",
+        "kzalloc_node",
+        "ldv_zalloc",
+        "kmalloc_array",
+        "kcalloc",
+        "ldv_xmalloc",
+        "ldv_xzalloc",
+        "ldv_calloc",
+        "ldv_kzalloc"
+      ]
+    },
+    "base": {
+      "arrays": {
+        "domain": "partitioned"
+      }
+    },
+    "race": {
+      "free": false,
+      "call": false
+    },
+    "autotune": {
+      "enabled": false
+    }
+  },
+  "exp": {
+    "region-offsets": true
+  },
+  "solver": "td3",
+  "sem": {
+    "unknown_function": {
+      "spawn": false
+    },
+    "int": {
+      "signed_overflow": "assume_none"
+    },
+    "null-pointer": {
+      "dereference": "assume_none"
+    }
+  },
+  "witness": {
+    "graphml": {
+      "enabled": true,
+      "id": "enumerate",
+      "unknown": false
+    },
+    "yaml": {
+      "enabled": true,
+      "format-version": "2.0",
+      "entry-types": [
+        "invariant_set"
+      ],
+      "invariant-types": [
+        "loop_invariant"
+      ]
+    },
+    "invariant": {
+      "loop-head": true,
+      "after-lock": false,
+      "other": false,
+      "accessed": false,
+      "exact": true,
+      "exclude-vars": [
+        "tmp\\(___[0-9]+\\)?",
+        "cond",
+        "RETURN",
+        "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
+        ".*____CPAchecker_TMP_[0-9]+",
+        "__VERIFIER_assert__cond",
+        "__ksymtab_.*",
+        "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
+      ]
+    }
+  },
+  "pre": {
+    "enabled": false
+  },
+  "warn": {
+    "integer": false
+  }
+}
\ No newline at end of file
diff --git a/conf/relational-vla.json b/conf/relational-vla.json
new file mode 100644
index 00000000000..5f3c815c782
--- /dev/null
+++ b/conf/relational-vla.json
@@ -0,0 +1,138 @@
+{
+    "ana": {
+        "sv-comp": {
+            "enabled": true,
+            "functions": true
+        },
+        "int": {
+            "def_exc": true,
+            "enums": false,
+            "interval": true
+        },
+        "float": {
+            "interval": true
+        },
+        "apron": {
+            "domain": "polyhedra"
+        },
+        "arrayoob": true,
+        "activated": [
+            "base",
+            "threadid",
+            "threadflag",
+            "threadreturn",
+            "mallocWrapper",
+            "mutexEvents",
+            "mutex",
+            "access",
+            "race",
+            "escape",
+            "expRelation",
+            "mhp",
+            "assert",
+            "var_eq",
+            "symb_locks",
+            "region",
+            "thread",
+            "threadJoins",
+            "apron"
+        ],
+        "path_sens": [
+            "mutex",
+            "malloc_null",
+            "uninit",
+            "expsplit",
+            "activeSetjmp",
+            "memLeak",
+            "threadflag"
+        ],
+        "context": {
+            "widen": false
+        },
+        "malloc": {
+            "wrappers": [
+                "kmalloc",
+                "__kmalloc",
+                "usb_alloc_urb",
+                "__builtin_alloca",
+                "kzalloc",
+                "ldv_malloc",
+                "kzalloc_node",
+                "ldv_zalloc",
+                "kmalloc_array",
+                "kcalloc",
+                "ldv_xmalloc",
+                "ldv_xzalloc",
+                "ldv_calloc",
+                "ldv_kzalloc"
+            ]
+        },
+        "base": {
+            "arrays": {
+                "domain": "partitioned"
+            }
+        },
+        "race": {
+            "free": false,
+            "call": false
+        },
+        "autotune": {
+            "enabled": false
+        }
+    },
+    "exp": {
+        "region-offsets": true
+    },
+    "solver": "td3",
+    "sem": {
+        "unknown_function": {
+            "spawn": false
+        },
+        "int": {
+            "signed_overflow": "assume_none"
+        },
+        "null-pointer": {
+            "dereference": "assume_none"
+        }
+    },
+    "witness": {
+        "graphml": {
+            "enabled": true,
+            "id": "enumerate",
+            "unknown": false
+        },
+        "yaml": {
+            "enabled": true,
+            "format-version": "2.0",
+            "entry-types": [
+                "invariant_set"
+            ],
+            "invariant-types": [
+                "loop_invariant"
+            ]
+        },
+        "invariant": {
+            "loop-head": true,
+            "after-lock": false,
+            "other": false,
+            "accessed": false,
+            "exact": true,
+            "exclude-vars": [
+                "tmp\\(___[0-9]+\\)?",
+                "cond",
+                "RETURN",
+                "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
+                ".*____CPAchecker_TMP_[0-9]+",
+                "__VERIFIER_assert__cond",
+                "__ksymtab_.*",
+                "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
+            ]
+        }
+    },
+    "pre": {
+        "enabled": false
+    },
+    "warn": {
+        "integer": false
+    }
+}
\ No newline at end of file
diff --git a/conf/vla.json b/conf/vla.json
new file mode 100644
index 00000000000..8e92f11a310
--- /dev/null
+++ b/conf/vla.json
@@ -0,0 +1,137 @@
+{
+    "ana": {
+        "sv-comp": {
+            "enabled": true,
+            "functions": true
+        },
+        "int": {
+            "def_exc": true,
+            "enums": false,
+            "interval": true
+        },
+        "float": {
+            "interval": true
+        },
+        "apron": {
+            "domain": "polyhedra"
+        },
+        "arrayoob": true,
+        "activated": [
+            "base",
+            "threadid",
+            "threadflag",
+            "threadreturn",
+            "mallocWrapper",
+            "mutexEvents",
+            "mutex",
+            "access",
+            "race",
+            "escape",
+            "expRelation",
+            "mhp",
+            "assert",
+            "var_eq",
+            "symb_locks",
+            "region",
+            "thread",
+            "threadJoins"
+        ],
+        "path_sens": [
+            "mutex",
+            "malloc_null",
+            "uninit",
+            "expsplit",
+            "activeSetjmp",
+            "memLeak",
+            "threadflag"
+        ],
+        "context": {
+            "widen": false
+        },
+        "malloc": {
+            "wrappers": [
+                "kmalloc",
+                "__kmalloc",
+                "usb_alloc_urb",
+                "__builtin_alloca",
+                "kzalloc",
+                "ldv_malloc",
+                "kzalloc_node",
+                "ldv_zalloc",
+                "kmalloc_array",
+                "kcalloc",
+                "ldv_xmalloc",
+                "ldv_xzalloc",
+                "ldv_calloc",
+                "ldv_kzalloc"
+            ]
+        },
+        "base": {
+            "arrays": {
+                "domain": "partitioned"
+            }
+        },
+        "race": {
+            "free": false,
+            "call": false
+        },
+        "autotune": {
+            "enabled": false
+        }
+    },
+    "exp": {
+        "region-offsets": true
+    },
+    "solver": "td3",
+    "sem": {
+        "unknown_function": {
+            "spawn": false
+        },
+        "int": {
+            "signed_overflow": "assume_none"
+        },
+        "null-pointer": {
+            "dereference": "assume_none"
+        }
+    },
+    "witness": {
+        "graphml": {
+            "enabled": true,
+            "id": "enumerate",
+            "unknown": false
+        },
+        "yaml": {
+            "enabled": true,
+            "format-version": "2.0",
+            "entry-types": [
+                "invariant_set"
+            ],
+            "invariant-types": [
+                "loop_invariant"
+            ]
+        },
+        "invariant": {
+            "loop-head": true,
+            "after-lock": false,
+            "other": false,
+            "accessed": false,
+            "exact": true,
+            "exclude-vars": [
+                "tmp\\(___[0-9]+\\)?",
+                "cond",
+                "RETURN",
+                "__\\(cil_\\)?tmp_?[0-9]*\\(_[0-9]+\\)?",
+                ".*____CPAchecker_TMP_[0-9]+",
+                "__VERIFIER_assert__cond",
+                "__ksymtab_.*",
+                "\\(ldv_state_variable\\|ldv_timer_state\\|ldv_timer_list\\|ldv_irq_\\(line_\\|data_\\)?[0-9]+\\|ldv_retval\\)_[0-9]+"
+            ]
+        }
+    },
+    "pre": {
+        "enabled": false
+    },
+    "warn": {
+        "integer": false
+    }
+}
\ No newline at end of file