[SMTChecker] Support to external calls to unknown code

Changelog.md

@@ -10,6 +10,8 @@ Compiler Features:
  * Commandline Interface: Prevent some incompatible commandline options from being used together.
  * NatSpec: Support NatSpec comments on events.
  * Yul Optimizer: Store knowledge about storage / memory after ``a := sload(x)`` / ``a := mload(x)``.
+ * SMTChecker: Support to external calls to unknown code and to known view/pure functions.
+
 
 Bugfixes:
  * NatSpec: Do not consider ``////`` and ``/***`` as NatSpec comments.

libsolidity/formal/CHC.cpp

@@ -197,8 +197,11 @@ void CHC::endVisit(ContractDefinition const& _contract)
 
 bool CHC::visit(FunctionDefinition const& _function)
 {
-	if (!shouldVisit(_function))
+	if (!_function.isImplemented())
+	{
+		connectBlocks(genesis(), summary(_function));
 		return false;
+	}
 
 	// This is the case for base constructor inlining.
 	if (m_currentFunction)
@@ -243,7 +246,7 @@ bool CHC::visit(FunctionDefinition const& _function)
 
 void CHC::endVisit(FunctionDefinition const& _function)
 {
-	if (!shouldVisit(_function))
+	if (!_function.isImplemented())
 		return;
 
 	// This is the case for base constructor inlining.
@@ -474,11 +477,14 @@ void CHC::endVisit(FunctionCall const& _funCall)
 		internalFunctionCall(_funCall);
 		break;
 	case FunctionType::Kind::External:
+	case FunctionType::Kind::BareStaticCall:
+		externalFunctionCall(_funCall);
+		SMTEncoder::endVisit(_funCall);
+		break;
 	case FunctionType::Kind::DelegateCall:
 	case FunctionType::Kind::BareCall:
 	case FunctionType::Kind::BareCallCode:
 	case FunctionType::Kind::BareDelegateCall:
-	case FunctionType::Kind::BareStaticCall:
 	case FunctionType::Kind::Creation:
 	case FunctionType::Kind::KECCAK256:
 	case FunctionType::Kind::ECRecover:
@@ -574,6 +580,33 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 	m_context.addAssertion(m_error.currentValue() == previousError);
 }
 
+void CHC::externalFunctionCall(FunctionCall const& _funCall)
+{
+	solAssert(m_currentContract, "");
+
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	auto kind = funType.kind();
+	solAssert(kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
+
+	auto const* function = functionCallToDefinition(_funCall);
+	if (!function)
+		return;
+
+	auto preCallState = currentStateVariables();
+	bool noStateChanges = kind == FunctionType::Kind::BareStaticCall ||
+		function->stateMutability() == StateMutability::Pure ||
+		function->stateMutability() == StateMutability::View;
+	if (!noStateChanges)
+		for (auto const* var: m_stateVariables)
+			m_context.variable(*var)->increaseIndex();
+
+	auto nondet = (*m_nondetInterfaces.at(m_currentContract))(preCallState + currentStateVariables());
+	m_context.addAssertion(nondet);
+	m_context.addAssertion(predicate(_funCall));
+
+	m_context.addAssertion(m_error.currentValue() == 0);
+}
+
 void CHC::unknownFunctionCall(FunctionCall const&)
 {
 	/// Function calls are not handled at the moment,
@@ -651,11 +684,6 @@ void CHC::clearIndices(ContractDefinition const* _contract, FunctionDefinition c
 	}
 }
 
-bool CHC::shouldVisit(FunctionDefinition const& _function) const
-{
-	return _function.isImplemented();
-}
-
 void CHC::setCurrentBlock(
 	smt::SymbolicFunctionVariable const& _block,
 	vector<smtutil::Expression> const* _arguments
@@ -710,10 +738,14 @@ smtutil::SortPointer CHC::constructorSort()
 
 smtutil::SortPointer CHC::interfaceSort()
 {
-	return make_shared<smtutil::FunctionSort>(
+	solAssert(m_currentContract, "");
-		m_stateSorts,
+	return interfaceSort(*m_currentContract);
-		smtutil::SortProvider::boolSort
+}
-	);
+
+smtutil::SortPointer CHC::nondetInterfaceSort()
+{
+	solAssert(m_currentContract, "");
+	return nondetInterfaceSort(*m_currentContract);
 }
 
 smtutil::SortPointer CHC::interfaceSort(ContractDefinition const& _contract)
@@ -724,6 +756,15 @@ smtutil::SortPointer CHC::interfaceSort(ContractDefinition const& _contract)
 	);
 }
 
+smtutil::SortPointer CHC::nondetInterfaceSort(ContractDefinition const& _contract)
+{
+	auto sorts = stateSorts(_contract);
+	return make_shared<smtutil::FunctionSort>(
+		sorts + sorts,
+		smtutil::SortProvider::boolSort
+	);
+}
+
 smtutil::SortPointer CHC::arity0FunctionSort()
 {
 	return make_shared<smtutil::FunctionSort>(
@@ -802,11 +843,47 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 			{
 				string suffix = base->name() + "_" + to_string(base->id());
 				m_interfaces[base] = createSymbolicBlock(interfaceSort(*base), "interface_" + suffix);
+				m_nondetInterfaces[base] = createSymbolicBlock(nondetInterfaceSort(*base), "nondet_interface_" + suffix);
+
 				for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*base))
 					if (!m_context.knownVariable(*var))
 						createVariable(*var);
+
+				/// Base nondeterministic interface that allows
+				/// 0 steps to be taken, used as base for the inductive
+				/// rule for each function.
+				auto const& iface = *m_nondetInterfaces.at(base);
+				auto state0 = stateVariablesAtIndex(0, *base);
+				addRule(iface(state0 + state0), "base_nondet");
+
 				for (auto const* function: base->definedFunctions())
+				{
+					for (auto var: function->parameters())
+						createVariable(*var);
+					for (auto var: function->returnParameters())
+						createVariable(*var);
+					for (auto const* var: function->localVariables())
+						createVariable(*var);
+
 					m_summaries[contract].emplace(function, createSummaryBlock(*function, *contract));
+
+					if (!base->isLibrary() && !base->isInterface() && !function->isConstructor())
+					{
+						auto state1 = stateVariablesAtIndex(1, *base);
+						auto state2 = stateVariablesAtIndex(2, *base);
+
+						auto nondetPre = iface(state0 + state1);
+						auto nondetPost = iface(state0 + state2);
+
+						vector<smtutil::Expression> args{m_error.currentValue()};
+						args += state1 +
+							applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
+							state2 +
+							applyMap(function->returnParameters(), [this](auto _var) { return valueAtIndex(*_var, 1); });
+
+						connectBlocks(nondetPre, nondetPost, (*m_summaries.at(base).at(function))(args));
+					}
+				}
 			}
 }
 
