From abb3ac5388d27557d16bbde21301acba6906f425 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 22 Apr 2024 17:04:09 +0300
Subject: [PATCH 01/22] Remove TODOs from 36-apron/21-traces-cluster-based
 (issue #1425)

---
 tests/regression/36-apron/21-traces-cluster-based.c | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/tests/regression/36-apron/21-traces-cluster-based.c b/tests/regression/36-apron/21-traces-cluster-based.c
index 360a3f3df2..1628e986ca 100644
--- a/tests/regression/36-apron/21-traces-cluster-based.c
+++ b/tests/regression/36-apron/21-traces-cluster-based.c
@@ -1,6 +1,6 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.sv-comp.functions
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.sv-comp.functions --set ana.relation.privatization mutex-meet
 extern int __VERIFIER_nondet_int();
-
+// TODO: rename? this doesn't require clusters
 #include <pthread.h>
 #include <goblint.h>
 
@@ -45,7 +45,7 @@ void *t3_fun(void *arg) {
   y = h;
   pthread_mutex_unlock(&A);
   pthread_mutex_unlock(&B);
-  __goblint_check(y == x); // TODO (mutex-meet succeeds, protection unknown)
+  __goblint_check(y == x); // mutex-meet succeeds, protection unknown
   return NULL;
 }
 
@@ -63,9 +63,9 @@ int main(void) {
   x = g;
   y = h;
   pthread_mutex_lock(&B);
-  __goblint_check(y == x); // TODO (mutex-meet succeeds, protection unknown)
+  __goblint_check(y == x); // mutex-meet succeeds, protection unknown
   pthread_mutex_unlock(&B);
   pthread_mutex_unlock(&A);
-  __goblint_check(y == x); // TODO (mutex-meet succeeds, protection unknown)
+  __goblint_check(y == x); // mutex-meet succeeds, protection unknown
   return 0;
 }

From 6abbd8a530d5a92f1c5863a410543d555e604ea3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 22 Apr 2024 17:13:45 +0300
Subject: [PATCH 02/22] Remove TODO from
 36-apron/22-traces-write-centered-vs-mutex-meet (issue #1425)

---
 .../36-apron/22-traces-write-centered-vs-meet-mutex.c       | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/tests/regression/36-apron/22-traces-write-centered-vs-meet-mutex.c b/tests/regression/36-apron/22-traces-write-centered-vs-meet-mutex.c
index 1d3a6d7b21..65f5c54348 100644
--- a/tests/regression/36-apron/22-traces-write-centered-vs-meet-mutex.c
+++ b/tests/regression/36-apron/22-traces-write-centered-vs-meet-mutex.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.sv-comp.functions
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.sv-comp.functions --set ana.relation.privatization mutex-meet
 extern int __VERIFIER_nondet_int();
 
 #include <pthread.h>
@@ -22,11 +22,11 @@ void *t_fun(void *arg) {
     y = h;
     __goblint_check(y <= x);
     pthread_mutex_lock(&B);
-    __goblint_check(x == y); // TODO (mutex-meet succeeds, write unknown)
+    __goblint_check(x == y); // mutex-meet succeeds, (now-defunct) write unknown
     pthread_mutex_unlock(&B);
     i = x + 31;
     z = i;
-    __goblint_check(z >= x); // TODO (write succeeds, mutex-meet unknown)
+    __goblint_check(z >= x); // TODO ((now-defunct) write succeeds, mutex-meet unknown)
     pthread_mutex_unlock(&A);
     pthread_mutex_unlock(&C);
   }

From c58607213e8a99a0bcb212d0449256e967033016 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 22 Apr 2024 17:16:26 +0300
Subject: [PATCH 03/22] Remove TODO from 36-apron/38-branch-global (issue
 #1425)

---
 tests/regression/36-apron/38-branch-global.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/regression/36-apron/38-branch-global.c b/tests/regression/36-apron/38-branch-global.c
index 26d5e0d94a..9a80b71068 100644
--- a/tests/regression/36-apron/38-branch-global.c
+++ b/tests/regression/36-apron/38-branch-global.c
@@ -10,6 +10,6 @@ int main() {
         __goblint_check(count < ARR_SIZE);
         count++;
     }
-    __goblint_check(count == ARR_SIZE); // TODO (requires threshold)
+    __goblint_check(count == ARR_SIZE); // requires narrowing
     return 0 ;
 }

From d0364dbbdc8dcb3ace1755729b696ec9ecaaa626 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 22 Apr 2024 17:25:11 +0300
Subject: [PATCH 04/22] Update TODO in 36-apron/91-mine14-5b-no-threshold
 (issue #1425)

---
 tests/regression/36-apron/90-mine14-5b.c               | 2 ++
 tests/regression/36-apron/91-mine14-5b-no-threshhold.c | 4 +++-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/tests/regression/36-apron/90-mine14-5b.c b/tests/regression/36-apron/90-mine14-5b.c
index 13dbd9d41c..a5c4853722 100644
--- a/tests/regression/36-apron/90-mine14-5b.c
+++ b/tests/regression/36-apron/90-mine14-5b.c
@@ -46,6 +46,8 @@ int main(void) {
   pthread_create(&id2, NULL, t_fun2, NULL);
   pthread_mutex_lock(&mutex);
   __goblint_check(x==y);
+  __goblint_check(0 <= x);
+  __goblint_check(x <= 10);
   pthread_mutex_unlock(&mutex);
   return 0;
 }
diff --git a/tests/regression/36-apron/91-mine14-5b-no-threshhold.c b/tests/regression/36-apron/91-mine14-5b-no-threshhold.c
index 05f1cee914..2e1e76dc39 100644
--- a/tests/regression/36-apron/91-mine14-5b-no-threshhold.c
+++ b/tests/regression/36-apron/91-mine14-5b-no-threshhold.c
@@ -46,7 +46,9 @@ int main(void) {
   pthread_create(&id, NULL, t_fun, NULL);
   pthread_create(&id2, NULL, t_fun2, NULL);
   pthread_mutex_lock(&mutex);
-  __goblint_check(x==y); //TODO
+  __goblint_check(x==y);
+  __goblint_check(0 <= x);
+  __goblint_check(x <= 10); // TODO
   pthread_mutex_unlock(&mutex);
   return 0;
 }

From 3e8882b4e484c9dafd317ddcf5d082f2785fe108 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 22 Apr 2024 17:34:39 +0300
Subject: [PATCH 05/22] Disable expRelation in 36-apron/34-large-bigint

This makes the check meaningful again.
---
 tests/regression/36-apron/34-large-bigint.c | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tests/regression/36-apron/34-large-bigint.c b/tests/regression/36-apron/34-large-bigint.c
index 22d29311ad..47bb269ac9 100644
--- a/tests/regression/36-apron/34-large-bigint.c
+++ b/tests/regression/36-apron/34-large-bigint.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --set ana.activated[-] expRelation
 #include <goblint.h>
 
 void main() {
@@ -17,6 +17,7 @@ void main() {
       __goblint_check(18446744073709551614ull <= z); // TODO (unknown with D, success with MPQ)
       __goblint_check(z <= 18446744073709551615ull); // TODO (unknown with D, success with MPQ)
 
+      // disable expRelation to prevent base from simplifying x - x to 0
       __goblint_check(x >= x - x); // avoid base from answering to check if apron doesn't say x == -3
       __goblint_check(y >= y - y); // avoid base from answering to check if apron doesn't say y == -3
       __goblint_check(z >= z - z); // avoid base from answering to check if apron doesn't say z == -3

From 8e2004f8251bc823aadc73a32854f20f29e7bdec Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 22 Apr 2024 17:38:05 +0300
Subject: [PATCH 06/22] Fix 36-apron/34-large-bigint to not pass due to def_exc
 range (issue #1425)

---
 tests/regression/36-apron/34-large-bigint.c | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/tests/regression/36-apron/34-large-bigint.c b/tests/regression/36-apron/34-large-bigint.c
index 47bb269ac9..1eead3a1d4 100644
--- a/tests/regression/36-apron/34-large-bigint.c
+++ b/tests/regression/36-apron/34-large-bigint.c
@@ -9,13 +9,13 @@ void main() {
     __goblint_check(y < z);
     __goblint_check(x < z);
 
-    if (18446744073709551612ull <= x && z <= 18446744073709551615ull) {
-      __goblint_check(18446744073709551612ull <= x); // TODO (unknown with D, success with MPQ)
-      __goblint_check(x <= 18446744073709551613ull); // TODO (unknown with D, success with MPQ)
-      __goblint_check(18446744073709551613ull <= y); // TODO (unknown with D, success with MPQ)
-      __goblint_check(y <= 18446744073709551614ull); // TODO (unknown with D, success with MPQ)
-      __goblint_check(18446744073709551614ull <= z); // TODO (unknown with D, success with MPQ)
-      __goblint_check(z <= 18446744073709551615ull); // TODO (unknown with D, success with MPQ)
+    if (18446744073709551611ull <= x && z <= 18446744073709551614ull) {
+      __goblint_check(18446744073709551611ull <= x); // TODO (unknown with D, success with MPQ)
+      __goblint_check(x <= 18446744073709551612ull); // TODO (unknown with D, success with MPQ)
+      __goblint_check(18446744073709551612ull <= y); // TODO (unknown with D, success with MPQ)
+      __goblint_check(y <= 18446744073709551613ull); // TODO (unknown with D, success with MPQ)
+      __goblint_check(18446744073709551613ull <= z); // TODO (unknown with D, success with MPQ)
+      __goblint_check(z <= 18446744073709551614ull); // TODO (unknown with D, success with MPQ)
 
       // disable expRelation to prevent base from simplifying x - x to 0
       __goblint_check(x >= x - x); // avoid base from answering to check if apron doesn't say x == -3

From 29de6bc0639bb42c88c87f46da627604b9143bb7 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 22 Apr 2024 17:41:30 +0300
Subject: [PATCH 07/22] Remove TODO from 36-apron/42-threadenter-arg (issue
 #1425)

---
 tests/regression/36-apron/42-threadenter-arg.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/regression/36-apron/42-threadenter-arg.c b/tests/regression/36-apron/42-threadenter-arg.c
index 0ccb8712a4..27b13c21f8 100644
--- a/tests/regression/36-apron/42-threadenter-arg.c
+++ b/tests/regression/36-apron/42-threadenter-arg.c
@@ -2,8 +2,8 @@
 #include <pthread.h>
 #include <goblint.h>
 
-void *t_fun(int arg) {
-  __goblint_check(arg == 3); // TODO (cast through void*)
+void *t_fun(int arg) { // check that apron doesn't crash with tracked thread argument
+  __goblint_check(arg == 3); // cast through void*, passes by base
   return NULL;
 }
 

From fa55034febbd88614e9c274ca53f639408269360 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 23 Apr 2024 10:40:12 +0300
Subject: [PATCH 08/22] Enable base protection-atomic in
 46-apron2/75-mutex_with_ghosts (issue #1425)

This was used before f754362c61302119850cd97fe777678ebfc565b8 changed the default.
---
 tests/regression/46-apron2/75-mutex_with_ghosts.c | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tests/regression/46-apron2/75-mutex_with_ghosts.c b/tests/regression/46-apron2/75-mutex_with_ghosts.c
index c784720aee..7808feea39 100644
--- a/tests/regression/46-apron2/75-mutex_with_ghosts.c
+++ b/tests/regression/46-apron2/75-mutex_with_ghosts.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none
+// SKIP PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set sem.int.signed_overflow assume_none --set ana.base.privatization protection-atomic
 /*-----------------------------------------------------------------------------
  * mutex_with_ghosts.c - Annotated concurrent program with ghost variables for
  *                       witness validation using locking to access a shared
@@ -53,6 +53,7 @@ int main()
   pthread_mutex_lock(&m);
   __VERIFIER_atomic_end();
 
+  // TODO: works with base protection privatization but not protection-atomic
   __goblint_check(used == 0); // TODO (read/refine? of used above makes used write-unprotected)
 
   __VERIFIER_atomic_begin();

From d5081d7dd47d1e5c274d41e427df08c668593b37 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 23 Apr 2024 10:47:58 +0300
Subject: [PATCH 09/22] Remove TODO from
 78-termination/25-leave-loop-goto-terminating (issue #1425)

Passing again since f81ca2c0346716ada6abfc51f09dbf9143dc34c1.
---
 .../regression/78-termination/25-leave-loop-goto-terminating.c  | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/regression/78-termination/25-leave-loop-goto-terminating.c b/tests/regression/78-termination/25-leave-loop-goto-terminating.c
index b882759bff..61c8b8f58d 100644
--- a/tests/regression/78-termination/25-leave-loop-goto-terminating.c
+++ b/tests/regression/78-termination/25-leave-loop-goto-terminating.c
@@ -1,4 +1,4 @@
-// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra
+// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra
 #include <stdio.h>
 
 int main()

From 46b9096bbf4dd2feb75ca2da7d086b989d9c495d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 23 Apr 2024 11:04:48 +0300
Subject: [PATCH 10/22] Remove TODO from
 78-termination/28-do-while-continue-terminating (issue #1425)

Passing again since 5d291caf43da73d24f3093ec36cced018972cc30.
It provides more precise locations.
---
 .../78-termination/28-do-while-continue-terminating.c        | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tests/regression/78-termination/28-do-while-continue-terminating.c b/tests/regression/78-termination/28-do-while-continue-terminating.c
index a61174d295..d3b424f9b0 100644
--- a/tests/regression/78-termination/28-do-while-continue-terminating.c
+++ b/tests/regression/78-termination/28-do-while-continue-terminating.c
@@ -1,4 +1,4 @@
-// SKIP TODO TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra
+// SKIP TERM PARAM: --set "ana.activated[+]" termination --set ana.activated[+] apron --enable ana.int.interval --set ana.apron.domain polyhedra
 #include <stdio.h>
 
 int main()
@@ -22,7 +22,8 @@ int main()
 }
 
 /*
-NOTE:
+NOTE: The description below is probably outdated. This works since 5d291caf43da73d24f3093ec36cced018972cc30.
+
 Test 28: does not terminate but should terminate (test case
 "28-do-while-continue-terminating.c") Reason: upjumping goto
 

From 78289be423430ac31cd68e8d9487b8e71b0ee962 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Apr 2024 10:41:40 +0300
Subject: [PATCH 11/22] Add OSX reachability workaround to
 04-mutex/58-pthread-lock-return

---
 .../04-mutex/58-pthread-lock-return.c         | 20 +++++++++++++++----
 1 file changed, 16 insertions(+), 4 deletions(-)

diff --git a/tests/regression/04-mutex/58-pthread-lock-return.c b/tests/regression/04-mutex/58-pthread-lock-return.c
index 3e2a05c94e..1753cd4349 100644
--- a/tests/regression/04-mutex/58-pthread-lock-return.c
+++ b/tests/regression/04-mutex/58-pthread-lock-return.c
@@ -68,9 +68,10 @@ void *t_fun(void *arg) {
     __goblint_check(1); // reachable
   }
 
+  int reach1 = 0, reach2 = 0, reach3 = 0;
 #ifndef __APPLE__
   if (!pthread_spin_lock(&spin)) {
-    __goblint_check(1); // TODO reachable (TODO for OSX)
+    reach1 = 1;
     g_spin++; // NORACE
     pthread_spin_unlock(&spin);
   }
@@ -79,14 +80,25 @@ void *t_fun(void *arg) {
   }
 
   if (!pthread_spin_trylock(&spin)) {
-    __goblint_check(1); // TODO reachable (TODO for OSX)
+    reach2 = 1;
     g_spin++; // NORACE
     pthread_spin_unlock(&spin);
   }
   else {
-    __goblint_check(1); // TODO reachable (TODO for OSX)
-  }
+    reach3 = 1;
+  }
+#else
+  // fake values so test passes on OSX
+  reach1 = 1;
+  int r;
+  if (r)
+    reach2 = 1;
+  else
+    reach3 = 1;
 #endif
+  __goblint_check(reach1); // always reached
+  __goblint_check(reach2); // UNKNOWN (sometimes reached)
+  __goblint_check(reach3); // UNKNOWN (sometimes reached)
 
   return NULL;
 }

From a072b2101c6de723433385af981bfb8ef51a8ffc Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Apr 2024 10:50:41 +0300
Subject: [PATCH 12/22] Add OSX workaround to 57-floats/15-more-library

---
 tests/regression/57-floats/15-more-library.c | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/tests/regression/57-floats/15-more-library.c b/tests/regression/57-floats/15-more-library.c
index 29c6cec185..59aa9081f0 100644
--- a/tests/regression/57-floats/15-more-library.c
+++ b/tests/regression/57-floats/15-more-library.c
@@ -39,7 +39,13 @@ int main(void)
     // On OS X this gets expanded differently than on Linux where it is equivalent to the one below
     // Might make sense to check what is needed for OS X support in the future, but this is not a deal-breaker
     // and not high priority for now.
-    __goblint_check(isinf(INFINITY) && signbit(c)); //TODO
+    int check1;
+#ifndef __APPLE__
+    check1 = isinf(INFINITY) && signbit(c);
+#else
+    check1 = 1; // fake value so test passes on OSX
+#endif
+    __goblint_check(check1);
     __goblint_check(isinf(INFINITY) && __builtin_signbit(c));
 
     __goblint_check(floor(2.7) == 2.0);
@@ -53,7 +59,13 @@ int main(void)
     // On OS X this gets expanded differently than on Linux where it is equivalent to the one below
     // Might make sense to check what is needed for OS X support in the future, but this is not a deal-breaker
     // and not high priority for now.
-    __goblint_check(isinf(INFINITY) && signbit(c)); //TODO
+    int check2;
+#ifndef __APPLE__
+    check2 = isinf(INFINITY) && signbit(c);
+#else
+    check2 = 1; // fake value so test passes on OSX
+#endif
+    __goblint_check(check2);
     __goblint_check(isinf(INFINITY) && __builtin_signbit(c));
 
     // Check globals have not been invalidated

From 1ae609aedf52655779eb32dc780abe0eb2920a43 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Apr 2024 10:51:52 +0300
Subject: [PATCH 13/22] Add OSX workaround to 57-floats/17-other

---
 tests/regression/57-floats/17-other.c | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/tests/regression/57-floats/17-other.c b/tests/regression/57-floats/17-other.c
index 239921bfb7..fba7c3f4b5 100644
--- a/tests/regression/57-floats/17-other.c
+++ b/tests/regression/57-floats/17-other.c
@@ -15,7 +15,13 @@ int main()
   // On OS X this gets expanded differently than on Linux where it is equivalent to the one below
   // Might make sense to check what is needed for OS X support in the future, but this is not a deal-breaker
   // and not high priority for now.
-  __goblint_check((isnormal(FLT_MAX))); //TODO
+  int check1;
+#ifndef __APPLE__
+  check1 = (isnormal(FLT_MAX));
+#else
+  check1 = 1; // fake value so test passes on OSX
+#endif
+    __goblint_check(check1);
   __goblint_check((__builtin_isnormal(FLT_MAX)));
 
   __goblint_check((isinf(HUGE_VAL)));

From bc4572a2eddc4cef86d79370dc4a0d14469e77a1 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Apr 2024 12:18:19 +0300
Subject: [PATCH 14/22] Fix OSX hack UNKNOWN annotations in
 04-mutex/58-pthread-lock-return

---
 tests/regression/04-mutex/58-pthread-lock-return.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/regression/04-mutex/58-pthread-lock-return.c b/tests/regression/04-mutex/58-pthread-lock-return.c
index 1753cd4349..0ec85117d0 100644
--- a/tests/regression/04-mutex/58-pthread-lock-return.c
+++ b/tests/regression/04-mutex/58-pthread-lock-return.c
@@ -97,8 +97,8 @@ void *t_fun(void *arg) {
     reach3 = 1;
 #endif
   __goblint_check(reach1); // always reached
-  __goblint_check(reach2); // UNKNOWN (sometimes reached)
-  __goblint_check(reach3); // UNKNOWN (sometimes reached)
+  __goblint_check(reach2); // UNKNOWN! (sometimes reached)
+  __goblint_check(reach3); // UNKNOWN! (sometimes reached)
 
   return NULL;
 }

From 86790738ec0e46f6083311355f7a2330cfa1d16e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 25 Apr 2024 12:22:35 +0300
Subject: [PATCH 15/22] Add 36-apron/21-traces-cluster-based name explanation

---
 tests/regression/36-apron/21-traces-cluster-based.c | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tests/regression/36-apron/21-traces-cluster-based.c b/tests/regression/36-apron/21-traces-cluster-based.c
index 1628e986ca..c9d6db7f4a 100644
--- a/tests/regression/36-apron/21-traces-cluster-based.c
+++ b/tests/regression/36-apron/21-traces-cluster-based.c
@@ -1,6 +1,7 @@
 // SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag --enable ana.sv-comp.functions --set ana.relation.privatization mutex-meet
 extern int __VERIFIER_nondet_int();
-// TODO: rename? this doesn't require clusters
+// Normal mutex-meet is enough here, this doesn't require mutex-meet-tid-cluster* (despite the name).
+// The name is "cluster-based" for historical reasons to match the example name in more-traces paper repository.
 #include <pthread.h>
 #include <goblint.h>
 

From 8347413efa5c3536be87503772ee8530d14c6ca5 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 29 Apr 2024 12:20:59 +0300
Subject: [PATCH 16/22] Add tests for top witness invariants

---
 .../56-witness/46-top-bool-invariant.c        |   6 +
 .../56-witness/46-top-bool-invariant.t        | 207 ++++++++++++++++++
 .../56-witness/47-top-int-invariant.c         |   6 +
 .../56-witness/47-top-int-invariant.t         | 176 +++++++++++++++
 4 files changed, 395 insertions(+)
 create mode 100644 tests/regression/56-witness/46-top-bool-invariant.c
 create mode 100644 tests/regression/56-witness/46-top-bool-invariant.t
 create mode 100644 tests/regression/56-witness/47-top-int-invariant.c
 create mode 100644 tests/regression/56-witness/47-top-int-invariant.t

diff --git a/tests/regression/56-witness/46-top-bool-invariant.c b/tests/regression/56-witness/46-top-bool-invariant.c
new file mode 100644
index 0000000000..a70b4202b6
--- /dev/null
+++ b/tests/regression/56-witness/46-top-bool-invariant.c
@@ -0,0 +1,6 @@
+// PARAM: --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set 46-top-bool-invariant.c --disable witness.invariant.inexact-type-bounds
+
+int main() {
+  _Bool x;
+  return 0;
+}
diff --git a/tests/regression/56-witness/46-top-bool-invariant.t b/tests/regression/56-witness/46-top-bool-invariant.t
new file mode 100644
index 0000000000..8503701d71
--- /dev/null
+++ b/tests/regression/56-witness/46-top-bool-invariant.t
@@ -0,0 +1,207 @@
+def_exc only:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    total generation entries: 2
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: 46-top-bool-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: x <= (_Bool)1
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 46-top-bool-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: (_Bool)0 <= x
+      type: assertion
+      format: C
+
+interval only:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable ana.int.def_exc --enable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    total generation entries: 2
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: 46-top-bool-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: x <= (_Bool)1
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 46-top-bool-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: (_Bool)0 <= x
+      type: assertion
+      format: C
+
+enums only:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --enable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    total generation entries: 1
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: 46-top-bool-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: x == (_Bool)0 || x == (_Bool)1
+      type: assertion
+      format: C
+
+congruence only:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --enable ana.int.congruence --disable ana.int.interval_set 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    total generation entries: 0
+
+  $ yamlWitnessStrip < witness.yml
+  []
+
+interval_set only:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --enable ana.int.interval_set 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    total generation entries: 2
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: 46-top-bool-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: x <= (_Bool)1
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 46-top-bool-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: (_Bool)0 <= x
+      type: assertion
+      format: C
+
+all:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set 46-top-bool-invariant.c --enable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    total generation entries: 3
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: 46-top-bool-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: x == (_Bool)0 || x == (_Bool)1
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 46-top-bool-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: x <= (_Bool)1
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 46-top-bool-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: (_Bool)0 <= x
+      type: assertion
+      format: C
+
+all without inexact-type-bounds:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set 46-top-bool-invariant.c --disable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    total generation entries: 1
+
+TODO: should not have any invariants
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: 46-top-bool-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: x == (_Bool)0 || x == (_Bool)1
+      type: assertion
+      format: C
diff --git a/tests/regression/56-witness/47-top-int-invariant.c b/tests/regression/56-witness/47-top-int-invariant.c
new file mode 100644
index 0000000000..84b058e591
--- /dev/null
+++ b/tests/regression/56-witness/47-top-int-invariant.c
@@ -0,0 +1,6 @@
+// PARAM: --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set 47-top-int-invariant.c --disable witness.invariant.inexact-type-bounds
+
+int main() {
+  int x;
+  return 0;
+}
diff --git a/tests/regression/56-witness/47-top-int-invariant.t b/tests/regression/56-witness/47-top-int-invariant.t
new file mode 100644
index 0000000000..0fa7e9a11c
--- /dev/null
+++ b/tests/regression/56-witness/47-top-int-invariant.t
@@ -0,0 +1,176 @@
+def_exc only:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    total generation entries: 2
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: 47-top-int-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: x <= 2147483647
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 47-top-int-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: (-0x7FFFFFFF-1) <= x
+      type: assertion
+      format: C
+
+interval only:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable ana.int.def_exc --enable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    total generation entries: 2
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: 47-top-int-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: x <= 2147483647
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 47-top-int-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: (-0x7FFFFFFF-1) <= x
+      type: assertion
+      format: C
+
+enums only:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --enable ana.int.enums --disable ana.int.congruence --disable ana.int.interval_set 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    total generation entries: 0
+
+TODO: should have range invariants
+
+  $ yamlWitnessStrip < witness.yml
+  []
+
+congruence only:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --enable ana.int.congruence --disable ana.int.interval_set 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    total generation entries: 0
+
+  $ yamlWitnessStrip < witness.yml
+  []
+
+interval_set only:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --disable ana.int.def_exc --disable ana.int.interval --disable ana.int.enums --disable ana.int.congruence --enable ana.int.interval_set 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    total generation entries: 2
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: 47-top-int-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: x <= 2147483647
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 47-top-int-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: (-0x7FFFFFFF-1) <= x
+      type: assertion
+      format: C
+
+all:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set 47-top-int-invariant.c --enable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    total generation entries: 2
+
+  $ yamlWitnessStrip < witness.yml
+  - entry_type: location_invariant
+    location:
+      file_name: 47-top-int-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: x <= 2147483647
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 47-top-int-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: (-0x7FFFFFFF-1) <= x
+      type: assertion
+      format: C
+
+all without inexact-type-bounds:
+
+  $ goblint --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set 47-top-int-invariant.c --disable witness.invariant.inexact-type-bounds
+  [Info][Deadcode] Logical lines of code (LLoC) summary:
+    live: 2
+    dead: 0
+    total lines: 2
+  [Info][Witness] witness generation summary:
+    total generation entries: 0
+
+  $ yamlWitnessStrip < witness.yml
+  []

From a09b7207df4a0c4a5679b457bac58bfb22c7a33c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 29 Apr 2024 12:23:47 +0300
Subject: [PATCH 17/22] Add range invariants to enums domain

---
 src/cdomain/value/cdomains/intDomain.ml       | 14 ++++++++--
 .../56-witness/47-top-int-invariant.t         | 27 ++++++++++++++++---
 2 files changed, 35 insertions(+), 6 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index b18a732be0..ecacdaee87 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -2731,11 +2731,21 @@ module Enums : S with type int_t = Z.t = struct
           ) (Invariant.bot ()) (BISet.elements ps)
       else
         Invariant.top ()
-    | Exc (ns, _) ->
+    | Exc (ns, r) ->
+      (* Emit range invariant if tighter than ikind bounds.
+         This can be more precise than interval, which has been widened. *)
+      let (rmin, rmax) = (Exclusion.min_of_range r, Exclusion.max_of_range r) in
+      let (ikmin, ikmax) =
+        let ikr = size ik in
+        (Exclusion.min_of_range ikr, Exclusion.max_of_range ikr)
+      in
+      let inexact_type_bounds = get_bool "witness.invariant.inexact-type-bounds" in
+      let imin = if inexact_type_bounds || Z.compare ikmin rmin <> 0 then Invariant.of_exp Cil.(BinOp (Le, kintegerCilint ik rmin, e, intType)) else Invariant.none in
+      let imax = if inexact_type_bounds || Z.compare rmax ikmax <> 0 then Invariant.of_exp Cil.(BinOp (Le, e, kintegerCilint ik rmax, intType)) else Invariant.none in
       List.fold_left (fun a x ->
           let i = Invariant.of_exp Cil.(BinOp (Ne, e, kintegerCilint ik x, intType)) in
           Invariant.(a && i)
-        ) (Invariant.top ()) (BISet.elements ns)
+        ) Invariant.(imin && imax) (BISet.elements ns)
 
 
   let arbitrary ik =
diff --git a/tests/regression/56-witness/47-top-int-invariant.t b/tests/regression/56-witness/47-top-int-invariant.t
index 0fa7e9a11c..cdfe65673f 100644
--- a/tests/regression/56-witness/47-top-int-invariant.t
+++ b/tests/regression/56-witness/47-top-int-invariant.t
@@ -74,12 +74,31 @@ enums only:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
-    total generation entries: 0
-
-TODO: should have range invariants
+    total generation entries: 2
 
   $ yamlWitnessStrip < witness.yml
-  []
+  - entry_type: location_invariant
+    location:
+      file_name: 47-top-int-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: x <= 2147483647
+      type: assertion
+      format: C
+  - entry_type: location_invariant
+    location:
+      file_name: 47-top-int-invariant.c
+      file_hash: $FILE_HASH
+      line: 5
+      column: 3
+      function: main
+    location_invariant:
+      string: (-0x7FFFFFFF-1) <= x
+      type: assertion
+      format: C
 
 congruence only:
 

From 0ab54ba7b11aa286705af5b8534be61f31564430 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 29 Apr 2024 12:25:35 +0300
Subject: [PATCH 18/22] Use Set.fold in IntDomain.Enums.invariant_ikind

---
 src/cdomain/value/cdomains/intDomain.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index ecacdaee87..fb0b78c6f7 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -2725,10 +2725,10 @@ module Enums : S with type int_t = Z.t = struct
     match x with
     | Inc ps ->
       if BISet.cardinal ps > 1 || get_bool "witness.invariant.exact" then
-        List.fold_left (fun a x ->
+        BISet.fold (fun x a ->
             let i = Invariant.of_exp Cil.(BinOp (Eq, e, kintegerCilint ik x, intType)) in
             Invariant.(a || i) [@coverage off] (* bisect_ppx cannot handle redefined (||) *)
-          ) (Invariant.bot ()) (BISet.elements ps)
+          ) ps (Invariant.bot ())
       else
         Invariant.top ()
     | Exc (ns, r) ->
@@ -2742,10 +2742,10 @@ module Enums : S with type int_t = Z.t = struct
       let inexact_type_bounds = get_bool "witness.invariant.inexact-type-bounds" in
       let imin = if inexact_type_bounds || Z.compare ikmin rmin <> 0 then Invariant.of_exp Cil.(BinOp (Le, kintegerCilint ik rmin, e, intType)) else Invariant.none in
       let imax = if inexact_type_bounds || Z.compare rmax ikmax <> 0 then Invariant.of_exp Cil.(BinOp (Le, e, kintegerCilint ik rmax, intType)) else Invariant.none in
-      List.fold_left (fun a x ->
+      BISet.fold (fun x a ->
           let i = Invariant.of_exp Cil.(BinOp (Ne, e, kintegerCilint ik x, intType)) in
           Invariant.(a && i)
-        ) Invariant.(imin && imax) (BISet.elements ns)
+        ) ns Invariant.(imin && imax)
 
 
   let arbitrary ik =

From 9734040eadfe49545c0958c43bb4038bca16fad3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 29 Apr 2024 12:36:45 +0300
Subject: [PATCH 19/22] Fix PARAM for
 56-witness/{46,47}-top-{bool,int}-invariant

---
 tests/regression/56-witness/46-top-bool-invariant.c | 2 +-
 tests/regression/56-witness/47-top-int-invariant.c  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/regression/56-witness/46-top-bool-invariant.c b/tests/regression/56-witness/46-top-bool-invariant.c
index a70b4202b6..2c90a55a2d 100644
--- a/tests/regression/56-witness/46-top-bool-invariant.c
+++ b/tests/regression/56-witness/46-top-bool-invariant.c
@@ -1,4 +1,4 @@
-// PARAM: --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set 46-top-bool-invariant.c --disable witness.invariant.inexact-type-bounds
+// PARAM: --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set --disable witness.invariant.inexact-type-bounds
 
 int main() {
   _Bool x;
diff --git a/tests/regression/56-witness/47-top-int-invariant.c b/tests/regression/56-witness/47-top-int-invariant.c
index 84b058e591..45f6106ce8 100644
--- a/tests/regression/56-witness/47-top-int-invariant.c
+++ b/tests/regression/56-witness/47-top-int-invariant.c
@@ -1,4 +1,4 @@
-// PARAM: --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set 47-top-int-invariant.c --disable witness.invariant.inexact-type-bounds
+// PARAM: --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant"]' --enable ana.int.def_exc --enable ana.int.interval --enable ana.int.enums --enable ana.int.congruence --enable ana.int.interval_set --disable witness.invariant.inexact-type-bounds
 
 int main() {
   int x;

From 4f97122028d628d85a365b991e853a4aa060121b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 29 Apr 2024 12:37:01 +0300
Subject: [PATCH 20/22] Remove duplicate IntDomain.Dec_exc.top_of

---
 src/cdomain/value/cdomains/intDomain.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index fb0b78c6f7..ee7d098ca2 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -1910,7 +1910,6 @@ struct
     | `Definite x -> if i = x then `Eq else `Neq
     | `Excluded (s,r) -> if S.mem i s then `Neq else `Top
 
-  let top_of ik = `Excluded (S.empty (), size ik)
   let cast_to ?(suppress_ovwarn=false) ?torg ?no_ov ik = function
     | `Excluded (s,r) ->
       let r' = size ik in

From 2eb288f1dd258fd7b3011e49a1a2b6b906cfebfc Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 29 Apr 2024 12:39:28 +0300
Subject: [PATCH 21/22] Fix IntDomain.Enums.invariant_ikind for top_bool

---
 src/cdomain/value/cdomains/intDomain.ml          |  9 +++++++--
 .../56-witness/46-top-bool-invariant.t           | 16 ++--------------
 2 files changed, 9 insertions(+), 16 deletions(-)

diff --git a/src/cdomain/value/cdomains/intDomain.ml b/src/cdomain/value/cdomains/intDomain.ml
index ee7d098ca2..d8fe147d67 100644
--- a/src/cdomain/value/cdomains/intDomain.ml
+++ b/src/cdomain/value/cdomains/intDomain.ml
@@ -2418,10 +2418,13 @@ module Enums : S with type int_t = Z.t = struct
   type int_t = Z.t
   let name () = "enums"
   let bot () = failwith "bot () not implemented for Enums"
-  let top_of ik = Exc (BISet.empty (), size ik)
   let top () = failwith "top () not implemented for Enums"
   let bot_of ik = Inc (BISet.empty ())
   let top_bool = Inc (BISet.of_list [Z.zero; Z.one])
+  let top_of ik =
+    match ik with
+    | IBool -> top_bool
+    | _ -> Exc (BISet.empty (), size ik)
 
   let range ik = Size.range ik
 
@@ -2721,7 +2724,10 @@ module Enums : S with type int_t = Z.t = struct
   let ne ik x y = c_lognot ik (eq ik x y)
 
   let invariant_ikind e ik x =
+    let inexact_type_bounds = get_bool "witness.invariant.inexact-type-bounds" in
     match x with
+    | Inc ps when not inexact_type_bounds && ik = IBool && is_top_of ik x ->
+      Invariant.none
     | Inc ps ->
       if BISet.cardinal ps > 1 || get_bool "witness.invariant.exact" then
         BISet.fold (fun x a ->
@@ -2738,7 +2744,6 @@ module Enums : S with type int_t = Z.t = struct
         let ikr = size ik in
         (Exclusion.min_of_range ikr, Exclusion.max_of_range ikr)
       in
-      let inexact_type_bounds = get_bool "witness.invariant.inexact-type-bounds" in
       let imin = if inexact_type_bounds || Z.compare ikmin rmin <> 0 then Invariant.of_exp Cil.(BinOp (Le, kintegerCilint ik rmin, e, intType)) else Invariant.none in
       let imax = if inexact_type_bounds || Z.compare rmax ikmax <> 0 then Invariant.of_exp Cil.(BinOp (Le, e, kintegerCilint ik rmax, intType)) else Invariant.none in
       BISet.fold (fun x a ->
diff --git a/tests/regression/56-witness/46-top-bool-invariant.t b/tests/regression/56-witness/46-top-bool-invariant.t
index 8503701d71..b04d33dda8 100644
--- a/tests/regression/56-witness/46-top-bool-invariant.t
+++ b/tests/regression/56-witness/46-top-bool-invariant.t
@@ -189,19 +189,7 @@ all without inexact-type-bounds:
     dead: 0
     total lines: 2
   [Info][Witness] witness generation summary:
-    total generation entries: 1
-
-TODO: should not have any invariants
+    total generation entries: 0
 
   $ yamlWitnessStrip < witness.yml
-  - entry_type: location_invariant
-    location:
-      file_name: 46-top-bool-invariant.c
-      file_hash: $FILE_HASH
-      line: 5
-      column: 3
-      function: main
-    location_invariant:
-      string: x == (_Bool)0 || x == (_Bool)1
-      type: assertion
-      format: C
+  []

From a9bb17c91092bd8477b4c326ea33dfb498da8dc6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 30 Apr 2024 12:37:01 +0300
Subject: [PATCH 22/22] Add bounds checks on y to 36-apron/{90,91}-mine14-5b*

---
 tests/regression/36-apron/90-mine14-5b.c               | 2 ++
 tests/regression/36-apron/91-mine14-5b-no-threshhold.c | 2 ++
 2 files changed, 4 insertions(+)

diff --git a/tests/regression/36-apron/90-mine14-5b.c b/tests/regression/36-apron/90-mine14-5b.c
index a5c4853722..9cffbc574f 100644
--- a/tests/regression/36-apron/90-mine14-5b.c
+++ b/tests/regression/36-apron/90-mine14-5b.c
@@ -48,6 +48,8 @@ int main(void) {
   __goblint_check(x==y);
   __goblint_check(0 <= x);
   __goblint_check(x <= 10);
+  __goblint_check(0 <= y);
+  __goblint_check(y <= 10);
   pthread_mutex_unlock(&mutex);
   return 0;
 }
diff --git a/tests/regression/36-apron/91-mine14-5b-no-threshhold.c b/tests/regression/36-apron/91-mine14-5b-no-threshhold.c
index 2e1e76dc39..3185274a2d 100644
--- a/tests/regression/36-apron/91-mine14-5b-no-threshhold.c
+++ b/tests/regression/36-apron/91-mine14-5b-no-threshhold.c
@@ -49,6 +49,8 @@ int main(void) {
   __goblint_check(x==y);
   __goblint_check(0 <= x);
   __goblint_check(x <= 10); // TODO
+  __goblint_check(0 <= y);
+  __goblint_check(y <= 10); // TODO
   pthread_mutex_unlock(&mutex);
   return 0;
 }