diff --git a/Changelog.md b/Changelog.md
index a8af33eb4..b44121578 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -9,6 +9,7 @@ Compiler Features:
  * Command Line interface: Report proper error for each output file which could not be written. Previously an exception was thrown, and execution aborted, on the first error.
  * SMTChecker: Add division by zero checks in the CHC engine.
  * SMTChecker: Support ``selector`` for expressions with value known at compile-time.
+ * SMTChecker: More precise analysis of external calls using ``this``.
  * Command Line Interface: New option ``--model-checker-timeout`` sets a timeout in milliseconds for each individual query performed by the SMTChecker.
  * Standard JSON: New option ``modelCheckerSettings.timeout`` sets a timeout in milliseconds for each individual query performed by the SMTChecker.
  * Assembler: Perform linking in assembly mode when library addresses are provided.
diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index 6013f1cd1..b6e05bdd0 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -96,20 +96,7 @@ bool BMC::shouldInlineFunctionCall(FunctionCall const& _funCall)
 
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 	if (funType.kind() == FunctionType::Kind::External)
-	{
-		auto memberAccess = dynamic_cast<MemberAccess const*>(&_funCall.expression());
-		if (!memberAccess)
-			return false;
-
-		auto identifier = dynamic_cast<Identifier const*>(&memberAccess->expression());
-		if (!(
-			identifier &&
-			identifier->name() == "this" &&
-			identifier->annotation().referencedDeclaration &&
-			dynamic_cast<MagicVariableDeclaration const*>(identifier->annotation().referencedDeclaration)
-		))
-			return false;
-	}
+		return isTrustedExternalCall(&_funCall.expression());
 	else if (funType.kind() != FunctionType::Kind::Internal)
 		return false;
 
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 6fc432d06..be3413770 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -562,8 +562,6 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 			m_context.addAssertion(interface(*contract));
 	}
 
-	auto previousError = errorFlag().currentValue();
-
 	m_context.addAssertion(predicate(_funCall));
 
 	connectBlocks(
@@ -572,8 +570,6 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 		(errorFlag().currentValue() > 0)
 	);
 	m_context.addAssertion(errorFlag().currentValue() == 0);
-	errorFlag().increaseIndex();
-	m_context.addAssertion(errorFlag().currentValue() == previousError);
 }
 
 void CHC::externalFunctionCall(FunctionCall const& _funCall)
@@ -583,6 +579,11 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	/// so we just add the nondet_interface predicate.
 
 	solAssert(m_currentContract, "");
+	if (isTrustedExternalCall(&_funCall.expression()))
+	{
+		externalFunctionCallToTrustedCode(_funCall);
+		return;
+	}
 
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 	auto kind = funType.kind();
@@ -615,6 +616,42 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	m_context.addAssertion(errorFlag().currentValue() == 0);
 }
 
