diff --git a/tests/regression/63-affeq/20-svcomp-signextension.c b/tests/regression/63-affeq/20-svcomp-signextension.c new file mode 100644 index 0000000000..c5ca3e360a --- /dev/null +++ b/tests/regression/63-affeq/20-svcomp-signextension.c @@ -0,0 +1,25 @@ +// SKIP PARAM: --set ana.activated[+] affeq --set sem.int.signed_overflow assume_none + +#include +int main() { + + unsigned short int allbits = -1; + short int signedallbits = allbits; + int unsignedtosigned = allbits; + unsigned int unsignedtounsigned = allbits; + int signedtosigned = signedallbits; + unsigned int signedtounsigned = signedallbits; + + /* + printf ("unsignedtosigned: %d\n", unsignedtosigned); + printf ("unsignedtounsigned: %u\n", unsignedtounsigned); + printf ("signedtosigned: %d\n", signedtosigned); + printf ("signedtounsigned: %u\n", signedtounsigned); + */ + + if (signedtounsigned == 4294967295) { + return (-1); + } + + return (0); +} diff --git a/tests/regression/77-lin2vareq/34-svcomp-signextension.c b/tests/regression/77-lin2vareq/34-svcomp-signextension.c index 4ebd3bdd02..bebb8e4bf6 100644 --- a/tests/regression/77-lin2vareq/34-svcomp-signextension.c +++ b/tests/regression/77-lin2vareq/34-svcomp-signextension.c @@ -17,8 +17,7 @@ int main() { printf ("signedtounsigned: %u\n", signedtounsigned); */ - if (unsignedtosigned == 65535 && unsignedtounsigned == 65535 && - signedtosigned == -1 && signedtounsigned == 4294967295) { + if (signedtounsigned == 4294967295) { return (-1); }