Merge pull request #10850 from ethereum/smt_fix_super

[SMTChecker] Fix buggy virtual and super

libsolidity/formal/BMC.cpp

@@ -101,9 +101,13 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 	m_errorReporter.clear();
 }
 
-bool BMC::shouldInlineFunctionCall(FunctionCall const& _funCall, ContractDefinition const* _contract)
+bool BMC::shouldInlineFunctionCall(
+	FunctionCall const& _funCall,
+	ContractDefinition const* _scopeContract,
+	ContractDefinition const* _contextContract
+)
 {
-	auto [funDef, contextContract] = functionCallToDefinition(_funCall, _contract);
+	auto funDef = functionCallToDefinition(_funCall, _scopeContract, _contextContract);
 	if (!funDef || !funDef->isImplemented())
 		return false;
 
@@ -508,8 +512,8 @@ void BMC::visitAddMulMod(FunctionCall const& _funCall)
 
 void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 {
-	solAssert(shouldInlineFunctionCall(_funCall, m_currentContract), "");
+	solAssert(shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract), "");
-	auto [funDef, contextContract] = functionCallToDefinition(_funCall, m_currentContract);
+	auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
 	solAssert(funDef, "");
 
 	if (visitedFunction(funDef))
@@ -541,7 +545,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 void BMC::internalOrExternalFunctionCall(FunctionCall const& _funCall)
 {
 	auto const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
-	if (shouldInlineFunctionCall(_funCall, m_currentContract))
+	if (shouldInlineFunctionCall(_funCall, currentScopeContract(), m_currentContract))
 		inlineFunctionCall(_funCall);
 	else if (isPublicGetter(_funCall.expression()))
 	{

libsolidity/formal/BMC.h

@@ -74,7 +74,13 @@ public:
 	std::vector<std::string> unhandledQueries() { return m_interface->unhandledQueries(); }
 
 	/// @returns true if _funCall should be inlined, otherwise false.
-	static bool shouldInlineFunctionCall(FunctionCall const& _funCall, ContractDefinition const* _contract);
+	/// @param _scopeContract The contract that contains the current function being analyzed.
+	/// @param _contextContract The most derived contract, currently being analyzed.
+	static bool shouldInlineFunctionCall(
+		FunctionCall const& _funCall,
+		ContractDefinition const* _scopeContract,
+		ContractDefinition const* _contextContract
+	);
 
 private:
 	/// AST visitors.

libsolidity/formal/CHC.cpp

@@ -254,17 +254,18 @@ void CHC::endVisit(FunctionDefinition const& _function)
 	// Query placeholders for constructors are not created here because
 	// of contracts without constructors.
 	// Instead, those are created in endVisit(ContractDefinition).
-	if (!_function.isConstructor())
+	if (
+		!_function.isConstructor() &&
+		_function.isPublic() &&
+		contractFunctions(*m_currentContract).count(&_function)
+	)
 	{
 		auto sum = summary(_function);
 		auto ifacePre = smt::interfacePre(*m_interfaces.at(m_currentContract), *m_currentContract, m_context);
-		if (_function.isPublic())
-		{
 		auto txConstraints = m_context.state().txConstraints(_function);
 		m_queryPlaceholders[&_function].push_back({txConstraints && sum, errorFlag().currentValue(), ifacePre});
 		connectBlocks(ifacePre, interface(), txConstraints && sum && errorFlag().currentValue() == 0);
 	}
-	}
 
 	m_currentFunction = nullptr;
 
@@ -622,7 +623,8 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 {
 	solAssert(m_currentContract, "");
 
-	auto [function, contract] = functionCallToDefinition(_funCall, m_currentContract);
+	auto scopeContract = currentScopeContract();
+	auto function = functionCallToDefinition(_funCall, scopeContract, m_currentContract);
 	if (function)
 	{
 		if (m_currentFunction && !m_currentFunction->isConstructor())
@@ -633,7 +635,7 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 		// Libraries can have constants as their "state" variables,
 		// so we need to ensure they were constructed correctly.
 		if (function->annotation().contract->isLibrary())
-			m_context.addAssertion(interface(*contract));
+			m_context.addAssertion(interface(*scopeContract));
 	}
 
 	m_context.addAssertion(predicate(_funCall));
@@ -665,7 +667,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
 	solAssert(m_currentContract, "");
-	auto [function, contextContract] = functionCallToDefinition(_funCall, m_currentContract);
+	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
 	if (!function)
 		return;
 
@@ -721,7 +723,7 @@ void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
 	solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
 	solAssert(m_currentContract, "");
-	auto [function, contextContract] = functionCallToDefinition(_funCall, m_currentContract);
+	auto function = functionCallToDefinition(_funCall, currentScopeContract(), m_currentContract);
 	if (!function)
 		return;
 
@@ -959,7 +961,8 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 			auto const& iface = *m_nondetInterfaces.at(contract);
 			addRule(smtutil::Expression::implies(errorFlag().currentValue() == 0, smt::nondetInterface(iface, *contract, m_context, 0, 0)), "base_nondet");
 
-			for (auto const* function: contractFunctions(*contract))
+			auto const& resolved = contractFunctions(*contract);
+			for (auto const* function: contractFunctionsWithoutVirtual(*contract))
 			{
 				for (auto var: function->parameters())
 					createVariable(*var);
@@ -970,7 +973,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 
 				m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));
 
-				if (!function->isConstructor() && function->isPublic())
+				if (!function->isConstructor() && function->isPublic() && resolved.count(function))
 				{
 					auto state1 = stateVariablesAtIndex(1, *contract);
 					auto state2 = stateVariablesAtIndex(2, *contract);
@@ -1215,7 +1218,8 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 	solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
 	solAssert(m_currentContract, "");
-	auto [function, contextContract] = functionCallToDefinition(_funCall, m_currentContract);
+	auto scopeContract = currentScopeContract();
+	auto function = functionCallToDefinition(_funCall, scopeContract, m_currentContract);
 	if (!function)
 		return smtutil::Expression(true);
 
@@ -1232,13 +1236,13 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 
 	auto const* contract = function->annotation().contract;
 	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
-	solAssert(kind != FunctionType::Kind::Internal || contract->isLibrary() || contains(hierarchy, contextContract), "");
+	solAssert(kind != FunctionType::Kind::Internal || contract->isLibrary() || contains(hierarchy, contract), "");
 
 	/// If the call is to a library, we use that library as the called contract.
 	/// If the call is to a contract not in the inheritance hierarchy, we also use that as the called contract.
 	/// Otherwise, the call is to some contract in the inheritance hierarchy of the current contract.
 	/// In this case we use current contract as the called one since the interfaces/predicates are different.
-	auto const* calledContract = contains(hierarchy, contract) ? contextContract : contract;
+	auto const* calledContract = contains(hierarchy, contract) ? m_currentContract : contract;
 	solAssert(calledContract, "");
 
 	bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View;

libsolidity/formal/SMTEncoder.cpp

@@ -30,6 +30,8 @@
 #include <libsmtutil/SMTPortfolio.h>
 #include <libsmtutil/Helpers.h>
 
+#include <range/v3/view.hpp>
+
 #include <boost/range/adaptors.hpp>
 #include <boost/range/adaptor/reversed.hpp>
 
@@ -112,7 +114,7 @@ bool SMTEncoder::visit(ContractDefinition const& _contract)
 	// the constructor.
 	// Constructors are visited as part of the constructor
 	// hierarchy inlining.
-	for (auto const* function: contractFunctions(_contract))
+	for (auto const* function: contractFunctionsWithoutVirtual(_contract))
 		if (!function->isConstructor())
 			function->accept(*this);
 
@@ -776,6 +778,7 @@ void SMTEncoder::initFunction(FunctionDefinition const& _function)
 	createLocalVariables(_function);
 	m_arrayAssignmentHappened = false;
 	clearIndices(m_currentContract, &_function);
+	m_variableUsage.setCurrentFunction(_function);
 	m_checked = true;
 }
 
@@ -2534,6 +2537,14 @@ bool SMTEncoder::visitedFunction(FunctionDefinition const* _funDef)
 	return false;
 }
 
+ContractDefinition const* SMTEncoder::currentScopeContract()
+{
+	for (auto&& f: m_callStack | ranges::views::reverse | ranges::views::keys)
+		if (auto fun = dynamic_cast<FunctionDefinition const*>(f))
+			return fun->annotation().contract;
+	return nullptr;
+}
+
 SMTEncoder::VariableIndices SMTEncoder::copyVariableIndices()
 {
 	VariableIndices indices;
@@ -2678,7 +2689,11 @@ string SMTEncoder::extraComment()
 	return extra;
 }
 
-pair<FunctionDefinition const*, ContractDefinition const*> SMTEncoder::functionCallToDefinition(FunctionCall const& _funCall, ContractDefinition const* _contract)
+FunctionDefinition const* SMTEncoder::functionCallToDefinition(
+	FunctionCall const& _funCall,
+	ContractDefinition const* _scopeContract,
+	ContractDefinition const* _contextContract
+)
 {
 	if (*_funCall.annotation().kind != FunctionCallKind::FunctionCall)
 		return {};
@@ -2690,32 +2705,27 @@ pair<FunctionDefinition const*, ContractDefinition const*> SMTEncoder::functionC
 		calledExpr = innermostTuple(*calledExpr);
 	}
 
-	auto resolveVirtual = [&](auto const* _ref) -> pair<FunctionDefinition const*, ContractDefinition const*> {
+	auto resolveVirtual = [&](auto const* _ref) -> FunctionDefinition const* {
 		VirtualLookup lookup = *_ref->annotation().requiredLookup;
-		solAssert(_contract || lookup == VirtualLookup::Static, "No contract context provided for function lookup resolution!");
+		solAssert(_contextContract || lookup == VirtualLookup::Static, "No contract context provided for function lookup resolution!");
 		auto funDef = dynamic_cast<FunctionDefinition const*>(_ref->annotation().referencedDeclaration);
 		if (!funDef)
-			return {funDef, _contract};
+			return funDef;
-		ContractDefinition const* contextContract = nullptr;
 		switch (lookup)
 		{
 		case VirtualLookup::Virtual:
-			funDef = &funDef->resolveVirtual(*_contract);
+			return &(funDef->resolveVirtual(*_contextContract));
-			contextContract = _contract;
-			break;
 		case VirtualLookup::Super:
 		{
-			auto super = _contract->superContract(*_contract);
+			solAssert(_scopeContract, "");
+			auto super = _scopeContract->superContract(*_contextContract);
 			solAssert(super, "Super contract not available.");
-			funDef = &funDef->resolveVirtual(*_contract, super);
+			return &funDef->resolveVirtual(*_contextContract, super);
-			contextContract = super;
-			break;
 		}
 		case VirtualLookup::Static:
-			contextContract = funDef->annotation().contract;
+			return funDef;
-			break;
 		}
-		return {funDef, contextContract};
+		solAssert(false, "");
 	};
 
 	if (Identifier const* fun = dynamic_cast<Identifier const*>(calledExpr))
@@ -2810,11 +2820,12 @@ ModifierDefinition const* SMTEncoder::resolveModifierInvocation(ModifierInvocati
 	return modifier;
 }
 
-vector<FunctionDefinition const*> const& SMTEncoder::contractFunctions(ContractDefinition const& _contract)
+set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contractFunctions(ContractDefinition const& _contract)
 {
 	if (!m_contractFunctions.count(&_contract))
 	{
-		vector<FunctionDefinition const *> resolvedFunctions = _contract.definedFunctions();
+		auto const& functions = _contract.definedFunctions();
+		set<FunctionDefinition const*, ASTNode::CompareByID> resolvedFunctions(begin(functions), end(functions));
 		for (auto const* base: _contract.annotation().linearizedBaseContracts)
 		{
 			if (base == &_contract)
@@ -2836,7 +2847,7 @@ vector<FunctionDefinition const*> const& SMTEncoder::contractFunctions(ContractD
 						break;
 					}
 				if (!overridden)
-					resolvedFunctions.push_back(baseFunction);
+					resolvedFunctions.insert(baseFunction);
 			}
 		}
 		m_contractFunctions.emplace(&_contract, move(resolvedFunctions));
@@ -2844,6 +2855,22 @@ vector<FunctionDefinition const*> const& SMTEncoder::contractFunctions(ContractD
 	return m_contractFunctions.at(&_contract);
 }
 
+set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contractFunctionsWithoutVirtual(ContractDefinition const& _contract)
+{
+	if (!m_contractFunctionsWithoutVirtual.count(&_contract))
+	{
+		auto allFunctions = contractFunctions(_contract);
+		for (auto const* base: _contract.annotation().linearizedBaseContracts)
+			for (auto const* baseFun: base->definedFunctions())
+				if (!baseFun->isConstructor())
+					allFunctions.insert(baseFun);
+
+		m_contractFunctionsWithoutVirtual.emplace(&_contract, move(allFunctions));
+
+	}
+	return m_contractFunctionsWithoutVirtual.at(&_contract);
+}
+
 SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable)
 {
 	for (auto const* s = &_scopable; s; s = dynamic_cast<Scopable const*>(s->scope()))
@@ -2926,9 +2953,9 @@ set<FunctionCall const*> SMTEncoder::collectABICalls(ASTNode const* _node)
 	return ABIFunctions(_node).abiCalls;
 }
 
-void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contract)
+void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
 {
-	auto [funDef, contextContract] = functionCallToDefinition(_funCall, _contract);
+	auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
 	if (!funDef)
 		return;
 
@@ -2954,9 +2981,9 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall, Contrac
 		defineExpr(_funCall, currentValue(*returnParams.front()));
 }
 
-vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contract)
+vector<smtutil::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract)
 {
-	auto [funDef, contextContract] = functionCallToDefinition(_funCall, _contract);
+	auto funDef = functionCallToDefinition(_funCall, currentScopeContract(), _contextContract);
 	solAssert(funDef, "");
 
 	vector<smtutil::Expression> args;

libsolidity/formal/SMTEncoder.h

@@ -70,7 +70,19 @@ public:
 
 	/// @returns the FunctionDefinition of a FunctionCall
 	/// if possible or nullptr.
-	static std::pair<FunctionDefinition const*, ContractDefinition const*> functionCallToDefinition(FunctionCall const& _funCall, ContractDefinition const* _contract = nullptr);
+	/// @param _scopeContract is the contract that contains the function currently being
+	///        analyzed, if applicable.
+	/// @param _contextContract is the most derived contract currently being analyzed.
+	/// The difference between the two parameters appears in the case of inheritance.
+	/// Let A and B be two contracts so that B derives from A, and A defines a function `f`
+	/// that `B` does not override. Function `f` is visited twice:
+	/// - Once when A is the most derived contract, where both _scopeContract and _contextContract are A.
+	/// - Once when B is the most derived contract, where _scopeContract is A and _contextContract is B.
+	static FunctionDefinition const* functionCallToDefinition(
+		FunctionCall const& _funCall,
+		ContractDefinition const* _scopeContract,
+		ContractDefinition const* _contextContract
+	);
 
 	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
 	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
@@ -339,12 +351,12 @@ protected:
 
 	/// Creates symbolic expressions for the returned values
 	/// and set them as the components of the symbolic tuple.
-	void createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contract);
+	void createReturnedExpressions(FunctionCall const& _funCall, ContractDefinition const* _contextContract);
 
 	/// @returns the symbolic arguments for a function call,
 	/// taking into account bound functions and
 	/// type conversion.