+void CHC::externalFunctionCallToTrustedCode(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;
+
+	// External call creates a new transaction.
+	auto originalTx = state().tx();
+	auto txOrigin = state().txMember("tx.origin");
+	state().newTx();
+	// set the transaction sender as this contract
+	m_context.addAssertion(state().txMember("msg.sender") == state().thisAddress());
+	// set the origin to be the current transaction origin
+	m_context.addAssertion(state().txMember("tx.origin") == txOrigin);
+
+	smtutil::Expression pred = predicate(_funCall);
+
+	auto txConstraints = m_context.state().txConstraints(*function);
+	m_context.addAssertion(pred && txConstraints);
+	// restore the original transaction data
+	state().newTx();
+	m_context.addAssertion(originalTx == state().tx());
+
+	connectBlocks(
+		m_currentBlock,
+		(m_currentFunction && !m_currentFunction->isConstructor()) ? summary(*m_currentFunction) : summary(*m_currentContract),
+		(errorFlag().currentValue() > 0)
+	);
+	m_context.addAssertion(errorFlag().currentValue() == 0);
+}
+
 void CHC::unknownFunctionCall(FunctionCall const&)
 {
 	/// Function calls are not handled at the moment,
@@ -1011,27 +1048,34 @@ smtutil::Expression CHC::predicate(Predicate const& _block)
 
 smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 {
-	/// Used only for internal calls.
+	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
+	auto kind = funType.kind();
+	solAssert(kind == FunctionType::Kind::Internal || kind == FunctionType::Kind::External || kind == FunctionType::Kind::BareStaticCall, "");
 
 	auto const* function = functionCallToDefinition(_funCall);
 	if (!function)
 		return smtutil::Expression(true);
 
+	auto contractAddressValue = [this](FunctionCall const& _f) {
+		FunctionType const& funType = dynamic_cast<FunctionType const&>(*_f.expression().annotation().type);
+		if (funType.kind() == FunctionType::Kind::Internal)
+			return state().thisAddress();
+		if (MemberAccess const* callBase = dynamic_cast<MemberAccess const*>(&_f.expression()))
+			return expr(callBase->expression());
+		solAssert(false, "Unreachable!");
+	};
 	errorFlag().increaseIndex();
-	vector<smtutil::Expression> args{errorFlag().currentValue(), state().thisAddress(), state().crypto(), state().tx(), state().state()};
+	vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().crypto(), state().tx(), state().state()};
 
-	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
-	solAssert(funType.kind() == FunctionType::Kind::Internal, "");
-
-	/// Internal calls can be made to the contract itself or a library.
 	auto const* contract = function->annotation().contract;
 	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
-	solAssert(contract->isLibrary() || find(hierarchy.begin(), hierarchy.end(), contract) != hierarchy.end(), "");
+	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 it is not, we use the current contract even if it is a call to a contract
-	/// up in the inheritance hierarchy, since the interfaces/predicates are different.
-	auto const* calledContract = contract->isLibrary() ? contract : m_currentContract;
+	/// 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) ?  m_currentContract : contract;
 	solAssert(calledContract, "");
 
 	bool usesStaticCall = function->stateMutability() == StateMutability::Pure || function->stateMutability() == StateMutability::View;
diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h
index 8a169e86d..9f712ba39 100644
--- a/libsolidity/formal/CHC.h
+++ b/libsolidity/formal/CHC.h
@@ -88,6 +88,7 @@ private:
 	void visitAddMulMod(FunctionCall const& _funCall) override;
 	void internalFunctionCall(FunctionCall const& _funCall);
 	void externalFunctionCall(FunctionCall const& _funCall);
+	void externalFunctionCallToTrustedCode(FunctionCall const& _funCall);
 	void unknownFunctionCall(FunctionCall const& _funCall);
 	void makeArrayPopVerificationTarget(FunctionCall const& _arrayPop) override;
 	/// Creates underflow/overflow verification targets.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 7ee339b1e..d58abc2ee 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -2391,6 +2391,19 @@ MemberAccess const* SMTEncoder::isEmptyPush(Expression const& _expr) const
 	return nullptr;
 }
 
+bool SMTEncoder::isTrustedExternalCall(Expression const* _expr) {
+	auto memberAccess = dynamic_cast<MemberAccess const*>(_expr);
+	if (!memberAccess)
+		return false;
+
+	auto identifier = dynamic_cast<Identifier const*>(&memberAccess->expression());
+	return identifier &&
+		identifier->name() == "this" &&
+		identifier->annotation().referencedDeclaration &&
+		dynamic_cast<MagicVariableDeclaration const*>(identifier->annotation().referencedDeclaration)
+	;
+}
+
 string SMTEncoder::extraComment()
 {
 	string extra;
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 49cac0082..d56eeca18 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -295,6 +295,10 @@ protected:
 	/// otherwise nullptr.
 	MemberAccess const* isEmptyPush(Expression const& _expr) const;
 
+	/// @returns true if the given identifier is a contract which is known and trusted.
+	/// This means we don't have to abstract away effects of external function calls to this contract.
+	static bool isTrustedExternalCall(Expression const* _expr);
+
 	/// Creates symbolic expressions for the returned values
 	/// and set them as the components of the symbolic tuple.
 	void createReturnedExpressions(FunctionCall const& _funCall);
diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_call.sol b/test/libsolidity/smtCheckerTests/functions/this_external_call.sol
index 489d7f44e..de69baf53 100644
--- a/test/libsolidity/smtCheckerTests/functions/this_external_call.sol
+++ b/test/libsolidity/smtCheckerTests/functions/this_external_call.sol
@@ -9,9 +9,7 @@ contract C
 	function g(uint y) public {
 		require(y < 1000);
 		this.f(y);
-		// Fails as false positive because CHC does not support `this`.
 		assert(x < 1000);
 	}
 }
 // ----
