Use threshold widening in Freiburg nondet_inc_with_ghosts

goblint · Oct 20, 2023 · e1e0813 · e1e0813
1 parent 4c54140
commit e1e0813
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c b/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening
 #include <pthread.h>
 #include <assert.h>
 
@@ -19,7 +19,7 @@ void* inc()
     __VERIFIER_atomic_end();
 
     __VERIFIER_atomic_begin();
-    assert(x >= g); // TODO
+    assert(x >= g);
     __VERIFIER_atomic_end();
   }
 

diff --git a/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c b/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening
 #include <pthread.h>
 #include <assert.h>
 
@@ -16,7 +16,7 @@ void* inc()
   __VERIFIER_atomic_end();
 
   __VERIFIER_atomic_begin();
-  assert(x >= g); // TODO
+  assert(x >= g);
   __VERIFIER_atomic_end();
   return 0;
 }