@@ -842,15 +919,21 @@ smtutil::Expression CHC::summary(ContractDefinition const&)
 	);
 }
 
-smtutil::Expression CHC::summary(FunctionDefinition const& _function)
+smtutil::Expression CHC::summary(FunctionDefinition const& _function, ContractDefinition const& _contract)
 {
 	vector<smtutil::Expression> args{m_error.currentValue()};
 	auto contract = _function.annotation().contract;
-	args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables();
+	args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : initialStateVariables(_contract);
 	args += applyMap(_function.parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); });
-	args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables();
+	args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables(_contract);
 	args += applyMap(_function.returnParameters(), [this](auto _var) { return currentValue(*_var); });
-	return (*m_summaries.at(m_currentContract).at(&_function))(args);
+	return (*m_summaries.at(&_contract).at(&_function))(args);
+}
+
+smtutil::Expression CHC::summary(FunctionDefinition const& _function)
+{
+	solAssert(m_currentContract, "");
+	return summary(_function, *m_currentContract);
 }
 
 unique_ptr<smt::SymbolicFunctionVariable> CHC::createBlock(ASTNode const* _node, string const& _prefix)
@@ -893,13 +976,18 @@ vector<smtutil::Expression> CHC::initialStateVariables()
 	return stateVariablesAtIndex(0);
 }
 
-vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index)
+vector<smtutil::Expression> CHC::initialStateVariables(ContractDefinition const& _contract)
 {
-	solAssert(m_currentContract, "");
+	return stateVariablesAtIndex(0, _contract);
-	return applyMap(m_stateVariables, [&](auto _var) { return valueAtIndex(*_var, _index); });
 }
 
-vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract)
+vector<smtutil::Expression> CHC::stateVariablesAtIndex(int _index)
+{
+	solAssert(m_currentContract, "");
+	return stateVariablesAtIndex(_index, *m_currentContract);
+}
+
+vector<smtutil::Expression> CHC::stateVariablesAtIndex(int _index, ContractDefinition const& _contract)
 {
 	return applyMap(
 		stateVariablesIncludingInheritedAndPrivate(_contract),
@@ -910,7 +998,12 @@ vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, Contract
 vector<smtutil::Expression> CHC::currentStateVariables()
 {
 	solAssert(m_currentContract, "");
-	return applyMap(m_stateVariables, [this](auto _var) { return currentValue(*_var); });
+	return currentStateVariables(*m_currentContract);
+}
+
+vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const& _contract)
+{
+	return applyMap(stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); });
 }
 
 vector<smtutil::Expression> CHC::currentFunctionVariables()
@@ -978,12 +1071,17 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 	m_error.increaseIndex();
 	vector<smtutil::Expression> args{m_error.currentValue()};
 	auto const* contract = function->annotation().contract;
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	bool otherContract = contract->isLibrary() ||
+		funType.kind() == FunctionType::Kind::External ||
+		funType.kind() == FunctionType::Kind::BareStaticCall;
 
-	args += contract->isLibrary() ? stateVariablesAtIndex(0, *contract) : currentStateVariables();
+	args += otherContract ? stateVariablesAtIndex(0, *contract) : currentStateVariables();
 	args += symbolicArguments(_funCall);
-	for (auto const& var: m_stateVariables)
+	if (!otherContract)
-		m_context.variable(*var)->increaseIndex();
+		for (auto const& var: m_stateVariables)
-	args += contract->isLibrary() ? stateVariablesAtIndex(1, *contract) : currentStateVariables();
+			m_context.variable(*var)->increaseIndex();
+	args += otherContract ? stateVariablesAtIndex(1, *contract) : currentStateVariables();
 
 	auto const& returnParams = function->returnParameters();
 	for (auto param: returnParams)
@@ -993,7 +1091,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 			createVariable(*param);
 	args += applyMap(function->returnParameters(), [this](auto _var) { return currentValue(*_var); });
 
-	if (contract->isLibrary())
+	if (otherContract)
 		return (*m_summaries.at(contract).at(function))(args);
 
 	solAssert(m_currentContract, "");

libsolidity/formal/CHC.h

@@ -77,6 +77,7 @@ private:
 
 	void visitAssert(FunctionCall const& _funCall);
 	void internalFunctionCall(FunctionCall const& _funCall);
+	void externalFunctionCall(FunctionCall const& _funCall);
 	void unknownFunctionCall(FunctionCall const& _funCall);
 	void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override;
 	//@}
@@ -95,7 +96,6 @@ private:
 	void resetContractAnalysis();
 	void eraseKnowledge();
 	void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
-	bool shouldVisit(FunctionDefinition const& _function) const;
 	void setCurrentBlock(smt::SymbolicFunctionVariable const& _block, std::vector<smtutil::Expression> const* _arguments = nullptr);
 	std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
 	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
@@ -106,7 +106,9 @@ private:
 	static std::vector<smtutil::SortPointer> stateSorts(ContractDefinition const& _contract);
 	smtutil::SortPointer constructorSort();
 	smtutil::SortPointer interfaceSort();
+	smtutil::SortPointer nondetInterfaceSort();
 	static smtutil::SortPointer interfaceSort(ContractDefinition const& _const);
