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()

---
 Changelog.md | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'Changelog.md')

diff --git a/Changelog.md b/Changelog.md
index b2b03ae4..fae28bb7 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -6,6 +6,8 @@ Language Features:
 Compiler Features:
  * Build System: LLL is not built anymore by default. Must configure it with CMake as `-DLLL=ON`.
  * Code generator: Do not perform redundant double cleanup on unsigned integers when loading from calldata.
+ * SMTChecker: Support ``msg``, ``tx`` and ``block`` member variables.
+ * SMTChecker: Support ``gasleft()`` and ``blockhash()`` functions.
 
 
 Bugfixes:
-- 
cgit v1.2.3