2 files changed, 14 insertions, 0 deletions
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