From 533389d18ab33445e6885609e121e5f33fa7155e Mon Sep 17 00:00:00 2001 From: Nikhil Date: Thu, 1 Aug 2019 10:13:38 +0530 Subject: [PATCH] Add a few more tests --- tests/laser/smt/concat_extract_invariance_test.py | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/tests/laser/smt/concat_extract_invariance_test.py b/tests/laser/smt/concat_extract_invariance_test.py index 7c9198d5..4fea3bad 100644 --- a/tests/laser/smt/concat_extract_invariance_test.py +++ b/tests/laser/smt/concat_extract_invariance_test.py @@ -49,3 +49,14 @@ def test_bitvecfunc_arithmetic4(): construct = Concat(output2_, symbol_factory.BitVecVal(0, 256)) assert Extract(511, 256, Extract(511, 256, construct).input_).input_ == input_ + + +def test_bitvecfunc_arithmetic5(): + input_ = symbol_factory.BitVecSym("input", 256) + i1 = symbol_factory.BitVecSym("i", 256) + i1.pseudo_input = input_ + output_ = symbol_factory.BitVecFuncSym( + "Keccak[input]", size=256, func_name="keccak256", input_=i1 + ) + construct = Concat(output_, symbol_factory.BitVecVal(0, 256)) + assert Extract(511, 256, construct).input_.pseudo_input == i1.pseudo_input