-	std::vector<smtutil::Expression> symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contract);
+	std::vector<smtutil::Expression> symbolicArguments(FunctionCall const& _funCall, ContractDefinition const* _contextContract);
 
 	/// @returns a note to be added to warnings.
 	std::string extraComment();
@@ -384,12 +396,21 @@ protected:
 	bool isRootFunction();
 	/// Returns true if _funDef was already visited.
 	bool visitedFunction(FunctionDefinition const* _funDef);
+	/// @returns the contract that contains the current FunctionDefinition that is being visited,
+	/// or nullptr if the analysis is not inside a FunctionDefinition.
+	ContractDefinition const* currentScopeContract();
 
 	/// @returns FunctionDefinitions of the given contract (including its constructor and inherited methods),
 	/// taking into account overriding of the virtual functions.
-	std::vector<FunctionDefinition const*> const& contractFunctions(ContractDefinition const& _contract);
+	std::set<FunctionDefinition const*, ASTNode::CompareByID> const& contractFunctions(ContractDefinition const& _contract);
 	/// Cache for the method contractFunctions.
-	std::map<ContractDefinition const*, std::vector<FunctionDefinition const*>> m_contractFunctions;
+	std::map<ContractDefinition const*, std::set<FunctionDefinition const*, ASTNode::CompareByID>> m_contractFunctions;
+
+	/// @returns FunctionDefinitions of the given contract (including its constructor and methods of bases),
+	/// without taking into account overriding of the virtual functions.
+	std::set<FunctionDefinition const*, ASTNode::CompareByID> const& contractFunctionsWithoutVirtual(ContractDefinition const& _contract);
+	/// Cache for the method contractFunctionsWithoutVirtual.
+	std::map<ContractDefinition const*, std::set<FunctionDefinition const*, ASTNode::CompareByID>> m_contractFunctionsWithoutVirtual;
 
 	/// Depth of visit to modifiers.
 	/// When m_modifierDepth == #modifiers the function can be visited