+	static smtutil::SortPointer nondetInterfaceSort(ContractDefinition const& _const);
 	smtutil::SortPointer arity0FunctionSort();
 	smtutil::SortPointer sort(FunctionDefinition const& _function);
 	smtutil::SortPointer sort(ASTNode const* _block);
@@ -149,10 +151,12 @@ private:
 	/// @returns the symbolic values of the state variables at the beginning
 	/// of the current transaction.
 	std::vector<smtutil::Expression> initialStateVariables();
-	std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index);
+	std::vector<smtutil::Expression> initialStateVariables(ContractDefinition const& _contract);
-	std::vector<smtutil::Expression> stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract);
+	std::vector<smtutil::Expression> stateVariablesAtIndex(int _index);
+	std::vector<smtutil::Expression> stateVariablesAtIndex(int _index, ContractDefinition const& _contract);
 	/// @returns the current symbolic values of the current state variables.
 	std::vector<smtutil::Expression> currentStateVariables();
+	std::vector<smtutil::Expression> currentStateVariables(ContractDefinition const& _contract);
 
 	/// @returns the current symbolic values of the current function's
 	/// input and output parameters.
@@ -173,6 +177,7 @@ private:
 	smtutil::Expression summary(ContractDefinition const& _contract);
 	/// @returns a predicate that defines a function summary.
 	smtutil::Expression summary(FunctionDefinition const& _function);
+	smtutil::Expression summary(FunctionDefinition const& _function, ContractDefinition const& _contract);
 	//@}
 
 	/// Solver related.
@@ -212,6 +217,12 @@ private:
 	/// Single entry block for all functions.
 	std::map<ContractDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>> m_interfaces;
 
+	/// Nondeterministic interfaces.
+	/// These are used when the analyzed contract makes external calls to unknown code,
+	/// which means that the analyzed contract can potentially be called
+	/// nondeterministically.
+	std::map<ContractDefinition const*, std::unique_ptr<smt::SymbolicFunctionVariable>> m_nondetInterfaces;
+
 	/// Artificial Error predicate.
 	/// Single error block for all assertions.
 	std::unique_ptr<smt::SymbolicFunctionVariable> m_errorPredicate;

test/libsolidity/smtCheckerTests/external_calls/external.sol

@@ -0,0 +1,20 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	uint x;
+	D d;
+	function f() public {
+		if (x < 10)
+			++x;
+	}
+	function g() public {
+		d.d();
+		assert(x < 10);
+	}
+}
+// ----
+// Warning 4661: (200-214): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+abstract contract Crypto {
+	function hash(bytes32) external pure virtual returns (bytes32);
+}
+
+contract C {
+	address owner;
+	bytes32 sig_1;
+	bytes32 sig_2;
+	Crypto d;
+
+	constructor() public {
+		owner = msg.sender;
+	}
+
+	function f1(bytes32 _msg) public {
+		address prevOwner = owner;
+		sig_1 = d.hash(_msg);
+		sig_2 = d.hash(_msg);
+		assert(prevOwner == owner);
+	}
+
+	function inv() public view {
+		assert(sig_1 == sig_2);
+	}
+}
+// ----
+// Warning 4661: (430-452): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_pure.sol

@@ -0,0 +1,29 @@
+pragma experimental SMTChecker;
+
+contract Crypto {
+	function hash(bytes32) external pure returns (bytes32) {
+		return bytes32(0);
+	}
+}
+
+contract C {
+	address owner;
+	bytes32 sig_1;
+	bytes32 sig_2;
+	Crypto d;
+
+	constructor() public {
+		owner = msg.sender;
+	}
+
+	function f1(bytes32 _msg) public {
+		address prevOwner = owner;
+		sig_1 = d.hash(_msg);
+		sig_2 = d.hash(_msg);
+		assert(prevOwner == owner);
+	}
+
+	function inv() public view {
+		assert(sig_1 == sig_2);
+	}
+}

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state.sol

