ModelCacheMixin does not handle extra_constraints correctly for min

[g-kouv]

Description

Calling min with non-empty extra constraints results in an incorrect value, because the expression is found in _min_exhausted and cached results are incorrectly used to calculate the minimum.

A simple reproducer:

import claripy

s = claripy.Solver()
x = claripy.BVS("x", 64)
y = claripy.BVS("y", 64)
s.add(x - y >= 4)
s.add(y > 0)
print(s.min(x))
print(s.min(x, extra_constraints=[x > 1]))

The last line prints 3 even though the correct answer is 2.

A simple solution would skip checking _min_exhausted and using cached results when extra constraints are passed. A related bug seems to has been fixed previously in 9d4b861.

The issue also seems to apply to max and possibly eval.

Steps to reproduce the bug

No response

Environment

No response

Additional context

No response

[SanWieb]

I found a bug which I think it casued by the same issue: ModelCacheMixin takes a invalid solution from the cache.

Reproducer:

import claripy

ast = claripy.BVS("a", 64) + 0xff

s = claripy.Solver()

print("Min 1: ", s.min(ast))
print("Max 1: ", s.max(ast))

print("Min 2: ", s.min(ast))
print("Max 2: ", s.max(ast))

s = claripy.Solver()

print("")
print("Max 1: ", s.max(ast))
print("Min 1: ", s.min(ast))

print("Max 2: ", s.max(ast))
print("Min 2: ", s.min(ast))

Produced output:

Min 1:  0
Max 1:  18446744073709551615
Min 2:  255
Max 2:  18446744073709551615

Max 1:  18446744073709551615
Min 1:  0
Max 2:  257
Min 2:  0