diff options
| author | Leonardo <leo@ethereum.org> | 2018-11-17 16:48:22 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-11-17 16:48:22 +0800 |
| commit | 5be45e736d2b111c9352ca2990a1c7a653c60c55 (patch) | |
| tree | 1c52fe27dbdd73fc43967a427236e1662b74d47c /test | |
| parent | 460c58fbd194fef5add699405238d3ed302a003f (diff) | |
| parent | 70bb0eaf95ab6a549f875b845395b31a5d49f99e (diff) | |
| download | dexon-solidity-5be45e736d2b111c9352ca2990a1c7a653c60c55.tar dexon-solidity-5be45e736d2b111c9352ca2990a1c7a653c60c55.tar.gz dexon-solidity-5be45e736d2b111c9352ca2990a1c7a653c60c55.tar.bz2 dexon-solidity-5be45e736d2b111c9352ca2990a1c7a653c60c55.tar.lz dexon-solidity-5be45e736d2b111c9352ca2990a1c7a653c60c55.tar.xz dexon-solidity-5be45e736d2b111c9352ca2990a1c7a653c60c55.tar.zst dexon-solidity-5be45e736d2b111c9352ca2990a1c7a653c60c55.zip | |
Merge pull request #5307 from ethereum/smt_uf
[SMTChecker] Uninterpreted functions for blockhash()
Diffstat (limited to 'test')
| -rw-r--r-- | test/libsolidity/smtCheckerTests/special/blockhash.sol | 8 |
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 |