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