From 051ab662fb3ffaa85c12340f8fd52de1eb1aaec2 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 16 Jul 2024 18:25:58 +0200
Subject: [PATCH 01/10] Add witness cram test

---
 .../46-apron2/95-witness-mm-escape.c          |  19 +
 .../46-apron2/95-witness-mm-escape.t          |  25 +
 .../46-apron2/95-witness-mm-escape.yml        | 449 ++++++++++++++++++
 tests/regression/46-apron2/dune               |   2 +-
 4 files changed, 494 insertions(+), 1 deletion(-)
 create mode 100644 tests/regression/46-apron2/95-witness-mm-escape.c
 create mode 100644 tests/regression/46-apron2/95-witness-mm-escape.t
 create mode 100644 tests/regression/46-apron2/95-witness-mm-escape.yml

diff --git a/tests/regression/46-apron2/95-witness-mm-escape.c b/tests/regression/46-apron2/95-witness-mm-escape.c
new file mode 100644
index 0000000000..e6f2d5d429
--- /dev/null
+++ b/tests/regression/46-apron2/95-witness-mm-escape.c
@@ -0,0 +1,19 @@
+// PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
+#include <pthread.h>
+#include <goblint.h>
+
+int *b;
+pthread_mutex_t e;
+
+void main() {
+
+    int g = 8;
+    int a;
+    if(a) {
+        g = 10;
+    }
+
+    b = &g;
+
+    pthread_mutex_lock(&e);
+}
diff --git a/tests/regression/46-apron2/95-witness-mm-escape.t b/tests/regression/46-apron2/95-witness-mm-escape.t
new file mode 100644
index 0000000000..c5cee8cfdb
--- /dev/null
+++ b/tests/regression/46-apron2/95-witness-mm-escape.t
@@ -0,0 +1,25 @@
+  $ goblint --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml 95-witness-mm-escape.c
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 7
+    dead: 0
+    total lines: 7
+  [Success][Witness] invariant confirmed: 0 <= g (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 0 <= *b (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: g <= 127 (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: *b <= 127 (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: (2147483638LL + (long long )a) + (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: (2147483637LL - (long long )a) + (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: (2147483658LL + (long long )a) - (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: (2147483657LL - (long long )a) - (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: b == & g (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: g != 0 (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: *b != 0 (95-witness-mm-escape.c:19:1)
+  [Info][Witness] witness validation summary:
+    confirmed: 22
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 22
diff --git a/tests/regression/46-apron2/95-witness-mm-escape.yml b/tests/regression/46-apron2/95-witness-mm-escape.yml
new file mode 100644
index 0000000000..bf99e03f97
--- /dev/null
+++ b/tests/regression/46-apron2/95-witness-mm-escape.yml
@@ -0,0 +1,449 @@
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: bd605de4-9e24-4df2-a8b6-7a20973f08c3
+    creation_time: 2024-07-16T16:10:49Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: 0 <= g
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: d52450ae-a439-4c7e-9cd7-88a4d7b2729d
+    creation_time: 2024-07-16T16:10:49Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: 0 <= *b
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: 934e24ac-ff4e-4ce8-b10e-28c96d1d9a85
+    creation_time: 2024-07-16T16:10:49Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: g <= 127
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: b67ec3d2-1506-4a5a-a019-b959fa02c710
+    creation_time: 2024-07-16T16:10:49Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: '*b <= 127'
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: 799dbde2-5854-4786-b784-22941410dd4c
+    creation_time: 2024-07-16T16:10:49Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: (2147483638LL + (long long )a) + (long long )g >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: fbf9961a-853f-4bc0-be9b-a12f6d49ab20
+    creation_time: 2024-07-16T16:10:49Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: (2147483637LL - (long long )a) + (long long )g >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: c7d1d801-2b2a-4f34-a0ed-29e496ae2bbf
+    creation_time: 2024-07-16T16:10:49Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: (2147483658LL + (long long )a) - (long long )g >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: f626d0f0-9ab2-4e7e-8568-194a3ba0f671
+    creation_time: 2024-07-16T16:10:49Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: (2147483657LL - (long long )a) - (long long )g >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: 70ebfa4c-8b42-439e-bb6f-f8b87b8bebe9
+    creation_time: 2024-07-16T16:10:49Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: b == & g
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: 1b25d102-ebc5-4dde-854d-ac5525aa4fed
+    creation_time: 2024-07-16T16:10:49Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: g != 0
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: bc5e8286-3029-4002-b87b-1288f32e44c4
+    creation_time: 2024-07-16T16:10:49Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: '*b != 0'
+    type: assertion
+    format: C
+- entry_type: invariant_set
+  metadata:
+    format_version: "0.1"
+    uuid: 8cad3de5-98bb-4400-833c-bae232e13530
+    creation_time: 2024-07-16T16:10:49Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+      data_model: LP64
+      language: C
+  content:
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        line: 19
+        column: 1
+        function: main
+      value: 0 <= g
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        line: 19
+        column: 1
+        function: main
+      value: 0 <= *b
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        line: 19
+        column: 1
+        function: main
+      value: g <= 127
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        line: 19
+        column: 1
+        function: main
+      value: '*b <= 127'
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        line: 19
+        column: 1
+        function: main
+      value: (2147483638LL + (long long )a) + (long long )g >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        line: 19
+        column: 1
+        function: main
+      value: (2147483637LL - (long long )a) + (long long )g >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        line: 19
+        column: 1
+        function: main
+      value: (2147483658LL + (long long )a) - (long long )g >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        line: 19
+        column: 1
+        function: main
+      value: (2147483657LL - (long long )a) - (long long )g >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        line: 19
+        column: 1
+        function: main
+      value: b == & g
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        line: 19
+        column: 1
+        function: main
+      value: g != 0
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        line: 19
+        column: 1
+        function: main
+      value: '*b != 0'
+      format: c_expression
diff --git a/tests/regression/46-apron2/dune b/tests/regression/46-apron2/dune
index 89efde3083..8395e69ea3 100644
--- a/tests/regression/46-apron2/dune
+++ b/tests/regression/46-apron2/dune
@@ -12,4 +12,4 @@
 (cram
  (alias runaprontest)
  (enabled_if %{lib-available:apron})
- (deps (glob_files *.c)))
+ (deps (glob_files *.c) (glob_files *.yml)))

From 0e5043dd7cf084596483a46a72f78e5a5d3a5319 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 16 Jul 2024 18:26:22 +0200
Subject: [PATCH 02/10] Fix `read_global`

---
 src/analyses/apron/relationAnalysis.apron.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index df3cf545c5..616cc84e8b 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -56,7 +56,8 @@ struct
       Priv.read_global ask getg st g x
     else (
       let rel = st.rel in
-      let g_var = RV.global g in
+      (* If it has escaped and we have never been multi-threaded, we can still refer to the local *)
+      let g_var = if g.vglob then RV.global g else RV.local g in
       let x_var = RV.local x in
       let rel' = RD.add_vars rel [g_var] in
       let rel' = RD.assign_var rel' x_var g_var in
@@ -88,7 +89,7 @@ struct
     let e' = visitCilExpr visitor e in
     let rel = RD.add_vars st.rel (List.map RV.local (VH.values v_ins |> List.of_enum)) in (* add temporary g#in-s *)
     let rel' = VH.fold (fun v v_in rel ->
-        if M.tracing then M.trace "relation" "read_global %a %a" CilType.Varinfo.pretty v CilType.Varinfo.pretty v_in;
+        if M.tracing then M.trace "gurki" "read_global %a %a" CilType.Varinfo.pretty v CilType.Varinfo.pretty v_in;
         read_global ask getg {st with rel} v v_in (* g#in = g; *)
       ) v_ins rel
     in

From 9fa4e23718c8bca773bc80dbb0094720095f2328 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 16 Jul 2024 18:27:27 +0200
Subject: [PATCH 03/10] Spurious tracing

---
 src/analyses/apron/relationAnalysis.apron.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 616cc84e8b..6c914bb513 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -89,7 +89,6 @@ struct
     let e' = visitCilExpr visitor e in
     let rel = RD.add_vars st.rel (List.map RV.local (VH.values v_ins |> List.of_enum)) in (* add temporary g#in-s *)
     let rel' = VH.fold (fun v v_in rel ->
-        if M.tracing then M.trace "gurki" "read_global %a %a" CilType.Varinfo.pretty v CilType.Varinfo.pretty v_in;
         read_global ask getg {st with rel} v v_in (* g#in = g; *)
       ) v_ins rel
     in

From d54dfcc89fd689bcb95d03667c3c0938114ffdb4 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 16 Jul 2024 18:32:45 +0200
Subject: [PATCH 04/10] Fix tracing

---
 src/analyses/apron/relationAnalysis.apron.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 6c914bb513..bc024fd4a2 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -89,6 +89,7 @@ struct
     let e' = visitCilExpr visitor e in
     let rel = RD.add_vars st.rel (List.map RV.local (VH.values v_ins |> List.of_enum)) in (* add temporary g#in-s *)
     let rel' = VH.fold (fun v v_in rel ->
+        if M.tracing then M.trace "relation" "read_global %a %a" CilType.Varinfo.pretty v CilType.Varinfo.pretty v_in;
         read_global ask getg {st with rel} v v_in (* g#in = g; *)
       ) v_ins rel
     in

From cf2641f705ea53036bf7e47e57e317b38b54a013 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 16 Jul 2024 18:39:16 +0200
Subject: [PATCH 05/10] Update cram test

---
 .../46-apron2/95-witness-mm-escape.t          |   8 +-
 .../46-apron2/95-witness-mm-escape.yml        | 312 ++++++++++++++----
 2 files changed, 248 insertions(+), 72 deletions(-)

diff --git a/tests/regression/46-apron2/95-witness-mm-escape.t b/tests/regression/46-apron2/95-witness-mm-escape.t
index c5cee8cfdb..047cb15718 100644
--- a/tests/regression/46-apron2/95-witness-mm-escape.t
+++ b/tests/regression/46-apron2/95-witness-mm-escape.t
@@ -7,19 +7,23 @@
   [Success][Witness] invariant confirmed: 0 <= *b (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: g <= 127 (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: *b <= 127 (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: -8LL + (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 2147483648LL + (long long )a >= 0LL (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: (2147483638LL + (long long )a) + (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: (2147483637LL - (long long )a) + (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 10LL - (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
+  [Success][Witness] invariant confirmed: 2147483647LL - (long long )a >= 0LL (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: (2147483658LL + (long long )a) - (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: (2147483657LL - (long long )a) - (long long )g >= 0LL (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: b == & g (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: g != 0 (95-witness-mm-escape.c:19:1)
   [Success][Witness] invariant confirmed: *b != 0 (95-witness-mm-escape.c:19:1)
   [Info][Witness] witness validation summary:
-    confirmed: 22
+    confirmed: 30
     unconfirmed: 0
     refuted: 0
     error: 0
     unchecked: 0
     unsupported: 0
     disabled: 0
-    total validation entries: 22
+    total validation entries: 30
diff --git a/tests/regression/46-apron2/95-witness-mm-escape.yml b/tests/regression/46-apron2/95-witness-mm-escape.yml
index bf99e03f97..66715bd382 100644
--- a/tests/regression/46-apron2/95-witness-mm-escape.yml
+++ b/tests/regression/46-apron2/95-witness-mm-escape.yml
@@ -1,25 +1,26 @@
 - entry_type: location_invariant
   metadata:
     format_version: "0.1"
-    uuid: bd605de4-9e24-4df2-a8b6-7a20973f08c3
-    creation_time: 2024-07-16T16:10:49Z
+    uuid: f88caf27-fbfe-4ce8-a15d-463646cca899
+    creation_time: 2024-07-16T16:36:39Z
     producer:
       name: Goblint
       version: heads/check_overflow_convert-0-gc35fd8620-dirty
       command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
         ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
         ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
-        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
     task:
       input_files:
       - 95-witness-mm-escape.c
       input_file_hashes:
-        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
       data_model: LP64
       language: C
   location:
     file_name: 95-witness-mm-escape.c
-    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
     line: 19
     column: 1
     function: main
@@ -30,25 +31,26 @@
 - entry_type: location_invariant
   metadata:
     format_version: "0.1"
-    uuid: d52450ae-a439-4c7e-9cd7-88a4d7b2729d
-    creation_time: 2024-07-16T16:10:49Z
+    uuid: 7949534c-6edd-4412-9778-fc58745e7cc5
+    creation_time: 2024-07-16T16:36:39Z
     producer:
       name: Goblint
       version: heads/check_overflow_convert-0-gc35fd8620-dirty
       command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
         ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
         ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
-        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
     task:
       input_files:
       - 95-witness-mm-escape.c
       input_file_hashes:
-        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
       data_model: LP64
       language: C
   location:
     file_name: 95-witness-mm-escape.c
-    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
     line: 19
     column: 1
     function: main
@@ -59,25 +61,26 @@
 - entry_type: location_invariant
   metadata:
     format_version: "0.1"
-    uuid: 934e24ac-ff4e-4ce8-b10e-28c96d1d9a85
-    creation_time: 2024-07-16T16:10:49Z
+    uuid: ffe5f8b3-569c-4d42-8e9b-21c48312e6ce
+    creation_time: 2024-07-16T16:36:39Z
     producer:
       name: Goblint
       version: heads/check_overflow_convert-0-gc35fd8620-dirty
       command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
         ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
         ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
-        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
     task:
       input_files:
       - 95-witness-mm-escape.c
       input_file_hashes:
-        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
       data_model: LP64
       language: C
   location:
     file_name: 95-witness-mm-escape.c
-    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
     line: 19
     column: 1
     function: main
@@ -88,25 +91,26 @@
 - entry_type: location_invariant
   metadata:
     format_version: "0.1"
-    uuid: b67ec3d2-1506-4a5a-a019-b959fa02c710
-    creation_time: 2024-07-16T16:10:49Z
+    uuid: cad5c137-4373-4431-b8c8-c5d1e537a716
+    creation_time: 2024-07-16T16:36:39Z
     producer:
       name: Goblint
       version: heads/check_overflow_convert-0-gc35fd8620-dirty
       command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
         ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
         ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
-        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
     task:
       input_files:
       - 95-witness-mm-escape.c
       input_file_hashes:
-        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
       data_model: LP64
       language: C
   location:
     file_name: 95-witness-mm-escape.c
-    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
     line: 19
     column: 1
     function: main
@@ -117,25 +121,86 @@
 - entry_type: location_invariant
   metadata:
     format_version: "0.1"
-    uuid: 799dbde2-5854-4786-b784-22941410dd4c
-    creation_time: 2024-07-16T16:10:49Z
+    uuid: aa21493b-1338-4004-90b7-046b9e826169
+    creation_time: 2024-07-16T16:36:39Z
     producer:
       name: Goblint
       version: heads/check_overflow_convert-0-gc35fd8620-dirty
       command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
         ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
         ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
-        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
     task:
       input_files:
       - 95-witness-mm-escape.c
       input_file_hashes:
-        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
       data_model: LP64
       language: C
   location:
     file_name: 95-witness-mm-escape.c
-    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: -8LL + (long long )g >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: b640fdf6-abc8-45b9-ad4f-2695e0d66a3d
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: 2147483648LL + (long long )a >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: ecc017f2-d045-45c7-a795-d3d16088368d
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
     line: 19
     column: 1
     function: main
@@ -146,25 +211,26 @@
 - entry_type: location_invariant
   metadata:
     format_version: "0.1"
-    uuid: fbf9961a-853f-4bc0-be9b-a12f6d49ab20
-    creation_time: 2024-07-16T16:10:49Z
+    uuid: 52ace953-715d-4d44-9c44-5b40c1124593
+    creation_time: 2024-07-16T16:36:39Z
     producer:
       name: Goblint
       version: heads/check_overflow_convert-0-gc35fd8620-dirty
       command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
         ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
         ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
-        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
     task:
       input_files:
       - 95-witness-mm-escape.c
       input_file_hashes:
-        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
       data_model: LP64
       language: C
   location:
     file_name: 95-witness-mm-escape.c
-    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
     line: 19
     column: 1
     function: main
@@ -175,25 +241,86 @@
 - entry_type: location_invariant
   metadata:
     format_version: "0.1"
-    uuid: c7d1d801-2b2a-4f34-a0ed-29e496ae2bbf
-    creation_time: 2024-07-16T16:10:49Z
+    uuid: 661e7eee-b5c0-4de3-89ed-369f6978ba28
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: 10LL - (long long )g >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: 7878f84e-a951-4247-a196-97f9195cf2fb
+    creation_time: 2024-07-16T16:36:39Z
     producer:
       name: Goblint
       version: heads/check_overflow_convert-0-gc35fd8620-dirty
       command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
         ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
         ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
-        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
     task:
       input_files:
       - 95-witness-mm-escape.c
       input_file_hashes:
-        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
       data_model: LP64
       language: C
   location:
     file_name: 95-witness-mm-escape.c
-    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+    line: 19
+    column: 1
+    function: main
+  location_invariant:
+    string: 2147483647LL - (long long )a >= 0LL
+    type: assertion
+    format: C
+- entry_type: location_invariant
+  metadata:
+    format_version: "0.1"
+    uuid: e80582ed-4527-4773-97fd-08631c673c21
+    creation_time: 2024-07-16T16:36:39Z
+    producer:
+      name: Goblint
+      version: heads/check_overflow_convert-0-gc35fd8620-dirty
+      command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
+        ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
+        ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+    task:
+      input_files:
+      - 95-witness-mm-escape.c
+      input_file_hashes:
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+      data_model: LP64
+      language: C
+  location:
+    file_name: 95-witness-mm-escape.c
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
     line: 19
     column: 1
     function: main
@@ -204,25 +331,26 @@
 - entry_type: location_invariant
   metadata:
     format_version: "0.1"
-    uuid: f626d0f0-9ab2-4e7e-8568-194a3ba0f671
-    creation_time: 2024-07-16T16:10:49Z
+    uuid: 49f62de7-3bfc-45ee-8709-0ff295f23b7a
+    creation_time: 2024-07-16T16:36:39Z
     producer:
       name: Goblint
       version: heads/check_overflow_convert-0-gc35fd8620-dirty
       command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
         ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
         ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
-        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
     task:
       input_files:
       - 95-witness-mm-escape.c
       input_file_hashes:
-        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
       data_model: LP64
       language: C
   location:
     file_name: 95-witness-mm-escape.c
-    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
     line: 19
     column: 1
     function: main
@@ -233,25 +361,26 @@
 - entry_type: location_invariant
   metadata:
     format_version: "0.1"
-    uuid: 70ebfa4c-8b42-439e-bb6f-f8b87b8bebe9
-    creation_time: 2024-07-16T16:10:49Z
+    uuid: cb86dd3a-2ff5-420b-8d49-42240a324a26
+    creation_time: 2024-07-16T16:36:39Z
     producer:
       name: Goblint
       version: heads/check_overflow_convert-0-gc35fd8620-dirty
       command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
         ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
         ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
-        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
     task:
       input_files:
       - 95-witness-mm-escape.c
       input_file_hashes:
-        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
       data_model: LP64
       language: C
   location:
     file_name: 95-witness-mm-escape.c
-    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
     line: 19
     column: 1
     function: main
@@ -262,25 +391,26 @@
 - entry_type: location_invariant
   metadata:
     format_version: "0.1"
-    uuid: 1b25d102-ebc5-4dde-854d-ac5525aa4fed
-    creation_time: 2024-07-16T16:10:49Z
+    uuid: 2573f907-0386-4098-9b0c-7f1ec86d3f90
+    creation_time: 2024-07-16T16:36:39Z
     producer:
       name: Goblint
       version: heads/check_overflow_convert-0-gc35fd8620-dirty
       command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
         ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
         ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
-        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
     task:
       input_files:
       - 95-witness-mm-escape.c
       input_file_hashes:
-        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
       data_model: LP64
       language: C
   location:
     file_name: 95-witness-mm-escape.c
-    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
     line: 19
     column: 1
     function: main
@@ -291,25 +421,26 @@
 - entry_type: location_invariant
   metadata:
     format_version: "0.1"
-    uuid: bc5e8286-3029-4002-b87b-1288f32e44c4
-    creation_time: 2024-07-16T16:10:49Z
+    uuid: 15693293-61f1-431b-867e-86add36e4d80
+    creation_time: 2024-07-16T16:36:39Z
     producer:
       name: Goblint
       version: heads/check_overflow_convert-0-gc35fd8620-dirty
       command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
         ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
         ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
-        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
     task:
       input_files:
       - 95-witness-mm-escape.c
       input_file_hashes:
-        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
       data_model: LP64
       language: C
   location:
     file_name: 95-witness-mm-escape.c
-    file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+    file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
     line: 19
     column: 1
     function: main
@@ -320,20 +451,21 @@
 - entry_type: invariant_set
   metadata:
     format_version: "0.1"
-    uuid: 8cad3de5-98bb-4400-833c-bae232e13530
-    creation_time: 2024-07-16T16:10:49Z
+    uuid: 5f4a70a3-8b30-4b5a-a260-56bb341a6283
+    creation_time: 2024-07-16T16:36:39Z
     producer:
       name: Goblint
       version: heads/check_overflow_convert-0-gc35fd8620-dirty
       command_line: '''../../../goblint'' ''95-witness-mm-escape.c'' ''--set'' ''ana.activated[+]''
         ''apron'' ''--set'' ''ana.path_sens[+]'' ''threadflag'' ''--set'' ''ana.relation.privatization''
         ''mutex-meet-tid-cluster12'' ''--enable'' ''witness.yaml.enabled'' ''--disable''
-        ''witness.invariant.other'' ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
+        ''witness.invariant.other'' ''--enable'' ''ana.relation.invariant.one-var''
+        ''--set'' ''witness.yaml.path'' ''95-witness-mm-escape.yml'''
     task:
       input_files:
       - 95-witness-mm-escape.c
       input_file_hashes:
-        95-witness-mm-escape.c: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        95-witness-mm-escape.c: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
       data_model: LP64
       language: C
   content:
@@ -341,7 +473,7 @@
       type: location_invariant
       location:
         file_name: 95-witness-mm-escape.c
-        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
         line: 19
         column: 1
         function: main
@@ -351,7 +483,7 @@
       type: location_invariant
       location:
         file_name: 95-witness-mm-escape.c
-        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
         line: 19
         column: 1
         function: main
@@ -361,7 +493,7 @@
       type: location_invariant
       location:
         file_name: 95-witness-mm-escape.c
-        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
         line: 19
         column: 1
         function: main
@@ -371,7 +503,7 @@
       type: location_invariant
       location:
         file_name: 95-witness-mm-escape.c
-        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
         line: 19
         column: 1
         function: main
@@ -381,7 +513,27 @@
       type: location_invariant
       location:
         file_name: 95-witness-mm-escape.c
-        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: -8LL + (long long )g >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: 2147483648LL + (long long )a >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
         line: 19
         column: 1
         function: main
@@ -391,7 +543,7 @@
       type: location_invariant
       location:
         file_name: 95-witness-mm-escape.c
-        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
         line: 19
         column: 1
         function: main
@@ -401,7 +553,27 @@
       type: location_invariant
       location:
         file_name: 95-witness-mm-escape.c
-        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: 10LL - (long long )g >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
+        line: 19
+        column: 1
+        function: main
+      value: 2147483647LL - (long long )a >= 0LL
+      format: c_expression
+  - invariant:
+      type: location_invariant
+      location:
+        file_name: 95-witness-mm-escape.c
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
         line: 19
         column: 1
         function: main
@@ -411,7 +583,7 @@
       type: location_invariant
       location:
         file_name: 95-witness-mm-escape.c
-        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
         line: 19
         column: 1
         function: main
@@ -421,7 +593,7 @@
       type: location_invariant
       location:
         file_name: 95-witness-mm-escape.c
-        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
         line: 19
         column: 1
         function: main
@@ -431,7 +603,7 @@
       type: location_invariant
       location:
         file_name: 95-witness-mm-escape.c
-        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
         line: 19
         column: 1
         function: main
@@ -441,7 +613,7 @@
       type: location_invariant
       location:
         file_name: 95-witness-mm-escape.c
-        file_hash: 59ef053c97b76b763526674d2e5f5a4bb304200ec4b738e93dcf7b42738b8ebe
+        file_hash: bc9de79e9c6aebc20f4284c088f10093ed99a05b0758005a17a5f39a9cc1b7e8
         line: 19
         column: 1
         function: main

From 775c15f97d93205167a71fbd942469bc1b0eb30a Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Wed, 24 Jul 2024 11:19:46 +0200
Subject: [PATCH 06/10] Apron: Do not produce invariants about stale locals
 that have escaped

---
 src/analyses/apron/relationAnalysis.apron.ml  |  4 ++++
 .../46-apron2/96-witness-mm-escape2.c         | 22 +++++++++++++++++++
 .../46-apron2/96-witness-mm-escape2.t         | 18 +++++++++++++++
 3 files changed, 44 insertions(+)
 create mode 100644 tests/regression/46-apron2/96-witness-mm-escape2.c
 create mode 100644 tests/regression/46-apron2/96-witness-mm-escape2.t

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index bc024fd4a2..c151ed1f75 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -603,6 +603,10 @@ struct
           | Some (Local v) ->
             if VH.mem v_ins_inv v then
               keep_global
+            else if ThreadEscape.has_escaped ask v then
+              (* Escaped local variables should be read in via their v#in# variables, this apron var may refer to stale values only *)
+              (* and is not a sound description of the C variable. *)
+              false
             else
               keep_local
           | _ -> false
diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.c b/tests/regression/46-apron2/96-witness-mm-escape2.c
new file mode 100644
index 0000000000..2fa3530679
--- /dev/null
+++ b/tests/regression/46-apron2/96-witness-mm-escape2.c
@@ -0,0 +1,22 @@
+// PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
+#include<pthread.h>
+int *b;
+pthread_mutex_t e;
+
+void* other(void* arg) {
+    pthread_mutex_lock(&e);
+    *b = -100;
+    pthread_mutex_unlock(&e);
+
+    return NULL;
+}
+
+void main() {
+    pthread_t t;
+    pthread_create(&t, NULL, other, NULL);
+    int g = 8;
+
+    b = &g;
+
+    pthread_mutex_lock(&e);
+}
diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.t b/tests/regression/46-apron2/96-witness-mm-escape2.t
new file mode 100644
index 0000000000..9311af8306
--- /dev/null
+++ b/tests/regression/46-apron2/96-witness-mm-escape2.t
@@ -0,0 +1,18 @@
+  $ goblint --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 96-witness-mm-escape2.c --set witness.yaml.path 96-witness-mm-escape2.yml
+  [Info][Witness] witness generation summary:
+    total generation entries: 5
+
+  $ goblint --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 96-witness-mm-escape2.yml 96-witness-mm-escape2.c
+  [Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (96-witness-mm-escape2.c:8:5)
+  [Success][Witness] invariant confirmed: -128 <= g (96-witness-mm-escape2.c:22:1)
+  [Success][Witness] invariant confirmed: g <= 127 (96-witness-mm-escape2.c:22:1)
+  [Success][Witness] invariant confirmed: g != 0 (96-witness-mm-escape2.c:22:1)
+  [Info][Witness] witness validation summary:
+    confirmed: 8
+    unconfirmed: 0
+    refuted: 0
+    error: 0
+    unchecked: 0
+    unsupported: 0
+    disabled: 0
+    total validation entries: 8

From 267f25ea15776d5427538fdaf49f7c11c8661605 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 17 Dec 2024 09:39:25 +0100
Subject: [PATCH 07/10] Update tests

---
 tests/regression/46-apron2/95-witness-mm-escape.c  |  2 +-
 tests/regression/46-apron2/96-witness-mm-escape2.c |  2 +-
 tests/regression/46-apron2/96-witness-mm-escape2.t | 10 +++++++---
 3 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/tests/regression/46-apron2/95-witness-mm-escape.c b/tests/regression/46-apron2/95-witness-mm-escape.c
index e6f2d5d429..e18c8e0499 100644
--- a/tests/regression/46-apron2/95-witness-mm-escape.c
+++ b/tests/regression/46-apron2/95-witness-mm-escape.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
+// CRAM PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
 #include <pthread.h>
 #include <goblint.h>
 
diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.c b/tests/regression/46-apron2/96-witness-mm-escape2.c
index 2fa3530679..22384b9238 100644
--- a/tests/regression/46-apron2/96-witness-mm-escape2.c
+++ b/tests/regression/46-apron2/96-witness-mm-escape2.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
+// CRAM PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
 #include<pthread.h>
 int *b;
 pthread_mutex_t e;
diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.t b/tests/regression/46-apron2/96-witness-mm-escape2.t
index 9311af8306..a8fee12c79 100644
--- a/tests/regression/46-apron2/96-witness-mm-escape2.t
+++ b/tests/regression/46-apron2/96-witness-mm-escape2.t
@@ -1,18 +1,22 @@
   $ goblint --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 96-witness-mm-escape2.c --set witness.yaml.path 96-witness-mm-escape2.yml
   [Info][Witness] witness generation summary:
-    total generation entries: 5
+    location invariants: 8
+    loop invariants: 0
+    flow-insensitive invariants: 1
+    total generation entries: 6
 
   $ goblint --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 96-witness-mm-escape2.yml 96-witness-mm-escape2.c
   [Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (96-witness-mm-escape2.c:8:5)
   [Success][Witness] invariant confirmed: -128 <= g (96-witness-mm-escape2.c:22:1)
   [Success][Witness] invariant confirmed: g <= 127 (96-witness-mm-escape2.c:22:1)
   [Success][Witness] invariant confirmed: g != 0 (96-witness-mm-escape2.c:22:1)
+  [Warning][Witness] cannot validate entry of type flow_insensitive_invariant
   [Info][Witness] witness validation summary:
     confirmed: 8
     unconfirmed: 0
     refuted: 0
     error: 0
     unchecked: 0
-    unsupported: 0
+    unsupported: 1
     disabled: 0
-    total validation entries: 8
+    total validation entries: 9

From 2fd5321556492da04d6da89821ed2c91d25ea24a Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 17 Dec 2024 10:28:35 +0100
Subject: [PATCH 08/10] Enable `warn.deterministic`

---
 tests/regression/46-apron2/96-witness-mm-escape2.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.c b/tests/regression/46-apron2/96-witness-mm-escape2.c
index 22384b9238..c7e57908ca 100644
--- a/tests/regression/46-apron2/96-witness-mm-escape2.c
+++ b/tests/regression/46-apron2/96-witness-mm-escape2.c
@@ -1,4 +1,4 @@
-// CRAM PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
+// CRAM PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable warn.deterministic --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 95-witness-mm-escape.yml
 #include<pthread.h>
 int *b;
 pthread_mutex_t e;

From ced9396952f14ed63e32e69cf047efafbbb4e447 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 17 Dec 2024 10:56:06 +0100
Subject: [PATCH 09/10] Enable deterministic warnings

---
 tests/regression/46-apron2/96-witness-mm-escape2.t | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.t b/tests/regression/46-apron2/96-witness-mm-escape2.t
index a8fee12c79..a109e44b48 100644
--- a/tests/regression/46-apron2/96-witness-mm-escape2.t
+++ b/tests/regression/46-apron2/96-witness-mm-escape2.t
@@ -1,11 +1,11 @@
-  $ goblint --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 96-witness-mm-escape2.c --set witness.yaml.path 96-witness-mm-escape2.yml
+  $ goblint --disable ana.dead-code.lines --disable warn.race --enable warn.deterministic --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --enable witness.yaml.enabled --disable witness.invariant.other --disable witness.invariant.loop-head 96-witness-mm-escape2.c --set witness.yaml.path 96-witness-mm-escape2.yml
   [Info][Witness] witness generation summary:
     location invariants: 8
     loop invariants: 0
     flow-insensitive invariants: 1
     total generation entries: 6
 
-  $ goblint --disable ana.dead-code.lines --disable warn.race --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 96-witness-mm-escape2.yml 96-witness-mm-escape2.c
+  $ goblint --disable ana.dead-code.lines --disable warn.race --enable warn.deterministic --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 96-witness-mm-escape2.yml 96-witness-mm-escape2.c
   [Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (96-witness-mm-escape2.c:8:5)
   [Success][Witness] invariant confirmed: -128 <= g (96-witness-mm-escape2.c:22:1)
   [Success][Witness] invariant confirmed: g <= 127 (96-witness-mm-escape2.c:22:1)

From 1795a2bd3ffdb765cd34e650af0aca81f67cc723 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Tue, 17 Dec 2024 11:10:32 +0100
Subject: [PATCH 10/10] dune promote

---
 tests/regression/46-apron2/96-witness-mm-escape2.t | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/tests/regression/46-apron2/96-witness-mm-escape2.t b/tests/regression/46-apron2/96-witness-mm-escape2.t
index a109e44b48..07825f2af5 100644
--- a/tests/regression/46-apron2/96-witness-mm-escape2.t
+++ b/tests/regression/46-apron2/96-witness-mm-escape2.t
@@ -6,10 +6,6 @@
     total generation entries: 6
 
   $ goblint --disable ana.dead-code.lines --disable warn.race --enable warn.deterministic --disable warn.behavior --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.relation.privatization mutex-meet-tid-cluster12 --set witness.yaml.validate 96-witness-mm-escape2.yml 96-witness-mm-escape2.c
-  [Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (96-witness-mm-escape2.c:8:5)
-  [Success][Witness] invariant confirmed: -128 <= g (96-witness-mm-escape2.c:22:1)
-  [Success][Witness] invariant confirmed: g <= 127 (96-witness-mm-escape2.c:22:1)
-  [Success][Witness] invariant confirmed: g != 0 (96-witness-mm-escape2.c:22:1)
   [Warning][Witness] cannot validate entry of type flow_insensitive_invariant
   [Info][Witness] witness validation summary:
     confirmed: 8
@@ -20,3 +16,7 @@
     unsupported: 1
     disabled: 0
     total validation entries: 9
+  [Success][Witness] invariant confirmed: (unsigned long )arg == 0UL (96-witness-mm-escape2.c:8:5)
+  [Success][Witness] invariant confirmed: -128 <= g (96-witness-mm-escape2.c:22:1)
+  [Success][Witness] invariant confirmed: g != 0 (96-witness-mm-escape2.c:22:1)
+  [Success][Witness] invariant confirmed: g <= 127 (96-witness-mm-escape2.c:22:1)