diff --git a/Changelog.md b/Changelog.md
index 9ac2667e2..e34e6021a 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -6,7 +6,7 @@ Language Features:
 Compiler Features:
  * SMTChecker: Support shifts.
  * SMTChecker: Support structs.
- * SMTChecker: Support ``type(T).min`` and ``type(T).max``.
+ * SMTChecker: Support ``type(T).min``, ``type(T).max``, and ``type(I).interfaceId``.
  * Yul Optimizer: Prune unused parameters in functions.
  * Yul Optimizer: Inline into functions further down in the call graph first.
  * Yul Optimizer: Try to simplify function names.
diff --git a/libsolidity/ast/AST.cpp b/libsolidity/ast/AST.cpp
index cac28eac0..dd3e99854 100644
--- a/libsolidity/ast/AST.cpp
+++ b/libsolidity/ast/AST.cpp
@@ -208,6 +208,14 @@ vector<pair<util::FixedHash<4>, FunctionTypePointer>> const& ContractDefinition:
 	});
 }
 
+uint64_t ContractDefinition::interfaceId() const
+{
+	uint64_t result{0};
+	for (auto const& function: interfaceFunctionList(false))
+		result ^= util::fromBigEndian<uint64_t>(function.first.ref());
+	return result;
+}
+
 TypePointer ContractDefinition::type() const
 {
 	return TypeProvider::typeType(TypeProvider::contract(*this));
diff --git a/libsolidity/ast/AST.h b/libsolidity/ast/AST.h
index 2f328759c..4b1ecd2ca 100644
--- a/libsolidity/ast/AST.h
+++ b/libsolidity/ast/AST.h
@@ -509,6 +509,8 @@ public:
 	/// as intended for use by the ABI.
 	std::map<util::FixedHash<4>, FunctionTypePointer> interfaceFunctions(bool _includeInheritedFunctions = true) const;
 	std::vector<std::pair<util::FixedHash<4>, FunctionTypePointer>> const& interfaceFunctionList(bool _includeInheritedFunctions = true) const;
+	/// @returns the EIP-165 compatible interface identifier. This will exclude inherited functions.
+	uint64_t interfaceId() const;
 
 	/// @returns a list of all declarations in this contract
 	std::vector<Declaration const*> declarations() const { return filteredNodes<Declaration>(m_subNodes); }
diff --git a/libsolidity/codegen/ExpressionCompiler.cpp b/libsolidity/codegen/ExpressionCompiler.cpp
index d4f70691f..f92117689 100644
--- a/libsolidity/codegen/ExpressionCompiler.cpp
+++ b/libsolidity/codegen/ExpressionCompiler.cpp
@@ -1598,10 +1598,7 @@ bool ExpressionCompiler::visit(MemberAccess const& _memberAccess)
 		{
 			TypePointer arg = dynamic_cast<MagicType const&>(*_memberAccess.expression().annotation().type).typeArgument();
 			ContractDefinition const& contract = dynamic_cast<ContractType const&>(*arg).contractDefinition();
-			uint64_t result{0};
-			for (auto const& function: contract.interfaceFunctionList(false))
-				result ^= fromBigEndian<uint64_t>(function.first.ref());
-			m_context << (u256{result} << (256 - 32));
+			m_context << (u256{contract.interfaceId()} << (256 - 32));
 		}
 		else if (member == "min" || member == "max")
 		{
diff --git a/libsolidity/codegen/ir/IRGeneratorForStatements.cpp b/libsolidity/codegen/ir/IRGeneratorForStatements.cpp
index cacfade33..34b677c9c 100644
--- a/libsolidity/codegen/ir/IRGeneratorForStatements.cpp
+++ b/libsolidity/codegen/ir/IRGeneratorForStatements.cpp
@@ -1549,10 +1549,7 @@ void IRGeneratorForStatements::endVisit(MemberAccess const& _memberAccess)
 		{
 			TypePointer arg = dynamic_cast<MagicType const&>(*_memberAccess.expression().annotation().type).typeArgument();
 			ContractDefinition const& contract = dynamic_cast<ContractType const&>(*arg).contractDefinition();
-			uint64_t result{0};
-			for (auto const& function: contract.interfaceFunctionList(false))
-				result ^= fromBigEndian<uint64_t>(function.first.ref());
-			define(_memberAccess) << formatNumber(u256{result} << (256 - 32)) << "\n";
+			define(_memberAccess) << formatNumber(u256{contract.interfaceId()} << (256 - 32)) << "\n";
 		}
 		else if (member == "min" || member == "max")
 		{
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 1cd3264e8..bf9e02010 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -888,6 +888,11 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 				IntegerType const& integerType = dynamic_cast<IntegerType const&>(*magicType->typeArgument());
 				defineExpr(_memberAccess, memberName == "min" ? integerType.minValue() : integerType.maxValue());
 			}
+			else if (memberName == "interfaceId")
+			{
+				ContractDefinition const& contract = dynamic_cast<ContractType const&>(*magicType->typeArgument()).contractDefinition();
+				defineExpr(_memberAccess, contract.interfaceId());
+			}
 			else
 				// NOTE: supporting name, creationCode, runtimeCode would be easy enough, but the bytes/string they return are not
 				//       at all useable in the SMT checker currently
diff --git a/test/libsolidity/smtCheckerTests/types/type_interfaceid.sol b/test/libsolidity/smtCheckerTests/types/type_interfaceid.sol
new file mode 100644
index 000000000..04ce9f568
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/type_interfaceid.sol
@@ -0,0 +1,32 @@
+pragma experimental SMTChecker;
+
+interface I1 {
+}
+
+interface I2 {
+	function f() external;
+}
+
+interface I3 {
+	function f() external;
+	function g(uint, address) external;
+}
+
+contract C {
+	function f() public pure {
+		assert(type(I1).interfaceId == 0);
+		assert(type(I2).interfaceId != 0);
+		assert(type(I2).interfaceId == 0x26121ff0);
+		assert(type(I2).interfaceId != 0);
+		assert(type(I3).interfaceId == 0x822b51c6);
+	}
+	function g() public pure {
+		assert(type(I1).interfaceId == type(I2).interfaceId);
+	}
+	function h() public pure {
+		assert(type(I2).interfaceId == type(I3).interfaceId);
+	}
+}
+// ----
+// Warning 6328: (449-501): Assertion violation happens here.
+// Warning 6328: (536-588): Assertion violation happens here.