From 70bb0eaf95ab6a549f875b845395b31a5d49f99e Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 25 Oct 2018 16:00:09 +0200 Subject: [SMTChecker] Implement uninterpreted functions and use it for blockhash() --- test/libsolidity/smtCheckerTests/special/blockhash.sol | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'test/libsolidity') diff --git a/test/libsolidity/smtCheckerTests/special/blockhash.sol b/test/libsolidity/smtCheckerTests/special/blockhash.sol index 1c693914..59a52922 100644 --- a/test/libsolidity/smtCheckerTests/special/blockhash.sol +++ b/test/libsolidity/smtCheckerTests/special/blockhash.sol @@ -2,9 +2,13 @@ pragma experimental SMTChecker; contract C { - function f() public payable { + function f(uint x) public payable { + assert(blockhash(x) > 0); assert(blockhash(2) > 0); + uint y = x; + assert(blockhash(x) == blockhash(y)); } } // ---- -// Warning: (79-103): Assertion violation happens here +// Warning: (85-109): Assertion violation happens here +// Warning: (113-137): Assertion violation happens here -- cgit