[klee-dev] Fatal Error in BVTypeCheck

[Jingde Liu]

Hi everyone,

I encounter the following problem when using KLEE to execute a simple
program.

The code of the program is as bellow:
________________________________________
int test(int x) {
    int a;
    if(x>100)
    {
        a = x / 100;
        if(a > 10)
            return x;
    }
    return 0;
}
_________________________________________
After ran it using KLEE, it showed this error:
Fatal Error: BVTypeCheck: terms in atomic formulas must be of equal length
But when I ran it using Cloud9, it was OK.
I don't know how to handle this problem.
Any help is truly appreciated.
-------------- next part --------------
HTML attachment scrubbed and removed