From c395516058f5d0c756c892066d07cb074b415140 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Sun, 25 Jun 2017 22:19:42 +0100
Subject: [PATCH] Adjusted rlimit increments in theory_arith to avoid
 non-termination issues

---
 src/smt/theory_arith_core.h | 2 +-
 src/util/mpq.h              | 4 +++-
 src/util/mpz.h              | 4 ++--
 src/util/rational.h         | 2 ++
 4 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h
index ae015c08f..bee744c34 100644
--- a/src/smt/theory_arith_core.h
+++ b/src/smt/theory_arith_core.h
@@ -1984,7 +1984,7 @@ namespace smt {
                         a_kj = r2[it->m_row_idx].m_coeff;
                         a_kj.neg();
                         add_row(it->m_row_id, a_kj, r_id, apply_gcd_test);
-                        get_manager().limit().inc(r1_sz + r2.size());
+                        get_manager().limit().inc((r1_sz + r2.size()) * (a_kj.storage_size()));
                     }
                 }
                 else { 
diff --git a/src/util/mpq.h b/src/util/mpq.h
index 474d38802..11e17bbf9 100644
--- a/src/util/mpq.h
+++ b/src/util/mpq.h
@@ -176,7 +176,7 @@ public:
 
     static bool is_small(mpz const & a) { return mpz_manager<SYNCH>::is_small(a); }
 
-    static bool is_small(mpq const & a) { return is_small(a.m_num) && is_small(a.m_den); }
+    static bool is_small(mpq const & a) { return is_small(a.m_num) && is_small(a.m_den); }    
 
     static mpq mk_q(int v) { return mpq(v); }
 
@@ -786,6 +786,8 @@ public:
 
     unsigned bitsize(mpz const & a) { return mpz_manager<SYNCH>::bitsize(a); }
     unsigned bitsize(mpq const & a) { return is_int(a) ? bitsize(a.m_num) : bitsize(a.m_num) + bitsize(a.m_den); }
+    unsigned storage_size(mpz const & a) { return mpz_manager<SYNCH>::size_info(a); }
+    unsigned storage_size(mpq const & a) { return mpz_manager<SYNCH>::size_info(a.m_num) + mpz_manager<SYNCH>::size_info(a.m_den); }
 
     /**
        \brief Return true if the number is a perfect square, and 
diff --git a/src/util/mpz.h b/src/util/mpz.h
index 67947b602..c02ac7c36 100644
--- a/src/util/mpz.h
+++ b/src/util/mpz.h
@@ -316,11 +316,11 @@ class mpz_manager {
     void big_rem(mpz const & a, mpz const & b, mpz & c);
 
     int big_compare(mpz const & a, mpz const & b);
-    
+
+public:
     unsigned size_info(mpz const & a);
     struct sz_lt;
 
-public:
     static bool precise() { return true; }
     static bool field() { return false; }
 
diff --git a/src/util/rational.h b/src/util/rational.h
index 4fa3382ec..26ef7dbb1 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -68,6 +68,8 @@ public:
     mpq const & to_mpq() const { return m_val; }
 
     unsigned bitsize() const { return m().bitsize(m_val); }
+
+    unsigned storage_size() const { return m().storage_size(m_val); }
     
     void reset() { m().reset(m_val); }