From e18e4e3200f31b47dfed5a668837452b37c54e8d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 15 Nov 2015 11:48:34 -0800
Subject: [PATCH] fix(library/user_recursors): bug at get_num_minors

---
 src/library/user_recursors.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/library/user_recursors.cpp b/src/library/user_recursors.cpp
index 1cd8ba3d3..559f5e283 100644
--- a/src/library/user_recursors.cpp
+++ b/src/library/user_recursors.cpp
@@ -24,8 +24,8 @@ bool recursor_info::is_minor(unsigned pos) const {
 
 unsigned recursor_info::get_num_minors() const {
     unsigned r = m_num_args;
-    lean_assert(r >= get_motive_pos());
-    r -= get_motive_pos();
+    lean_assert(r >= get_motive_pos() + 1);
+    r -= (get_motive_pos() + 1);
     lean_assert(m_major_pos >= get_first_index_pos());
     lean_assert(r >= m_major_pos - get_first_index_pos() + 1);
     r -= (m_major_pos - get_first_index_pos() + 1);