aboutsummaryrefslogtreecommitdiffstats
path: root/test
diff options
context:
space:
mode:
authorLeonardo Alt <leo@ethereum.org>2018-10-25 22:00:09 +0800
committerLeonardo Alt <leo@ethereum.org>2018-11-15 16:12:42 +0800
commit70bb0eaf95ab6a549f875b845395b31a5d49f99e (patch)
tree99853ad465f155d92598d2a152510b066efa395a /test
parent92ebf6606764748229acf07e83dbe3824bde540e (diff)
downloaddexon-solidity-70bb0eaf95ab6a549f875b845395b31a5d49f99e.tar.gz
dexon-solidity-70bb0eaf95ab6a549f875b845395b31a5d49f99e.tar.zst
dexon-solidity-70bb0eaf95ab6a549f875b845395b31a5d49f99e.zip
[SMTChecker] Implement uninterpreted functions and use it for blockhash()
Diffstat (limited to 'test')
-rw-r--r--test/libsolidity/smtCheckerTests/special/blockhash.sol8
1 files changed, 6 insertions, 2 deletions
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