From dd4e9382651951c71d3454ff70a644071d5a8511 Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Tue, 30 Apr 2019 19:07:57 +0200
Subject: [PATCH] [SMTChecker] Fix ICE in inherited state var

---
 Changelog.md                                  |  2 ++
 libsolidity/formal/SMTChecker.cpp             |  6 ++++--
 .../inheritance/state_variables.sol           | 17 +++++++++++++++
 .../inheritance/state_variables_2.sol         | 21 +++++++++++++++++++
 .../inheritance/state_variables_3.sol         | 18 ++++++++++++++++
 5 files changed, 62 insertions(+), 2 deletions(-)
 create mode 100644 test/libsolidity/smtCheckerTests/inheritance/state_variables.sol
 create mode 100644 test/libsolidity/smtCheckerTests/inheritance/state_variables_2.sol
 create mode 100644 test/libsolidity/smtCheckerTests/inheritance/state_variables_3.sol

diff --git a/Changelog.md b/Changelog.md
index 32a3a3c95..02bbcc353 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -4,10 +4,12 @@ Language Features:
 
 
 Compiler Features:
+ * SMTChecker: Support inherited state variables.
 
 
 Bugfixes:
  * SMTChecker: Fix bad cast in base constructor modifier.
+ * SMTChecker: Fix internal error when visiting state variable inherited from base class.
 
 
 
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 5c062edb2..ae429ea3b 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -78,8 +78,10 @@ void SMTChecker::analyze(SourceUnit const& _source, shared_ptr<Scanner> const& _
 
 bool SMTChecker::visit(ContractDefinition const& _contract)
 {
-	for (auto _var : _contract.stateVariables())
-		createVariable(*_var);
+	for (auto const& contract: _contract.annotation().linearizedBaseContracts)
+		for (auto var : contract->stateVariables())
+			if (*contract == _contract || var->isVisibleInDerivedContracts())
+				createVariable(*var);
 	return true;
 }
 
diff --git a/test/libsolidity/smtCheckerTests/inheritance/state_variables.sol b/test/libsolidity/smtCheckerTests/inheritance/state_variables.sol
new file mode 100644
index 000000000..e0c54d8b9
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/inheritance/state_variables.sol
@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract Base {
+	uint x;
+	uint z;
+	uint private t;
+}
+
+contract C is Base {
+	function f(uint y) public {
+		require(x < 10);
+		require(y < 100);
+		z = x + y;
+		assert(z < 150);
+	}
+}
+// ----
diff --git a/test/libsolidity/smtCheckerTests/inheritance/state_variables_2.sol b/test/libsolidity/smtCheckerTests/inheritance/state_variables_2.sol
new file mode 100644
index 000000000..00d35923f
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/inheritance/state_variables_2.sol
@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract Base1 {
+	uint x;
+	uint private t;
+}
+
+contract Base2 is Base1 {
+	uint z;
+	uint private t;
+}
+
+contract C is Base2 {
+	function f(uint y) public {
+		require(x < 10);
+		require(y < 100);
+		z = x + y;
+		assert(z < 150);
+	}
+}
+// ----
diff --git a/test/libsolidity/smtCheckerTests/inheritance/state_variables_3.sol b/test/libsolidity/smtCheckerTests/inheritance/state_variables_3.sol
new file mode 100644
index 000000000..fda7a1b0d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/inheritance/state_variables_3.sol
@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+contract Base {
+	uint x;
+	uint private t;
+}
+
+contract C is Base {
+
+	uint private z;
+	function f(uint y) public {
+		require(x < 10);
+		require(y < 100);
+		z = x + y;
+		assert(z < 150);
+	}
+}
+// ----