Why the result of the solver is wrong in this sample?

[CAFA1]

This is the tested sample in c code(data_flow.c).

#include <stdio.h>
#include <unistd.h>
#include <string.h>
char check(char*x,char*y)
{
    if(strcmp(x,y))
        return strcmp(x,y);
    else
        return strcmp(x,y);
}
int main(int argc, char*argv[])
{
    char x[100];
    read(0,x,100);
    if(check(x,"pwdpwdpwd\n")==0)
        printf("pwd cmd\n");
    else
        printf("no pwd cmd\n");
    if(check(x,"cwdcwdcwd\n")==0)
        printf("cwd cmd\n");
    else
        printf("no cwd cmd\n");
    return 1;
}

Compile it with the command: gcc -g -o data_flow data_flow.c Fuzz it using the command: ./shellphuzz -c 1 -d 1 -f 10 --no-dictionary ../test/data_flow/data_flow I find the solved value of the new sample by driller is wrong . For example, it should be "pwdpwdpwd\n", but the solved value is "pwdp". I print out the constraints( state.se.constraints), and I confirm that it should be "pwdpwdpwd\n" manually. Is the solver wrong???? My github url is git@github.com:CAFA1/long-driller.git.

[rhelmot]

Can you set this up as a testcase which doesn't involve invoking driller?

[CAFA1]

I have solve this problem. Thank you.