Solver.is_true and is_false providing inconsistent behavior

[crclark96]

When using a solver to evaluate boolean expressions, I get different results when using the is_true and is_false functions than I do when using eval. The docs for is_true and is_false state that they may be incorrect if the expression has been simplified by z3, but the following example is extremely simple and I would not expect it to be simplified:

In [1]: import claripy

In [2]: s = claripy.Solver()

In [3]: x = claripy.BVS("x",32)

In [4]: s.add(x==4)
Out[4]: (<Bool x_0_32 == 0x4>,)

In [5]: s.is_true(x==4)
Out[5]: False

In [6]: s.is_false(x!=4)
Out[6]: False

In [7]: s.is_false(x==4)
Out[7]: False

In [8]: s.eval(x==4,1)
Out[8]: (True,)

In [9]: s.eval(x!=4,1)
Out[9]: (False,)

In [10]: s.constraints
Out[10]: [<Bool x_0_32 == 0x4>]

Running python3.6.9 on ubuntu 18.04.

Name: claripy
Version: 8.20.1.7
Summary: An abstraction layer for constraint solvers
Home-page: https://github.com/angr/claripy
Author: None
Author-email: None
License: UNKNOWN
Location: /home/<redacted>/.local/lib/python3.6/site-packages
Requires: decorator, z3-solver, pysmt, future, cachetools
Required-by: angr

[rhelmot]

is_true and is_false are only meant to catch extremely simple cases. In general, our simplifications only handle purely local simplifications, i.e. not requiring context from constraints.

I believe your example will be handled if you use the replacement solver and add x == 4 as a replacement, though.

[crclark96]

I don't pretend to know claripy internals well enough to fully understand why this doesn't work, but it seems to be intended behaviour, so I'll close the issue

Thanks for getting back so quickly!