From 9bfa73ee062370b35eb0dedc9611b6443f83939b Mon Sep 17 00:00:00 2001
From: Johannes Kanig <kanig@adacore.com>
Date: Wed, 8 Jun 2016 11:17:26 +0900
Subject: [PATCH] Take into account number of monomials for rlimit counting

Should fix issue #611
---
 src/math/grobner/grobner.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/math/grobner/grobner.cpp b/src/math/grobner/grobner.cpp
index 0c96dfde3..baa16b405 100644
--- a/src/math/grobner/grobner.cpp
+++ b/src/math/grobner/grobner.cpp
@@ -446,6 +446,7 @@ void grobner::merge_monomials(ptr_vector<monomial> & monomials) {
     SASSERT(&m_del_monomials != &monomials);
     ptr_vector<monomial>& to_delete = m_del_monomials;
     to_delete.reset();
+    m_manager.limit().inc(sz);
     for (unsigned i = 1; i < sz; ++i) {
         monomial * m1 = monomials[j];
         monomial * m2 = monomials[i];