diff --git a/tests/test_regressions.py b/tests/test_regressions.py index fa969b512..bad78541b 100644 --- a/tests/test_regressions.py +++ b/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() diff --git a/tests/test_strings.py b/tests/test_strings.py index eab801360..4d110c1f2 100644 --- a/tests/test_strings.py +++ b/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")