SMTChecker fails to handle arrays of pure/view functions

[lum7na]

Description

The following code triggers an SMT logic error. This appears to be due to solc treating function () external returns (uint256)_array_tuple as distinct from function () view external returns (uint256)_array_tuple. However, the code compiles successfully, indicating that solc's type checking deems it valid.

contract C {

  function() external returns(uint)[1] a;

  function b() external view returns(uint) {
    return 1;
  }

  function test() public returns(uint) {
    a = [this.b];
    return a[0]();
  }
}

Compile: solc --model-checker-engine all a.sol

Output:

SMT logic error:
/solidity/libsmtutil/Z3Interface.cpp(270): Throw in function z3::expr solidity::smtutil::Z3Interface::toZ3Expr(const solidity::smtutil::Expression&)
Dynamic exception type: boost::wrapexcept<solidity::smtutil::SMTLogicError>
std::exception::what: Sorts |function () external returns (uint256)_array_tuple| and |function () view external returns (uint256)_array_tuple| are incompatible
[solidity::util::tag_comment*] = Sorts |function () external returns (uint256)_array_tuple| and |function () view external returns (uint256)_array_tuple| are incompatible

The same issue occurs if function b is defined as a pure function.

Environment

• Compiler version: 0.8.25