satisfiable state with conflict constraints

[ww9210]

During a ctf, I am using angr to analyze a pwnable challenge, but it seems the satisfiable() function is not working as expected.
The following is one example of a satisfiable state, but its constraints are in conflict, obviously.
Any advice or comments are appreciated, thanks!

The options passed to the state are:
{angr.options.REVERSE_MEMORY_NAME_MAP,
angr.options.SYMBOLIC,
angr.options.TRACK_CONSTRAINTS,
angr.options.TRACK_ACTION_HISTORY,
angr.options.CONSERVATIVE_WRITE_STRATEGY,
angr.options.KEEP_IP_SYMBOLIC,
angr.options.TRACK_CONSTRAINT_ACTIONS,
angr.options.CONSTRAINT_TRACKING_IN_SOLVER
}

In [18]: state.solver._solver.constraints
Out[18]:
[<Bool exp_stdin_mem1283_1322_8 == 48>,
<Bool exp_stdin_mem1286_1325_8 == 0>,
<Bool exp_stdin_mem1281_1320_8 == 5>,
<Bool exp_stdin_mem1285_1324_8 == 0>,
<Bool exp_stdin_mem1280_1319_8 == 96>,
<Bool exp_stdin_mem1282_1321_8 == 0>,
<Bool exp_stdin_mem1287_1326_8 == 0>,
<Bool exp_stdin_mem1284_1323_8 == 0>,
<Bool exp_stdin_mem1380_1419_8 == 0>,
<Bool exp_stdin_mem1377_1416_8 == 0>,
<Bool exp_stdin_mem1383_1422_8 == 0>,
<Bool exp_stdin_mem1382_1421_8 == 0>,
<Bool exp_stdin_mem1378_1417_8 == 0>,
<Bool exp_stdin_mem1376_1415_8 == 0>,
<Bool exp_stdin_mem1381_1420_8 == 0>,
<Bool exp_stdin_mem1379_1418_8 == 0>,
<Bool exp_stdin_mem1384_1423_8 == 0>,
<Bool exp_stdin_mem1385_1424_8 == 0>,
<Bool exp_stdin_mem1386_1425_8 == 0>,
<Bool exp_stdin_mem1387_1426_8 == 0>,
<Bool exp_stdin_mem1388_1427_8 == 0>,
<Bool exp_stdin_mem1389_1428_8 == 0>,
<Bool exp_stdin_mem1390_1429_8 == 0>,
<Bool exp_stdin_mem1391_1430_8 == 0>,
<Bool (exp_stdin_mem1287_1326_8 .. exp_stdin_mem1286_1325_8 .. exp_stdin_mem1285_1324_8 .. exp_stdin_mem1284_1323_8 .. exp_stdin_mem1283_1322_8 .. exp_stdin_mem1282_1321_8 .. exp_stdin_mem1281_1320_8 .. exp_stdin_mem1280_1319_8 + 0x10) == 0xfffff00000000010>,
<Bool mem_fffff00000000010_4135_64{UNINITIALIZED} != 0x0>]

In [19]: state.solver.satisfiable()
Out[19]: True

[ltfish]

Which constraints are conflicting?

[ww9210]

for example, as is shown in the IPython output, the following two constraints are conflicting:

1.exp_stdin_mem1287_1326_8 .. exp_stdin_mem1286_1325_8 .. exp_stdin_mem1285_1324_8 .. exp_stdin_mem1284_1323_8 .. exp_stdin_mem1283_1322_8 .. exp_stdin_mem1282_1321_8 .. exp_stdin_mem1281_1320_8 .. exp_stdin_mem1280_1319_8 + 0x10) == 0xfffff00000000010

2.exp_stdin_mem1283_1322_8 == 48

the above two formulas have different constraints for a symbolic byte: exp_stdin_mem1283_1322_8 .
Maybe I misunderstood the functionality/purpose of state.solver.satisfiable() that it does not actually check if there is any confilicting constraint of a state.

---update---
Maybe the key is in the backend solver.
The reason behind, seems to be, although the state has some constraints(e.g. by print state.solver.constraints), but these constraints seems to be overlooked by the backend solver when it is doing evaluation of expressions or checking satisfiability.
I am not familiar with the solver backend, so the above is just a guess.

[Lukas-Dresel]

@ww9210 can you pull claripy with the newest commit and check if the problem still occurs?

[ww9210]

The fix for claripy works for me, thanks!