diff --git a/Changelog.md b/Changelog.md
index 50a3e4d1e..f37d9e096 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -8,6 +8,7 @@ Compiler Features:
 
 Bugfixes:
  * SMTChecker: Fix internal error when fixed points are used.
+ * SMTChecker: Fix internal error when using array slices.
  * Type Checker: Disallow ``virtual`` and ``override`` for constructors.
  * Type Checker: Fix several internal errors by performing size and recursiveness checks of types before the full type checking.
  * Type Checker: Perform recursiveness check on structs declared at the file level.
diff --git a/libsolidity/formal/SymbolicTypes.cpp b/libsolidity/formal/SymbolicTypes.cpp
index 0364a0458..b8da5da0c 100644
--- a/libsolidity/formal/SymbolicTypes.cpp
+++ b/libsolidity/formal/SymbolicTypes.cpp
@@ -69,8 +69,14 @@ SortPointer smtSort(frontend::Type const& _type)
 		}
 		else
 		{
-			solAssert(isArray(_type.category()), "");
-			auto arrayType = dynamic_cast<frontend::ArrayType const*>(&_type);
+			frontend::ArrayType const* arrayType = nullptr;
+			if (auto const* arr = dynamic_cast<frontend::ArrayType const*>(&_type))
+				arrayType = arr;
+			else if (auto const* slice = dynamic_cast<frontend::ArraySliceType const*>(&_type))
+				arrayType = &slice->arrayType();
+			else
+				solAssert(false, "");
+
 			solAssert(arrayType, "");
 			return make_shared<ArraySort>(SortProvider::intSort, smtSortAbstractFunction(*arrayType->baseType()));
 		}
@@ -297,7 +303,8 @@ bool isMapping(frontend::Type::Category _category)
 bool isArray(frontend::Type::Category _category)
 {
 	return _category == frontend::Type::Category::Array ||
-		_category == frontend::Type::Category::StringLiteral;
+		_category == frontend::Type::Category::StringLiteral ||
+		_category == frontend::Type::Category::ArraySlice;
 }
 
 bool isTuple(frontend::Type::Category _category)
diff --git a/test/libsolidity/smtCheckerTests/operators/slices_1.sol b/test/libsolidity/smtCheckerTests/operators/slices_1.sol
new file mode 100644
index 000000000..c723472a8
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/slices_1.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(bytes calldata x) external pure {
+		x[:18726387213];
+		x[18726387213:];
+		x[18726387213:111111111111111111];
+	}
+}
+// ----
+// Warning: (94-109): Assertion checker does not yet implement this expression.
+// Warning: (113-128): Assertion checker does not yet implement this expression.
+// Warning: (132-165): Assertion checker does not yet implement this expression.
diff --git a/test/libsolidity/smtCheckerTests/typecast/slice_to_bytes.sol b/test/libsolidity/smtCheckerTests/typecast/slice_to_bytes.sol
new file mode 100644
index 000000000..1fb74bac9
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/typecast/slice_to_bytes.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+
+contract C {
+	function f(bytes calldata x) external pure {
+		bytes(x[:18726387213]);
+		bytes(x[18726387213:]);
+		bytes(x[18726387213:111111111111111111]);
+	}
+}
+// ----
+// Warning: (100-115): Assertion checker does not yet implement this expression.
+// Warning: (126-141): Assertion checker does not yet implement this expression.
+// Warning: (152-185): Assertion checker does not yet implement this expression.