Calling solver max twice changes the result.

[zwimer]

Description

Calling s.max(x) twice in a row yields different results. I imagine this might be due to caching, as I can see the first invocation of s.max(x) calls out to z3's backend, where as the second one does not. This invocation also adds extra constraints to the solver.

Note: calling min twice also has odd effects, though since the initial return value of s.min(x) is 0, the return value still returns correctly the second time.

Steps to reproduce the bug

>>> import claripy
>>> s = claripy.Solver()
>>> x = claripy.BVS("x", 32)
>>> s.max(x)
4294967295
>>> s.max(x)
0

Environment

New venv with fresh clone of master: https://github.com/angr/claripy/commit/33483ea55d6074270f65e2e2b106016be814430f

Additional context

Notice that s.constraints is changed by the max invocation:

>>> import claripy
>>> s = claripy.Solver()
>>> x = claripy.BVS("x", 32)
>>> s.constraints
[]
>>> s.max(x)
4294967295
>>> s.constraints
[<Bool x_0_32 <= 0xffffffff>]
>>> s.max(x)
0

[zwimer]

PR: https://github.com/angr/claripy/pull/310