Add test cases for issues in #324

claripy/frontend_mixins/model_cache_mixin.py

@@ -120,6 +120,7 @@ def __init__(self, *args, **kwargs):
         self._min_exhausted = weakref.WeakSet()
         self._max_signed_exhausted = weakref.WeakSet()
         self._min_signed_exhausted = weakref.WeakSet()
+        self._extra_variables = set()
 
     def _blank_copy(self, c):
         super()._blank_copy(c)
@@ -130,6 +131,7 @@ def _blank_copy(self, c):
         c._min_exhausted = weakref.WeakSet()
         c._max_signed_exhausted = weakref.WeakSet()
         c._min_signed_exhausted = weakref.WeakSet()
+        c._extra_variables = set()
 
     def _copy(self, c):
         super()._copy(c)
@@ -140,6 +142,7 @@ def _copy(self, c):
         c._min_exhausted = weakref.WeakSet(self._min_exhausted)
         c._max_signed_exhausted = weakref.WeakSet(self._max_signed_exhausted)
         c._min_signed_exhausted = weakref.WeakSet(self._min_signed_exhausted)
+        c._extra_variables = set(self._extra_variables)
 
     def __setstate__(self, base_state):
         super().__setstate__(base_state)
@@ -150,6 +153,7 @@ def __setstate__(self, base_state):
         self._min_exhausted = weakref.WeakSet()
         self._max_signed_exhausted = weakref.WeakSet()
         self._min_signed_exhausted = weakref.WeakSet()
+        self._extra_variables = set()
 
     #
     # Model cleaning
@@ -257,7 +261,7 @@ def update(self, other):
     def _model_hook(self, m):
         # Z3 might give us solutions for variables that we did not ask for. so we create a new dict with solutions for
         # only the variables that are under the solver's control
-        m_ = {k: v for k, v in m.items() if k in self.variables}
+        m_ = {k: v for k, v in m.items() if k in self.variables or k in self._extra_variables}
         if m_:
             model = ModelCache(m_)
             self._models.add(model)
@@ -351,6 +355,8 @@ def signed_key(v):
 
             return min(cached, key=signed_key if signed else lambda v: v)
 
+        if len(extra_constraints) == 0:
+            self._extra_variables.update(e.variables)
         m = super().min(e, extra_constraints=extra_constraints, signed=signed, exact=exact)
         if len(extra_constraints) == 0:
             (self._min_signed_exhausted if signed else self._min_exhausted).add(e.cache_key)
@@ -368,6 +374,8 @@ def signed_key(v):
 
             return max(cached, key=signed_key if signed else lambda v: v)
 
+        if len(extra_constraints) == 0:
+            self._extra_variables.update(e.variables)
         m = super().max(e, extra_constraints=extra_constraints, signed=signed, exact=exact)
         if len(extra_constraints) == 0:
             (self._max_signed_exhausted if signed else self._max_exhausted).add(e.cache_key)

tests/test_regressions.py

@@ -7,7 +7,7 @@
 
 
 class TestRegressions(unittest.TestCase):
-    def test_issue16(self):
+    def test_issue_16(self):
         s = claripy.SolverComposite()
 
         c = claripy.BVS("test", 32)
@@ -19,6 +19,38 @@ def test_issue16(self):
         assert not s.satisfiable(extra_constraints=[claripy.BVS("lol", 32) == 0])
         assert not s.satisfiable()
 
+    def test_issue_324(self):
+        s = claripy.Solver()
+        x = claripy.BVS("x", 64)
+        y = claripy.BVS("y", 64)
+        s.add(x - y >= 4)
+        s.add(y > 0)
+        assert s.min(x) == 0
+        assert s.min(x, extra_constraints=[x > 0]) == 1
+
+    def test_issue_324_2(self):
+        ast = claripy.BVS("a", 64) + 0xFF
+
+        s1 = claripy.Solver()
+
+        min_1 = s1.min(ast)
+        max_1 = s1.max(ast)
+        min_2 = s1.min(ast)
+        max_2 = s1.max(ast)
+
+        assert min_1 == min_2
+        assert max_1 == max_2
+
+        s2 = claripy.Solver()
+
+        min_3 = s2.min(ast)
+        max_3 = s2.max(ast)
+        min_4 = s2.min(ast)
+        max_4 = s2.max(ast)
+
+        assert min_1 == min_2 == min_3 == min_4
+        assert max_1 == max_2 == max_3 == max_4
+
 
 if __name__ == "__main__":
     unittest.main()