diff --git a/src/test/algebraic.cpp b/src/test/algebraic.cpp
index 7c0fb4a95..af7270825 100644
--- a/src/test/algebraic.cpp
+++ b/src/test/algebraic.cpp
@@ -19,35 +19,37 @@ Notes:
 #include"algebraic_numbers.h"
 #include"polynomial_var2value.h"
 #include"mpbq.h"
+#include"rlimit.h"
 
 static void display_anums(std::ostream & out, scoped_anum_vector const & rs) {
     out << "numbers in decimal:\n";
     algebraic_numbers::manager & m = rs.m();
     for (unsigned i = 0; i < rs.size(); i++) {
-        m.display_decimal(out, rs[i], 10);  
+        m.display_decimal(out, rs[i], 10);
         out << "\n";
     }
     out << "numbers as root objects\n";
     for (unsigned i = 0; i < rs.size(); i++) {
-        m.display_root(out, rs[i]);  
+        m.display_root(out, rs[i]);
         out << "\n";
-    } 
+    }
     out << "numbers as intervals\n";
     for (unsigned i = 0; i < rs.size(); i++) {
-        m.display_interval(out, rs[i]);  
+        m.display_interval(out, rs[i]);
         out << "\n";
-    } 
+    }
 }
 
 static void tst1() {
+    reslimit rl;
     unsynch_mpq_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     polynomial_ref p(m);
     p = 3*x - 2;
 
-    algebraic_numbers::manager am(nm);
+    algebraic_numbers::manager am(rl, nm);
     scoped_anum_vector rs1(am);
     std::cout << "p: " << p << "\n";
     am.isolate_roots(p, rs1);
@@ -69,16 +71,16 @@ static void tst1() {
     nm.set(q, 1, 3);
     scoped_anum aq(am);
     am.set(aq, q); // create algebraic number representing 1/3
-    
+
     am.add(sqrt2, aq, aq);
-    std::cout << "sqrt(2) + 1/3: "; 
-    am.display_decimal(std::cout, aq, 10); std::cout << " "; am.display_interval(std::cout, aq); 
+    std::cout << "sqrt(2) + 1/3: ";
+    am.display_decimal(std::cout, aq, 10); std::cout << " "; am.display_interval(std::cout, aq);
     std::cout << " "; am.display_root(std::cout, aq); std::cout << "\n";
 
-    am.set(aq, q); 
+    am.set(aq, q);
     am.add(rs1[0], aq, aq);
-    std::cout << "-sqrt(2) + 1/3: "; 
-    am.display_decimal(std::cout, aq, 10); std::cout << " "; am.display_interval(std::cout, aq); 
+    std::cout << "-sqrt(2) + 1/3: ";
+    am.display_decimal(std::cout, aq, 10); std::cout << " "; am.display_interval(std::cout, aq);
     std::cout << " "; am.display_root(std::cout, aq); std::cout << "\n";
 
     p = ((x^5) - x - 1)*(x-1)*(x-2);
@@ -92,7 +94,7 @@ static void tst1() {
     am.set(gauss, rs1[1]);
 
     std::cout << "compare(" << sqrt2 << ", " << gauss << "): " << am.compare(sqrt2, gauss) << "\n";
-    
+
     statistics st;
     am.collect_statistics(st);
     st.display_smt2(std::cout);
@@ -103,7 +105,7 @@ static void tst1() {
     am.isolate_roots(p, rs1);
     display_anums(std::cout, rs1);
     SASSERT(rs1.size() == 4);
-    
+
     scoped_anum hidden_sqrt2(am);
     am.set(hidden_sqrt2, rs1[2]);
 
@@ -116,7 +118,7 @@ static void tst1() {
 
     SASSERT(is_int(power(sqrt2, 4)));
     SASSERT(power(sqrt2, 4) == 4);
-    
+
     scoped_anum sqrt2_gauss(am);
     am.add(sqrt2, gauss, sqrt2_gauss);
     std::cout << "sqrt2 + gauss: " << sqrt2_gauss << " "; am.display_root(std::cout, sqrt2_gauss); std::cout << "\n";
@@ -151,22 +153,22 @@ static void tst1() {
     am.mul(tmp, sqrt2, tmp);
     std::cout << "sqrt(2)*4*(1/sqrt2): " << tmp << "  " << root_obj_pp(tmp) << "\n";
     std::cout << "is_int(sqrt(2)*4*(1/sqrt2)): " << am.is_int(tmp) << ", after is-int: " << tmp << "\n";
-    
+
     p = (998*x - 1414)*((x^2) - 15);
     std::cout << "p: " << p << "\n";
     rs1.reset();
     am.isolate_roots(p, rs1);
-    
+
     std::cout << "is-rational(sqrt2): " << am.is_rational(sqrt2) << "\n";
-    
+
     scoped_anum qr(am);
     am.set(qr, rs1[1]);
-    
+
     std::cout << "qr: " << root_obj_pp(qr);
     std::cout << ", is-rational: " << am.is_rational(qr) << ", val: " << root_obj_pp(qr) << "\n";
 
     return;
-    
+
     std::cout << "compare(" << sqrt2 << ", " << gauss << "): " << am.compare(sqrt2, gauss) << "\n";
 
     p = (x^16) - 136*(x^14) + 6476*(x^12) - 141912*(x^10) + 1513334*(x^8) - 7453176*(x^6) + 13950764*(x^4) - 5596840*(x^2) + 46225;
@@ -216,25 +218,26 @@ void tst_mpbq_root() {
     mpbq_manager        bqm(qm);
     // scoped_mpbq q(bqm);
     // q.set(q1, 1.4142135 , 7);
-    
+
 }
 
 static void tst_wilkinson() {
     // Test Wilkinson Polynomial
+    reslimit rl;
     unsynch_mpq_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     polynomial_ref p(m);
     for (int i = 1; i <= 20; i++) {
-        if (i > 1) 
+        if (i > 1)
             p = p*(x - i);
-        else 
+        else
             p = (x - i);
     }
     std::cout << "Wilkinson's polynomial: " << p << "\n";
 
-    algebraic_numbers::manager am(nm);
+    algebraic_numbers::manager am(rl, nm);
     scoped_anum_vector rs1(am);
     std::cout << "p: " << p << "\n";
     am.isolate_roots(p, rs1);
@@ -246,9 +249,10 @@ static void tst_wilkinson() {
 }
 
 static void tst_dejan() {
+    reslimit rl;
     unsynch_mpq_manager qm;
-    algebraic_numbers::manager am(qm);
-    
+    algebraic_numbers::manager am(rl, qm);
+
     scoped_anum two101(am);
     am.set(two101, 2);
     am.root(two101, 11, two101);
@@ -256,7 +260,7 @@ static void tst_dejan() {
     scoped_anum two103(am);
     am.set(two103, 2);
     am.root(two103, 7, two103);
-    
+
     std::cout << "two101: " << two101 << " " << root_obj_pp(two101) << std::endl;
     std::cout << "two103: " << two103 << " " << root_obj_pp(two103) << std::endl;
 
@@ -332,9 +336,10 @@ static void tst_eval_sign(polynomial_ref const & p, anum_manager & am,
 
 static void tst_eval_sign() {
     enable_trace("anum_eval_sign");
+    reslimit rl;
     unsynch_mpq_manager        qm;
-    polynomial::manager        pm(qm);
-    algebraic_numbers::manager am(qm);
+    polynomial::manager        pm(rl, qm);
+    algebraic_numbers::manager am(rl, qm);
     polynomial_ref x0(pm);
     polynomial_ref x1(pm);
     polynomial_ref x2(pm);
@@ -351,7 +356,7 @@ static void tst_eval_sign() {
     am.set(v1,  1);
     am.set(v0, -3);
     tst_eval_sign(p, am, 0, v0, 1, v1, 2, v2, -1);
-    
+
     am.set(v0, 2);
     am.root(v0, 2, v0);
     am.set(v1, 0);
@@ -412,9 +417,10 @@ static void tst_isolate_roots(polynomial_ref const & p, anum_manager & am,
 
 static void tst_isolate_roots() {
     enable_trace("isolate_roots");
+    reslimit rl;
     unsynch_mpq_manager        qm;
-    polynomial::manager        pm(qm);
-    algebraic_numbers::manager am(qm);
+    polynomial::manager        pm(rl, qm);
+    algebraic_numbers::manager am(rl, qm);
     polynomial_ref x0(pm);
     polynomial_ref x1(pm);
     polynomial_ref x2(pm);
@@ -423,7 +429,7 @@ static void tst_isolate_roots() {
     x1 = pm.mk_polynomial(pm.mk_var());
     x2 = pm.mk_polynomial(pm.mk_var());
     x3 = pm.mk_polynomial(pm.mk_var());
-    
+
     polynomial_ref p(pm);
     p = x3*x1 + 1;
 
@@ -432,44 +438,44 @@ static void tst_isolate_roots() {
     tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);
 
     am.set(v1, 1);
-    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);    
+    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);
 
     am.set(v1, 2);
     am.root(v1, 2, v1);
-    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);    
-    
+    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);
+
     p = (x1 + x2)*x3 + 1;
     am.set(v2, v1);
-    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);    
-    
+    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);
+
     p = (x1 + x2)*x3 + x1*x2 + 2;
-    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);    
+    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);
 
     p = (x1 + x2)*(x3^3) + x1*x2 + 2;
-    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);    
+    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);
 
     p = (x1 + x2)*(x3^2) - x1*x2 - 2;
-    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);    
-    
+    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);
+
     p = x0*(x1 + x2)*(x3^2) - x0*x1*x2 - 2;
-    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);    
+    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);
 
     p = (x1 - x2)*x3 + x1*x2 - 2;
-    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);    
+    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);
 
     p = (x1 - x2)*(x3^3) + x1*x2 - 2;
-    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);    
- 
+    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);
+
     p = (x3 - x0)*(x3 - x0 - x1);
     am.set(v0, 2);
     am.root(v0, 2, v0); // x2 -> sqrt(2)
     am.set(v1, 3);
     am.root(v1, 2, v1); // x1 -> sqrt(3)
     am.reset(v2);
-    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);    
-    
+    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);
+
     p = (x3 - x0)*((x3 - x0 - x1)^2);
-    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);    
+    tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);
 
     p = (x3 - x0)*(x3 - 2)*((x3 - 1)^2)*(x3 - x1);
     tst_isolate_roots(p, am, 0, v0, 1, v1, 2, v2);
