[klee-dev] symbolic arguments

[Suhabe Bugrara]

Hello,

I'm running KLEE on the following program:

int main(int argc, char* argv[]) {
        if (argc >= 1) {
                printf("zero ");

                if (argv[0][0] == 'c') {
                        printf("one ");
                }
                else {
                        printf("two ");
                }
        }
        else {
                printf("three ");
        }

        return 0;
}

using the following command:

klee --libc=klee --posix-runtime --init-env test.bc --sym-args 0 1 15

I expected the output to be "zero one two three", but actual output is
"zero two". It looks like it's not forking at each of the branches.
Any ideas on where I'm going wrong?

Thanks.

Suhabe