diff --git a/src/smt/theory_arith.h b/src/smt/theory_arith.h
index 9a4c21ee6..3c7fe26be 100644
--- a/src/smt/theory_arith.h
+++ b/src/smt/theory_arith.h
@@ -1040,6 +1040,7 @@ namespace smt {
         enum gb_result { GB_PROGRESS, GB_NEW_EQ, GB_FAIL };
         gb_result compute_grobner(svector<theory_var> const & nl_cluster);
         bool compute_basis_loop(grobner & gb);
+        void compute_basis(grobner&, bool&);
         void update_statistics(grobner&);
         void set_gb_exhausted();
         bool pass_over_gb_eqs_for_conflict(ptr_vector<grobner::equation>& eqs, grobner&);
diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h
index 1f055c305..2c42bcc33 100644
--- a/src/smt/theory_arith_nl.h
+++ b/src/smt/theory_arith_nl.h
@@ -2317,7 +2317,14 @@ bool theory_arith<Ext>::compute_basis_loop(grobner & gb) {
     }
     return false;
 }
-
+template<typename Ext>
+void theory_arith<Ext>::compute_basis(grobner& gb, bool& warn) {
+    gb.compute_basis_init();        
+    if (!compute_basis_loop(gb) && !warn) {
+        set_gb_exhausted();
+        warn = true;
+    }
+}
 /**
    \brief Compute Grobner basis, return true if a conflict or new fixed variables were detected.
 */
@@ -2334,16 +2341,11 @@ typename theory_arith<Ext>::gb_result theory_arith<Ext>::compute_grobner(svector
 
     do {
         TRACE("non_linear_gb", tout << "before:\n"; gb.display(tout););
-        gb.compute_basis_init();        
-        if (!compute_basis_loop(gb) && !warn) {
-            set_gb_exhausted();
-            warn = true;
-        }
+        compute_basis(gb, warn);
         update_statistics(gb);
-        if (get_context().get_cancel_flag()) {
-            return GB_FAIL;
-        }
         TRACE("non_linear_gb", tout << "after:\n"; gb.display(tout););
+        if (get_context().get_cancel_flag())
+            return GB_FAIL;
         if (pass_over_gb_eqs_for_conflict(eqs, gb))
             return GB_PROGRESS;
     }