From 72ce00d3d03e243f4143edacf7d1ecee67794194 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 5 Dec 2016 20:51:03 -0800
Subject: [PATCH] fix(library/type_context): assertion violation at unification
 hints

---
 src/library/type_context.cpp | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index de7bb3d3ae..0df7fb5e03 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -2593,10 +2593,8 @@ public:
             auto instantiate_assignment_fn = [&](expr const & e, unsigned offset) {
                 if (is_var(e)) {
                     unsigned idx = var_idx(e) + offset;
-                    if (idx < m_assignment.size()) {
-                        lean_assert(m_assignment[idx]);
+                    if (idx < m_assignment.size() && m_assignment[idx])
                         return m_assignment[idx];
-                    }
                 }
                 return none_expr();
             };