Fix internal compiler error in model checker: do not require function…

… to be external
ethereum · Jun 20, 2023 · cd5c113 · cd5c113
1 parent 3ecf968
commit cd5c113
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 1 deletion.
diff --git 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
@@ -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
+// ----