[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash

1 files changed, 14 insertions, 0 deletions

diff --git a/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol
new file mode 100644
index 00000000..ad45d076
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/special/msg_sender_2.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f() public view {
+		require(msg.sender != address(0));
+		address a = msg.sender;
+		address b = msg.sender;
+		assert(a == b);
+	}
+}
+// ----
+// Warning: (98-108): Assertion checker does not yet implement this expression.
+// Warning: (98-108): Internal error: Expression undefined for SMT solver.