Bug #336: Interpolants where real numbers are used are ignored by BLAST - BLAST - Open-Source Projects

Actions

Copy link

Bug #336

open

Interpolants where real numbers are used are ignored by BLAST

Added by Pavel Shved over 13 years ago. Updated over 12 years ago.

Status:

Open

Priority:

Normal

Assignee:

Pavel Shved

Category:

Target version:

Start date:

08/03/2010

Due date:

% Done:

Estimated time:

Detected in build:

pre-ldv

Platform:

Published in build:

Description

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...