From cd5c113a9b746c3c1f60a5570ff7885c4aeef5a5 Mon Sep 17 00:00:00 2001
From: Pawel Gebal <pawel.gebal@imapp.pl>
Date: Tue, 20 Jun 2023 19:38:30 +0200
Subject: [PATCH] Fix internal compiler error in model checker: do not require
 function to be external

---
 libsolidity/formal/SMTEncoder.cpp                  |  2 +-
 .../functions/functions_library_internal.sol       | 14 ++++++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)
 create mode 100644 test/libsolidity/smtCheckerTests/functions/functions_library_internal.sol

diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 818efac5cbb1..31841fca2940 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1358,7 +1358,7 @@ bool SMTEncoder::visit(MemberAccess const& _memberAccess)
 	{
 		auto const* functionType = dynamic_cast<FunctionType const*>(_memberAccess.annotation().type);
 		if (functionType && functionType->hasDeclaration())
-			defineExpr(_memberAccess, functionType->externalIdentifier());
+			defineExpr(_memberAccess, u256(_memberAccess.id()));
 
 		return true;
 	}
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_library_internal.sol b/test/libsolidity/smtCheckerTests/functions/functions_library_internal.sol
new file mode 100644
index 000000000000..405c3f71507e
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_library_internal.sol
@@ -0,0 +1,14 @@
+library L {
+	function value(function()internal a, uint256 b) internal {}
+}
+contract C {
+	using L for function()internal;
+
+	function f() public {
+		function()internal x;
+		x.value(42);
+ 	}
+}
+// ====
+// SMTEngine: all
+// ----