@@ -0,0 +1,38 @@
+pragma experimental SMTChecker;
+
+contract State {
+	uint x;
+	function f() public returns (uint) {
+		if (x == 0) x = 1;
+		else if (x == 1) x = 2;
+		else if (x == 2) x = 0;
+		return x;
+	}
+}
+
+contract C {
+	address owner;
+	uint y;
+	uint z;
+	State s;
+
+	constructor() public {
+		owner = msg.sender;
+	}
+
+	function f() public {
+		address prevOwner = owner;
+		y = s.f();
+		z = s.f();
+		assert(prevOwner == owner);
+	}
+
+	function inv() public view {
+		// This is safe but external calls do not yet support the state
+		// of the called contract.
+		assert(owner == address(0) || y != z);
+	}
+}
+// ----
+// Warning 5084: (551-561): Type conversion is not yet fully supported and might yield false positives.
+// Warning 4661: (535-572): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy.sol

@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+contract State {
+	uint x;
+	C c;
+	function f() public view returns (uint) {
+		return c.g();
+	}
+}
+
+contract C {
+	address owner;
+	uint y;
+	State s;
+
+	constructor() public {
+		owner = msg.sender;
+	}
+
+	function f() public view {
+		address prevOwner = owner;
+		uint z = s.f();
+		assert(z == y);
+		assert(prevOwner == owner);
+	}
+
+	function g() public view returns (uint) {
+		return y;
+	}
+}
+// ----
+// Warning 4661: (306-320): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_indirect.sol

@@ -0,0 +1,47 @@
+pragma experimental SMTChecker;
+
+contract Other {
+	C c;
+	function h() public {
+		c.setOwner(address(0));
+	}
+}
+
+contract State {
+	uint x;
+	Other o;
+	C c;
+	function f() public returns (uint) {
+		o.h();
+		return c.g();
+	}
+}
+
+contract C {
+	address owner;
+	uint y;
+	State s;
+
+	constructor() public {
+		owner = msg.sender;
+	}
+
+	function setOwner(address _owner) public {
+		owner = _owner;
+	}
+
+	function f() public {
+		address prevOwner = owner;
+		uint z = s.f();
+		assert(z == y);
+		assert(prevOwner == owner);
+	}
+
+	function g() public view returns (uint) {
+		return y;
+	}
+}
+// ----
+// Warning 5084: (92-102): Type conversion is not yet fully supported and might yield false positives.
+// Warning 4661: (459-473): Assertion violation happens here
+// Warning 4661: (477-503): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_reentrancy_unsafe.sol

@@ -0,0 +1,39 @@
+pragma experimental SMTChecker;
+
+contract State {
+	uint x;
+	C c;
+	function f() public returns (uint) {
+		c.setOwner(address(0));
+		return c.g();
+	}
+}
+
+contract C {
+	address owner;
+	uint y;
+	State s;
+
+	constructor() public {
+		owner = msg.sender;
+	}
+
+	function setOwner(address _owner) public {
+		owner = _owner;
+	}
+
+	function f() public {
+		address prevOwner = owner;
+		uint z = s.f();
+		assert(z == y);
+		assert(prevOwner == owner);
+	}
+
+	function g() public view returns (uint) {
+		return y;
+	}
+}
+// ----
+// Warning 5084: (116-126): Type conversion is not yet fully supported and might yield false positives.
+// Warning 4661: (388-402): Assertion violation happens here
+// Warning 4661: (406-432): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_hash_known_code_state_unsafe.sol

@@ -0,0 +1,43 @@
+pragma experimental SMTChecker;
+
+contract State {
+	uint x;
+	function f() public returns (uint) {
+		if (x == 0) x = 1;
+		else if (x == 1) x = 2;
+		else if (x == 2) x = 0;
+		return x;
+	}
+}
+
+contract C {
+	address owner;
+	uint y;
+	uint z;
+	State s;
+
+	constructor() public {
+		owner = msg.sender;
+	}
+
+	function setOwner(address _owner) public {
+		owner = _owner;
+	}
+
+	function f() public {
+		address prevOwner = owner;
+		y = s.f();
+		z = s.f();
+		assert(prevOwner == owner);
+	}
+
+	function inv() public view {
+		// This is safe but external calls do not yet support the state
+		// of the called contract.
+		assert(owner == address(0) || y != z);
+	}
+}
+// ----
+// Warning 4661: (442-468): Assertion violation happens here
+// Warning 5084: (617-627): Type conversion is not yet fully supported and might yield false positives.
+// Warning 4661: (601-638): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_inc.sol

