From 9fde9fe3a20fcba744363442cffcc8f5062324d8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 2 Feb 2019 19:49:16 +0100
Subject: [PATCH] fix #2122 for code that isn't exception safe

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/polynomial/upolynomial.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp
index 0290a5924..f300dc4ab 100644
--- a/src/math/polynomial/upolynomial.cpp
+++ b/src/math/polynomial/upolynomial.cpp
@@ -524,11 +524,11 @@ namespace upolynomial {
         set(sz1, p1, buffer);
         if (sz1 <= 1)
             return;
+		
         numeral const & b_n = p2[sz2-1];
         SASSERT(!m().is_zero(b_n));
         scoped_numeral a_m(m());
-        while (true) {
-            checkpoint();
+        while (m_limit.inc()) {			
             TRACE("rem_bug", tout << "rem loop, p2:\n"; display(tout, sz2, p2); tout << "\nbuffer:\n"; display(tout, buffer); tout << "\n";);
             sz1 = buffer.size();
             if (sz1 < sz2) {