From e2cf5f6ed94c571c7478b9a313f8e4fceee2aec3 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Mon, 22 Oct 2018 18:19:11 +0200
Subject: Add gasleft constraint and use full member access name

---
 test/libsolidity/smtCheckerTests/special/difficulty.sol | 10 ++++++++++
 test/libsolidity/smtCheckerTests/special/gasleft.sol    |  4 ++++
 2 files changed, 14 insertions(+)
 create mode 100644 test/libsolidity/smtCheckerTests/special/difficulty.sol

(limited to 'test/libsolidity/smtCheckerTests/special')

diff --git a/test/libsolidity/smtCheckerTests/special/difficulty.sol b/test/libsolidity/smtCheckerTests/special/difficulty.sol
new file mode 100644
index 00000000..4469d4e5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/difficulty.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(uint difficulty) public view {
+		assert(block.difficulty == difficulty);
+	}
+}
+// ----
+// Warning: (91-129): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/special/gasleft.sol b/test/libsolidity/smtCheckerTests/special/gasleft.sol
index ec56d957..857230fe 100644
--- a/test/libsolidity/smtCheckerTests/special/gasleft.sol
+++ b/test/libsolidity/smtCheckerTests/special/gasleft.sol
@@ -4,7 +4,11 @@ contract C
 {
 	function f() public view {
 		assert(gasleft() > 0);
+		uint g = gasleft();
+		assert(g < gasleft());
+		assert(g >= gasleft());
 	}
 }
 // ----
 // Warning: (76-97): Assertion violation happens here
+// Warning: (123-144): Assertion violation happens here
-- 
cgit