From 84b803d30b6128a014e6cb72f3efccd1e7083ed9 Mon Sep 17 00:00:00 2001
From: Nikhil <nikhilparasaram@gmail.com>
Date: Thu, 24 Oct 2019 14:30:14 +0100
Subject: [PATCH] Add more tests

---
 tests/laser/keccak_tests.py | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

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