From 6027383ae5eeaae25b34a195d613bd2482cb76f4 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Wed, 8 May 2019 17:10:30 +0200
Subject: [PATCH] [SMTChecker] Fix call to function at state var init

---
 libsolidity/formal/SMTChecker.cpp             |  1 -
 .../complex/slither/const_state_variables.sol | 60 +++++++++++++++++++
 2 files changed, 60 insertions(+), 1 deletion(-)
 create mode 100644 test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index d70aa188a..96e7a2f27 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -196,7 +196,6 @@ void SMTChecker::endVisit(FunctionDefinition const&)
 	if (m_callStack.empty())
 	{
 		checkUnderOverflow();
-		removeLocalVariables();
 		solAssert(m_callStack.empty(), "");
 	}
 }
diff --git a/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol b/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol
new file mode 100644
index 000000000..283461876
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/complex/slither/const_state_variables.sol
@@ -0,0 +1,60 @@
+pragma experimental SMTChecker;
+
+
+contract A {
+
+    address constant public MY_ADDRESS = 0xE0f5206BBD039e7b0592d8918820024e2a7437b9;
+    address public myFriendsAddress = 0xc0ffee254729296a45a3885639AC7E10F9d54979;
+
+    uint public used;
+    uint public test = 5;
+
+    uint constant X = 32**22 + 8;
+    string constant TEXT1 = "abc";
+    string text2 = "xyz";
+
+    function setUsed() public {
+        if (msg.sender == MY_ADDRESS) {
+            used = test;
+        }
+    }
+}
+
+
+contract B is A {
+
+    address public mySistersAddress = 0x999999cf1046e68e36E1aA2E0E07105eDDD1f08E;
+
+    function () external {
+        used = 0;
+    }
+
+    function setUsed(uint a) public {
+        if (msg.sender == MY_ADDRESS) {
+            used = a;
+        }
+    }
+}
+
+contract MyConc{
+
+    uint constant A = 1;
+    bytes32 should_be_constant = sha256('abc');
+    uint should_be_constant_2 = A + 1;
+    address not_constant = msg.sender;
+    uint not_constant_2 = getNumber();
+    uint not_constant_3 = 10 + block.number;
+
+    function getNumber() public returns(uint){
+        return block.number;
+    }
+
+}
+// ----
+// Warning: (773-792): This declaration shadows an existing declaration.
+// Warning: (1009-1086): Function state mutability can be restricted to view
+// Warning: (327-332): Assertion checker does not yet support the type of this literal (literal_string "abc").
+// Warning: (353-358): Assertion checker does not yet support the type of this literal (literal_string "xyz").
+// Warning: (834-839): Assertion checker does not yet support the type of this literal (literal_string "abc").
+// Warning: (874-879): Underflow (resulting value less than 0) happens here.
+// Warning: (874-879): Overflow (resulting value larger than 2**256 - 1) happens here.