libsolidity/formal/VariableUsage.cpp

@@ -60,11 +60,9 @@ void VariableUsage::endVisit(IndexAccess const& _indexAccess)
 
 void VariableUsage::endVisit(FunctionCall const& _funCall)
 {
-	if (m_inlineFunctionCalls(_funCall, m_currentContract))
+	auto scopeContract = m_currentFunction->annotation().contract;
-		if (
+	if (m_inlineFunctionCalls(_funCall, scopeContract, m_currentContract))
-			auto [funDef, contextContract] = SMTEncoder::functionCallToDefinition(_funCall, m_currentContract);
+		if (auto funDef = SMTEncoder::functionCallToDefinition(_funCall, scopeContract, m_currentContract))
-			funDef
-		)
 			if (find(m_callStack.begin(), m_callStack.end(), funDef) == m_callStack.end())
 				funDef->accept(*this);
 }

libsolidity/formal/VariableUsage.h

@@ -36,9 +36,10 @@ public:
 	std::set<VariableDeclaration const*> touchedVariables(ASTNode const& _node, std::vector<CallableDeclaration const*> const& _outerCallstack);
 
 	/// Sets whether to inline function calls.
-	void setFunctionInlining(std::function<bool(FunctionCall const&, ContractDefinition const*)> _inlineFunctionCalls) { m_inlineFunctionCalls = _inlineFunctionCalls; }
+	void setFunctionInlining(std::function<bool(FunctionCall const&, ContractDefinition const*, ContractDefinition const*)> _inlineFunctionCalls) { m_inlineFunctionCalls = _inlineFunctionCalls; }
 
 	void setCurrentContract(ContractDefinition const& _contract) { m_currentContract = &_contract; }
