Linux Driver Verification » BLAST

Here's a sample code:

int undef();
void error_state()
{
    ERROR: goto ERROR;
}
int main()
{
    int M,x;
    M = 3333;
    undef();
    x = M;
    if (x == 0) error_state();
}

Instead of interpolant M <= 10000, an equivalent 0.0002 * M <= 2 is yielded by CSISAT. However, BLAST yields "false" interpolant when reading it. This is seemingly caused by mere discarding interpolant expressed in terms BLAST doesn't understand.

We should convert such interpolant to the one using integers only, or think about something else...