-// Warning 6328: (227-243): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_call_2.sol b/test/libsolidity/smtCheckerTests/functions/this_external_call_2.sol
new file mode 100644
index 000000000..7fca557ad
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/this_external_call_2.sol
@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+
+contract C {
+    uint a;
+    function f(uint x) public {
+        this.g(x);
+        assert(a == x);
+        assert(a != 42);
+    }
+
+    function g(uint x) public {
+        a = x;
+    }
+}
+// ----
+// Warning 6328: (141-156): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol b/test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol
index 0307490dc..cb94af867 100644
--- a/test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol
+++ b/test/libsolidity/smtCheckerTests/functions/this_external_call_return.sol
@@ -10,9 +10,7 @@ contract C
 	function g(uint y) public {
 		require(y < 1000);
 		uint z = this.f(y);
-		// Fails as false positive because CHC does not support `this`.
 		assert(z < 1000);
 	}
 }
 // ----
-// Warning 6328: (263-279): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_call_sender.sol b/test/libsolidity/smtCheckerTests/functions/this_external_call_sender.sol
new file mode 100644
index 000000000..78f4169cc
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/this_external_call_sender.sol
@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+
+contract C {
+    address lastCaller;
+
+    constructor() {
+        lastCaller = msg.sender;
+    }
+
+    modifier log {
+        lastCaller = msg.sender;
+        _;
+    }
+
+    function test() log public {
+        assert(lastCaller == msg.sender);
+        this.g();
+        assert(lastCaller == address(this));
+        assert(lastCaller == msg.sender);
+        assert(lastCaller == address(0));
+    }
+
+    function g() log public {
+    }
+}
+// ----
+// Warning 6328: (347-379): CHC: Assertion violation happens here.
+// Warning 6328: (389-421): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_call_tx_origin.sol b/test/libsolidity/smtCheckerTests/functions/this_external_call_tx_origin.sol
new file mode 100644
index 000000000..04dd5599d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/this_external_call_tx_origin.sol
@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+
+contract C {
+
+	function test() view public {
+		require(address(this) != tx.origin);
+		assert(!this.g());
+	}
+
+	function g() view public returns (bool) {
+		return msg.sender == tx.origin;
+	}
+}
+// ----
diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol b/test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol
new file mode 100644
index 000000000..60c1a57d5
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/this_external_getter_1.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	uint public x;
+
+	function f() public view {
+		uint y = this.x();
+		assert(y == x); // This fails as false positive because of lack of support for external getters.
+	}
+}
+// ----
+// Warning 6328: (114-128): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol b/test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol
new file mode 100644
index 000000000..5091da3f3
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/this_external_getter_2.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => uint) public map;
+
+	function f() public view {
+		uint y = this.map(2);
+		assert(y == map[2]); // This fails as false positive because of lack of support for external getters.
+	}
+}
+// ----
+// Warning 6328: (137-156): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol b/test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol
new file mode 100644
index 000000000..aaa9605cc
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/this_external_getter_3.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+
+contract C {
+	mapping (uint => mapping (uint => uint)) public map;
+
+	function f() public view {
+		uint y = this.map(2, 3);
+		assert(y == map[2][3]); // This fails as false positive because of lack of support for external getters.
+	}
+}
+// ----
+// Warning 6328: (158-180): CHC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/functions/this_state.sol b/test/libsolidity/smtCheckerTests/functions/this_state.sol
index 7cef58b3e..9f417380e 100644
--- a/test/libsolidity/smtCheckerTests/functions/this_state.sol
+++ b/test/libsolidity/smtCheckerTests/functions/this_state.sol
@@ -6,7 +6,6 @@ contract C
     function g() public {
 		x = 0;
         this.h();
-		// Fails as false positive because CHC does not support `this`.
 		assert(x == 2);
     }
     function h() public {
@@ -14,4 +13,3 @@ contract C
     }
 }
 // ----
-// Warning 6328: (186-200): CHC: Assertion violation happens here.