diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 85ec5e776..421bfb3b6 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -748,6 +748,12 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 		return;
 	}
 
+	if (!_indexAccess.indexExpression())
+	{
+		solAssert(_indexAccess.annotation().type->category() == Type::Category::TypeType, "");
+		return;
+	}
+
 	solAssert(array, "");
 	defineExpr(_indexAccess, smt::Expression::select(
 		array->currentValue(),
diff --git a/test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol b/test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol
new file mode 100644
index 000000000..f63e6aef3
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/type_expression_array_2d.sol
@@ -0,0 +1,11 @@
+pragma experimental SMTChecker;
+contract C {
+
+function f() public pure { int[][]; }
+
+}
+// ----
+// Warning: (73-80): Statement has no effect.
+// Warning: (73-78): Assertion checker does not yet implement type type(int256[] memory)
+// Warning: (73-78): Assertion checker does not yet implement this expression.
+// Warning: (73-80): Assertion checker does not yet implement type type(int256[] memory[] memory)
diff --git a/test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol b/test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol
new file mode 100644
index 000000000..2588ee98d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/type_expression_array_3d.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract C {
+
+function f() public pure { int[][][]; }
+
+}
+// ----
+// Warning: (73-82): Statement has no effect.
+// Warning: (73-78): Assertion checker does not yet implement type type(int256[] memory)
+// Warning: (73-78): Assertion checker does not yet implement this expression.
+// Warning: (73-80): Assertion checker does not yet implement type type(int256[] memory[] memory)
+// Warning: (73-82): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)
diff --git a/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol b/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol
new file mode 100644
index 000000000..02c2ac056
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_2d.sol
@@ -0,0 +1,12 @@
+pragma experimental SMTChecker;
+contract C {
+
+function f() public pure { (int[][]); }
+
+}
+// ----
+// Warning: (73-82): Statement has no effect.
+// Warning: (74-79): Assertion checker does not yet implement type type(int256[] memory)
+// Warning: (74-79): Assertion checker does not yet implement this expression.
+// Warning: (74-81): Assertion checker does not yet implement type type(int256[] memory[] memory)
+// Warning: (73-82): Assertion checker does not yet implement type type(int256[] memory[] memory)
diff --git a/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol b/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol
new file mode 100644
index 000000000..893f30581
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/types/type_expression_tuple_array_3d.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+
+function f() public pure { (int[][][]); }
+
+}
+// ----
+// Warning: (73-84): Statement has no effect.
+// Warning: (74-79): Assertion checker does not yet implement type type(int256[] memory)
+// Warning: (74-79): Assertion checker does not yet implement this expression.
+// Warning: (74-81): Assertion checker does not yet implement type type(int256[] memory[] memory)
+// Warning: (74-83): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)
+// Warning: (73-84): Assertion checker does not yet implement type type(int256[] memory[] memory[] memory)