From 5dacaf57bc224823097753267437d27715615b2c Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Fri, 8 Nov 2019 17:29:40 +0100
Subject: [PATCH] Fix ICE in FixedBytes IndexAccess

---
 Changelog.md                                           |  1 +
 libsolidity/formal/SMTEncoder.cpp                      |  9 +++++++++
 .../operators/index_access_for_bytes.sol               | 10 ++++++++++
 3 files changed, 20 insertions(+)
 create mode 100644 test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol

diff --git a/Changelog.md b/Changelog.md
index a3660ab94..511873074 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -15,6 +15,7 @@ Bugfixes:
  * Type Checker: Disallow constructor of the same class to be used as modifier
  * Code Generator: Fixed a faulty assert that would wrongly trigger for array sizes exceeding unsigned integer
  * Type Checker: Treat magic variables as unknown identifiers in inline assembly
+ * SMTChecker: Fix internal error when accessing indices of fixed bytes.
 
 
 
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 9a0b0065c..c55f2a52f 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -766,6 +766,15 @@ void SMTEncoder::endVisit(IndexAccess const& _indexAccess)
 		auto varDecl = identifierToVariable(*id);
 		solAssert(varDecl, "");
 		array = m_context.variable(*varDecl);
+
+		if (varDecl->type()->category() == Type::Category::FixedBytes)
+		{
+			m_errorReporter.warning(
+				_indexAccess.location(),
+				"Assertion checker does not yet support index accessing fixed bytes."
+			);
+			return;
+		}
 	}
 	else if (auto const& innerAccess = dynamic_cast<IndexAccess const*>(&_indexAccess.baseExpression()))
 	{
diff --git a/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol b/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol
new file mode 100644
index 000000000..0169efaec
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/index_access_for_bytes.sol
@@ -0,0 +1,10 @@
+pragma experimental SMTChecker;
+contract C {
+    bytes20 x;
+    function f(bytes16 b) public view {
+        b[uint8(x[2])];
+    }
+}
+// ----
+// Warning: (116-120): Assertion checker does not yet support index accessing fixed bytes.
+// Warning: (108-122): Assertion checker does not yet support index accessing fixed bytes.