Add test cases for issues in #324

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,35 @@ 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_325_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)
+
+        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()

tests/test_strings.py

@@ -10,7 +10,7 @@
 
 class TestStrings(unittest.TestCase):
     def get_solver(self):
-        return claripy.SolverStrings(backend=claripy.backends.z3)
+        return claripy.SolverStrings()
 
     def test_concat(self):
         str_concrete = claripy.StringV("conc")