incorrect answer: loop-invgen/heapsort_true-unreach-call.i

[mchalupa]

incorrect answer with and without slicing

[mchalupa]

this code runs ok with klee:

  1 #include <assert.h>
  2 int __VERIFIER_nondet_int();
  3 
  4 void klee_make_symbolic(void *, unsigned long size, const char *);
  5 int main(void)
  6 {
  7   int n,l;
  8   klee_make_symbolic(&n, sizeof n, "n");
  9   if (!(1 <= n && n <= 1000000))
 10         return 0;
 11 
 12   l = n/2 + 1;
 13 
 14   if(l>1) {
 15     l--;
 16   }
 17   assert(l != 0);
 18 
 19   return 0;
 20 }

(we get TRUE), but after optimizing with -instcombine we get FALSE. When running this code with symbiotic (with no -instcombine instruction), we get FALSE and without slicing we get TRUE. With slicing and without any optimizations we get TRUE

[mchalupa]

the wrong answer was because in 'before' optimizations we had -instcombine