diff --git a/tests/laser/keccak_tests.py b/tests/laser/keccak_tests.py index 4e018148..8a3ae00e 100644 --- a/tests/laser/keccak_tests.py +++ b/tests/laser/keccak_tests.py @@ -32,13 +32,28 @@ def test_keccak_basic(input1, input2, expected): o1, c1 = keccak_function_manager.create_keccak(input1) o2, c2 = keccak_function_manager.create_keccak(input2) - s.add(c1) - s.add(c2) + s.add(And(c1, c2)) s.add(o1 == o2) assert s.check() == expected +def test_keccak_symbol_and_val(): + """ + check keccak(100) == keccak(n) && n == 10 + :return: + """ + s = Solver() + hundred = symbol_factory.BitVecVal(100, 256) + n = symbol_factory.BitVecSym("n", 256) + o1, c1 = keccak_function_manager.create_keccak(hundred) + o2, c2 = keccak_function_manager.create_keccak(n) + s.add(And(c1, c2)) + s.add(o1 == o2) + s.add(n == symbol_factory.BitVecVal(10, 256)) + assert s.check() == z3.unsat + + def test_keccak_complex_eq(): """ check for keccak(keccak(b)*2) == keccak(keccak(a)*2) && a != b