@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	uint x;
+	D d;
+
+	function inc() public {
+		++x;
+	}
+
+	function f() public {
+		d.d();
+		assert(x < 10);
+	}
+}
+// ----
+// Warning 2661: (146-149): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (189-203): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_inc1_inc2.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	uint x;
+	uint y;
+	D d;
+
+	function inc2() public {
+		if (y == 1)
+			x = 1;
+	}
+	function inc1() public {
+		if (x == 0)
+			y = 1;
+	}
+
+	function f() public {
+		uint oldX = x;
+		d.d();
+		assert(oldX == x);
+	}
+}
+// ----
+// Warning 4661: (286-303): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/external_safe.sol

@@ -0,0 +1,18 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	uint x;
+	D d;
+	function f() public {
+		if (x < 10)
+			++x;
+	}
+	function g() public {
+		d.d();
+		assert(x < 11);
+	}
+}

test/libsolidity/smtCheckerTests/external_calls/external_single_inc.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	uint x;
+	uint y;
+	D d;
+
+	function inc() public {
+		if (y == 1)
+			x = 1;
+		if (x == 0)
+			y = 1;
+	}
+
+	function f() public {
+		uint oldX = x;
+		d.d();
+		assert(oldX == x);
+	}
+}
+// ----
+// Warning 4661: (256-273): Assertion violation happens here

test/libsolidity/smtCheckerTests/external_calls/mutex.sol

@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	uint x;
+	D d;
+
+	bool lock;
+	modifier mutex {
+		require(!lock);
+		lock = true;
+		_;
+		lock = false;
+	}
+
+	function set(uint _x) mutex public {
+		x = _x;
+	}
+
+	function f() mutex public {
+		uint y = x;
+		d.d();
+		assert(y == x);
+	}
+}

test/libsolidity/smtCheckerTests/external_calls/mutex_f_no_guard.sol

@@ -0,0 +1,30 @@
+pragma experimental SMTChecker;
+
+abstract contract D {
+	function d() external virtual;
+}
+
+contract C {
+	uint x;
+	D d;
+
+	bool lock;
+	modifier mutex {
+		require(!lock);
+		lock = true;
+		_;
+		lock = false;
+	}
+
+	function set(uint _x) mutex public {
+		x = _x;
+	}
+
+	function f() public {
+		uint y = x;
+		d.d();
+		assert(y == x);
+	}
+}
+// ----
+// Warning 4661: (307-321): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_external_1.sol

@@ -17,4 +17,3 @@ contract C
 	}
 }
 // ----
-// Warning 4661: (257-271): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_external_3.sol

@@ -18,4 +18,3 @@ contract C
 	}
 }
 // ----
-// Warning 4661: (355-379): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_external_4.sol

@@ -16,4 +16,3 @@ contract D
 	}
 }
 // ----
-// Warning 4661: (191-206): Assertion violation happens here

test/libsolidity/smtCheckerTests/loops/for_1_false_positive.sol

@@ -14,4 +14,6 @@ contract C
 	}
 }
 // ----
+// Warning 1218: (296-309): Error trying to invoke SMT solver.
 // Warning 2661: (176-181): Overflow (resulting value larger than 2**256 - 1) happens here
+// Warning 4661: (296-309): Assertion violation happens here

test/libsolidity/smtCheckerTests/types/address_staticcall.sol

@@ -20,6 +20,3 @@ contract C
 // ----
 // Warning 2072: (224-240): Unused local variable.
 // Warning 4661: (266-281): Assertion violation happens here
-// Warning 4661: (285-299): Assertion violation happens here
-// Warning 4661: (303-322): Assertion violation happens here
-// Warning 4661: (326-350): Assertion violation happens here