+	void setCurrentFunction(FunctionDefinition const& _function) { m_currentFunction = &_function; }
 
 private:
 	void endVisit(Identifier const& _node) override;
@@ -56,8 +57,9 @@ private:
 	std::vector<CallableDeclaration const*> m_callStack;
 	CallableDeclaration const* m_lastCall = nullptr;
 	ContractDefinition const* m_currentContract = nullptr;
+	FunctionDefinition const* m_currentFunction = nullptr;
 
-	std::function<bool(FunctionCall const&, ContractDefinition const*)> m_inlineFunctionCalls = [](FunctionCall const&, ContractDefinition const*) { return false; };
+	std::function<bool(FunctionCall const&, ContractDefinition const*, ContractDefinition const*)> m_inlineFunctionCalls = [](FunctionCall const&, ContractDefinition const*, ContractDefinition const*) { return false; };
 };
 
 }

test/libsolidity/smtCheckerTests/imports/import_base.sol

@@ -20,9 +20,9 @@ contract Der is Base {
 // ====
 // SMTIgnoreCex: yes
 // ----
+// Warning 4984: (base:100-103): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 4984: (der:101-109): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 6328: (der:113-126): CHC: Assertion violation happens here.
-// Warning 4984: (base:100-103): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 2661: (base:100-103): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (base:100-103): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
 // Warning 2661: (der:101-109): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
-// Warning 2661: (base:100-103): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_3.sol

@@ -0,0 +1,31 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x;
+	function f() internal virtual {
+		v();
+		assert(x == 0); // should fail
+		assert(x == 2); // should hold
+	}
+	function v() internal virtual {
+		x = 0;
+	}
+}
+
+contract B is A {
+	function f() internal virtual override {
+		super.f();
+	}
+}
+
+contract C is B {
+	function g() public {
+		x = 1;
+		f();
+	}
+	function v() internal override {
+		x = 2;
+	}
+}
+// ----
+// Warning 6328: (97-111): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n    B.f() -- internal call\n        A.f() -- internal call\n            C.v() -- internal call

