diff options
Diffstat (limited to 'test/Feature/Optimize.c')
-rw-r--r-- | test/Feature/Optimize.c | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/test/Feature/Optimize.c b/test/Feature/Optimize.c new file mode 100644 index 00000000..3c9159c7 --- /dev/null +++ b/test/Feature/Optimize.c @@ -0,0 +1,22 @@ +// RUN: %llvmgcc %s --emit-llvm -O0 -c -o %t2.bc +// RUN: rm -f %t2.log +// RUN: %klee --stop-after-n-instructions=100 --optimize %t2.bc > %t3.log +// RUN: echo "good" > %t3.good +// RUN: diff %t3.log %t3.good + +// should complete by 100 instructions if opt is on + +int main() { + int i, res = 0; + + for (i=1; i<=1000; i++) + res += i; + + if (res == (1000*1001)/2) { + printf("good\n"); + } else { + printf("bad\n"); + } + + return 0; +} |