diff --git a/Changelog.md b/Changelog.md
index 7b828a989..93cb33af7 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -17,6 +17,7 @@ Build System:
 
 Bugfixes:
  * SMTChecker: Fix internal error when using ``abi.decode``.
+ * SMTChecker: Fix internal error when using arrays or mappings of functions.
 
 
 
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 591158a25..0fe05e723 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -63,7 +63,7 @@ SortPointer smtSort(solidity::Type const& _type)
 		{
 			auto mapType = dynamic_cast<solidity::MappingType const*>(&_type);
 			solAssert(mapType, "");
-			return make_shared<ArraySort>(smtSort(*mapType->keyType()), smtSort(*mapType->valueType()));
+			return make_shared<ArraySort>(smtSortAbstractFunction(*mapType->keyType()), smtSortAbstractFunction(*mapType->valueType()));
 		}
 		else if (isStringLiteral(_type.category()))
 		{
@@ -77,7 +77,7 @@ SortPointer smtSort(solidity::Type const& _type)
 			solAssert(isArray(_type.category()), "");
 			auto arrayType = dynamic_cast<solidity::ArrayType const*>(&_type);
 			solAssert(arrayType, "");
-			return make_shared<ArraySort>(make_shared<Sort>(Kind::Int), smtSort(*arrayType->baseType()));
+			return make_shared<ArraySort>(make_shared<Sort>(Kind::Int), smtSortAbstractFunction(*arrayType->baseType()));
 		}
 	}
 	default:
@@ -94,6 +94,13 @@ vector<SortPointer> smtSort(vector<solidity::TypePointer> const& _types)
 	return sorts;
 }
 
+SortPointer smtSortAbstractFunction(solidity::Type const& _type)
+{
+	if (isFunction(_type.category()))
+		return make_shared<Sort>(Kind::Int);
+	return smtSort(_type);
+}
+
 Kind smtKind(solidity::Type::Category _category)
 {
 	if (isNumber(_category))
diff --git a/libsolidity/formal/SymbolicTypes.h b/libsolidity/formal/SymbolicTypes.h
index 30a341431..2db2807ac 100644
--- a/libsolidity/formal/SymbolicTypes.h
+++ b/libsolidity/formal/SymbolicTypes.h
@@ -32,6 +32,9 @@ namespace smt
 /// Returns the SMT sort that models the Solidity type _type.
 SortPointer smtSort(solidity::Type const& _type);
 std::vector<SortPointer> smtSort(std::vector<solidity::TypePointer> const& _types);
+/// If _type has type Function, abstract it to Integer.
+/// Otherwise return smtSort(_type).
+SortPointer smtSortAbstractFunction(solidity::Type const& _type);
 /// Returns the SMT kind that models the Solidity type type category _category.
 Kind smtKind(solidity::Type::Category _category);
 
diff --git a/test/libsolidity/smtCheckerTests/types/data_location_in_function_type.sol b/test/libsolidity/smtCheckerTests/types/data_location_in_function_type.sol
new file mode 100644
index 000000000..9aa72ea7d
--- /dev/null
+++ b/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 {}
+}
diff --git a/test/libsolidity/smtCheckerTests/types/function_type_array_as_reference_type.sol b/test/libsolidity/smtCheckerTests/types/function_type_array_as_reference_type.sol
new file mode 100644
index 000000000..2500d3ec7
--- /dev/null
+++ b/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 {}
+}
+// ----
diff --git a/test/libsolidity/smtCheckerTests/types/function_type_arrays.sol b/test/libsolidity/smtCheckerTests/types/function_type_arrays.sol
new file mode 100644
index 000000000..f004b5514
--- /dev/null
+++ b/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.
diff --git a/test/libsolidity/smtCheckerTests/types/mapping_and_array_of_functions.sol b/test/libsolidity/smtCheckerTests/types/mapping_and_array_of_functions.sol
new file mode 100644
index 000000000..a10559ece
--- /dev/null
+++ b/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;
+}