I am checking this branch on this example, and the subsumptions are not happening. @xuanlinhha can you please check why here the WP interpolant is empty?
#include <klee/klee.h>
int main() {
int count = 2, sum = 0;
int a[5] = {1, 10, 100, 1000, -1};
while (count--) {
int c;
c = choice(a);
if (c == -1) exit(0);
sum += c;
printf("Choice %d Sum %d\n", c, sum);
}
printf("Final Sum %d\n", sum);
klee_assert(sum <= 9000);
}
int choice(int *a) {
int c;
printf("choice(): a[0] = %d\n", a[0]);
klee_make_symbolic(&c, sizeof(unsigned), "c");
if (*a == -1) return -1;
if (c) return choice(a + 1); else { printf("Return %d\n", a[0]); return a[0]; }
}
I am checking this branch on this example, and the subsumptions are not happening. @xuanlinhha can you please check why here the WP interpolant is empty?