diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 3ad2731c1..dfc8f7428 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -121,6 +121,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function)
 		initializeLocalVariables(_function);
 		m_loopExecutionHappened = false;
 		m_arrayAssignmentHappened = false;
+		m_externalFunctionCallHappened = false;
 	}
 	_function.parameterList().accept(*this);
 	if (_function.returnParameterList())
@@ -607,6 +608,7 @@ void SMTChecker::endVisit(FunctionCall const& _funCall)
 		popCallStack();
 		break;
 	case FunctionType::Kind::External:
+		m_externalFunctionCallHappened = true;
 		resetStateVariables();
 		resetStorageReferences();
 		break;
@@ -1295,6 +1297,12 @@ void SMTChecker::checkCondition(
 			" therefore all mapping information is erased after"
 			" a mapping local variable/parameter is assigned.\n"
 			"You can re-introduce information using require().";
+	if (m_externalFunctionCallHappened)
+		extraComment +=
+			"\nNote that external function calls are not inlined,"
+			" even if the source code of the function is available."
+			" This is due to the possibility that the actual called contract"
+			" has the same ABI but implements the function differently.";
 
 	SecondarySourceLocation secondaryLocation{};
 	secondaryLocation.append(extraComment, SourceLocation{});
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index faa0b97d4..ad840c771 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -277,6 +277,7 @@ private:
 	VariableUsage m_variableUsage;
 	bool m_loopExecutionHappened = false;
 	bool m_arrayAssignmentHappened = false;
+	bool m_externalFunctionCallHappened = false;
 	// True if the "No SMT solver available" warning was already created.
 	bool m_noSolverWarning = false;
 	/// An Expression may have multiple smt::Expression due to