test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_4.sol

@@ -0,0 +1,38 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x;
+	function f() internal virtual {
+		v();
+		assert(x == 0); // should fail
+		assert(x == 2); // should hold
+	}
+	function v() internal virtual {
+		x = 0;
+	}
+}
+contract A1 is A {
+	function f() internal virtual override {
+		super.f();
+	}
+}
+contract B is A {
+	function f() internal virtual override {
+		super.f();
+	}
+}
+
+contract C is B, A1 {
+	function g() public {
+		x = 1;
+		f();
+	}
+	function f() internal override(B, A1) {
+		super.f();
+	}
+	function v() internal override {
+		x = 2;
+	}
+}
+// ----
+// Warning 6328: (97-111): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n    C.f() -- internal call\n        A1.f() -- internal call\n            B.f() -- internal call\n                A.f() -- internal call\n                    C.v() -- internal call

test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_5.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x;
+	function f() internal virtual {
+		v();
+		assert(x == 0); // should hold
+		assert(x == 2); // should fail
+	}
+	function v() internal virtual {
+		x = 0;
+	}
+}
+
+contract B is A {
+	function f() internal virtual override {
+		super.f();
+	}
+}
+
+contract C is B {
+	function g() public {
+		x = 1;
+		f();
+	}
+	function v() internal override {
+		x = 2;
+		super.v();
+	}
+}
+// ----
+// Warning 6328: (130-144): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n    B.f() -- internal call\n        A.f() -- internal call\n            C.v() -- internal call\n                A.v() -- internal call

