From d5c7d078eb847731c0e9bf2f46f0bfe86f9364fe Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Mon, 29 May 2017 14:58:05 +0200
Subject: [PATCH] fix(library/type_context): check for stack overflow

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

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index b1e2a65be8..1bf2f8ec44 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -2718,6 +2718,7 @@ bool type_context::on_is_def_eq_failure(expr const & e1, expr const & e2) {
 
 /* If e is a numeral, then return it. Otherwise return none. */
 static optional<mpz> eval_num(expr const & e) {
+    check_system("eval_num");
     if (is_constant(e, get_nat_zero_name())) {
         return some(mpz(0));
     } else if (is_app_of(e, get_has_zero_zero_name(), 2)) {