From cb479a75aeb40f80fea31372466024fbc7c07245 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 17 Apr 2014 13:25:21 -0700 Subject: [PATCH] fix(kernel/expr): make sure we cannot create a free variable with index uint_max, reason: get_free_var_range would return an incorrect value Signed-off-by: Leonardo de Moura --- src/kernel/expr.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index aa7dfcdf78..245b07f8e6 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -79,7 +79,10 @@ void expr_cell::set_is_arrow(bool flag) { // Expr variables expr_var::expr_var(unsigned idx): expr_cell(expr_kind::Var, idx, false, false, false), - m_vidx(idx) {} + m_vidx(idx) { + if (idx == std::numeric_limits::max()) + throw exception("invalid free variable index, de Bruijn index is too big"); +} // Expr constants expr_const::expr_const(name const & n, levels const & ls):