Over subsumption in TRACER-X due to missing UNSAT Core from Pi

[rasoolmaghareh]

The following program exhibits over-subsumption. KLEE is able to find the bug. However, TX misses the bug:

int kappa = 0;

int calculate_output(int input, int a21, int a15, int a12, int a24) {

    if((((a24==1) && (((input == 2) && 
        ((a21==10) || ((a21==8) || (a21==9)))) &&  a12 <=  -43 )) && (a15==8)))
    {
    a15 = 5; 
    a21 = 6; 
    return -1;
    } else if((((a24==1) && ( a12 <=  -43  && ((((a21==7) || (a21==8)) || 
        (a21==9)) && (input == 3)))) && (a15==9)))
    {
    a21 = 10; 
        return 22;
    } else if(( (((a21==7) && ((input == 2) && (a24==1))) &&  a12 <=  -43 )))
    {
    kappa++;
    a15 = 5; 
    a21 = 6; 
    return -1;
    } 
    return -2;
}

int input, output;
int a21;
int a15;
int a12;
int a24;

int main()
{
    // default output
    output = -1;
    klee_make_symbolic(&input, sizeof(int), "input");
    klee_make_symbolic(&a21, sizeof(int), "a21");
    klee_make_symbolic(&a15, sizeof(int), "a15");
    klee_make_symbolic(&a12, sizeof(int), "a12");
    klee_make_symbolic(&a24, sizeof(int), "a24");
    // operate eca engine
    output = calculate_output(input, a21, a15, a12, a24);
    klee_assert(kappa<1);
}

This seems to be due to the pre-solver removing some of the constraints and if a24==1 is changed to a24>1 the error path is found by TRACER-X.

[rasoolmaghareh]

Fixed by #337.