From eb97eca09e20c94924c2235d0ecd1a7cad12b626 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Wed, 27 Sep 2023 11:26:18 +0300
Subject: [PATCH] Remove TODO annotations from passing checks

---
 tests/regression/01-cpa/33-asserts.c                    | 8 ++++----
 tests/regression/28-race_reach/22-deref_read_racefree.c | 2 +-
 tests/regression/66-interval-set-one/51-widen-sides.c   | 6 +++---
 3 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/tests/regression/01-cpa/33-asserts.c b/tests/regression/01-cpa/33-asserts.c
index f8bf6c3132..26efad44fc 100644
--- a/tests/regression/01-cpa/33-asserts.c
+++ b/tests/regression/01-cpa/33-asserts.c
@@ -26,14 +26,14 @@ int main(){
   check(j==6); // assert UNKNOWN
 
   unknown(&k);
-  assume(k==4); // TODO? assert SUCCESS
+  assume(k==4);
   check(k==4);  // assert SUCCESS
 
   unknown(&k);
-  assume(k+1==n); // TODO? FAIL
+  assume(k+1==n);
 
-  assume(n==5);  // TODO? NOWARN
-  assert(0);     // NOWARN
+  assume(n==5);  // contradiction
+  assert(0);     // NOWARN (unreachable)
 
   return 0;
 }
\ No newline at end of file
diff --git a/tests/regression/28-race_reach/22-deref_read_racefree.c b/tests/regression/28-race_reach/22-deref_read_racefree.c
index 3386277083..2e4c5ebbb6 100644
--- a/tests/regression/28-race_reach/22-deref_read_racefree.c
+++ b/tests/regression/28-race_reach/22-deref_read_racefree.c
@@ -17,7 +17,7 @@ int main() {
   create_threads(t);
   q = p;
   pthread_mutex_lock(&mutex);
-  assert_racefree(*q);  // TODO
+  assert_racefree(*q);
   pthread_mutex_unlock(&mutex);
   return 0;
 }
diff --git a/tests/regression/66-interval-set-one/51-widen-sides.c b/tests/regression/66-interval-set-one/51-widen-sides.c
index 72eb1396b1..b086baf026 100644
--- a/tests/regression/66-interval-set-one/51-widen-sides.c
+++ b/tests/regression/66-interval-set-one/51-widen-sides.c
@@ -3,13 +3,13 @@
 
 int further(int n) {
     // Even sides-local can not save us here :(
-    __goblint_check(n <= 1); //TODO
+    __goblint_check(n <= 2); //TODO
 }
 
 
 int fun(int n, const char* arg) {
     // Fails with solvers.td3.side_widen sides, needs sides-local
-    __goblint_check(n <= 1);
+    __goblint_check(n <= 2);
     further(n);
 }
 
@@ -26,5 +26,5 @@ int main() {
     doIt("two");
 
     // In the setting with solvers.td3.side_widen sides, widening happens and the bound is lost
-    fun(1, "org");
+    fun(2, "org");
 }