From 01a2c32d3874fb4fccd24f4624c7dfe0e438a59b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 3 Sep 2016 16:21:34 -0700 Subject: [PATCH] fix(library/old_default_converter): avoid underflow --- src/library/old_default_converter.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/old_default_converter.cpp b/src/library/old_default_converter.cpp index fde4d75246..1bceda81d5 100644 --- a/src/library/old_default_converter.cpp +++ b/src/library/old_default_converter.cpp @@ -524,8 +524,8 @@ auto old_default_converter::lazy_delta_reduction_step(expr & t_n, expr & s_n, co } } } - t_n = whnf_core(unfold_names(t_n, d_t->get_height() - 1)); - s_n = whnf_core(unfold_names(s_n, d_s->get_height() - 1)); + t_n = whnf_core(unfold_names(t_n, d_t->get_height() > 0 ? d_t->get_height() - 1 : 0)); + s_n = whnf_core(unfold_names(s_n, d_s->get_height() > 0 ? d_s->get_height() - 1 : 0)); } switch (quick_is_def_eq(t_n, s_n, cs)) { case l_true: return reduction_status::DefEqual;