Merge pull request #7851 from ethereum/smt_fix_function_type

[SMTChecker] Fix ICE for arrays and mappings of functions.

test/libsolidity/smtCheckerTests/types/data_location_in_function_type.sol

@@ -0,0 +1,5 @@
+pragma experimental SMTChecker;
+library L {
+    struct Nested { uint y; }
+    function c(function(Nested memory) external returns (uint)[] storage) external pure {}
+}

test/libsolidity/smtCheckerTests/types/function_type_array_as_reference_type.sol

@@ -0,0 +1,9 @@
+pragma experimental SMTChecker;
+contract C {
+    struct Nested { uint y; }
+    // ensure that we consider array of function pointers as reference type
+    function b(function(Nested memory) external returns (uint)[] storage) internal pure {}
+    function c(function(Nested memory) external returns (uint)[] memory) public pure {}
+    function d(function(Nested memory) external returns (uint)[] calldata) external pure {}
+}
+// ----

test/libsolidity/smtCheckerTests/types/function_type_arrays.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C {
+    function(uint) external returns (uint)[] public x;
+    function(uint) internal returns (uint)[10] y;
+    function f() view public {
+        function(uint) returns (uint)[10] memory a;
+        function(uint) returns (uint)[10] storage b = y;
+        function(uint) external returns (uint)[] memory c;
+        c = new function(uint) external returns (uint)[](200);
+        a; b;
+    }
+}
+// ----
+// Warning: (361-410): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/types/mapping_and_array_of_functions.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract test {
+    mapping (address => function() internal returns (uint)) a;
+    mapping (address => function() external) b;
+    mapping (address => function() external[]) c;
+    function() external[] d;
+}