From e9100c68589f9cfab4121376b4d5606ccb88b732 Mon Sep 17 00:00:00 2001 From: "Dr. Michael Petter" Date: Fri, 20 Dec 2024 11:17:44 +0100 Subject: [PATCH] duplicate regression test --- .../36-refinement-oppositebounds.c | 19 ------------------- 1 file changed, 19 deletions(-) delete mode 100644 tests/regression/77-lin2vareq/36-refinement-oppositebounds.c 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; -} - -