From 70bb0eaf95ab6a549f875b845395b31a5d49f99e Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
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')

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