From 5c118127ae1862f2a428677bebe5f4201343bb82 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 7 Jan 2015 17:06:41 -0800 Subject: [PATCH] fix(library/definitional/equations): memory access violation --- src/library/definitional/equations.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp index c750397a3..09f3809fe 100644 --- a/src/library/definitional/equations.cpp +++ b/src/library/definitional/equations.cpp @@ -967,7 +967,8 @@ class equation_compiler_fn { unsigned nindices = *inductive::get_num_indices(env(), const_name(I)); if (nindices > 0) { buffer args; - get_app_args(I, args); + get_app_args(t, args); + lean_assert(args.size() >= nindices); return all_distinct_locals(nindices, args.end() - nindices) && std::all_of(args.end() - nindices, args.end(),