diff --git a/tests/regression/77-lin2vareq/36-refinement-oppositebounds.c b/tests/regression/77-lin2vareq/36-refinement-oppositebounds.c deleted file mode 100644 index c930a1610d..0000000000 --- a/tests/regression/77-lin2vareq/36-refinement-oppositebounds.c +++ /dev/null @@ -1,19 +0,0 @@ -//SKIP PARAM: --enable ana.int.interval --set sem.int.signed_overflow assume_none --set ana.activated[+] lin2vareq -// motivated from SVCOMP's terminator_02-1.c -// checks, whether the lin2var interval refinement meddles with the wrong bounds - -#include - -int main() -{ - int x; - if(x<100) - { - __goblint_check(x<100); //SUCCESS - x=x; - } - __goblint_check(x>=-2147483647); //UNKNOWN - return 0; -} - -