diff --git a/src/ast/rewriter/poly_rewriter.h b/src/ast/rewriter/poly_rewriter.h
index 85ce5fcf8..5f263ce1d 100644
--- a/src/ast/rewriter/poly_rewriter.h
+++ b/src/ast/rewriter/poly_rewriter.h
@@ -65,7 +65,7 @@ protected:
 
     void set_curr_sort(sort * s) { m_curr_sort = s; }
 
-    expr * const * get_monomials(expr * & t, unsigned & sz) {
+    expr * const * get_monomials(expr * & t, unsigned & sz) const {
         if (is_add(t)) {
             sz = to_app(t)->get_num_args();
             return to_app(t)->get_args();
@@ -86,7 +86,7 @@ protected:
     bool hoist_multiplication(expr_ref& som);
     expr* merge_muls(expr* x, expr* y);
 
-    bool is_mul(expr * t, numeral & c, expr * & pp);
+    bool is_mul(expr * t, numeral & c, expr * & pp) const;
 
     class mon_lt {
         poly_rewriter& rw;
@@ -124,6 +124,8 @@ public:
     bool is_var_plus_ground(expr * n, bool & inv, var * & v, expr_ref & t);
     bool is_zero(expr* e) const;
 
+    bool gcd_test(expr* lhs, expr* rhs) const;
+
 
     br_status mk_mul_core(unsigned num_args, expr * const * args, expr_ref & result) {
         SASSERT(num_args > 0);
diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h
index b7ff3d1b6..60ec53f88 100644
--- a/src/ast/rewriter/poly_rewriter_def.h
+++ b/src/ast/rewriter/poly_rewriter_def.h
@@ -445,7 +445,7 @@ inline expr * poly_rewriter<Config>::get_power_product(expr * t, numeral & a) {
 }
 
 template<typename Config>
-bool poly_rewriter<Config>::is_mul(expr * t, numeral & c, expr * & pp) {
+bool poly_rewriter<Config>::is_mul(expr * t, numeral & c, expr * & pp) const {
     if (!is_mul(t) || to_app(t)->get_num_args() != 2)
         return false;
     if (!is_numeral(to_app(t)->get_arg(0), c))
@@ -454,6 +454,42 @@ bool poly_rewriter<Config>::is_mul(expr * t, numeral & c, expr * & pp) {
     return true;
 }
 
+template<typename Config>
+bool poly_rewriter<Config>::gcd_test(expr* lhs, expr* rhs) const {
+    numeral g(0), offset(0), c;
+    expr* t = nullptr;
+    unsigned sz = 0; 
+    expr* const* args = get_monomials(lhs, sz);
+    auto test = [&](bool side, expr* e) {
+        if (is_numeral(e, c)) {
+            if (!c.is_int())
+                return false;
+            if (side)                
+                offset += c;
+            else
+                offset -= c;
+            return true;
+        }
+        else if (is_mul(e, c, t)) {
+            if (!c.is_int() || c.is_zero())
+                return false;
+            g = gcd(abs(c), g);
+            return !g.is_one();
+        }
+        return false;
+    };
+    for (unsigned i = 0; i < sz; ++i) 
+        if (!test(true, args[i]))
+            return true;        
+    args = get_monomials(rhs, sz);
+    for (unsigned i = 0; i < sz; ++i) 
+        if (!test(false, args[i]))
+            return true;
+    if (!offset.is_zero() && !g.is_zero() && !divides(g, offset))
+        return false;
+    return true;
+}
+
 
 template<typename Config>
 bool poly_rewriter<Config>::mon_lt::operator()(expr* e1, expr * e2) const {
diff --git a/src/util/rational.h b/src/util/rational.h
index c4f96c3c5..e0a76d9ee 100644
--- a/src/util/rational.h
+++ b/src/util/rational.h
@@ -387,8 +387,11 @@ public:
     }
 
     friend inline std::ostream & operator<<(std::ostream & target, rational const & r) {
-        target << m().to_string(r.m_val);
-        return target;
+        return target << m().to_string(r.m_val);
+    }
+
+    friend inline bool divides(rational const& a, rational const& b) {
+        return m().divides(a.to_mpq(), b.to_mpq());
     }
 
     friend inline rational gcd(rational const & r1, rational const & r2);