test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_6.sol

@@ -0,0 +1,34 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x;
+	function f() internal virtual {
+		v();
+		assert(x == 2); // should hold
+	}
+	function v() internal virtual {
+		x = 0;
+	}
+	function g() public virtual {
+		v();
+		assert(x == 2); // should fail
+	}
+}
+
+contract B is A {
+	function f() internal virtual override {
+		super.f();
+	}
+}
+
+contract C is B {
+	function g() public override {
+		x = 1;
+		f();
+	}
+	function v() internal override {
+		x = 2;
+	}
+}
+// ----
+// Warning 6328: (216-230): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.g()\n    A.v() -- internal call

test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_7.sol

@@ -0,0 +1,25 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x;
+	function f() internal {
+		v();
+		assert(x == 0); // should fail
+		assert(x == 2); // should hold
+	}
+	function v() internal virtual {
+		x = 0;
+	}
+}
+
+contract C is A {
+	function g() public {
+		x = 1;
+		f();
+	}
+	function v() internal override {
+		x = 2;
+	}
+}
+// ----
+// Warning 6328: (89-103): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nC.g()\n    A.f() -- internal call\n        C.v() -- internal call

test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_8.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+abstract contract A {
+	uint x;
+	function f() public view {
+		assert(x == 2);
+	}
+}
+
+contract C is  A {
+	function g() public {
+		x = 2;
+		f();
+		x = 0;
+	}
+}
+// ----
+// Warning 6328: (94-108): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()

