eval output is not accurate

[John2008Jm]

I run my program and I store constraint throw one path then I use claripy.solver to solve that constraints, but solver doesn't gave me the accurate values. for example in the code below :

int isleap(int year){
        if(year > 2020){
                return -1;
        }else{
                   if (year % 400 == 0) {
                        if(year > 1999)
                              return 1;
                        else
                              return 0;
                   }
                   else if (year % 100 == 0) {
                      return 0;
                   }

                   else if (year % 4 == 0) {
                        if(year > 1999)
                              return 1;
                        else
                              return 0;
                   }

                   else {
                     return 0;
                   }
        }
}

I have these constraints :

cons=[<Bool (var_1[7:0] .. var_1[15:8] .. var_1[23:16] .. var_1[31:24]) <=s 0x7e4>,
 <Bool (var_1[7:0] .. var_1[15:8] .. var_1[23:16] .. var_1[31:24]) - (SignExt(32, SignExt(32, (var_1[7:0] .. var_1[15:8] .. var_1[23:16] .. var_1[31:24])) * 0x51eb851f[63:32]) >> 0x7[31:0] - SignExt(32, (var_1[7:0] .. var_1[15:8] .. var_1[23:16] .. var_1[31:24])) >> 0x1f[31:0]) * 0x190 == 0x0>,
 <Bool (var_1[7:0] .. var_1[15:8] .. var_1[23:16] .. var_1[31:24]) >s 0x7cf>]

then :

s=claripy.Solver()
s.add(cons)
s.eval(x,5)

solver gave me :

(3490119680,)

I tried this with other programs but I had this problem with them too.
is there any way that I can get accurate values from solver ?

[github-actions]

This issue has been marked as stale because it has no recent activity. Please comment or add the pinned tag to prevent this issue from being closed.

[github-actions]

This issue has been closed due to inactivity.