Fix inherited state vars for BMC

Changelog.md

@@ -12,6 +12,7 @@ Bugfixes:
  * SMTChecker: Fix internal error when assigning state variable via contract's name.
  * SMTChecker: Fix incorrect counterexamples reported by the CHC engine.
  * SMTChecker: Fix false negative in modifier applied multiple times.
+ * SMTChecker: Fix internal error in the BMC engine when inherited contract from a different source unit has private state variables.
  * Code generator: Fix missing creation dependency tracking for abstract contracts.
 
 

libsolidity/ast/AST.cpp

@@ -84,16 +84,6 @@ TypePointer ImportDirective::type() const
 	return TypeProvider::module(*annotation().sourceUnit);
 }
 
-vector<VariableDeclaration const*> ContractDefinition::stateVariablesIncludingInherited() const
-{
-	vector<VariableDeclaration const*> stateVars;
-	for (auto const& contract: annotation().linearizedBaseContracts)
-		for (auto var: contract->stateVariables())
-			if (*contract == *this || var->isVisibleInDerivedContracts())
-				stateVars.push_back(var);
-	return stateVars;
-}
-
 bool ContractDefinition::derivesFrom(ContractDefinition const& _base) const
 {
 	return util::contains(annotation().linearizedBaseContracts, &_base);

libsolidity/ast/AST.h

@@ -500,7 +500,6 @@ public:
 	std::vector<StructDefinition const*> definedStructs() const { return filteredNodes<StructDefinition>(m_subNodes); }
 	std::vector<EnumDefinition const*> definedEnums() const { return filteredNodes<EnumDefinition>(m_subNodes); }
 	std::vector<VariableDeclaration const*> stateVariables() const { return filteredNodes<VariableDeclaration>(m_subNodes); }
-	std::vector<VariableDeclaration const*> stateVariablesIncludingInherited() const;
 	std::vector<ModifierDefinition const*> functionModifiers() const { return filteredNodes<ModifierDefinition>(m_subNodes); }
 	std::vector<FunctionDefinition const*> definedFunctions() const { return filteredNodes<FunctionDefinition>(m_subNodes); }
 	std::vector<EventDefinition const*> events() const { return filteredNodes<EventDefinition>(m_subNodes); }

libsolidity/formal/SMTEncoder.cpp

@@ -1973,7 +1973,7 @@ void SMTEncoder::initializeFunctionCallParameters(CallableDeclaration const& _fu
 
 void SMTEncoder::createStateVariables(ContractDefinition const& _contract)
 {
-	for (auto var: _contract.stateVariablesIncludingInherited())
+	for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
 		createVariable(*var);
 }
 
@@ -2257,7 +2257,7 @@ void SMTEncoder::resetVariableIndices(VariableIndices const& _indices)
 void SMTEncoder::clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function)
 {
 	solAssert(_contract, "");
-	for (auto var: _contract->stateVariablesIncludingInherited())
+	for (auto var: stateVariablesIncludingInheritedAndPrivate(*_contract))
 		m_context.variable(*var)->resetIndex();
 	if (_function)
 	{

test/libsolidity/smtCheckerTests/imports/private_vars.sol

@@ -0,0 +1,16 @@
+==== Source: ERC20.sol ====
+pragma experimental SMTChecker;
+contract ERC20 {
+    uint256 private a;
+    function f() internal virtual {
+        a = 2;
+    }
+}
+==== Source: Token.sol ====
+pragma experimental SMTChecker;
+import "ERC20.sol";
+contract Token is ERC20 {
+    constructor() {
+      f();
+    }
+}