/* VERIFY_OPTS: --symbolic */ #include #include #define __sym __attribute__((__annotate__("lart.abstract.symbolic"))) int main() { __sym int x; x = x % 32; int sum = 0; for ( int i = 0; i < x; ++i ) { sum += i; } assert( sum <= 465 ); }