@@ -485,7 +491,8 @@ static void pp(polynomial_ref const & p, polynomial::var x) {
 
 static void ex1() {
     unsynch_mpq_manager        qm;
-    polynomial::manager        pm(qm);
+    reslimit rl;
+    polynomial::manager        pm(rl, qm);
     polynomial_ref x(pm);
     polynomial_ref a(pm);
     polynomial_ref b(pm);
@@ -508,7 +515,7 @@ static void ex1() {
     std::cout << "d: " << d << "\n";
     std::cout << "h3: "; pp(h3, 0); std::cout << "\n";
 
-    algebraic_numbers::manager am(qm);
+    algebraic_numbers::manager am(rl, qm);
     scoped_anum v1(am), v2(am);
     am.set(v1, 2);
     am.root(v1, 3, v1);
@@ -542,8 +549,9 @@ static void ex1() {
 }
 
 static void tst_root() {
+    reslimit rl;
     unsynch_mpq_manager        qm;
-    algebraic_numbers::manager am(qm);
+    algebraic_numbers::manager am(rl, qm);
     scoped_anum v1(am), v2(am);
     am.set(v1, 4);
     am.root(v1, 2, v2);
@@ -551,7 +559,7 @@ static void tst_root() {
     am.set(v1, 4);
     am.root(v1, 4, v2);
     std::cout << "root: " << root_obj_pp(v2) << "\n";
-    
+
 }
 
 void tst_algebraic() {
diff --git a/src/test/hilbert_basis.cpp b/src/test/hilbert_basis.cpp
index 57c8c5050..b46ede849 100644
--- a/src/test/hilbert_basis.cpp
+++ b/src/test/hilbert_basis.cpp
@@ -12,6 +12,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "tactic.h"
 #include "tactic2solver.h"
 #include "solver.h"
+#include "rlimit.h"
 #include <signal.h>
 #include <time.h>
 #include <sstream>
@@ -38,7 +39,7 @@ class hilbert_basis_validate {
     }
 
 public:
-        
+
     hilbert_basis_validate(ast_manager& m);
 
     expr_ref mk_validate(hilbert_basis& hb);
@@ -46,7 +47,7 @@ public:
 };
 
 
-hilbert_basis_validate::hilbert_basis_validate(ast_manager& m): 
+hilbert_basis_validate::hilbert_basis_validate(ast_manager& m):
     m(m) {
 }
 
@@ -86,7 +87,7 @@ void hilbert_basis_validate::validate_solution(hilbert_basis& hb, vector<rationa
         }
         std::cout << "\n";
         std::cout << "sum: " << sum << "\n";
-    }        
+    }
 }
 
 expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
@@ -94,7 +95,7 @@ expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
     unsigned sz = hb.get_basis_size();
     vector<rational> v;
 
-    // check that claimed solution really satisfies inequalities:        
+    // check that claimed solution really satisfies inequalities:
     for (unsigned i = 0; i < sz; ++i) {
         bool is_initial;
         hb.get_basis_solution(i, v, is_initial);
@@ -111,7 +112,7 @@ expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
     sort_ref_vector sorts(m);
 
 #define mk_mul(_r,_x) (_r.is_one()?((expr*)_x):((expr*)a.mk_mul(a.mk_numeral(_r,true),_x)))
-    
+
 
     for (unsigned i = 0; i < sz; ++i) {
         bool is_initial;
@@ -169,7 +170,7 @@ expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
     }
     fml1 = m.mk_or(fmls.size(), fmls.c_ptr());
     fmls.reset();
-    
+
     sz = hb.get_num_ineqs();
     for (unsigned i = 0; i < sz; ++i) {
         bool is_eq;
@@ -194,7 +195,7 @@ expr_ref hilbert_basis_validate::mk_validate(hilbert_basis& hb) {
     }
     fml2 = m.mk_and(fmls.size(), fmls.c_ptr());
     fml = m.mk_eq(fml1, fml2);
-    
+
     bounds.reset();
     for (unsigned i = 0; i < xs.size(); ++i) {
         if (!hb.get_is_int(i)) {
@@ -221,7 +222,7 @@ static void display_statistics(hilbert_basis& hb) {
 }
 
 static void on_ctrl_c(int) {
-    signal (SIGINT, SIG_DFL);    
+    signal (SIGINT, SIG_DFL);
     display_statistics(*g_hb);
     raise(SIGINT);
 }
@@ -258,17 +259,17 @@ static void saturate_basis(hilbert_basis& hb) {
     lbool is_sat = hb.saturate();
 
     switch(is_sat) {
-    case l_true:  
-        std::cout << "sat\n"; 
+    case l_true:
+        std::cout << "sat\n";
         hb.display(std::cout);
         //validate_sat(hb);
         break;
-    case l_false: 
-        std::cout << "unsat\n"; 
+    case l_false:
+        std::cout << "unsat\n";
+        break;
+    case l_undef:
+        std::cout << "undef\n";
         break;
-    case l_undef: 
-        std::cout << "undef\n"; 
-        break;       
     }
     display_statistics(hb);
 }
@@ -283,7 +284,8 @@ static void saturate_basis(hilbert_basis& hb) {
 static void gorrila_test(unsigned seed, unsigned n, unsigned k, unsigned bound, unsigned num_ineqs) {
     std::cout << "Gorrila test\n";
     random_gen rand(seed);
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     SASSERT(0 < bound);
     SASSERT(k <= n);
     int ibound = static_cast<int>(bound);
@@ -303,7 +305,7 @@ static void gorrila_test(unsigned seed, unsigned n, unsigned k, unsigned bound,
         }
         a0 = rational(ibound - static_cast<int>(rand(2*bound+1)));
         hb.add_ge(nv, a0);
-    }    
+    }
     hb.display(std::cout << "Saturate\n");
     saturate_basis(hb);
 }
@@ -368,7 +370,8 @@ static vector<rational> vec(int i, int j, int k, int l, int x, int y, int z) {
 // -y + z <= 0
 
 static void tst1() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_eq(vec(1,1,-2));
     hb.add_eq(vec(1,0,-1));
     hb.add_le(vec(0,1,-1));
@@ -380,7 +383,8 @@ static void tst1() {
 // 23x - 12y - 9z <= 0
 // x   - 8y  - 8z <= 0
 void tst2() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
 
     hb.add_eq(vec(-23,12,9));
     hb.add_eq(vec(-1,8,8));
@@ -391,7 +395,8 @@ void tst2() {
 // example 6, Ajili, Contenjean
 // 3x + 2y - z - 2u <= 0
 static void tst3() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_le(vec(3,2,-1,-2));
     saturate_basis(hb);
 }
@@ -400,7 +405,8 @@ static void tst3() {
 
 // Sigma_1, table 1, Ajili, Contejean
 static void tst4() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_le(vec( 0,-2, 1, 3, 2,-2, 3), R(3));
     hb.add_le(vec(-1, 7, 0, 1, 3, 5,-4), R(2));
     hb.add_le(vec( 0,-1, 1,-1,-1, 0, 0), R(2));
@@ -416,7 +422,8 @@ static void tst4() {
 
 // Sigma_2 table 1,  Ajili, Contejean
 static void tst5() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_le(vec( 1, 2,-1, 1), R(3));
     hb.add_le(vec( 2, 4, 1, 2), R(12));
     hb.add_le(vec( 1, 4, 2, 1), R(9));
@@ -429,7 +436,8 @@ static void tst5() {
 
 // Sigma_3 table 1,  Ajili, Contejean
 static void tst6() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_le(vec( 4, 3, 0), R(6));
     hb.add_le(vec(-3,-4, 0), R(-1));
     hb.add_le(vec( 4, 0,-3), R(3));
@@ -441,7 +449,8 @@ static void tst6() {
 
 // Sigma_4 table 1,  Ajili, Contejean
 static void tst7() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_eq(vec( 1, 1, 1, 0),  R(5));
     hb.add_le(vec( 2, 1, 0, 1),  R(6));
     hb.add_le(vec( 1, 2, 1, 1),  R(7));
@@ -454,7 +463,8 @@ static void tst7() {
 
 // Sigma_5 table 1,  Ajili, Contejean
 static void tst8() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_le(vec( 2, 1, 1), R(2));
     hb.add_le(vec( 1, 2, 3), R(5));
     hb.add_le(vec( 2, 2, 3), R(6));
@@ -464,7 +474,8 @@ static void tst8() {
 
 // Sigma_6 table 1,  Ajili, Contejean
 static void tst9() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_le(vec( 1, 2, 3), R(11));
     hb.add_le(vec( 2, 2, 5), R(13));
     hb.add_le(vec( 1,-1,-11), R(3));
@@ -473,7 +484,8 @@ static void tst9() {
 
 // Sigma_7 table 1,  Ajili, Contejean
 static void tst10() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_le(vec( 1,-1,-1,-3), R(2));
     hb.add_le(vec(-2, 3, 3,-5), R(3));
     saturate_basis(hb);
@@ -481,14 +493,16 @@ static void tst10() {
 
 // Sigma_8 table 1,  Ajili, Contejean
 static void tst11() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_le(vec( 7,-2,11, 3, -5), R(5));
     saturate_basis(hb);
 }
 
 // Sigma_9 table 1,  Ajili, Contejean
 static void tst12() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_eq(vec( 1,-2,-3,4), R(0));
     hb.add_le(vec(100,45,-78,-67), R(0));
     saturate_basis(hb);
@@ -496,34 +510,39 @@ static void tst12() {
 
 // Sigma_10 table 1,  Ajili, Contejean
 static void tst13() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_le(vec( 23, -56, -34, 12, 11), R(0));
     saturate_basis(hb);
 }
 
 // Sigma_11 table 1,  Ajili, Contejean
 static void tst14() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_eq(vec(1, 0, -4, 8), R(2));
     hb.add_le(vec(12,19,-11,-7), R(-7));
     saturate_basis(hb);
 }
 
 static void tst15() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_le(vec(1, 0), R(1));
     hb.add_le(vec(0, 1), R(1));
     saturate_basis(hb);
 }
 
 static void tst16() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_le(vec(1, 0), R(100));
     saturate_basis(hb);
 }
 
 static void tst17() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_eq(vec(1,  0), R(0));
     hb.add_eq(vec(-1, 0), R(0));
     hb.add_eq(vec(0,  2), R(0));
@@ -533,26 +552,29 @@ static void tst17() {
 }
 
 static void tst18() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_eq(vec(0, 1), R(0));
     hb.add_eq(vec(1, -1), R(2));
-    saturate_basis(hb);    
+    saturate_basis(hb);
 }
 
 static void tst19() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     hb.add_eq(vec(0,  1, 0), R(0));
     hb.add_eq(vec(1, -1, 0), R(2));
-    saturate_basis(hb);    
+    saturate_basis(hb);
 }
 
 static void test_A_5_5_3() {
-    hilbert_basis hb;
+    reslimit rl;
+    hilbert_basis hb(rl);
     for (unsigned i = 0; i < 15; ++i) {
         vector<rational> v;
         for (unsigned j = 0; j < 5; ++j) {
             for (unsigned k = 0; k < 15; ++k) {
-                v.push_back(rational(k == i));                
+                v.push_back(rational(k == i));
             }
         }
         hb.add_ge(v, R(0));
diff --git a/src/test/interval.cpp b/src/test/interval.cpp
index ef733394b..ac242cc60 100644
--- a/src/test/interval.cpp
+++ b/src/test/interval.cpp
@@ -22,6 +22,7 @@ Revision History:
 #include"mpq.h"
 #include"ast.h"
 #include"debug.h"
+#include"rlimit.h"
 
 template class interval_manager<im_default_config>;
 typedef im_default_config::interval interval;
@@ -61,7 +62,7 @@ static void display_smt2_numeral(std::ostream & out, unsynch_mpq_manager & m, mp
     }
 }
 
-static void display_constraint(std::ostream & out, unsynch_mpq_manager & m, char const * a, interval const & i, 
+static void display_constraint(std::ostream & out, unsynch_mpq_manager & m, char const * a, interval const & i,
                                bool include_lower = true, bool include_upper = true) {
     out << "(and true";
     if (!i.m_lower_inf && include_lower) {
@@ -77,7 +78,7 @@ static void display_constraint(std::ostream & out, unsynch_mpq_manager & m, char
     out << ")";
 }
 
-static void assert_hyp(std::ostream & out, unsynch_mpq_manager & m, char const * a, interval const & i, 
+static void assert_hyp(std::ostream & out, unsynch_mpq_manager & m, char const * a, interval const & i,
                        bool include_lower = true, bool include_upper = true) {
     out << "(assert ";
     display_constraint(out, m, a, i, include_lower, include_upper);
@@ -99,7 +100,7 @@ static bool mk_interval(im_default_config & cfg, interval & a, bool l_inf, bool
         if (l_val == u_val && (l_open || u_open))
             return false;
     }
-    
+
     if (l_inf) {
         a.m_lower_open = true;
         a.m_lower_inf  = true;
@@ -119,7 +120,7 @@ static bool mk_interval(im_default_config & cfg, interval & a, bool l_inf, bool
         a.m_upper_inf  = false;
         cfg.m().set(a.m_upper, u_val);
     }
-    
+
     return true;
 }
 #endif
@@ -131,7 +132,7 @@ static void mk_random_interval(im_default_config & cfg, interval & a, unsigned m
         if (rand()%4 == 0) {
             a.m_lower_open = true;
             a.m_lower_inf  = true;
-            
+
             a.m_upper_open = (rand()%2 == 0);
             a.m_upper_inf  = false;
             cfg.m().set(a.m_upper, -static_cast<int>((rand()%magnitude)));
@@ -141,7 +142,7 @@ static void mk_random_interval(im_default_config & cfg, interval & a, unsigned m
             a.m_upper_inf  = false;
             int upper = -static_cast<int>((rand()%magnitude));
             cfg.m().set(a.m_upper, upper);
-            
+
             a.m_lower_open = (rand()%2 == 0);
             a.m_lower_inf  = false;
             cfg.m().set(a.m_lower, upper - static_cast<int>(rand()%magnitude) - (a.m_lower_open || a.m_upper_open ? 1 : 0));
@@ -149,7 +150,7 @@ static void mk_random_interval(im_default_config & cfg, interval & a, unsigned m
         break;
     case 1:
         // Neg, Pos
-        
+
         if (rand()%4 == 0) {
             a.m_lower_open = true;
             a.m_lower_inf  = true;
@@ -159,7 +160,7 @@ static void mk_random_interval(im_default_config & cfg, interval & a, unsigned m
             a.m_lower_inf  = false;
             cfg.m().set(a.m_lower, -static_cast<int>((rand()%magnitude)) - 1);
         }
-        
+
         if (rand()%4 == 0) {
             a.m_upper_open = true;
             a.m_upper_inf  = true;
@@ -175,7 +176,7 @@ static void mk_random_interval(im_default_config & cfg, interval & a, unsigned m
         if (rand()%4 == 0) {
             a.m_upper_open = true;
             a.m_upper_inf  = true;
-            
+
             a.m_lower_open = (rand()%2 == 0);
             a.m_lower_inf  = false;
             cfg.m().set(a.m_lower, (rand()%magnitude));
@@ -185,7 +186,7 @@ static void mk_random_interval(im_default_config & cfg, interval & a, unsigned m
             a.m_lower_inf  = false;
             int lower = (rand()%magnitude);
             cfg.m().set(a.m_lower, lower);
-            
+
             a.m_upper_open = (rand()%2 == 0);
             a.m_upper_inf  = false;
             cfg.m().set(a.m_upper, lower + rand()%magnitude + (a.m_lower_open || a.m_upper_open ? 1 : 0));
@@ -235,9 +236,10 @@ static void display_lemmas(unsynch_mpq_manager & nm, char const * result_term,
 
 #define MK_BINARY(NAME, RES_TERM)                                       \
 static void tst_ ## NAME(unsigned N, unsigned magnitude) {              \
+    reslimit                            rl;                             \
     unsynch_mpq_manager                 nm;                             \
     im_default_config                   imc(nm);                        \
-    interval_manager<im_default_config> im(imc);                        \
+    interval_manager<im_default_config> im(rl, imc);                    \
     interval a, b, r;                                                   \
                                                                         \
     for (unsigned i = 0; i < N; i++) {                                  \
@@ -255,130 +257,137 @@ MK_BINARY(mul, "(* a b)");
 MK_BINARY(add, "(+ a b)");
 MK_BINARY(sub, "(- a b)");
 
-static void tst_neg(unsigned N, unsigned magnitude) { 
-    unsynch_mpq_manager                 nm;     
+static void tst_neg(unsigned N, unsigned magnitude) {
+    reslimit rl;
+    unsynch_mpq_manager                 nm;
     im_default_config                   imc(nm);
-    interval_manager<im_default_config> im(imc);
-    interval a, b, r;                           
-                                                
-    for (unsigned i = 0; i < N; i++) {          
-        mk_random_interval(imc, a, magnitude);  
-        interval_deps deps;                     
-        im.neg(a, r, deps);                 
-        display_lemmas(nm, "(- a)", a, b, r, deps); 
-    }  
-    del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); 
-}
+    interval_manager<im_default_config> im(rl, imc);
+    interval a, b, r;
 
-static void tst_pw_2(unsigned N, unsigned magnitude) { 
-    unsynch_mpq_manager                 nm;     
-    im_default_config                   imc(nm);
-    interval_manager<im_default_config> im(imc);
-    interval a, b, r;                           
-                                                
-    for (unsigned i = 0; i < N; i++) {          
-        mk_random_interval(imc, a, magnitude);  
-        interval_deps deps;                     
-        im.power(a, 2, r, deps);                 
-        display_lemmas(nm, "(* a a)", a, b, r, deps); 
-    }  
-    del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); 
-}
-
-static void tst_pw_3(unsigned N, unsigned magnitude) { 
-    unsynch_mpq_manager                 nm;     
-    im_default_config                   imc(nm);
-    interval_manager<im_default_config> im(imc);
-    interval a, b, r;                           
-                                                
-    for (unsigned i = 0; i < N; i++) {          
-        mk_random_interval(imc, a, magnitude);  
-        interval_deps deps;                     
-        im.power(a, 3, r, deps);                 
-        display_lemmas(nm, "(* a a a)", a, b, r, deps); 
+    for (unsigned i = 0; i < N; i++) {
+        mk_random_interval(imc, a, magnitude);
+        interval_deps deps;
+        im.neg(a, r, deps);
+        display_lemmas(nm, "(- a)", a, b, r, deps);
     }
-    del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); 
+    del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);
 }
 
-static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) { 
-    unsynch_mpq_manager                 nm;     
+static void tst_pw_2(unsigned N, unsigned magnitude) {
+    reslimit rl;
+    unsynch_mpq_manager                 nm;
     im_default_config                   imc(nm);
-    interval_manager<im_default_config> im(imc);
-    interval a, b, r;                           
+    interval_manager<im_default_config> im(rl, imc);
+    interval a, b, r;
+
+    for (unsigned i = 0; i < N; i++) {
+        mk_random_interval(imc, a, magnitude);
+        interval_deps deps;
+        im.power(a, 2, r, deps);
+        display_lemmas(nm, "(* a a)", a, b, r, deps);
+    }
+    del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);
+}
+
+static void tst_pw_3(unsigned N, unsigned magnitude) {
+    reslimit rl;
+    unsynch_mpq_manager                 nm;
+    im_default_config                   imc(nm);
+    interval_manager<im_default_config> im(rl, imc);
+    interval a, b, r;
+
+    for (unsigned i = 0; i < N; i++) {
+        mk_random_interval(imc, a, magnitude);
+        interval_deps deps;
+        im.power(a, 3, r, deps);
+        display_lemmas(nm, "(* a a a)", a, b, r, deps);
+    }
+    del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);
+}
+
+static void tst_root_2(unsigned N, unsigned magnitude, unsigned precision) {
+    reslimit rl;
+    unsynch_mpq_manager                 nm;
+    im_default_config                   imc(nm);
+    interval_manager<im_default_config> im(rl, imc);
+    interval a, b, r;
     scoped_mpq                          p(nm);
     p = precision;
     nm.inv(p);
 
     unsigned i = 0;
     while (i < N) {
-        mk_random_interval(imc, a, magnitude);  
+        mk_random_interval(imc, a, magnitude);
         if (!im.lower_is_neg(a)) {
             i++;
-            interval_deps deps;                     
-            im.nth_root(a, 2, p, r, deps);                 
-            display_lemmas(nm, "(^ a (/ 1.0 2.0))", a, b, r, deps); 
-        } 
-    } 
-    del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); 
+            interval_deps deps;
+            im.nth_root(a, 2, p, r, deps);
+            display_lemmas(nm, "(^ a (/ 1.0 2.0))", a, b, r, deps);
+        }
+    }
+    del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);
 }
 
-static void tst_root_3(unsigned N, unsigned magnitude, unsigned precision) { 
-    unsynch_mpq_manager                 nm;     
+static void tst_root_3(unsigned N, unsigned magnitude, unsigned precision) {
+    reslimit rl;
+    unsynch_mpq_manager                 nm;
     im_default_config                   imc(nm);
-    interval_manager<im_default_config> im(imc);
-    interval a, b, r;                           
+    interval_manager<im_default_config> im(rl, imc);
+    interval a, b, r;
     scoped_mpq                          p(nm);
     p = precision;
     nm.inv(p);
 
     unsigned i = 0;
     while (i < N) {
-        mk_random_interval(imc, a, magnitude);  
+        mk_random_interval(imc, a, magnitude);
         i++;
-        interval_deps deps;                     
-        im.nth_root(a, 3, p, r, deps);                 
-        display_lemmas(nm, "(^ a (/ 1.0 3.0))", a, b, r, deps); 
-    } 
-    del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); 
+        interval_deps deps;
+        im.nth_root(a, 3, p, r, deps);
+        display_lemmas(nm, "(^ a (/ 1.0 3.0))", a, b, r, deps);
+    }
+    del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);
 }
 
-static void tst_inv(unsigned N, unsigned magnitude) { 
-    unsynch_mpq_manager                 nm;     
+static void tst_inv(unsigned N, unsigned magnitude) {
+    reslimit rl;
+    unsynch_mpq_manager                 nm;
     im_default_config                   imc(nm);
-    interval_manager<im_default_config> im(imc);
-    interval a, b, r;                           
-            
-    for (unsigned i = 0; i < N; i++) {          
+    interval_manager<im_default_config> im(rl, imc);
+    interval a, b, r;
+
+    for (unsigned i = 0; i < N; i++) {
         while (true) {
-            mk_random_interval(imc, a, magnitude);  
+            mk_random_interval(imc, a, magnitude);
             if (!im.contains_zero(a))
                 break;
         }
-        interval_deps deps;                     
-        im.inv(a, r, deps);                 
-        display_lemmas(nm, "(/ 1 a)", a, b, r, deps); 
-    }  
-    del_interval(imc, a); del_interval(imc, b); del_interval(imc, r); 
+        interval_deps deps;
+        im.inv(a, r, deps);
+        display_lemmas(nm, "(/ 1 a)", a, b, r, deps);
+    }
+    del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);
 }
 
-static void tst_div(unsigned N, unsigned magnitude) {                    
-    unsynch_mpq_manager                 nm;                       
-    im_default_config                   imc(nm);                  
-    interval_manager<im_default_config> im(imc);                  
-    interval a, b, r;                                                  
+static void tst_div(unsigned N, unsigned magnitude) {
+    reslimit rl;
+    unsynch_mpq_manager                 nm;
+    im_default_config                   imc(nm);
+    interval_manager<im_default_config> im(rl, imc);
+    interval a, b, r;
 
-    for (unsigned i = 0; i < N; i++) {                                 
-        mk_random_interval(imc, a, magnitude);                         
+    for (unsigned i = 0; i < N; i++) {
+        mk_random_interval(imc, a, magnitude);
         while (true) {
-            mk_random_interval(imc, b, magnitude);                         
+            mk_random_interval(imc, b, magnitude);
             if (!im.contains_zero(b))
                 break;
         }
-        interval_deps deps;                                             
-        im.div(a, b, r, deps);                                         
-        display_lemmas(nm, "(/ a b)", a, b, r, deps);  
-    }                                                 
-    del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);   
+        interval_deps deps;
+        im.div(a, b, r, deps);
+        display_lemmas(nm, "(/ a b)", a, b, r, deps);
+    }
+    del_interval(imc, a); del_interval(imc, b); del_interval(imc, r);
 }
 
 #include"im_float_config.h"
@@ -395,7 +404,7 @@ static void tst_float() {
     qm.set(one_third, 1, 3);
     qm.set(two_third, 2, 3);
     qm.set(minus_two_third, -2, 3);
-    
+
     ifc.round_to_minus_inf();
     ifc.m().set(a.m_lower, minus_one_third);
     ifc.round_to_plus_inf();
@@ -405,7 +414,7 @@ static void tst_float() {
     ifc.m().set(b.m_lower, minus_two_third);
     ifc.round_to_plus_inf();
     ifc.m().set(b.m_upper, one_third);
-    
+
     im.display(std::cout, a);
     std::cout << "\n";
     im.display(std::cout, b);
@@ -420,13 +429,14 @@ static void tst_float() {
 #endif
 
 void tst_pi() {
-    unsynch_mpq_manager                 nm;     
+    reslimit rl;
+    unsynch_mpq_manager                 nm;
     im_default_config                   imc(nm);
-    interval_manager<im_default_config> im(imc);
+    interval_manager<im_default_config> im(rl, imc);
     interval r;
     for (unsigned i = 0; i < 8; i++) {
         im.pi(i, r);
-        nm.display_decimal(std::cout, im.lower(r), 32); std::cout << "   "; 
+        nm.display_decimal(std::cout, im.lower(r), 32); std::cout << "   ";
         nm.display_decimal(std::cout, im.upper(r), 32); std::cout << "\n";
         SASSERT(nm.lt(im.lower(r), im.upper(r)));
     }
@@ -436,10 +446,11 @@ void tst_pi() {
 #if 0
 static void tst_pi_float() {
     std::cout << "pi float...\n";
+    reslimit rl;
     unsynch_mpq_manager   qm;
     mpf_manager           fm;
     im_float_config<mpf_manager>                    ifc(fm, 22, 106);
-    interval_manager<im_float_config<mpf_manager> > im(ifc);
+    interval_manager<im_float_config<mpf_manager> > im(rl, ifc);
     scoped_mpq q(qm);
     im_float_config<mpf_manager>::interval r;
     for (unsigned i = 0; i < 8; i++) {
@@ -451,7 +462,7 @@ static void tst_pi_float() {
     }
     del_f_interval(ifc, r);
 }
-#endif 
+#endif
 
 #define NUM_TESTS 1000
 #define SMALL_MAG 3
diff --git a/src/test/karr.cpp b/src/test/karr.cpp
index 4c0737230..c5581cc66 100644
--- a/src/test/karr.cpp
+++ b/src/test/karr.cpp
@@ -3,7 +3,7 @@
 Copyright (c) 2015 Microsoft Corporation
 
 --*/
-
+#include"rlimit.h"
 #include "hilbert_basis.h"
 
 /*
@@ -15,12 +15,12 @@ namespace karr {
     struct matrix {
         vector<vector<rational> > A;
         vector<rational>          b;
-        
+
         unsigned size() const { return A.size(); }
 
-        void reset() { 
-            A.reset(); 
-            b.reset(); 
+        void reset() {
+            A.reset();
+            b.reset();
         }
 
         matrix& operator=(matrix const& other) {
@@ -46,7 +46,8 @@ namespace karr {
 
     // treat src as a homogeneous matrix.
     void dualizeH(matrix& dst, matrix const& src) {
-        hilbert_basis hb;
+        reslimit rl;
+        hilbert_basis hb(rl);
         for (unsigned i = 0; i < src.size(); ++i) {
             vector<rational> v(src.A[i]);
             v.push_back(src.b[i]);
@@ -74,7 +75,8 @@ namespace karr {
 
     // treat src as an inhomegeneous matrix.
     void dualizeI(matrix& dst, matrix const& src) {
-        hilbert_basis hb;
+        reslimit rl;
+        hilbert_basis hb(rl);
         for (unsigned i = 0; i < src.size(); ++i) {
             hb.add_eq(src.A[i], -src.b[i]);
         }
@@ -136,7 +138,7 @@ namespace karr {
         }
         for (unsigned i = 0; i < src.size(); ++i) {
             T.A.push_back(src.A[i]);
-            T.A.back().append(zeros);            
+            T.A.back().append(zeros);
         }
         T.b.append(src.b);
         T.append(Ab);
@@ -146,7 +148,7 @@ namespace karr {
         dualizeI(TD, T);
         TD.display(std::cout << "TD:\n");
         for (unsigned i = 0; i < TD.size(); ++i) {
-            vector<rational> v;            
+            vector<rational> v;
             v.append(src.size(), TD.A[i].c_ptr() + src.size());
             dst.A.push_back(v);
             dst.b.push_back(TD.b[i]);
@@ -200,8 +202,8 @@ namespace karr {
     static void tst1() {
         matrix Theta;
         matrix Ab;
-        
-        // 
+
+        //
         Theta.A.push_back(V(1, 0));
         Theta.b.push_back(R(0));
         Theta.A.push_back(V(0, 1));
@@ -232,7 +234,7 @@ namespace karr {
         joinD(e2, t2D, ThetaD);
 
         t2D.display(std::cout << "t2D\n");
-        e2.display(std::cout << "e2\n");        
+        e2.display(std::cout << "e2\n");
     }
 
     void tst2() {
@@ -264,7 +266,7 @@ namespace karr {
 
         N.display(std::cout << "N\n");
 
-        
+
     }
 
     void tst3() {
@@ -288,7 +290,7 @@ namespace karr {
 
         N.display(std::cout << "N\n");
 
-        
+
     }
 
 };
diff --git a/src/test/nlsat.cpp b/src/test/nlsat.cpp
index d1ece65fc..7777a6c42 100644
--- a/src/test/nlsat.cpp
+++ b/src/test/nlsat.cpp
@@ -21,6 +21,7 @@ Notes:
 #include"nlsat_evaluator.h"
 #include"nlsat_solver.h"
 #include"util.h"
+#include"rlimit.h"
 
 nlsat::interval_set_ref tst_interval(nlsat::interval_set_ref const & s1,
                                      nlsat::interval_set_ref const & s2,
@@ -57,8 +58,9 @@ nlsat::interval_set_ref tst_interval(nlsat::interval_set_ref const & s1,
 
 static void tst3() {
     enable_trace("nlsat_interval");
+    reslimit rl;
     unsynch_mpq_manager         qm;
-    anum_manager                am(qm);
+    anum_manager                am(rl, qm);
     small_object_allocator      allocator;
     nlsat::interval_set_manager ism(am, allocator);
 
@@ -70,13 +72,13 @@ static void tst3() {
     am.set(m_sqrt2, sqrt2);
     am.neg(m_sqrt2);
     am.set(three, 3);
-    
+
     nlsat::literal p1(1, false);
     nlsat::literal p2(2, false);
     nlsat::literal p3(3, false);
     nlsat::literal p4(4, false);
     nlsat::literal np2(2, true);
-    
+
     nlsat::interval_set_ref s1(ism), s2(ism), s3(ism), s4(ism);
     s1 = ism.mk_empty();
     std::cout << "s1: " << s1 << "\n";
@@ -94,7 +96,7 @@ static void tst3() {
     s2 = ism.mk(false, false, zero, false, false, two, p2);
     tst_interval(s1, s2, 1);
 
-    // Case 
+    // Case
     // s1:   [ ... ]
     // s2: [ ... ]
     s1 = ism.mk(false, false, zero, false, false, two, p1);
@@ -102,28 +104,28 @@ static void tst3() {
     s3 = ism.mk_union(s1, s2);
     tst_interval(s1, s2, 2);
 
-    // Case 
+    // Case
     // s1:   [ ... ]
     // s2:      [ ... ]
     s1 = ism.mk(false, false, m_sqrt2, false, false, one, p1);
     s2 = ism.mk(false, false, zero, false, false, two, p2);
     tst_interval(s1, s2, 2);
 
-    // Case 
+    // Case
     // s1:   [ ... ]
     // s2:            [ ... ]
     s1 = ism.mk(false, false, m_sqrt2, false, false, one, p1);
     s2 = ism.mk(false, false, two, false, false, three, p2);
     tst_interval(s1, s2, 2);
 
-    // Case 
+    // Case
     // s1:   [    ...    ]
     // s2:      [ ... ]
     s1 = ism.mk(false, false, m_sqrt2, false, false, three, p1);
     s2 = ism.mk(false, false, zero, false, false, two, p2);
     tst_interval(s1, s2, 1);
 
-    // Case 
+    // Case
     // s1:   [    ...      ]
     // s2:      [ ... ] [  ...  ]
     s1 = ism.mk(false, false, m_two, false, false, two, p1);
@@ -214,7 +216,7 @@ static nlsat::interval_set_ref mk_random(nlsat::interval_set_manager & ism, anum
     return r;
 }
 
-static void check_subset_result(nlsat::interval_set_ref const & s1, 
+static void check_subset_result(nlsat::interval_set_ref const & s1,
                                 nlsat::interval_set_ref const & s2,
                                 nlsat::interval_set_ref const & r,
                                 nlsat::literal l1,
@@ -241,15 +243,16 @@ static void check_subset_result(nlsat::interval_set_ref const & s1,
 
 static void tst4() {
     enable_trace("nlsat_interval");
+    reslimit rl;
     unsynch_mpq_manager         qm;
-    anum_manager                am(qm);
+    anum_manager                am(rl, qm);
     small_object_allocator      allocator;
     nlsat::interval_set_manager ism(am, allocator);
     nlsat::interval_set_ref     s1(ism), s2(ism), r(ism);
 
     nlsat::literal l1(1, false);
     nlsat::literal l2(2, false);
-    
+
     for (unsigned i = 0; i < 100; i++) {
         s1 = mk_random(ism, am, 20, 3, 10, true, true, l1);
         s2 = mk_random(ism, am, 20, 3, 10, true, true, l2);
diff --git a/src/test/polynomial.cpp b/src/test/polynomial.cpp
index b51d14645..56eb61a11 100644
--- a/src/test/polynomial.cpp
+++ b/src/test/polynomial.cpp
@@ -22,11 +22,13 @@ Notes:
 #include"polynomial_var2value.h"
 #include"polynomial_cache.h"
 #include"linear_eq_solver.h"
+#include"rlimit.h"
 
 static void tst1() {
     std::cout << "\n----- Basic testing -------\n";
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -56,6 +58,7 @@ static void tst1() {
 }
 
 static void tst_pseudo_div(polynomial_ref const & A, polynomial_ref const & B, polynomial::var x) {
+    reslimit rl;
     polynomial::manager & m = A.m();
     std::cout << "---- Pseudo-division test ----\n";
     std::cout << "A: " << A << "\n";
@@ -81,8 +84,9 @@ static void tst_pseudo_div(polynomial_ref const & A, polynomial_ref const & B, p
 }
 
 static void tst2() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -98,8 +102,9 @@ static void tst2() {
 
 
 static void tst3() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     x0 = m.mk_polynomial(m.mk_var());
@@ -113,8 +118,9 @@ static void tst3() {
 
 static void tst4() {
     std::cout << "---- Testing renaming/reordering ----\n";
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -141,8 +147,9 @@ static void tst_quasi_resultant(polynomial_ref const & p, polynomial_ref const &
 }
 
 static void tst5() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -158,8 +165,9 @@ static void tst5() {
 }
 
 static void tst6() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -176,8 +184,9 @@ static void tst6() {
 }
 
 static void tst7() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -198,8 +207,9 @@ static void tst7() {
 }
 
 static void tst8() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -220,8 +230,9 @@ static void tst8() {
 
 
 static void tst9() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -261,8 +272,9 @@ static void tst9() {
 }
 
 static void tst10() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -300,8 +312,9 @@ static void tst10() {
 }
 
 static void tst11() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -342,8 +355,9 @@ static void tst_discriminant(polynomial_ref const & p, polynomial_ref const & ex
 }
 
 static void tst_discriminant() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref a(m);
     polynomial_ref b(m);
     polynomial_ref c(m);
@@ -354,13 +368,13 @@ static void tst_discriminant() {
     c = m.mk_polynomial(m.mk_var());
     d = m.mk_polynomial(m.mk_var());
     x = m.mk_polynomial(m.mk_var());
-    tst_discriminant(a*(x^2) + b*x  + c, 
+    tst_discriminant(a*(x^2) + b*x  + c,
                      (b^2) - 4*a*c);
-    tst_discriminant(a*(x^3) + b*(x^2) + c*x + d, 
+    tst_discriminant(a*(x^3) + b*(x^2) + c*x + d,
                      (b^2)*(c^2) - 4*a*(c^3) - 4*(b^3)*d + 18*a*b*c*d - 27*(a^2)*(d^2));
-    tst_discriminant(a*(x^3) + b*(x^2) + c*(x^2) + d, 
+    tst_discriminant(a*(x^3) + b*(x^2) + c*(x^2) + d,
                      -4*(b^3)*d - 12*(b^2)*c*d - 12*b*(c^2)*d - 4*(c^3)*d - 27*(a^2)*(d^2));
-    tst_discriminant(a*(x^3) + b*(x^2) + c*(x^2) + d, 
+    tst_discriminant(a*(x^3) + b*(x^2) + c*(x^2) + d,
                      -4*(b^3)*d - 12*(b^2)*c*d - 12*b*(c^2)*d - 4*(c^3)*d - 27*(a^2)*(d^2));
     tst_discriminant(a*(x^3) + (b^2)*d*(x^2) + c*(x^2) + d,
                      -4*(b^6)*(d^4) - 12*(b^4)*c*(d^3) - 12*(b^2)*(c^2)*(d^2) - 4*(c^3)*d - 27*(a^2)*(d^2));
@@ -402,7 +416,7 @@ static void tst_discriminant() {
     tst_discriminant((x^4) + (a + b)*(x^2) + (a + c)*x,
                      -4*(a^5) - 12*(a^4)*b - 12*(a^3)*(b^2) - 4*(a^2)*(b^3) - 8*(a^4)*c - 24*(a^3)*b*c -
                      24*(a^2)*(b^2)*c - 8*a*(b^3)*c - 4*(a^3)*(c^2) - 12*(a^2)*b*(c^2) - 12*a*(b^2)*(c^2) -
-                     4*(b^3)*(c^2) - 27*(a^4) - 108*(a^3)*c - 162*(a^2)*(c^2) - 108*a*(c^3) - 27*(c^4));                      
+                     4*(b^3)*(c^2) - 27*(a^4) - 108*(a^3)*c - 162*(a^2)*(c^2) - 108*a*(c^3) - 27*(c^4));
     tst_discriminant((x^4) + (a + c)*x + (c^2),
                      256*(c^6) - 27*(a^4) - 108*(a^3)*c - 162*(a^2)*(c^2) - 108*a*(c^3) - 27*(c^4)
                      );
@@ -425,7 +439,7 @@ static void tst_discriminant() {
                      max_var(b),
                      2048*(a^12) - 12288*(a^11) + 26112*(a^10) - 22528*(a^9) + 5664*(a^8) + 960*(a^7) +
                      32*(a^6));
-    tst_discriminant((x^4) + a*(x^2) + b*x + c, 
+    tst_discriminant((x^4) + a*(x^2) + b*x + c,
                      -4*(a^3)*(b^2) + 16*(a^4)*c - 27*(b^4) + 144*a*(b^2)*c - 128*(a^2)*(c^2) + 256*(c^3));
     tst_discriminant((((a-1)^2) + a*b + ((b-1)^2) - 1)*(x^3) + (a*b)*(x^2) + ((a^2) - (b^2))*x + c*a,
                      -4*(a^8) - 4*(a^7)*b + 9*(a^6)*(b^2) + 12*(a^5)*(b^3) - 2*(a^4)*(b^4) - 12*(a^3)*(b^5) -
@@ -460,8 +474,9 @@ static void tst_resultant(polynomial_ref const & p, polynomial_ref const & q, po
 }
 
 static void tst_resultant() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref a(m);
     polynomial_ref b(m);
     polynomial_ref c(m);
@@ -485,13 +500,13 @@ static void tst_resultant() {
                   3*(a^2)*(b^4) - (b^6));
 
 
-    tst_resultant(a*(x^5) + b, 
-                  c*x + d, 
+    tst_resultant(a*(x^5) + b,
+                  c*x + d,
                   a*(d^5) - b*(c^5));
     tst_resultant(a*(x^5) + 3*(c + d)*(x^2) + 2*b,
-                  c*x + d, 
+                  c*x + d,
                   -2*b*(c^5) - 3*(c^4)*(d^2) - 3*(c^3)*(d^3) + a*(d^5));
-    tst_resultant(c*x + d, 
+    tst_resultant(c*x + d,
                   a*(x^5) + 3*(c + d)*(x^2) + 2*b,
                   2*b*(c^5) + 3*(c^4)*(d^2) + 3*(c^3)*(d^3) - a*(d^5));
     tst_resultant((x^2) - (a^3)*(x^2) + b + 1,
@@ -545,23 +560,25 @@ static void tst_resultant() {
 }
 
 static void tst_compose() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     x0 = m.mk_polynomial(m.mk_var());
     x1 = m.mk_polynomial(m.mk_var());
     polynomial_ref p(m);
     p = (x0^3) - x0 + 3;
-    std::cout << "p: " << p << "\np(x - y): " << compose_x_minus_y(p, 1) 
+    std::cout << "p: " << p << "\np(x - y): " << compose_x_minus_y(p, 1)
               << "\np(x + y): " << compose_x_plus_y(p, 1) << "\np(x - x): " << compose_x_minus_y(p, 0) << "\np(x + x): " << compose_x_plus_y(p, 0) << "\n";
     SASSERT(eq(compose_x_minus_y(p, 1), (x0^3) - 3*(x0^2)*x1 + 3*x0*(x1^2) - (x1^3) - x0 + x1 + 3));
     SASSERT(eq(compose_x_plus_y(p, 1), (x0^3) + 3*(x0^2)*x1 + 3*x0*(x1^2) + (x1^3) - x0 - x1 + 3));
 }
 
 void tst_prem() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     polynomial_ref y(m);
     x = m.mk_polynomial(m.mk_var());
@@ -572,13 +589,14 @@ void tst_prem() {
     q = y*(x^3);
     std::cout << "p: " << p << "\n";
     std::cout << "q: " << q << "\n";
-    // unsigned d; 
+    // unsigned d;
     std::cout << "srem: " << exact_pseudo_remainder(q, p, 0) << "\n";
 }
 
 void tst_sqrt() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     polynomial_ref y(m);
     x = m.mk_polynomial(m.mk_var());
@@ -622,8 +640,9 @@ static void tst_gcd(polynomial_ref const & p, polynomial_ref const & q, polynomi
 }
 
 static void tst_gcd() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -648,7 +667,7 @@ static void tst_gcd() {
     tst_gcd(((x0^2) + x0*x1 + 1)*(x2*x2 + x3 + 2)*(x3*x1 + 2)*(x3*x1*x1 + x1*x2 + 1),
             (-1)*((x0^2) + x0*x1 + 1)*(x3*x1*x1 + x1*x2 + 1)*(x3*x1 + x1*x2 + 17),
             ((x0^2) + x0*x1 + 1)*(x3*x1*x1 + x1*x2 + 1));
-    
+
     tst_gcd((-1)*((x0^2) + x0*x1 + 1)*(x2*x2 + x3 + 2)*(x3*x1 + 2)*(x3*x1*x1 + x1*x2 + 1),
             (-1)*((x0^2) + x0*x1 + 1)*(x3*x1*x1 + x1*x2 + 1)*(x3*x1 + x1*x2 + 17),
             ((x0^2) + x0*x1 + 1)*(x3*x1*x1 + x1*x2 + 1));
@@ -661,17 +680,17 @@ static void tst_gcd() {
     tst_primitive((x0 + 1)*(2*x1) + (x0^2)*(x0 + 1), 1, 2*x1 + (x0^2));
     tst_primitive((x0 + 1)*(x2 + 1)*(x2^2)*(x0 + 1)*(x1^2) + (x0 + 1)*(x2^2)*x1 + (x0+1)*(x0+1), 1,
                   (x2 + 1)*(x2^2)*(x0 + 1)*(x1^2) + (x2^2)*x1 + (x0+1));
-    tst_primitive((x0 + (x3^2))*(x2 + x3 + 1)*(x2^2)*(x1^2) + 
+    tst_primitive((x0 + (x3^2))*(x2 + x3 + 1)*(x2^2)*(x1^2) +
                   (x0 + (x3^2))*(x2 + x3 + 1)*x1 +
                   (x0 + (x3^2))*(x2 + x3 + 1)*(x3^2),
                   1,
                   (x2^2)*(x1^2) + x1 + (x3^2));
-    tst_content((x0 + (x3^2))*(x2 + x3 + 1)*(x2^2)*(x1^2) + 
+    tst_content((x0 + (x3^2))*(x2 + x3 + 1)*(x2^2)*(x1^2) +
                 (x0 + (x3^2))*(x2 + x3 + 1)*x1 +
                 (x0 + (x3^2))*(x2 + x3 + 1)*(x3^2),
                 1,
                 (x0 + (x3^2))*(x2 + x3 + 1));
-    tst_primitive(4*(x0 + (x3^2))*(x2 + x3 + 1)*(x2^2)*(x1^2) + 
+    tst_primitive(4*(x0 + (x3^2))*(x2 + x3 + 1)*(x2^2)*(x1^2) +
                   2*(x0 + (x3^2))*(x2 + x3 + 1)*x1 +
                   4*(x0 + (x3^2))*(x2 + x3 + 1)*(x3^2),
                   1,
@@ -721,8 +740,9 @@ static void tst_psc_perf(polynomial_ref const & p, polynomial_ref const & q, pol
 #endif
 
 static void tst_psc() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -740,7 +760,7 @@ static void tst_psc() {
     x8 = m.mk_polynomial(m.mk_var());
     x9 = m.mk_polynomial(m.mk_var());
     x10 = m.mk_polynomial(m.mk_var());
-    tst_psc(x0*(x1^2) + (x0 + 1)*x1 + 2, x0*x1 + 3, 1, 
+    tst_psc(x0*(x1^2) + (x0 + 1)*x1 + 2, x0*x1 + 3, 1,
             6*x0 - (x0^2), x0);
     tst_psc(x0*(x1^4) + (x0 + 1)*(x1^3) + 2, x0*(x1^3) + 3, 1,
             72*(x0^3) - (x0^4) - 27*(x0^2) - 27*(x0), 9*(x0^3));
@@ -754,34 +774,34 @@ static void tst_psc() {
     tst_psc((x^4) + a*(x^2) + b*x + c, 4*(x^3) + 2*a*x + b, 9,
             16*(a^4)*c - 4*(a^3)*(b^2) - 128*(a^2)*(c^2) + 144*a*(b^2)*c - 27*(b^4) + 256*(c^3), 8*(a^3) - 32*a*c + 36*(b^2));
     polynomial_ref & y = x10;
-    
+
     tst_psc(((y^2) + 6)*(x - 1) - y*((x^2) + 1), ((x^2) + 6)*(y - 1) - x*((y^2) + 1), 10,
-            2*(x^6) - 22*(x^5) + 102*(x^4) - 274*(x^3) + 488*(x^2) - 552*x + 288, 
+            2*(x^6) - 22*(x^5) + 102*(x^4) - 274*(x^3) + 488*(x^2) - 552*x + 288,
             5*x - (x^2) - 6
             );
-    
+
     tst_psc(((y^3) + 6)*(x - 1) - y*((x^3) + 1), ((x^3) + 6)*(y - 1) - x*((y^3) + 1), 10,
             3*(x^11) - 3*(x^10) - 37*(x^9) + 99*(x^8) + 51*(x^7) - 621*(x^6) + 1089*(x^5) - 39*(x^4) - 3106*(x^3) + 5868*(x^2) - 4968*x + 1728,
             (x^6) - 10*(x^4) + 12*(x^3) + 25*(x^2) - 60*x + 36);
 
     polynomial_ref p = (x^6) + a * (x^3) + b;
     polynomial_ref q = (x^6) + c * (x^3) + d;
-   
-    tst_psc(p, q, 9, 
-            (b^6) - 3*a*(b^5)*c + 3*(a^2)*(b^4)*(c^2) + 3*(b^5)*(c^2) - (a^3)*(b^3)*(c^3) - 
-            6*a*(b^4)*(c^3) + 3*(a^2)*(b^3)*(c^4) + 3*(b^4)*(c^4) - 3*a*(b^3)*(c^5) + (b^3)*(c^6) + 
-            3*(a^2)*(b^4)*d - 6*(b^5)*d - 6*(a^3)*(b^3)*c*d + 9*a*(b^4)*c*d + 
-            3*(a^4)*(b^2)*(c^2)*d + 6*(a^2)*(b^3)*(c^2)*d - 12*(b^4)*(c^2)*d - 9*(a^3)*(b^2)*(c^3)*d + 
-            6*a*(b^3)*(c^3)*d + 9*(a^2)*(b^2)*(c^4)*d - 6*(b^3)*(c^4)*d - 3*a*(b^2)*(c^5)*d + 
-            3*(a^4)*(b^2)*(d^2) - 12*(a^2)*(b^3)*(d^2) + 15*(b^4)*(d^2) - 3*(a^5)*b*c*(d^2) + 
-            6*(a^3)*(b^2)*c*(d^2) - 6*a*(b^3)*c*(d^2) + 9*(a^4)*b*(c^2)*(d^2) - 
-            18*(a^2)*(b^2)*(c^2)*(d^2) + 18*(b^3)*(c^2)*(d^2) - 9*(a^3)*b*(c^3)*(d^2) + 
-            6*a*(b^2)*(c^3)*(d^2) + 3*(a^2)*b*(c^4)*(d^2) + 3*(b^2)*(c^4)*(d^2) + (a^6)*(d^3) - 
-            6*(a^4)*b*(d^3) + 18*(a^2)*(b^2)*(d^3) - 20*(b^3)*(d^3) - 3*(a^5)*c*(d^3) + 
-            6*(a^3)*b*c*(d^3) - 6*a*(b^2)*c*(d^3) + 3*(a^4)*(c^2)*(d^3) + 6*(a^2)*b*(c^2)*(d^3) - 
-            12*(b^2)*(c^2)*(d^3) - (a^3)*(c^3)*(d^3) - 6*a*b*(c^3)*(d^3) + 3*(a^4)*(d^4) - 
-            12*(a^2)*b*(d^4) + 15*(b^2)*(d^4) - 6*(a^3)*c*(d^4) + 9*a*b*c*(d^4) + 
-            3*(a^2)*(c^2)*(d^4) + 3*b*(c^2)*(d^4) + 3*(a^2)*(d^5) - 6*b*(d^5) - 
+
+    tst_psc(p, q, 9,
+            (b^6) - 3*a*(b^5)*c + 3*(a^2)*(b^4)*(c^2) + 3*(b^5)*(c^2) - (a^3)*(b^3)*(c^3) -
+            6*a*(b^4)*(c^3) + 3*(a^2)*(b^3)*(c^4) + 3*(b^4)*(c^4) - 3*a*(b^3)*(c^5) + (b^3)*(c^6) +
+            3*(a^2)*(b^4)*d - 6*(b^5)*d - 6*(a^3)*(b^3)*c*d + 9*a*(b^4)*c*d +
+            3*(a^4)*(b^2)*(c^2)*d + 6*(a^2)*(b^3)*(c^2)*d - 12*(b^4)*(c^2)*d - 9*(a^3)*(b^2)*(c^3)*d +
+            6*a*(b^3)*(c^3)*d + 9*(a^2)*(b^2)*(c^4)*d - 6*(b^3)*(c^4)*d - 3*a*(b^2)*(c^5)*d +
+            3*(a^4)*(b^2)*(d^2) - 12*(a^2)*(b^3)*(d^2) + 15*(b^4)*(d^2) - 3*(a^5)*b*c*(d^2) +
+            6*(a^3)*(b^2)*c*(d^2) - 6*a*(b^3)*c*(d^2) + 9*(a^4)*b*(c^2)*(d^2) -
+            18*(a^2)*(b^2)*(c^2)*(d^2) + 18*(b^3)*(c^2)*(d^2) - 9*(a^3)*b*(c^3)*(d^2) +
+            6*a*(b^2)*(c^3)*(d^2) + 3*(a^2)*b*(c^4)*(d^2) + 3*(b^2)*(c^4)*(d^2) + (a^6)*(d^3) -
+            6*(a^4)*b*(d^3) + 18*(a^2)*(b^2)*(d^3) - 20*(b^3)*(d^3) - 3*(a^5)*c*(d^3) +
+            6*(a^3)*b*c*(d^3) - 6*a*(b^2)*c*(d^3) + 3*(a^4)*(c^2)*(d^3) + 6*(a^2)*b*(c^2)*(d^3) -
+            12*(b^2)*(c^2)*(d^3) - (a^3)*(c^3)*(d^3) - 6*a*b*(c^3)*(d^3) + 3*(a^4)*(d^4) -
+            12*(a^2)*b*(d^4) + 15*(b^2)*(d^4) - 6*(a^3)*c*(d^4) + 9*a*b*c*(d^4) +
+            3*(a^2)*(c^2)*(d^4) + 3*b*(c^2)*(d^4) + 3*(a^2)*(d^5) - 6*b*(d^5) -
             3*a*c*(d^5) + (d^6),
             3*(a^2)*c - (a^3) - 3*a*(c^2) + (c^3)
             );
@@ -796,9 +816,9 @@ static void tst_psc() {
     zero = m.mk_zero();
 
     tst_psc( a*d*x + a*c*f + a*e - b*a,
-             d*x + c*f + e - b, 
+             d*x + c*f + e - b,
              9, zero, zero);
-                         
+
 
 #if 0
     tst_psc_perf((x^7) + a*(x^3) + b*(x^2) + c*x + d,
@@ -834,7 +854,7 @@ static void tst_vars(polynomial_ref const & p, unsigned sz, polynomial::var * xs
 
 static void tst_vars() {
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -850,7 +870,7 @@ static void tst_vars() {
     polynomial::var s012[3] = {0, 1, 2};
     polynomial::var s3[1] = {3};
     polynomial::var s01234[5] = {0, 1, 2, 3, 4};
-    
+
     tst_vars((x0 + 1)*((x0^2) + (x3^2))*(x2*x3), 3, s023);
     tst_vars((x0 + x2)*((x0^2) + (x3^2))*(x2*x3), 3, s023);
     tst_vars(((x1 + x4 + 1)^5), 2, s14);
@@ -874,7 +894,7 @@ static void tst_sqf(polynomial_ref const & p, polynomial_ref const & expected) {
 
 static void tst_sqf() {
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -897,7 +917,7 @@ static void tst_sqf() {
     tst_sqf(((x0 + x1 + x2 + x3)^5) + 1, ((x0 + x1 + x2 + x3)^5) + 1);
 }
 
-static void tst_substitute(polynomial_ref const & p, 
+static void tst_substitute(polynomial_ref const & p,
                            polynomial::var x1, mpz const & v1,
                            polynomial::var x2, mpz const & v2,
                            polynomial_ref const & expected) {
@@ -919,7 +939,7 @@ static void tst_substitute(polynomial_ref const & p,
 
 static void tst_substitute() {
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -960,7 +980,7 @@ static void tst_qsubstitute(polynomial_ref const & p,
 
 static void tst_qsubstitute() {
     unsynch_mpq_manager qm;
-    polynomial::manager m(qm);
+    reslimit rl; polynomial::manager m(rl, qm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -1013,7 +1033,7 @@ void tst_mfact(polynomial_ref const & p, unsigned num_distinct_factors) {
 
 static void tst_mfact() {
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -1083,7 +1103,7 @@ static void tst_mfact() {
     tst_mfact((x0^70) - 6*(x0^65) - (x0^60) + 60*(x0^55) - 54*(x0^50) - 230*(x0^45) + 274*(x0^40) + 542*(x0^35) - 615*(x0^30) - 1120*(x0^25) + 1500*(x0^20) - 160*(x0^15) - 395*(x0^10) + 76*(x0^5) + 34, 3);
     tst_mfact(((x0^4) - 8*(x0^2)), 2);
     tst_mfact((x0^5) - 2*(x0^3) + x0 - 1, 1);
-    tst_mfact( (x0^25) - 4*(x0^21) - 5*(x0^20) + 6*(x0^17) + 11*(x0^16) + 10*(x0^15) - 4*(x0^13) - 7*(x0^12) - 9*(x0^11) - 10*(x0^10) + 
+    tst_mfact( (x0^25) - 4*(x0^21) - 5*(x0^20) + 6*(x0^17) + 11*(x0^16) + 10*(x0^15) - 4*(x0^13) - 7*(x0^12) - 9*(x0^11) - 10*(x0^10) +
                (x0^9) + (x0^8) + (x0^7) + (x0^6) + 3*(x0^5) + x0 - 1, 2);
     tst_mfact( (x0^25) - 10*(x0^21) - 10*(x0^20) - 95*(x0^17) - 470*(x0^16) - 585*(x0^15) - 40*(x0^13) - 1280*(x0^12) - 4190*(x0^11) - 3830*(x0^10) + 400*(x0^9)+ 1760*(x0^8) + 760*(x0^7) - 2280*(x0^6) + 449*(x0^5) + 640*(x0^3) - 640*(x0^2) + 240*x0 - 32, 2);
     tst_mfact( x0^10, 1);
@@ -1099,7 +1119,7 @@ static void tst_mfact() {
     tst_mfact( (x0^50) - 10*(x0^40) + 38*(x0^30) - 2*(x0^25) - 100*(x0^20) - 40*(x0^15) + 121*(x0^10) - 38*(x0^5) - 17, 1);
     polynomial_ref & y = x0;
     tst_mfact(        (((y^5)  +  5*(y^4) +  10*(y^3) + 10*(y^2) + 5*y)^10)
-                 + 10*(((y^5)  +  5*(y^4) +  10*(y^3) + 10*(y^2) + 5*y)^9) 
+                 + 10*(((y^5)  +  5*(y^4) +  10*(y^3) + 10*(y^2) + 5*y)^9)
                  + 35*(((y^5)  +  5*(y^4) +  10*(y^3) + 10*(y^2) + 5*y)^8)
                  + 40*(((y^5)  +  5*(y^4) +  10*(y^3) + 10*(y^2) + 5*y)^7)
                  - 32*(((y^5)  +  5*(y^4) +  10*(y^3) + 10*(y^2) + 5*y)^6)
@@ -1113,32 +1133,32 @@ static void tst_mfact() {
     tst_mfact( ((y^5) - 15552)*
                ((y^20)- 15708*(y^15) + rational("138771724")*(y^10)- rational("432104148432")*(y^5) + rational("614198284585616")),
                2);
-    tst_mfact( (y^25) - 
-               rational("3125")*(y^21) - 
-               rational("15630")*(y^20) + 
-               rational("3888750")*(y^17) + 
-               rational("38684375")*(y^16) + 
-               rational("95765635")*(y^15) - 
-               rational("2489846500")*(y^13) - 
-               rational("37650481875")*(y^12) - 
-               rational("190548065625")*(y^11) - 
-               rational("323785250010")*(y^10) + 
-               rational("750249453025")*(y^9) + 
-               rational("14962295699875")*(y^8) + 
-               rational("111775113235000")*(y^7) + 
-               rational("370399286731250")*(y^6) + 
-               rational("362903064503129")*(y^5) - 
-               rational("2387239013984400")*(y^4) - 
-               rational("23872390139844000")*(y^3) - 
-               rational("119361950699220000")*(y^2) - 
-               rational("298404876748050000")*y - 
+    tst_mfact( (y^25) -
+               rational("3125")*(y^21) -
+               rational("15630")*(y^20) +
+               rational("3888750")*(y^17) +
+               rational("38684375")*(y^16) +
+               rational("95765635")*(y^15) -
+               rational("2489846500")*(y^13) -
+               rational("37650481875")*(y^12) -
+               rational("190548065625")*(y^11) -
+               rational("323785250010")*(y^10) +
+               rational("750249453025")*(y^9) +
+               rational("14962295699875")*(y^8) +
+               rational("111775113235000")*(y^7) +
+               rational("370399286731250")*(y^6) +
+               rational("362903064503129")*(y^5) -
+               rational("2387239013984400")*(y^4) -
+               rational("23872390139844000")*(y^3) -
+               rational("119361950699220000")*(y^2) -
+               rational("298404876748050000")*y -
                rational("298500366308609376"), 2);
 
     tst_mfact( rational("54")*(y^24) - (y^27) - 324*(y^21) + rational("17496")*(y^18) - 34992*(y^15)+ rational("1889568")*(y^12)- 1259712*(y^9) + rational("68024448")*(y^6), 3);
 
     tst_mfact( ((y^3)- 432)*(((y^3)+54)^2)*((y^6)+108)*((y^6)+6912)*((y^6)- 324*(y^3)+37044),
                5);
-    
+
     tst_mfact( ((y^6)- 6*(y^4) - 864*(y^3) + 12*(y^2) - 5184*y + 186616)*
                (((y^6) - 6*(y^4) + 108*(y^3) + 12*(y^2) + 648*y + 2908)^2)*
                ((y^12) - 12*(y^10) + 60*(y^8) + 56*(y^6) + 6720*(y^4) + 12768*(y^2) + 13456)*
@@ -1175,13 +1195,13 @@ static void tst_mfact() {
 
 static void tst_zp() {
     unsynch_mpz_manager    z;
-    polynomial::manager    pm(z);
-    
+    reslimit rl; polynomial::manager    pm(rl, z);
+
     polynomial_ref x(pm);
     polynomial_ref y(pm);
     x = pm.mk_polynomial(pm.mk_var());
     y = pm.mk_polynomial(pm.mk_var());
-    
+
     polynomial_ref p(pm);
     polynomial_ref q(pm);
     p = (x^4) + 2*(x^3) + 2*(x^2) + x;
@@ -1200,11 +1220,11 @@ static void tst_zp() {
         std::cout << "q[Z_3]: " << q3 << "\n";
         std::cout << "gcd[Z_3]: " << gcd(p3, q3) << "\n";
     }
-    
+
     std::cout << "back into Z[x,y]\ngcd: " << gcd(p, q) << "\n";
-    
+
     p = 5*(x^2)*(y^2) + 3*(x^3) + 7*(y^3) + 3;
-    { 
+    {
         polynomial::scoped_set_zp setZ11(pm, 11);
         polynomial_ref p11(pm);
 
@@ -1219,7 +1239,7 @@ static void tst_zp() {
     std::cout << "gcd: " << gcd(p, q) << "\n";
 }
 
-static void tst_translate(polynomial_ref const & p, polynomial::var x0, int v0, polynomial::var x1, int v1, polynomial::var x2, int v2, 
+static void tst_translate(polynomial_ref const & p, polynomial::var x0, int v0, polynomial::var x1, int v1, polynomial::var x2, int v2,
                           polynomial_ref const & expected) {
     std::cout << "---------------\n";
     std::cout << "p: " << p << std::endl;
@@ -1233,7 +1253,7 @@ static void tst_translate(polynomial_ref const & p, polynomial::var x0, int v0,
 
 static void tst_translate() {
     unsynch_mpq_manager qm;
-    polynomial::manager m(qm);
+    reslimit rl; polynomial::manager m(rl, qm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -1254,7 +1274,7 @@ static void tst_translate() {
     tst_translate(x3 + 1, 0, 1, 1, 2, 3, 10,
                   x3 + 11
                   );
-    tst_translate((x0^3)*(x1^2) + (x0^2)*(x1^3) + 10, 0, -3, 1, -2, 3, 0, 
+    tst_translate((x0^3)*(x1^2) + (x0^2)*(x1^3) + 10, 0, -3, 1, -2, 3, 0,
                   (x0^3)*(x1^2) + (x0^2)*(x1^3) - 4*(x0^3)*x1 - 15*(x0^2)*(x1^2) - 6*x0*(x1^3) + 4*(x0^3) +
                   48*(x0^2)*x1 + 63*x0*(x1^2) + 9*(x1^3) - 44*(x0^2) - 180*x0*x1 - 81*(x1^2) +
                   156*x0 + 216*x1 - 170
@@ -1264,7 +1284,7 @@ static void tst_translate() {
 #if 0
 static void tst_p25() {
     unsynch_mpq_manager qm;
-    polynomial::manager m(qm);
+    reslimit rl; polynomial::manager m(rl, qm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -1288,10 +1308,11 @@ static void tst_p25() {
 static void tst_mm() {
     unsynch_mpq_manager qm;
     // pm1 and pm2 share the same monomial manager
-    polynomial::manager * pm1_ptr = alloc(polynomial::manager, qm);
+    reslimit rl;
+    polynomial::manager * pm1_ptr = alloc(polynomial::manager, rl, qm);
     polynomial::manager & pm1 = *pm1_ptr;
-    polynomial::manager pm2(qm, &pm1.mm());
-    polynomial::manager pm3(qm); // pm3 has its own manager
+    polynomial::manager pm2(rl, qm, &pm1.mm());
+    polynomial::manager pm3(rl, qm); // pm3 has its own manager
     polynomial_ref p2(pm2);
     {
         polynomial_ref x0(pm1);
@@ -1302,7 +1323,7 @@ static void tst_mm() {
         x2 = pm1.mk_polynomial(pm1.mk_var());
         polynomial_ref p1(pm1);
         p1 = (x0 + x1 + x2)^2;
-        
+
         std::cout << "p1: " << p1 << "\n";
         p2 = convert(pm1, p1, pm2);
         std::cout << "p2: " << p2 << "\n";
@@ -1317,7 +1338,7 @@ static void tst_mm() {
     std::cout << "p2: " << p2 << "\n";
 }
 
-static void tst_eval(polynomial_ref const & p, polynomial::var x0, rational v0, polynomial::var x1, rational v1, polynomial::var x2, rational v2, 
+static void tst_eval(polynomial_ref const & p, polynomial::var x0, rational v0, polynomial::var x1, rational v1, polynomial::var x2, rational v2,
                      rational expected) {
     TRACE("eval_bug", tout << "tst_eval, " << p << "\n";);
     std::cout << "p: " << p << "\nx" << x0 << " -> " << v0 << "\nx" << x1 << " -> " << v1 << "\nx" << x2 << " -> " << v2 << "\n";
@@ -1336,7 +1357,7 @@ static void tst_eval(polynomial_ref const & p, polynomial::var x0, rational v0,
 
 static void tst_eval() {
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -1369,7 +1390,7 @@ static void tst_eval() {
 
 static void tst_mk_unique() {
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -1380,7 +1401,7 @@ static void tst_mk_unique() {
     polynomial_ref p(m);
     polynomial_ref q(m);
     polynomial_ref r(m);
-    
+
     p = (x0^3) + (x2^5) + x0*x1 + x0*x1*x1 + 3*x0*x0 + 5;
     q = x0*x1*x1 + (x0^3) + 3*x0*x0 + (x2^5) + 5 + x0*x1;
     r = x0*x1*x1 + (x0^3) + 3*x0*x0 + (x2^5) + 6 + x0*x1;
@@ -1414,7 +1435,7 @@ static void tst_del_eh() {
     dummy_del_eh eh2;
 
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     x0 = m.mk_polynomial(m.mk_var());
@@ -1423,7 +1444,7 @@ static void tst_del_eh() {
     m.add_del_eh(&eh1);
     x1 = 0;
     SASSERT(eh1.m_counter == 1);
-    
+
     m.add_del_eh(&eh2);
     x1 = m.mk_polynomial(m.mk_var());
     x1 = 0;
@@ -1444,7 +1465,7 @@ static void tst_del_eh() {
 
 static void tst_const_coeff() {
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     x0 = m.mk_polynomial(m.mk_var());
@@ -1453,7 +1474,7 @@ static void tst_const_coeff() {
     scoped_mpz c(nm);
 
     polynomial_ref p(m);
-    
+
     p = (x0^2)*x1 + 3*x0 + x1;
     SASSERT(!m.const_coeff(p, 0, 2, c));
     SASSERT(m.const_coeff(p, 0, 1, c) && c == 3);
@@ -1490,7 +1511,7 @@ static void tst_const_coeff() {
 static void tst_gcd2() {
     // enable_trace("mgcd");
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     polynomial_ref x1(m);
     polynomial_ref x2(m);
@@ -1525,11 +1546,11 @@ static void tst_gcd2() {
             (7*3*(x1^2) + 7*6*(x2^2) + 7*21*(x3^3))*(5*(x1^3) + 7*(x0^2) + 13),
             (3*(x1^2) + 6*(x2^2) + 21*(x3^3)));
 
-    tst_gcd((x2^6)*(x3^6) - 4*(x2^3)*(x3^6) + 2*(x2^6)*(x3^3) - 8*(x2^3)*(x3^3) + 4*(x1^3)*(x2^3)*(x3^3) - 8*(x1^3)*(x3^3) + 
+    tst_gcd((x2^6)*(x3^6) - 4*(x2^3)*(x3^6) + 2*(x2^6)*(x3^3) - 8*(x2^3)*(x3^3) + 4*(x1^3)*(x2^3)*(x3^3) - 8*(x1^3)*(x3^3) +
             4*(x3^6) + 8*(x3^3) + (x2^6) - 4*(x2^3) + 4*(x1^3)*(x2^3) - 8*(x1^3) + 4 + (x1^6),
             (-2)*(x2^3)*(x3^6) - 4*(x2^3)*(x3^3) + 4*(x3^6) + 8*(x3^3) - 2*(x1^3)*(x3^3) - 2*(x2^3) + 4 - 2*(x1^3),
             one);
-    
+
     tst_gcd((x1^2) - 2*x0 + 1 + (x0^2) + x0*x1 - 2*x1,
             x0*x1,
             one);
@@ -1541,7 +1562,7 @@ static void tst_gcd2() {
     p = 169*(x1^12)*(x2^16) - 468*x0*(x1^11)*(x2^16) + 428*(x0^2)*(x1^10)*(x2^16) - 92*(x0^3)*(x1^9)*(x2^16) - 82*(x0^4)*(x1^8)*(x2^16) + 52*(x0^5)*(x1^7)*(x2^16) - 4*(x0^6)*(x1^6)*(x2^16) - 4*(x0^7)*(x1^5)*(x2^16) + (x0^8)*(x1^4)*(x2^16) - 581*(x1^14)*(x2^14) + 1828*x0*(x1^13)*(x2^14) - 2452*(x0^2)*(x1^12)*(x2^14) + 548*(x0^3)*(x1^11)*(x2^14) + 1002*(x0^4)*(x1^10)*(x2^14) - 756*(x0^5)*(x1^9)*(x2^14) + 124*(x0^6)*(x1^8)*(x2^14) + 44*(x0^7)*(x1^7)*(x2^14) - 13*(x0^8)*(x1^6)*(x2^14) + 895*(x1^16)*(x2^12) - 1556*x0*(x1^15)*(x2^12) + 2864*(x0^2)*(x1^14)*(x2^12);
     tst_gcd(p, derivative(p, 2), (x1^4)*(x2^11));
 
-    tst_gcd((11*5*3)*((x0^2) + 1)*(x1 + 3), 
+    tst_gcd((11*5*3)*((x0^2) + 1)*(x1 + 3),
             (11*5*7)*((x0^2) + 1)*(x1 + 5),
             (11*5)*((x0^2) + 1));
 
@@ -1565,7 +1586,7 @@ static void tst_gcd2() {
             neg((-1)*(x0^2)*(x2^3)*(x3^6) + 2*x0*(x1^3)*(x2^3)*(x3^3) + (x0^3)*(x3^7) - (x1^6)*(x2^3) - 2*(x0^2)*(x1^3)*(x3^4) - (x0^3)*(x3^6) + x0*(x1^6)*x3 + 2*(x0^2)*(x1^3)*(x3^3) - 2*(x0^2)*(x2^3)*(x3^3) + 2*(x0^2)*(x3^6) - x0*(x1^6) + 2*x0*(x1^3)*(x2^3) - 4*x0*(x1^3)*(x3^3) + 2*(x0^3)*(x3^4) + 2*(x1^6) - 2*(x0^2)*(x1^3)*x3 - 2*(x0^3)*(x3^3) + 2*(x0^2)*(x1^3) - (x0^2)*(x2^3) + 4*(x0^2)*(x3^3) - 4*x0*(x1^3) + (x0^3)*x3 - (x0^3) + 2*(x0^2))
             );
 
-    tst_gcd(((11*5*3)*(x0^2) + 1)*(x1 + 3), 
+    tst_gcd(((11*5*3)*(x0^2) + 1)*(x1 + 3),
             ((11*5*3)*(x0^2) + 1)*(x1 + 5),
             ((11*5*3)*(x0^2) + 1));
 
@@ -1582,7 +1603,7 @@ static void tst_gcd3() {
     enable_trace("polynomial_gcd_detail");
     enable_trace("mpzzp");
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     polynomial_ref p(m);
@@ -1607,7 +1628,7 @@ static void tst_gcd4() {
     enable_trace("mgcd");
     // enable_trace("CRA");
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     polynomial_ref p(m);
@@ -1626,12 +1647,12 @@ static void tst_gcd4() {
         (1000000*x + 1)*(333333333*x + 1)*(77777777*x + 1)*(11111111*x + 1)*(x + 128384747)*(x + 82837437)*(x + 22848481);
     tst_gcd(p, derivative(p, 0), (x + 3)^9);
 }
-#endif 
+#endif
 
 static void tst_newton_interpolation() {
     // enable_trace("newton");
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     polynomial_ref y(m);
     x = m.mk_polynomial(m.mk_var());
@@ -1654,7 +1675,7 @@ static void tst_newton_interpolation() {
 
 static void tst_slow_mod_gcd() {
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x0(m), x1(m), x2(m), x3(m), x4(m), x5(m);
     x0 = m.mk_polynomial(m.mk_var());
     x1 = m.mk_polynomial(m.mk_var());
@@ -1675,17 +1696,17 @@ static void tst_slow_mod_gcd() {
     tst_gcd(p, q, b);
 
     return;
-    p = (x0^8) * 
-        (((x0^3)*x1*x2*x3*x4*x5 + x0*(x1^3)*x2*x3*x4*x5 + x0*x1*(x2^3)*x3*x4*x5 + x0*x1*x2*(x3^3)*x4*x5 + 
+    p = (x0^8) *
+        (((x0^3)*x1*x2*x3*x4*x5 + x0*(x1^3)*x2*x3*x4*x5 + x0*x1*(x2^3)*x3*x4*x5 + x0*x1*x2*(x3^3)*x4*x5 +
           x0*x1*x2*x3*(x4^3)*x5 + x0*x1*x2*x3*x4*(x5^3) - x0*x1*x2*x3*x4*x5 - 2)^2) *
-        (((x0^3)*x1*x2*x3*x4*x5 + x0*(x1^3)*x2*x3*x4*x5 + x0*x1*(x2^3)*x3*x4*x5 + x0*x1*x2*(x3^3)*x4*x5 + 
+        (((x0^3)*x1*x2*x3*x4*x5 + x0*(x1^3)*x2*x3*x4*x5 + x0*x1*(x2^3)*x3*x4*x5 + x0*x1*x2*(x3^3)*x4*x5 +
           x0*x1*x2*x3*(x4^3)*x5 + x0*x1*x2*x3*x4*(x5^3) - x0*x1*x2*x3*x4*x5 + 2)^2);
     p_prime = derivative(p, 0);
     tst_gcd(p, p_prime,
-            (x0^7) * 
-            ((x0^3)*x1*x2*x3*x4*x5 + x0*(x1^3)*x2*x3*x4*x5 + x0*x1*(x2^3)*x3*x4*x5 + x0*x1*x2*(x3^3)*x4*x5 + 
-             x0*x1*x2*x3*(x4^3)*x5 + x0*x1*x2*x3*x4*(x5^3) - x0*x1*x2*x3*x4*x5 - 2) * 
-            ((x0^3)*x1*x2*x3*x4*x5 + x0*(x1^3)*x2*x3*x4*x5 + x0*x1*(x2^3)*x3*x4*x5 + x0*x1*x2*(x3^3)*x4*x5 + 
+            (x0^7) *
+            ((x0^3)*x1*x2*x3*x4*x5 + x0*(x1^3)*x2*x3*x4*x5 + x0*x1*(x2^3)*x3*x4*x5 + x0*x1*x2*(x3^3)*x4*x5 +
+             x0*x1*x2*x3*(x4^3)*x5 + x0*x1*x2*x3*x4*(x5^3) - x0*x1*x2*x3*x4*x5 - 2) *
+            ((x0^3)*x1*x2*x3*x4*x5 + x0*(x1^3)*x2*x3*x4*x5 + x0*x1*(x2^3)*x3*x4*x5 + x0*x1*x2*(x3^3)*x4*x5 +
              x0*x1*x2*x3*(x4^3)*x5 + x0*x1*x2*x3*x4*(x5^3) - x0*x1*x2*x3*x4*x5 + 2));
 }
 
@@ -1698,7 +1719,7 @@ void tst_linear_solver() {
 
     solver.resize(3);
     xs.resize(3);
-    
+
     as.reset();
     as.push_back(mpq(2));  as.push_back(mpq(1));  as.push_back(mpq(-1)); qm.set(b, 8);
     solver.add(0, as.c_ptr(), b);
@@ -1710,7 +1731,7 @@ void tst_linear_solver() {
     as.reset();
     as.push_back(mpq(-2)); as.push_back(mpq(1));  as.push_back(mpq(2));  qm.set(b, -3);
     solver.add(2, as.c_ptr(), b);
-    
+
     VERIFY(solver.solve(xs.c_ptr()));
     SASSERT(qm.eq(xs[0], mpq(2)));
     SASSERT(qm.eq(xs[1], mpq(3)));
@@ -1719,7 +1740,7 @@ void tst_linear_solver() {
 
 static void tst_lex(polynomial_ref const & p1, polynomial_ref const & p2, int lex_expected, polynomial::var min, int lex2_expected) {
     polynomial::manager & m = p1.m();
-    std::cout << "compare "; 
+    std::cout << "compare ";
     m.display(std::cout, m.get_monomial(p1, 0));
     std::cout << " ";
     m.display(std::cout, m.get_monomial(p2, 0));
@@ -1735,7 +1756,7 @@ static void tst_lex(polynomial_ref const & p1, polynomial_ref const & p2, int le
 
 static void tst_lex() {
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x0(m), x1(m), x2(m), x3(m), x4(m), x5(m);
     x0 = m.mk_polynomial(m.mk_var());
     x1 = m.mk_polynomial(m.mk_var());
@@ -1743,13 +1764,13 @@ static void tst_lex() {
     x3 = m.mk_polynomial(m.mk_var());
     x4 = m.mk_polynomial(m.mk_var());
     x5 = m.mk_polynomial(m.mk_var());
-    
+
     polynomial_ref one(m);
     one = m.mk_const(mpz(1));
 
     tst_lex(x0*x4*x1, (x0^10)*(x1^3), 1, 4, -1);
     tst_lex(x0*x3*(x1^2)*x4, x0*(x3^2)*(x1^2)*x4, -1, 3, -1);
-    tst_lex((x0^2)*x3*(x1^2)*x4, x0*(x3^2)*(x1^2)*x4, -1, 3, 1); 
+    tst_lex((x0^2)*x3*(x1^2)*x4, x0*(x3^2)*(x1^2)*x4, -1, 3, 1);
     tst_lex(x0*x3*(x1^2)*x4, x0*x3*(x1^2)*x4, 0, 3, 0);
     tst_lex(x0*(x3^2)*(x1^2)*x4, x0*x3*(x1^2)*x4, 1, 3, 1);
     tst_lex((x1^2)*x4, x0*x2*x3*x4*x5, -1, 1, -1);
@@ -1772,18 +1793,18 @@ static void tst_lex() {
 
 static void tst_divides() {
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    reslimit rl; polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     x0 = m.mk_polynomial(m.mk_var());
     polynomial_ref q(m);
     polynomial_ref p(m);
 
-    q = 16*(x0^27) - 1984*(x0^26) + 1762*(x0^25) + 17351*(x0^24) - 14165*(x0^23) + 16460*(x0^22) + 2919*(x0^21) - 16823*(x0^20) + 1530*(x0^19) + 
+    q = 16*(x0^27) - 1984*(x0^26) + 1762*(x0^25) + 17351*(x0^24) - 14165*(x0^23) + 16460*(x0^22) + 2919*(x0^21) - 16823*(x0^20) + 1530*(x0^19) +
         10646*(x0^18) + 19217*(x0^17);
-    p = 16*(x0^39) - 3648*(x0^38) + 338136*(x0^37) - 16037936*(x0^36) + 392334357*(x0^35) - rational("3851617443")*(x0^34) - 
-        rational("14636221526")*(x0^33) + rational("377151717618")*(x0^32) + rational("677140776981")*(x0^31) - rational("4308280094419")*(x0^30) + 
-        rational("312708087606")*(x0^29) + rational("8205543533730")*(x0^28) + rational("3331586202704")*(x0^27) - rational("15291636627072")*(x0^26) + 
-        rational("433482645282")*(x0^25) + rational("7397104817486")*(x0^24) + rational("1021197979053")*(x0^23) - rational("1373737505247")*(x0^22) - 
+    p = 16*(x0^39) - 3648*(x0^38) + 338136*(x0^37) - 16037936*(x0^36) + 392334357*(x0^35) - rational("3851617443")*(x0^34) -
+        rational("14636221526")*(x0^33) + rational("377151717618")*(x0^32) + rational("677140776981")*(x0^31) - rational("4308280094419")*(x0^30) +
+        rational("312708087606")*(x0^29) + rational("8205543533730")*(x0^28) + rational("3331586202704")*(x0^27) - rational("15291636627072")*(x0^26) +
+        rational("433482645282")*(x0^25) + rational("7397104817486")*(x0^24) + rational("1021197979053")*(x0^23) - rational("1373737505247")*(x0^22) -
         rational("639394669026")*(x0^21) - rational("118513560618")*(x0^20) - rational("10405319535")*(x0^19) - rational("358722675")*(x0^18);
     std::cout << "----------------------\n";
     std::cout << "q: " << q << "\n";
@@ -1813,7 +1834,7 @@ void tst_polynomial() {
     tst_linear_solver();
     tst_newton_interpolation();
     tst_resultant();
-    // 
+    //
     // tst_gcd4();
     // tst_gcd3();
     tst_zp();
diff --git a/src/test/polynomial_factorization.cpp b/src/test/polynomial_factorization.cpp
index 7af0742ef..361ca4630 100644
--- a/src/test/polynomial_factorization.cpp
+++ b/src/test/polynomial_factorization.cpp
@@ -19,7 +19,7 @@ Notes:
 #include"upolynomial_factorization_int.h"
 #include"timeit.h"
 #include"polynomial.h"
-
+#include"rlimit.h"
 #if 0
 #include"polynomial_factorization.h"
 #endif
@@ -41,30 +41,30 @@ unsigned knuth_factors[2][11] = {
 
 // [k,l,i]: how many factors the S_k has over p_i, when i = 0 it's Z, p_1 = 2, for l=0 distinct, for l = 1 total
 unsigned swinnerton_dyer_factors[5][2][11] = {
-    // S1 = (x^2) - 2 
+    // S1 = (x^2) - 2
     {
-    //   2, 3, 5, 7,11,13,17,19,23,29, Z 
+    //   2, 3, 5, 7,11,13,17,19,23,29, Z
         {1, 1, 1, 2, 1, 1, 2, 1, 2, 1, 1},
         {2, 1, 1, 2, 1, 1, 2, 1, 2, 1, 1}
     },
-    // S2 = (x^4) - 10*(x^2) + 1 
+    // S2 = (x^4) - 10*(x^2) + 1
     {
         {1, 1, 2, 2, 2, 2, 2, 2, 4, 2, 1},
         {4, 2, 2, 2, 2, 2, 2, 2, 4, 2, 1}
     },
-    // S3 = (x^8) - 40*(x^6) + 352*(x^4) - 960*(x^2) + 576 
+    // S3 = (x^8) - 40*(x^6) + 352*(x^4) - 960*(x^2) + 576
     {
         {1, 2, 2, 4, 4, 4, 4, 4, 4, 4, 1},
         {8, 6, 4, 4, 4, 4, 4, 4, 4, 4, 1}
     },
-    // S4 = (x^16) - 136*(x^14) + 6476*(x^12) - 141912*(x^10) + 1513334*(x^8) - 7453176*(x^6) + 13950764*(x^4) - 5596840*(x^2) + 46225 
+    // S4 = (x^16) - 136*(x^14) + 6476*(x^12) - 141912*(x^10) + 1513334*(x^8) - 7453176*(x^6) + 13950764*(x^4) - 5596840*(x^2) + 46225
     {
         {1, 4, 3, 4, 8, 8, 8, 8, 8, 8, 1},
         {16, 12, 10, 8, 8, 8, 8, 8, 8, 8, 1}
     },
     // SA = S1*S2*S3*S4
     {
-    //p = 2,  3,  5,  7, 11, 13, 17, 19, 23, 29, Z 
+    //p = 2,  3,  5,  7, 11, 13, 17, 19, 23, 29, Z
         { 2,  6,  3,  6, 15, 11, 16, 15, 18, 15, 1},
         {30, 21, 17, 16, 15, 15, 16, 15, 18, 15, 1}
     }
@@ -176,17 +176,17 @@ int random_polynomial[20][2][11] = {
 #if 0
 static void tst_square_free_finite_1() {
     polynomial::numeral_manager nm;
-    polynomial::manager pm(nm);
+    reslimit rl; polynomial::manager pm(rl, nm);
 
     // example from Knuth, p. 442
     polynomial_ref x(pm);
     x = pm.mk_polynomial(pm.mk_var());
 
     // polynomials \prod_{i < p} (x - i)^i
-    for (unsigned prime_i = 0; prime_i < 5; ++ prime_i) 
+    for (unsigned prime_i = 0; prime_i < 5; ++ prime_i)
     {
         int p = primes[prime_i];
-        
+
         // make the polynomial
         polynomial_ref f(pm);
         f = x - 1;
@@ -222,19 +222,19 @@ static void tst_square_free_finite_1() {
 }
 
 static void tst_factor_finite_1() {
-    
+
     polynomial::numeral_manager nm;
-    polynomial::manager pm(nm);
+    reslimit rl; polynomial::manager pm(rl, nm);
 
     // example from Knuth, p. 442
     polynomial_ref x(pm);
     x = pm.mk_polynomial(pm.mk_var());
     polynomial_ref K(pm);
     K = (x^8) + (x^6) + 10*(x^4) + 10*(x^3) + 8*(x^2) + 2*x + 8;
-    
+
     // factor them for all the prime numbers
-    for (unsigned prime_i = 0; prime_i < sizeof(primes)/sizeof(unsigned); ++ prime_i) 
-    {        
+    for (unsigned prime_i = 0; prime_i < sizeof(primes)/sizeof(unsigned); ++ prime_i)
+    {
         // make the Z_p
         unsigned prime = primes[prime_i];
         upolynomial::zp_manager upm(nm);
@@ -246,35 +246,35 @@ static void tst_factor_finite_1() {
 
         cout << "Factoring " << K << "("; upm.display(cout, K_u); cout << ") in Z_" << prime << endl;
         cout << "Expecting " << knuth_factors[0][prime_i] << " distinct factors, " << knuth_factors[1][prime_i] << " total" << endl;
-        
+
         // factor it
-        upolynomial::zp_factors factors(upm);        
+        upolynomial::zp_factors factors(upm);
         /* bool factorized = */ upolynomial::zp_factor(upm, K_u, factors);
-    
+
         // check the result
         unsigned distinct = factors.distinct_factors();
-        unsigned total = factors.total_factors();            
+        unsigned total = factors.total_factors();
 
         cout << "Got " << factors << endl;
         cout << "Thats " << distinct << " distinct factors, " << total << " total" << endl;
 
         SASSERT(knuth_factors[0][prime_i] == distinct);
         SASSERT(knuth_factors[1][prime_i] == total);
-            
+
         upolynomial::numeral_vector multiplied;
         factors.multiply(multiplied);
         SASSERT(upm.eq(K_u, multiplied));
         upm.reset(multiplied);
-        
+
         // remove the temp
         upm.reset(K_u);
-    }    
+    }
 }
 
 static void tst_factor_finite_2() {
-    
+
     polynomial::numeral_manager nm;
-    polynomial::manager pm(nm);
+    reslimit rl; polynomial::manager pm(rl, nm);
 
     polynomial_ref x(pm);
     x = pm.mk_polynomial(pm.mk_var());
@@ -284,7 +284,7 @@ static void tst_factor_finite_2() {
     polynomial_ref S2 = (x^4) - 10*(x^2) + 1;
     polynomial_ref S3 = (x^8) - 40*(x^6) + 352*(x^4) - 960*(x^2) + 576;
     polynomial_ref S4 = (x^16) - 136*(x^14) + 6476*(x^12) - 141912*(x^10) + 1513334*(x^8) - 7453176*(x^6) + 13950764*(x^4) - 5596840*(x^2) + 46225;
-    
+
     vector<polynomial_ref> S;
     S.push_back(S1);
     S.push_back(S2);
@@ -294,9 +294,9 @@ static void tst_factor_finite_2() {
 
     // factor all the S_i them for all the prime numbers
     for (unsigned S_i = 0; S_i < S.size(); ++ S_i) {
-        for (unsigned prime_i = 0; prime_i < sizeof(primes)/sizeof(unsigned); ++ prime_i) {            
-            unsigned prime = primes[prime_i];            
-            
+        for (unsigned prime_i = 0; prime_i < sizeof(primes)/sizeof(unsigned); ++ prime_i) {
+            unsigned prime = primes[prime_i];
+
             upolynomial::zp_manager upm(nm);
             upm.set_zp(prime);
 
@@ -308,22 +308,22 @@ static void tst_factor_finite_2() {
 
             upolynomial::zp_factors factors(upm);
             upolynomial::zp_factor(upm, S_i_u, factors);
-    
+
             // check the result
             unsigned distinct = factors.distinct_factors();
-            unsigned total = factors.total_factors();            
+            unsigned total = factors.total_factors();
 
             cout << "Got " << factors << endl;
             cout << "Thats " << distinct << " distinct factors, " << total << " total" << endl;
 
             SASSERT(swinnerton_dyer_factors[S_i][0][prime_i] == distinct);
             SASSERT(swinnerton_dyer_factors[S_i][1][prime_i] == total);
-            
+
             upolynomial::numeral_vector multiplied;
             factors.multiply(multiplied);
             SASSERT(upm.eq(S_i_u, multiplied));
             upm.reset(multiplied);
-        
+
             // remove the temp
             upm.reset(S_i_u);
         }
@@ -331,9 +331,9 @@ static void tst_factor_finite_2() {
 }
 
 static void tst_factor_finite_3() {
-    
+
     polynomial::numeral_manager nm;
-    polynomial::manager pm(nm);
+    reslimit rl; polynomial::manager pm(rl, nm);
 
     polynomial_ref x(pm);
     x = pm.mk_polynomial(pm.mk_var());
@@ -360,15 +360,15 @@ static void tst_factor_finite_3() {
     random_p.push_back( 3*(x^10) + 2*(x^8) + 1*(x^7) + 1*(x^6) + 3*(x^4) + 3*(x^3) + 4*(x^2) + 3*x + 0 );
     random_p.push_back( 1*(x^10) + 2*(x^9) + 2*(x^6) + 4*(x^3) + 4*(x^2) + 0 );
     random_p.push_back( 1*(x^10) + 2*(x^9) + 2*(x^8) + 4*(x^7) + 4*(x^6) + 1*(x^5) + 1*(x^3) + 1*(x^2) + 3*x + 0 );
-    
+
     // factor all the randoms them for all the prime numbers
     for (unsigned random_i = 0; random_i < random_p.size(); ++ random_i) {
-        for (unsigned prime_i = 0; prime_i < sizeof(primes)/sizeof(unsigned); ++ prime_i) {            
-            unsigned prime = primes[prime_i];            
-            
+        for (unsigned prime_i = 0; prime_i < sizeof(primes)/sizeof(unsigned); ++ prime_i) {
+            unsigned prime = primes[prime_i];
+
             upolynomial::zp_manager upm(nm);
             upm.set_zp(prime);
-            
+
             upolynomial::numeral_vector poly;
             upm.to_numeral_vector(random_p[random_i], poly);
 
@@ -377,24 +377,24 @@ static void tst_factor_finite_3() {
 
             upolynomial::zp_factors factors(upm);
             upolynomial::zp_factor(upm, poly, factors);
-    
+
             // check the result
             unsigned distinct = factors.distinct_factors();
-            unsigned total = factors.total_factors();            
+            unsigned total = factors.total_factors();
 
             cout << "Got " << factors << endl;
             cout << "Thats " << distinct << " distinct factors, " << total << " total" << endl;
 
             // SASSERT(random_polynomial[random_i][0][prime_i] == distinct);
             // SASSERT(random_polynomial[random_i][1][prime_i] == total);
-            
+
             upolynomial::numeral_vector multiplied;
             factors.multiply(multiplied);
             bool equal = upm.eq(poly, multiplied);
             cout << (equal ? "equal" : "not equal") << endl;
             SASSERT(equal);
             upm.reset(multiplied);
-        
+
             // remove the temp
             upm.reset(poly);
         }
@@ -403,11 +403,11 @@ static void tst_factor_finite_3() {
 
 static void tst_factor_enumeration() {
     polynomial::numeral_manager nm;
-    polynomial::manager pm(nm);
+    reslimit rl; polynomial::manager pm(rl, nm);
 
     polynomial_ref x(pm);
     x = pm.mk_polynomial(pm.mk_var());
-    
+
     vector<polynomial_ref> factors;
     for (int i = 0; i < 5; ++ i) {
         polynomial_ref factor(pm);
@@ -419,12 +419,12 @@ static void tst_factor_enumeration() {
 
     upolynomial::zp_manager upm_13(nm);
     upm_13.set_zp(13);
-    upolynomial::zp_factors factors_13(upm_13);    
-    
+    upolynomial::zp_factors factors_13(upm_13);
+
     upolynomial::numeral constant;
     nm.set(constant, 10);
     factors_13.set_constant(constant);
-    
+
     for (unsigned i = 0; i < 5; ++ i) {
         upolynomial::numeral_vector ufactor;
         upm_13.to_numeral_vector(factors[i], ufactor);
@@ -463,7 +463,7 @@ static void tst_factor_enumeration() {
         factors_13.set_degree(i, factors_13.get_degree(i) + i);
     }
     cout << "Different: " << factors_13 << " of degree " << factors_13.get_degree() << endl;
-    upolynomial::factorization_degree_set degrees1(factors_13);    
+    upolynomial::factorization_degree_set degrees1(factors_13);
     degrees1.display(cout); cout << endl; // [0, ..., 15]
 
     polynomial_ref tmp1 = (x^3) + 1;
@@ -482,15 +482,15 @@ static void tst_factor_enumeration() {
     upm_13.reset(up3);
 
     cout << "Different: " << tmp << " of degree " << tmp.get_degree() << endl;
-    upolynomial::factorization_degree_set degrees2(tmp);    
-    degrees2.display(cout); cout << endl; 
+    upolynomial::factorization_degree_set degrees2(tmp);
+    degrees2.display(cout); cout << endl;
 
     tmp1 = (x^2) + 1;
     tmp2 = (x^10) + 2;
-    tmp3 = x + 3;    
+    tmp3 = x + 3;
     upm_13.to_numeral_vector(tmp1, up1);
     upm_13.to_numeral_vector(tmp2, up2);
-    upm_13.to_numeral_vector(tmp3, up3);    
+    upm_13.to_numeral_vector(tmp3, up3);
     tmp.clear();
     tmp.push_back(up1, 2);
     tmp.push_back(up2, 1);
@@ -499,23 +499,23 @@ static void tst_factor_enumeration() {
     upm_13.reset(up1);
     upm_13.reset(up2);
     upm_13.reset(up3);
-    upolynomial::factorization_degree_set degrees3(tmp);    
-    degrees3.display(cout); cout << endl; 
+    upolynomial::factorization_degree_set degrees3(tmp);
+    degrees3.display(cout); cout << endl;
     degrees1.intersect(degrees3);
     degrees1.display(cout); cout << endl;
 }
 
 static void tst_factor_square_free_univariate_1(unsigned max_length) {
-   
-    polynomial::numeral_manager nm;    
+
+    polynomial::numeral_manager nm;
     upolynomial::numeral test;
     upolynomial::numeral p;
     nm.set(test, -9);
     nm.set(p, 5);
     nm.mod(test, p, test);
 
-    polynomial::manager pm(nm);
-    
+    reslimit rl; polynomial::manager pm(rl, nm);
+
     polynomial_ref x(pm);
     x = pm.mk_polynomial(pm.mk_var());
 
@@ -527,8 +527,8 @@ static void tst_factor_square_free_univariate_1(unsigned max_length) {
     for(unsigned length = 1; length < max_length; ++ length) {
 
         // starting from prime_i going for length
-        for(unsigned start_i = 0; start_i < n_primes; ++ start_i) {            
-           
+        for(unsigned start_i = 0; start_i < n_primes; ++ start_i) {
+
             polynomial_ref f(pm);
 
             bool first = true;
@@ -541,18 +541,18 @@ static void tst_factor_square_free_univariate_1(unsigned max_length) {
                 } else {
                     f = f*(p1*(x^p2) - p2);
                 }
-            }            
-        
+            }
+
             upolynomial::manager upm(nm);
             scoped_mpz_vector f_u(nm);
             upm.to_numeral_vector(f, f_u);
-        
+
             cout << "factoring "; upm.display(cout, f_u); cout << endl;
             cout << "expecting " << length << " factors ";
             upolynomial::factors factors(upm);
-            /* bool ok = */ upolynomial::factor_square_free(upm, f_u, factors); 
+            /* bool ok = */ upolynomial::factor_square_free(upm, f_u, factors);
             cout << "got " << factors << endl;
-            
+
             SASSERT(factors.distinct_factors() == length);
         }
     }
@@ -560,7 +560,7 @@ static void tst_factor_square_free_univariate_1(unsigned max_length) {
 
 static void tst_factor_square_free_univariate_2() {
     polynomial::numeral_manager nm;
-    polynomial::manager pm(nm);
+    reslimit rl; polynomial::manager pm(rl, nm);
 
     polynomial_ref x(pm);
     x = pm.mk_polynomial(pm.mk_var());
@@ -570,7 +570,7 @@ static void tst_factor_square_free_univariate_2() {
     polynomial_ref S2 = (x^4) - 10*(x^2) + 1;
     polynomial_ref S3 = (x^8) - 40*(x^6) + 352*(x^4) - 960*(x^2) + 576;
     polynomial_ref S4 = (x^16) - 136*(x^14) + 6476*(x^12) - 141912*(x^10) + 1513334*(x^8) - 7453176*(x^6) + 13950764*(x^4) - 5596840*(x^2) + 46225;
-    
+
     vector<polynomial_ref> S;
     S.push_back(S1);
     S.push_back(S2);
@@ -580,17 +580,17 @@ static void tst_factor_square_free_univariate_2() {
     upolynomial::manager upm(nm);
 
     // factor all the S_i them for all the prime numbers
-    for (unsigned S_i = 0; S_i < S.size(); ++ S_i) {        
+    for (unsigned S_i = 0; S_i < S.size(); ++ S_i) {
         upolynomial::numeral_vector S_i_u;
         upm.to_numeral_vector(S[S_i], S_i_u);
 
         cout << "Factoring "; upm.display(cout, S_i_u); cout << " over Z " << endl;
         upolynomial::factors factors(upm);
         upolynomial::factor_square_free(upm, S_i_u, factors);
-    
+
         // check the result
         cout << "Got " << factors << endl;
-        
+
         // remove the temp
         upm.reset(S_i_u);
     }
@@ -598,31 +598,31 @@ static void tst_factor_square_free_univariate_2() {
 
 static void tst_factor_square_free_univariate_3() {
     polynomial::numeral_manager nm;
-    polynomial::manager pm(nm);
+    reslimit rl; polynomial::manager pm(rl, nm);
 
     polynomial_ref x(pm);
     x = pm.mk_polynomial(pm.mk_var());
 
     polynomial_ref deg70 = (x^70) - 6*(x^65) - (x^60) + 60*(x^55) - 54*(x^50) - 230*(x^45) + 274*(x^40) + 542*(x^35) - 615*(x^30)  - 1120*(x^25) + 1500*(x^20) - 160*(x^15) - 395*(x^10) + 76*(x^5) + 34;
-    
+
     upolynomial::manager upm(nm);
     upolynomial::numeral_vector deg70_u;
-    
+
     upm.to_numeral_vector(deg70, deg70_u);
 
     cout << "Factoring "; upm.display(cout, deg70_u); cout << " over Z " << endl;
     upolynomial::factors factors(upm);
     upolynomial::factor_square_free(upm, deg70_u, factors);
-    
+
     cout << "Got " << factors << endl;
-        
+
     upm.reset(deg70_u);
 }
 #endif
 
 void tst_factor_swinnerton_dyer_big(unsigned max) {
     polynomial::numeral_manager nm;
-    polynomial::manager pm(nm);
+    reslimit rl; polynomial::manager pm(rl, nm);
 
     polynomial_ref x(pm);
     x = pm.mk_polynomial(pm.mk_var());
@@ -631,8 +631,8 @@ void tst_factor_swinnerton_dyer_big(unsigned max) {
     vector<polynomial::var> vars;
 
     unsigned n = std::min(max, static_cast<unsigned>(sizeof(primes)/sizeof(unsigned)));
-    for(unsigned prime_i = 0; prime_i < n; ++ prime_i) {            
-        
+    for(unsigned prime_i = 0; prime_i < n; ++ prime_i) {
+
         int prime = primes[prime_i];
 
         cout << "Computing Swinnerton-Dyer[" << prime_i + 1 << "]" << endl;
@@ -643,7 +643,7 @@ void tst_factor_swinnerton_dyer_big(unsigned max) {
 
         polynomial_ref p(pm);
         p = (y^2) - prime;
-        roots.push_back(p);       
+        roots.push_back(p);
 
         polynomial_ref computation = x;
         for (unsigned i = 0; i < roots.size(); ++ i) {
@@ -663,17 +663,18 @@ void tst_factor_swinnerton_dyer_big(unsigned max) {
         }
 
         cout << "Computed Swinnerton-Dyer[" << prime_i + 1 << "], degree = " << pm.total_degree(computation) << ", size = " << pm.size(computation) << endl;
-        
+
         cout << "Starting factoring " << endl;
-        
+
         {
             timeit timer(true, "factoring swinnerton-dyer");
 
-            upolynomial::manager upm(nm);
-            scoped_mpz_vector sd_u(nm);    
-            upm.to_numeral_vector(computation, sd_u);            
+            reslimit rl;
+            upolynomial::manager upm(rl, nm);
+            scoped_mpz_vector sd_u(nm);
+            upm.to_numeral_vector(computation, sd_u);
             upolynomial::factors factors(upm);
-            upolynomial::factor_square_free(upm, sd_u, factors);   
+            upolynomial::factor_square_free(upm, sd_u, factors);
             cout << "Got " << factors.distinct_factors() << " factors" << endl;
         }
 
@@ -681,16 +682,16 @@ void tst_factor_swinnerton_dyer_big(unsigned max) {
 }
 
 static void tst_factor_square_free_multivariate_1(unsigned max_n) {
-#if 0   
-    polynomial::numeral_manager nm;    
+#if 0
+    polynomial::numeral_manager nm;
     upolynomial::numeral test;
     upolynomial::numeral p;
     nm.set(test, -9);
     nm.set(p, 5);
     nm.mod(test, p, test);
 
-    polynomial::manager pm(nm);
-    
+    reslimit rl; polynomial::manager pm(rl, nm);
+
     polynomial_ref x(pm);
     x = pm.mk_polynomial(pm.mk_var());
 
@@ -700,7 +701,7 @@ static void tst_factor_square_free_multivariate_1(unsigned max_n) {
     // lets start simple x^n - y^n
     for (unsigned prime_i = 0; prime_i < sizeof(primes)/sizeof(unsigned); ++ prime_i) {
 		unsigned prime = primes[prime_i];
-		
+
 		if (prime > max_n) {
 			break;
 		}
@@ -719,7 +720,7 @@ static void tst_factor_square_free_multivariate_1(unsigned max_n) {
 
 
 void tst_polynomial_factorization() {
-    
+
     enable_trace("polynomial::factorization");
     // enable_trace("polynomial::factorization::bughunt");
 	enable_trace("polynomial::factorization::multivariate");
@@ -727,12 +728,12 @@ void tst_polynomial_factorization() {
 
     // Z_p square-free factorization tests
     // tst_square_free_finite_1();
-    
+
     // Z_p factorization tests
     // tst_factor_finite_1();
     // tst_factor_finite_2();
     // tst_factor_finite_3();
-    
+
     // Z factorization
     // tst_factor_enumeration();
     // tst_factor_square_free_univariate_1(3);
diff --git a/src/test/rcf.cpp b/src/test/rcf.cpp
index 294a7df29..170c053f1 100644
--- a/src/test/rcf.cpp
+++ b/src/test/rcf.cpp
@@ -18,10 +18,12 @@ Notes:
 --*/
 #include"realclosure.h"
 #include"mpz_matrix.h"
+#include"rlimit.h"
 
 static void tst1() {
     unsynch_mpq_manager qm;
-    rcmanager m(qm);
+    reslimit rl;
+    rcmanager m(rl, qm);
     scoped_rcnumeral a(m);
 #if 0
     a = 10;
@@ -37,14 +39,14 @@ static void tst1() {
     qm.set(aux, 1, 3);
     m.set(a, aux);
 
-#if 0    
+#if 0
     std::cout << interval_pp(a) << std::endl;
     std::cout << decimal_pp(eps, 4) << std::endl;
     std::cout << decimal_pp(a) << std::endl;
     std::cout << a + eps << std::endl;
     std::cout << a * eps << std::endl;
     std::cout << (a + eps)*eps - eps << std::endl;
-#endif    
+#endif
     std::cout << interval_pp(a - eps*2) << std::endl;
     std::cout << interval_pp(eps + 1) << std::endl;
     scoped_rcnumeral t(m);
@@ -80,7 +82,7 @@ static void tst2() {
     // 0 1  1
     A.set(0, 0, 1); A.set(0, 1, 1); A.set(0, 2,  1);
     A.set(1, 0, 0); A.set(1, 1, 1); A.set(1, 2, -1);
-    A.set(2, 0, 0); A.set(2, 1, 1); A.set(2, 2,  1); 
+    A.set(2, 0, 0); A.set(2, 1, 1); A.set(2, 2,  1);
     std::cout << A;
     {
         int b[3];
@@ -143,8 +145,9 @@ static void tst_lin_indep(unsigned m, unsigned n, int _A[], unsigned ex_sz, unsi
 }
 
 static void tst_denominators() {
+    reslimit rl;
     unsynch_mpq_manager qm;
-    rcmanager m(qm);
+    rcmanager m(rl, qm);
     scoped_rcnumeral a(m);
     scoped_rcnumeral t(m);
     scoped_rcnumeral eps(m);
diff --git a/src/test/simplex.cpp b/src/test/simplex.cpp
index 3a5e58a4b..6f08bd04d 100644
--- a/src/test/simplex.cpp
+++ b/src/test/simplex.cpp
@@ -11,6 +11,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "mpq_inf.h"
 #include "vector.h"
 #include "rational.h"
+#include "rlimit.h"
 
 #define R rational
 typedef simplex::simplex<simplex::mpz_ext> Simplex;
@@ -99,7 +100,8 @@ static void feas(Simplex& S) {
 }
 
 static void test1() {
-    Simplex S;
+    reslimit rl;
+    Simplex S(rl);
     add_row(S, vec(1,0), R(1));
     add_row(S, vec(0,1), R(1));
     add_row(S, vec(1,1), R(1));
@@ -107,7 +109,7 @@ static void test1() {
 }
 
 static void test2() {
-    Simplex S;
+    reslimit rl; Simplex S(rl);
     add_row(S, vec(1, 0), R(1));
     add_row(S, vec(0, 1), R(1));
     add_row(S, vec(1, 1), R(1), true);
@@ -115,7 +117,7 @@ static void test2() {
 }
 
 static void test3() {
-    Simplex S;
+    reslimit rl; Simplex S(rl);
     add_row(S, vec(-1, 0), R(-1));
     add_row(S, vec(0, -1), R(-1));
     add_row(S, vec(1, 1), R(1), true);
@@ -123,7 +125,7 @@ static void test3() {
 }
 
 static void test4() {
-    Simplex S;
+    reslimit rl; Simplex S(rl);
     add_row(S, vec(1, 0), R(1));
     add_row(S, vec(0, -1), R(-1));
     add_row(S, vec(1, 1), R(1), true);
@@ -131,7 +133,7 @@ static void test4() {
 }
 
 void tst_simplex() {
-    Simplex S;
+    reslimit rl; Simplex S(rl);
 
     std::cout << "simplex\n";
 
@@ -152,7 +154,7 @@ void tst_simplex() {
     is_sat = S.make_feasible();
     std::cout << "feasible: " << is_sat << "\n";
     S.display(std::cout);
-    _scoped_numeral<unsynch_mpq_inf_manager> num(em); 
+    _scoped_numeral<unsynch_mpq_inf_manager> num(em);
     num = std::make_pair(mpq(1), mpq(0));
     S.set_lower(0, num);
     S.set_upper(0, num);
diff --git a/src/test/trigo.cpp b/src/test/trigo.cpp
index da26d0f39..809d94fc2 100644
--- a/src/test/trigo.cpp
+++ b/src/test/trigo.cpp
@@ -23,13 +23,14 @@ Revision History:
 #include"ast.h"
 #include"debug.h"
 #include"im_float_config.h"
+#include"rlimit.h"
 
 #define PREC 100000
 
 static void tst_sine_core(std::ostream & out, unsynch_mpq_manager & nm, interval_manager<im_default_config> & im, mpq & a, unsigned k) {
     scoped_mpq lo(nm), hi(nm);
     im.sine(a, k, lo, hi);
-    nm.display(out, lo); 
+    nm.display(out, lo);
     out << " <= Sin["; nm.display(out, a); out << "]\n";
     out << "Sin["; nm.display(out, a); out << "] <= ";
     nm.display(out, hi);
@@ -37,9 +38,10 @@ static void tst_sine_core(std::ostream & out, unsynch_mpq_manager & nm, interval
 }
 
 static void tst_sine(std::ostream & out, unsigned N, unsigned k) {
-    unsynch_mpq_manager                 nm;     
+    unsynch_mpq_manager                 nm;
     im_default_config                   imc(nm);
-    interval_manager<im_default_config> im(imc);
+    reslimit rl;
+    interval_manager<im_default_config> im(rl, imc);
     scoped_mpq a(nm);
     nm.set(a, 0);
     tst_sine_core(out, nm, im, a, 1);
@@ -55,7 +57,7 @@ static void tst_sine(std::ostream & out, unsigned N, unsigned k) {
 static void tst_cosine_core(std::ostream & out, unsynch_mpq_manager & nm, interval_manager<im_default_config> & im, mpq & a, unsigned k) {
     scoped_mpq lo(nm), hi(nm);
     im.cosine(a, k, lo, hi);
-    nm.display(out, lo); 
+    nm.display(out, lo);
     out << " <= Cos["; nm.display(out, a); out << "]\n";
     out << "Cos["; nm.display(out, a); out << "] <= ";
     nm.display(out, hi);
@@ -63,9 +65,10 @@ static void tst_cosine_core(std::ostream & out, unsynch_mpq_manager & nm, interv
 }
 
 static void tst_cosine(std::ostream & out, unsigned N, unsigned k) {
-    unsynch_mpq_manager                 nm;     
+    reslimit rl;
+    unsynch_mpq_manager                 nm;
     im_default_config                   imc(nm);
-    interval_manager<im_default_config> im(imc);
+    interval_manager<im_default_config> im(rl, imc);
     scoped_mpq a(nm);
     nm.set(a, 0);
     tst_cosine_core(out, nm, im, a, 1);
@@ -79,10 +82,10 @@ static void tst_cosine(std::ostream & out, unsigned N, unsigned k) {
 
 
 template<typename fmanager>
-static void tst_float_sine_core(std::ostream & out, 
-                                fmanager & fm, 
-                                interval_manager<im_float_config<fmanager> > & im, 
-                                typename fmanager::numeral & a, 
+static void tst_float_sine_core(std::ostream & out,
+                                fmanager & fm,
+                                interval_manager<im_float_config<fmanager> > & im,
+                                typename fmanager::numeral & a,
                                 unsigned k) {
     _scoped_numeral<fmanager> lo(fm), hi(fm);
     im.sine(a, k, lo, hi);
@@ -95,9 +98,10 @@ const unsigned SBITS = 53;
 
 template<typename fmanager>
 static void tst_float_sine(std::ostream & out, unsigned N, unsigned k) {
+    reslimit rl;
     fmanager                                     fm;
     im_float_config<fmanager>                    ifc(fm, EBITS, SBITS);
-    interval_manager<im_float_config<fmanager> > im(ifc);
+    interval_manager<im_float_config<fmanager> > im(rl, ifc);
     _scoped_numeral<fmanager> a(fm);
     fm.set(a, EBITS, SBITS, static_cast<int>(0));
     tst_float_sine_core(out, fm, im, a, 1);
@@ -130,9 +134,10 @@ static void tst_mpf_bug() {
 #endif
 
 static void tst_e(std::ostream & out) {
-    unsynch_mpq_manager                 nm;     
+    reslimit rl;
+    unsynch_mpq_manager                 nm;
     im_default_config                   imc(nm);
-    interval_manager<im_default_config> im(imc);
+    interval_manager<im_default_config> im(rl, imc);
     im_default_config::interval         r;
     for (unsigned i = 0; i < 64; i++) {
         im.e(i, r);
@@ -144,10 +149,11 @@ static void tst_e(std::ostream & out) {
 
 static void tst_e_float(std::ostream & out) {
     std::cout << "e float...\n";
+    reslimit rl;
     unsynch_mpq_manager   qm;
     mpf_manager           fm;
     im_float_config<mpf_manager>                    ifc(fm);
-    interval_manager<im_float_config<mpf_manager> > im(ifc);
+    interval_manager<im_float_config<mpf_manager> > im(rl, ifc);
     scoped_mpq q(qm);
     im_float_config<mpf_manager>::interval r;
     for (unsigned i = 0; i < 64; i++) {
diff --git a/src/test/upolynomial.cpp b/src/test/upolynomial.cpp
index b38c3af34..e7dcf2719 100644
--- a/src/test/upolynomial.cpp
+++ b/src/test/upolynomial.cpp
@@ -18,11 +18,13 @@ Notes:
 --*/
 #include"upolynomial.h"
 #include"timeit.h"
+#include"rlimit.h"
 
 static void tst1() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
-    upolynomial::manager um(nm);
+    polynomial::manager m(rl, nm);
+    upolynomial::manager um(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
@@ -36,7 +38,7 @@ static void tst1() {
 
     std::cout << "degree(q): " << um.degree(q) << "\n";
 
-    // display coefficients of q 
+    // display coefficients of q
     std::cout << "expanded q: ";
     for (unsigned i = 0; i < q.size(); i++)
         std::cout << nm.to_string(q[i]) << " ";
@@ -50,7 +52,7 @@ static void tst1() {
     // So, if we perform destructive operations on these coefficients, we must execute the "trim" operation
     // before invoking another operation of upolynomial::manager
     um.trim(q);
-    
+
     // q after adding 1 to all coefficients
     std::cout << "new q: "; um.display(std::cout, q); std::cout << "\n";
 
@@ -64,7 +66,8 @@ static void tst1() {
 }
 
 static void tst_isolate_roots(polynomial_ref const & p, unsigned prec, mpbq_manager & bqm, mpbq_vector & roots, mpbq_vector & lowers, mpbq_vector & uppers) {
-    upolynomial::manager um(p.m().m());
+    reslimit rl;
+    upolynomial::manager um(rl, p.m().m());
     upolynomial::scoped_numeral_vector q(um);
     um.to_numeral_vector(p, q);
     std::cout << "isolating roots of: "; um.display(std::cout, q); std::cout << "\n";
@@ -119,7 +122,7 @@ static void tst_isolate_roots(polynomial_ref const & p, unsigned prec, mpbq_mana
                     um.eval_sign_at(q.size(), q.c_ptr(), uppers[i]) == 0 ||
                     um.sign_variations_at(sseq, lowers[i]) - um.sign_variations_at(sseq, uppers[i]) == 1);
             // Fourier sequence may also be used to check if the interval is isolating
-            TRACE("upolynomial", 
+            TRACE("upolynomial",
                   tout << "lowers[i]: " << bqm.to_string(lowers[i]) << "\n";
                   tout << "uppers[i]: " << bqm.to_string(uppers[i]) << "\n";
                   tout << "fourier lower: " << um.sign_variations_at(fseq, lowers[i]) << "\n";
@@ -132,7 +135,7 @@ static void tst_isolate_roots(polynomial_ref const & p, unsigned prec, mpbq_mana
                     // fsv_upper - fsv_upper - num_roots is even
                     // Recall that num_roots == 1 in the interval.
                     (fsv_lower - fsv_upper >= 1 && (fsv_lower - fsv_upper - 1) % 2 == 0));
-            
+
             // Double checking using Descartes bounds for the interval
             // Must use square free component.
             unsigned dab = um.descartes_bound_a_b(q_sqf.size(), q_sqf.c_ptr(), bqm, lowers[i], uppers[i]);
@@ -189,28 +192,29 @@ static void tst_isolate_roots(polynomial_ref const & p, unsigned expected_sz, ra
 }
 
 static void tst_isolate_roots() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
     polynomial_ref p(m);
-    p = (x-1)*(x-2); 
-    { 
+    p = (x-1)*(x-2);
+    {
         rational ex[2] = { rational(1), rational(2) };
         tst_isolate_roots(p, 2, ex);
     }
     p = (x-1)*(x-1)*x*x*x;
-    { 
+    {
         rational ex[2] = { rational(1), rational(0) };
         tst_isolate_roots(p, 2, ex);
     }
     p = (x^5) - x - 1;
-    { 
+    {
         rational ex[1] = { rational(11673039, 10000000) }; // approximated root
         tst_isolate_roots(p, 1, ex);
     }
-    p = (x - 1)*(x + 1)*(x + 2)*(x + 3)*((x - 3)^2);    
+    p = (x - 1)*(x + 1)*(x + 2)*(x + 3)*((x - 3)^2);
     {
         rational ex[5] = { rational(1), rational(-1), rational(-2), rational(-3), rational(3) };
         tst_isolate_roots(p, 5, ex);
@@ -271,19 +275,20 @@ static void tst_isolate_roots() {
         };
         tst_isolate_roots(p, 3, ex, 10);
     }
-    
+
 }
 
 static void tst_remove_one_half() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
     polynomial_ref p(m), r(m);
     p = 4*(x^3) - 12*(x^2) - x + 3;
     r = 16*(x^2) - 40*x - 24;
-    upolynomial::manager um(nm);
+    upolynomial::manager um(rl, nm);
     upolynomial::scoped_numeral_vector _p(um), _q(um), _r(um);
     um.to_numeral_vector(p, _p);
     um.to_numeral_vector(r, _r);
@@ -321,15 +326,16 @@ static void tst_gcd(polynomial_ref const & p, polynomial_ref const & q, pmanager
 
 static void tst_gcd() {
     std::cout << "\n\nTesting GCD\n";
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
     polynomial_ref p(m);
     polynomial_ref q(m);
 
-    upolynomial::manager um(nm);
+    upolynomial::manager um(rl, nm);
 
     p = 13*((x - 3)^6)*((x - 5)^5)*((x - 11)^7);
     q = derivative(p, 0);
@@ -339,7 +345,7 @@ static void tst_gcd() {
 
     p = (x^8) + (x^6) - 3*(x^4) - 3*(x^3) + 8*(x^2) + 2*x - 5;
     q = 3*(x^6) + 5*(x^4) - 4*(x^2) - 9*x + 21;
-    
+
     tst_gcd(p, q, um);
 
     p = ((x - 1)^2)*(x - 3)*(x + 2)*((x - 5)^3);
@@ -351,8 +357,9 @@ static void tst_gcd() {
 
 static void tst_zp() {
     std::cout << "\n\nTesting Z_p\n";
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
@@ -363,20 +370,21 @@ static void tst_zp() {
 
     // Computing GCD of p an q in Z[x]
     std::cout << "GCD in Z[x]\n";
-    upolynomial::manager um(nm);
+    upolynomial::manager um(rl, nm);
     tst_gcd(p, q, um);
 
     // Computing GCD of p an q in Z_3[x]
-    std::cout << "GCD in Z_3[x]\n"; 
-    upolynomial::zp_manager um3(nm);
+    std::cout << "GCD in Z_3[x]\n";
+    upolynomial::zp_manager um3(rl, nm);
     um3.set_zp(3);
     tst_gcd(p, q, um3);
-}    
+}
 
 static void tst_zp2() {
     std::cout << "\n\nTesting Z_p\n";
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
@@ -387,20 +395,21 @@ static void tst_zp2() {
 
     // Computing GCD of p an q in Z[x]
     std::cout << "GCD in Z[x]\n";
-    upolynomial::manager um(nm);
+    upolynomial::manager um(rl, nm);
     tst_gcd(u, v, um);
 
     // Computing GCD of p an q in Z_3[x]
-    std::cout << "GCD in Z_13[x]\n"; 
-    upolynomial::zp_manager um13(nm);
+    std::cout << "GCD in Z_13[x]\n";
+    upolynomial::zp_manager um13(rl, nm);
     um13.set_zp(13);
     tst_gcd(u, v, um13);
-}    
+}
 
 static void tst_ext_gcd() {
     std::cout << "\nExtended GCD\n";
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
@@ -410,8 +419,8 @@ static void tst_ext_gcd() {
     b = (x^8) + (x^6) + 10*(x^4) + 10*(x^3) + 8*(x^2) + 2*x + 8;
 
     // Computing GCD of p an q in Z_3[x]
-    std::cout << "GCD in Z_13[x]\n"; 
-    upolynomial::zp_manager um(nm);
+    std::cout << "GCD in Z_13[x]\n";
+    upolynomial::zp_manager um(rl, nm);
     um.set_zp(13);
     mpzzp_manager & z13 = um.m();
     upolynomial::zp_manager::scoped_numeral_vector A(z13), B(z13), U(z13), V(z13), D(z13);
@@ -423,12 +432,13 @@ static void tst_ext_gcd() {
     std::cout << "U: "; um.display(std::cout, U); std::cout << "\n";
     std::cout << "V: "; um.display(std::cout, V); std::cout << "\n";
     std::cout << "D: "; um.display(std::cout, D); std::cout << "\n";
-}    
+}
 
 static void tst_ext_gcd_z7() {
     std::cout << "\nExtended GCD in Z_7\n";
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
@@ -440,8 +450,8 @@ static void tst_ext_gcd_z7() {
 
     // Computing GCD of a and b in Z_3[x]
     // expecting: D = 1, U = 3*x + 6, V = 3*x^2 + 6*x + 4
-    std::cout << "GCD in Z_7[x]\n"; 
-    upolynomial::zp_manager um(nm);
+    std::cout << "GCD in Z_7[x]\n";
+    upolynomial::zp_manager um(rl, nm);
     um.set_zp(7);
     mpzzp_manager & z7 = um.m();
     upolynomial::zp_manager::scoped_numeral_vector A(z7), B(z7), U(z7), V(z7), D(z7);
@@ -453,12 +463,13 @@ static void tst_ext_gcd_z7() {
     std::cout << "U: "; um.display(std::cout, U); std::cout << "\n";
     std::cout << "V: "; um.display(std::cout, V); std::cout << "\n";
     std::cout << "D: "; um.display(std::cout, D); std::cout << "\n";
-}    
+}
 
 static void tst_sturm() {
     std::cout << "\nSturm Seq\n";
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
@@ -467,7 +478,7 @@ static void tst_sturm() {
     // p = ((x^17) + 5*(x^16) + 3*(x^15) + 10*(x^13) + 13*(x^10) + (x^9) + 8*(x^5) + 3*(x^2) + 7)*(((x^5) - x - 1)^2)*(((x^3) - 2)^2);
     // p = ((x^17) + 5*(x^16) + 3*(x^15) + 10*(x^13) + 13*(x^10) + (x^9) + 8*(x^5) + 3*(x^2) + 7)*(((x^5) - x - 1))*(((x^3) - 2));
 
-    upolynomial::manager um(nm);
+    upolynomial::manager um(rl, nm);
     upolynomial::scoped_numeral_vector _p(um);
     upolynomial::scoped_upolynomial_sequence seq2(um);
     um.to_numeral_vector(p, _p);
@@ -478,7 +489,8 @@ static void tst_sturm() {
 
 
 static void tst_refinable(polynomial_ref const & p, mpbq_manager & bqm, mpbq & a, mpbq & b) {
-    upolynomial::manager um(p.m().m());
+    reslimit rl;
+    upolynomial::manager um(rl, p.m().m());
     upolynomial::scoped_numeral_vector _p(um);
     um.to_numeral_vector(p, _p);
     std::cout << "before (" << bqm.to_string(a) << ", " << bqm.to_string(b) << ")\n";
@@ -497,8 +509,9 @@ static void tst_refinable(polynomial_ref const & p, mpbq_manager & bqm, mpbq & a
 
 static void tst_refinable() {
     std::cout << "\nRefinable intervals\n";
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
@@ -539,12 +552,12 @@ static void tst_refinable() {
     bqm.set(a, 1);
     bqm.set(b, 3);
     tst_refinable(p, bqm, a, b);
-    
+
     bqm.del(a); bqm.del(b);
 }
 
 static void tst_refine(polynomial_ref const & p, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k=100) {
-    upolynomial::manager um(p.m().m());
+    reslimit rl; upolynomial::manager um(rl, p.m().m());
     upolynomial::scoped_numeral_vector _p(um);
     um.to_numeral_vector(p, _p);
     std::cout << "before (" << bqm.to_string(a) << ", " << bqm.to_string(b) << ")\n";
@@ -561,8 +574,9 @@ static void tst_refine(polynomial_ref const & p, mpbq_manager & bqm, mpbq & a, m
 
 static void tst_refine() {
     std::cout << "\nRefining intervals\n";
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
@@ -574,7 +588,7 @@ static void tst_refine() {
     a = 1;
     b = 2;
     tst_refine(p, bqm, a, b, 20);
-    
+
     p = (x^2) - 2;
     std::cout << "p: " << p << "\n";
     a = 1;
@@ -583,14 +597,15 @@ static void tst_refine() {
 }
 
 static void tst_translate_q() {
+    reslimit rl;
     unsynch_mpq_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
     polynomial_ref p(m);
     p = (x-1)*(x-2)*(x-3)*(x-4);
-    upolynomial::manager um(nm);
+    upolynomial::manager um(rl, nm);
     upolynomial::scoped_numeral_vector _p(um), _q(um);
     um.to_numeral_vector(p, _p);
     SASSERT(um.eval_sign_at(_p.size(), _p.c_ptr(), mpq(1)) == 0);
@@ -637,7 +652,8 @@ static void tst_translate_q() {
 }
 
 static void tst_convert_q2bq(unsynch_mpq_manager & m, polynomial_ref const & p, mpq const & a, mpq const & b) {
-    upolynomial::manager um(m);
+    reslimit rl;
+    upolynomial::manager um(rl, m);
     upolynomial::scoped_numeral_vector _p(um);
     um.to_numeral_vector(p, _p);
     std::cout << "\np: ";
@@ -657,8 +673,9 @@ static void tst_convert_q2bq(unsynch_mpq_manager & m, polynomial_ref const & p,
 }
 
 static void tst_convert_q2bq() {
+    reslimit rl;
     unsynch_mpq_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
@@ -704,8 +721,9 @@ static void tst_convert_q2bq() {
 }
 
 static void tst_sturm2() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
@@ -715,7 +733,7 @@ static void tst_sturm2() {
     p = (x^16) - 136*(x^14) + 6476*(x^12) - 141912*(x^10) + 1513334*(x^8) - 7453176*(x^6) + 13950764*(x^4) - 5596840*(x^2) + 46225;
     q = ((x^8) - 40*(x^6) + 352*(x^4) - 960*(x^2) + 576)^2;
 
-    upolynomial::manager um(nm);
+    upolynomial::manager um(rl, nm);
     upolynomial::scoped_numeral_vector _p(um), _q(um);
     upolynomial::scoped_upolynomial_sequence seq2(um);
     um.to_numeral_vector(p, _p);
@@ -735,7 +753,7 @@ static void tst_isolate_roots2() {
     // create univariate polynomial using multivariate polynomial package
     polynomial_ref p(m);
     p = (2*x - 1)*(x - 21)*(x + 12)*(x - 19)*(x + 11)*(x + 34)*(x - 9)*(x - 72)*(10000*x - 4999)*((x^5) - x - 1)*((x^2) - 2)*((x^2) - 3)*((x^7) - 3)*((x^101) - 3);
-    { 
+    {
         tst_isolate_roots(p, 10);
     }
 }
@@ -769,7 +787,7 @@ static void tst_isolate_roots3() {
     q = (x - x1 - x2 - x3 - x4 - x5 - x6);
     r = resultant(resultant(resultant(resultant(resultant(resultant(q, p1, 1), p2, 2), p3, 3), p4, 4), p5, 5), p6, 6);
     std::cout << "r: " << r << "\n";
-    { 
+    {
         timeit timer(true, "isolate");
         tst_isolate_roots(r, 10);
     }
@@ -784,7 +802,7 @@ static void tst_gcd2() {
     polynomial_ref p(m);
     p = ((x^1000) - x + 1)^5;
 
-    upolynomial::manager um(nm);
+    reslimit rl; upolynomial::manager um(rl, nm);
     upolynomial::scoped_numeral_vector _p(um);
     upolynomial::scoped_numeral_vector _p_sqf(um);
     um.to_numeral_vector(p, _p);
@@ -794,24 +812,26 @@ static void tst_gcd2() {
     }
     um.display(std::cout, _p_sqf.size(), _p_sqf.c_ptr()); std::cout << "\n";
 }
-#endif 
+#endif
 
 static void tst_isolate_roots5() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
     polynomial_ref p(m);
     p = (x^70) - 6*(x^65) - (x^60) + 60*(x^55) - 54*(x^50) - 230*(x^45) + 274*(x^40) + 542*(x^35) - 615*(x^30)
         - 1120*(x^25) + 1500*(x^20) - 160*(x^15) - 395*(x^10) + 76*(x^5) + 34;
-    { 
+    {
         tst_isolate_roots(p, 10);
     }
 }
 
 static void tst_exact_div(polynomial_ref const & p1, polynomial_ref const & p2, bool expected, polynomial_ref const & expected_q) {
-    upolynomial::manager um(p1.m().m());
+    reslimit rl;
+    upolynomial::manager um(rl, p1.m().m());
     upolynomial::scoped_numeral_vector _p1(um), _p2(um), _q(um), _r(um);
     um.to_numeral_vector(p1, _p1);
     um.to_numeral_vector(p2, _p2);
@@ -834,8 +854,9 @@ static void tst_exact_div(polynomial_ref const & p1, polynomial_ref const & p2,
 }
 
 static void tst_exact_div() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m);
     x = m.mk_polynomial(m.mk_var());
     // create univariate polynomial using multivariate polynomial package
@@ -860,7 +881,7 @@ static void tst_fact(polynomial_ref const & p, unsigned num_distinct_factors, up
     SASSERT(is_univariate(p));
     std::cout << "---------------\n";
     std::cout << "p: " << p << std::endl;
-    upolynomial::manager um(p.m().m());
+    reslimit rl; upolynomial::manager um(rl, p.m().m());
     upolynomial::scoped_numeral_vector _p(um);
     upolynomial::factors fs(um);
     um.to_numeral_vector(p, _p);
@@ -878,8 +899,9 @@ static void tst_fact(polynomial_ref const & p, unsigned num_distinct_factors, up
 }
 
 static void tst_fact() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m);
     x0 = m.mk_polynomial(m.mk_var());
     tst_fact((x0^4) + (x0^2) - 20, 3);
@@ -899,7 +921,7 @@ static void tst_fact() {
     tst_fact((x0^70) - 6*(x0^65) - (x0^60) + 60*(x0^55) - 54*(x0^50) - 230*(x0^45) + 274*(x0^40) + 542*(x0^35) - 615*(x0^30) - 1120*(x0^25) + 1500*(x0^20) - 160*(x0^15) - 395*(x0^10) + 76*(x0^5) + 34, 3);
     tst_fact(((x0^4) - 8*(x0^2)), 2);
     tst_fact((x0^5) - 2*(x0^3) + x0 - 1, 1);
-    tst_fact( (x0^25) - 4*(x0^21) - 5*(x0^20) + 6*(x0^17) + 11*(x0^16) + 10*(x0^15) - 4*(x0^13) - 7*(x0^12) - 9*(x0^11) - 10*(x0^10) + 
+    tst_fact( (x0^25) - 4*(x0^21) - 5*(x0^20) + 6*(x0^17) + 11*(x0^16) + 10*(x0^15) - 4*(x0^13) - 7*(x0^12) - 9*(x0^11) - 10*(x0^10) +
                (x0^9) + (x0^8) + (x0^7) + (x0^6) + 3*(x0^5) + x0 - 1, 2);
     tst_fact( (x0^25) - 10*(x0^21) - 10*(x0^20) - 95*(x0^17) - 470*(x0^16) - 585*(x0^15) - 40*(x0^13) - 1280*(x0^12) - 4190*(x0^11) - 3830*(x0^10) + 400*(x0^9)+ 1760*(x0^8) + 760*(x0^7) - 2280*(x0^6) + 449*(x0^5) + 640*(x0^3) - 640*(x0^2) + 240*x0 - 32, 2);
     tst_fact( x0^10, 1);
@@ -919,7 +941,7 @@ static void tst_fact() {
     tst_fact( (x0^50) - 10*(x0^40) + 38*(x0^30) - 2*(x0^25) - 100*(x0^20) - 40*(x0^15) + 121*(x0^10) - 38*(x0^5) - 17, 1);
 
     tst_fact(        (((x0^5)  +  5*(x0^4) +  10*(x0^3) + 10*(x0^2) + 5*x0)^10)
-                 + 10*(((x0^5)  +  5*(x0^4) +  10*(x0^3) + 10*(x0^2) + 5*x0)^9) 
+                 + 10*(((x0^5)  +  5*(x0^4) +  10*(x0^3) + 10*(x0^2) + 5*x0)^9)
                  + 35*(((x0^5)  +  5*(x0^4) +  10*(x0^3) + 10*(x0^2) + 5*x0)^8)
                  + 40*(((x0^5)  +  5*(x0^4) +  10*(x0^3) + 10*(x0^2) + 5*x0)^7)
                  - 32*(((x0^5)  +  5*(x0^4) +  10*(x0^3) + 10*(x0^2) + 5*x0)^6)
@@ -934,37 +956,37 @@ static void tst_fact() {
     tst_fact( ((x0^5) - 15552)*
               ((x0^20)- 15708*(x0^15) + rational("138771724")*(x0^10)- rational("432104148432")*(x0^5) + rational("614198284585616")),
               2);
-    tst_fact( (x0^25) - 
-              rational("3125")*(x0^21) - 
-              rational("15630")*(x0^20) + 
-              rational("3888750")*(x0^17) + 
-              rational("38684375")*(x0^16) + 
-              rational("95765635")*(x0^15) - 
-              rational("2489846500")*(x0^13) - 
-              rational("37650481875")*(x0^12) - 
-              rational("190548065625")*(x0^11) - 
-              rational("323785250010")*(x0^10) + 
-              rational("750249453025")*(x0^9) + 
-              rational("14962295699875")*(x0^8) + 
-              rational("111775113235000")*(x0^7) + 
-              rational("370399286731250")*(x0^6) + 
-              rational("362903064503129")*(x0^5) - 
-              rational("2387239013984400")*(x0^4) - 
-              rational("23872390139844000")*(x0^3) - 
-              rational("119361950699220000")*(x0^2) - 
-              rational("298404876748050000")*x0 - 
+    tst_fact( (x0^25) -
+              rational("3125")*(x0^21) -
+              rational("15630")*(x0^20) +
+              rational("3888750")*(x0^17) +
+              rational("38684375")*(x0^16) +
+              rational("95765635")*(x0^15) -
+              rational("2489846500")*(x0^13) -
+              rational("37650481875")*(x0^12) -
+              rational("190548065625")*(x0^11) -
+              rational("323785250010")*(x0^10) +
+              rational("750249453025")*(x0^9) +
+              rational("14962295699875")*(x0^8) +
+              rational("111775113235000")*(x0^7) +
+              rational("370399286731250")*(x0^6) +
+              rational("362903064503129")*(x0^5) -
+              rational("2387239013984400")*(x0^4) -
+              rational("23872390139844000")*(x0^3) -
+              rational("119361950699220000")*(x0^2) -
+              rational("298404876748050000")*x0 -
               rational("298500366308609376"), 2);
 
     tst_fact( rational("54")*(x0^24) - (x0^27) - 324*(x0^21) + rational("17496")*(x0^18) - 34992*(x0^15)+ rational("1889568")*(x0^12)- 1259712*(x0^9) + rational("68024448")*(x0^6), 3);
 
     tst_fact( ((x0^3)- 432)*(((x0^3)+54)^2)*((x0^6)+108)*((x0^6)+6912)*((x0^6)- 324*(x0^3)+37044),
                5);
-    
+
     tst_fact( ((x0^6)- 6*(x0^4) - 864*(x0^3) + 12*(x0^2) - 5184*x0 + 186616)*
               (((x0^6) - 6*(x0^4) + 108*(x0^3) + 12*(x0^2) + 648*x0 + 2908)^2)*
               ((x0^12) - 12*(x0^10) + 60*(x0^8) + 56*(x0^6) + 6720*(x0^4) + 12768*(x0^2) + 13456)*
               ((x0^12) - 12*(x0^10) + 60*(x0^8) + 13664*(x0^6) + 414960*(x0^4) + 829248*(x0^2) + 47886400)*
-              ((x0^12) - 12*(x0^10) - 648*(x0^9)+ 60*(x0^8) + 178904*(x0^6) + 15552*(x0^5) + 1593024*(x0^4) - 24045984*(x0^3) + 
+              ((x0^12) - 12*(x0^10) - 648*(x0^9)+ 60*(x0^8) + 178904*(x0^6) + 15552*(x0^5) + 1593024*(x0^4) - 24045984*(x0^3) +
                5704800*(x0^2) - 143995968*x0 + 1372010896),
               5);
 }
@@ -975,7 +997,7 @@ static void tst_rem(polynomial_ref const & p, polynomial_ref const & q, polynomi
     std::cout << "---------------\n";
     std::cout << "p: " << p << std::endl;
     std::cout << "q: " << q << std::endl;
-    upolynomial::manager um(p.m().m());
+    reslimit rl; upolynomial::manager um(rl, p.m().m());
     upolynomial::scoped_numeral_vector _p(um), _q(um), _r(um);
     um.to_numeral_vector(p, _p);
     um.to_numeral_vector(q, _q);
@@ -987,8 +1009,9 @@ static void tst_rem(polynomial_ref const & p, polynomial_ref const & q, polynomi
 }
 
 static void tst_rem() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x0(m), zero(m), one(m);
     x0 = m.mk_polynomial(m.mk_var());
     zero = m.mk_zero();
@@ -1002,7 +1025,7 @@ static void tst_lower_bound(polynomial_ref const & p) {
     SASSERT(is_univariate(p));
     std::cout << "---------------\n";
     std::cout << "p: " << p << std::endl;
-    upolynomial::manager um(p.m().m());
+    reslimit rl; upolynomial::manager um(rl, p.m().m());
     upolynomial::scoped_numeral_vector _p(um);
     um.to_numeral_vector(p, _p);
     std::cout << "_p: "; um.display(std::cout, _p); std::cout << "\n";
@@ -1012,8 +1035,9 @@ static void tst_lower_bound(polynomial_ref const & p) {
 }
 
 static void tst_lower_bound() {
+    reslimit rl;
     polynomial::numeral_manager nm;
-    polynomial::manager m(nm);
+    polynomial::manager m(rl, nm);
     polynomial_ref x(m), zero(m), one(m);
     x = m.mk_polynomial(m.mk_var());
     zero = m.mk_zero();
@@ -1031,7 +1055,7 @@ static void tst_lower_bound() {
     tst_lower_bound(((x^17) + 5*(x^16) + 3*(x^15) + 10*(x^13) + 13*(x^10) + (x^9) + 8*(x^5) + 3*(x^2) + 7)*(((x^5) - x - 1)^2)*(((x^3) - 2)^2));
     tst_lower_bound((((x^5) - 1000000000)^3)*((3*x - 10000000)^2)*((10*x - 632)^2));
 }
-    
+
 void tst_upolynomial() {
     set_verbosity_level(1000);
     enable_trace("mpz_gcd");