test/libsolidity/smtCheckerTests/inheritance/base_contract_assertion_fail_9.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+contract A {
+	uint x;
+	function f() public virtual {
+		v();
+		assert(x == 0); // should fail when C is the most derived contract
+		assert(x == 2); // should fail when A is the most derived contract
+	}
+	function v() internal virtual {
+		x = 0;
+	}
+}
+
+contract B is A {
+	function f() public virtual override {
+		super.f();
+	}
+}
+
+contract C is B {
+	function g() public {
+		x = 1;
+		f();
+	}
+	function v() internal override {
+		x = 2;
+	}
+}
+// ----
+// Warning 6328: (164-178): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n\nTransaction trace:\nA.constructor()\nState: x = 0\nA.f()\n    A.v() -- internal call
+// Warning 6328: (95-109): CHC: Assertion violation happens here.\nCounterexample:\nx = 2\n\nTransaction trace:\nC.constructor()\nState: x = 0\nB.f()\n    A.f() -- internal call\n        C.v() -- internal call

test/libsolidity/smtCheckerTests/inheritance/diamond_super_1.sol

@@ -0,0 +1,31 @@
+pragma experimental SMTChecker;
+contract A {
+	function f() public virtual returns (uint256 r) {
+		return 1;
+	}
+}
+
+
+contract B is A {
+	function f() public virtual override returns (uint256 r) {
+		return super.f() + 2;
+	}
+}
+
+
+contract C is A {
+	function f() public virtual override returns (uint256 r) {
+		return super.f() + 4;
+	}
+}
+
+
+contract D is B, C {
+	function f() public override(B, C) returns (uint256 r) {
+		r = super.f() + 8;
+		assert(r == 15); // should hold
+		assert(r == 13); // should fail
+	}
+}
+// ----
+// Warning 6328: (469-484): CHC: Assertion violation happens here.\nCounterexample:\n\nr = 15\n\nTransaction trace:\nD.constructor()\nD.f()\n    C.f() -- internal call\n        B.f() -- internal call\n            A.f() -- internal call

test/libsolidity/smtCheckerTests/inheritance/diamond_super_2.sol

@@ -0,0 +1,33 @@
+pragma experimental SMTChecker;
+contract A {
+	function f() public virtual returns (uint256 r) {
+		return 1;
+	}
+}
+
+
+contract B is A {
+	function f() public virtual override returns (uint256 r) {
+		return super.f() + 2;
+	}
+}
+
+
+contract C is A {
+	function f() public virtual override returns (uint256 r) {
+		return 2 * (super.f() + 4);
+	}
+}
+
+
+contract D is B, C {
+	function f() public override(B, C) returns (uint256 r) {
+		r = super.f() + 8;
+		assert(r == 22); // should hold
+		assert(r == 20); // should fail
+		assert(r == 18); // should fail
+	}
+}
+// ----
+// Warning 6328: (475-490): CHC: Assertion violation happens here.\nCounterexample:\n\nr = 22\n\nTransaction trace:\nD.constructor()\nD.f()\n    C.f() -- internal call\n        B.f() -- internal call\n            A.f() -- internal call
+// Warning 6328: (509-524): CHC: Assertion violation happens here.\nCounterexample:\n\nr = 22\n\nTransaction trace:\nD.constructor()\nD.f()\n    C.f() -- internal call\n        B.f() -- internal call\n            A.f() -- internal call

test/libsolidity/smtCheckerTests/inheritance/diamond_super_3.sol

@@ -0,0 +1,35 @@
+pragma experimental SMTChecker;
+
+contract A {
+	int public x;
+	function f() public virtual {
+		x = 1;
+	}
+}
+
+contract B is A {
+	function f() public virtual override {
+		super.f();
+		x += 100;
+	}
+}
+
+contract C is B {
+	function f() public virtual override {
+		super.f();
+		x += 10;
+	}
+}
+
+contract D is B {
+}
+
+contract E is C,D {
+	function f() public override(C,B) {
+		super.f();
+		assert(x == 111); // should hold
+		assert(x == 13); // should fail
+	}
+}
+// ----
+// Warning 6328: (412-427): CHC: Assertion violation happens here.\nCounterexample:\nx = 111\n\nTransaction trace:\nE.constructor()\nState: x = 0\nE.f()\n    C.f() -- internal call\n        B.f() -- internal call\n            A.f() -- internal call