diff --git a/src/math/lp/int_gcd_test.cpp b/src/math/lp/int_gcd_test.cpp
index b5b4b9547..55dedf151 100644
--- a/src/math/lp/int_gcd_test.cpp
+++ b/src/math/lp/int_gcd_test.cpp
@@ -278,16 +278,16 @@ namespace lp {
         if (modulus == 0)
             return true;
         SASSERT(modulus.is_int());
-        mpq parity = m_consts / m_least_coeff;
-        if (!parity.is_int())
+        mpq offset = m_consts / m_least_coeff;
+        if (!offset.is_int())
             return true;
-        parity = mod(parity, modulus);
-        if (!least_sign && parity != 0)
-            parity = modulus - parity;
-        TRACE("gcd_test", tout << least_idx << " modulus: " << modulus << " consts: " << m_consts << " sign " << least_sign << " parity: " << parity << "\n";);
+        offset = mod(offset, modulus);
+        if (!least_sign && offset != 0)
+            offset = modulus - offset;
+        TRACE("gcd_test", tout << least_idx << " modulus: " << modulus << " consts: " << m_consts << " sign " << least_sign << " offset: " << offset << "\n";);
 
-        SASSERT(0 <= parity && parity < modulus);
-        return insert_parity(least_idx, row, parity, modulus);
+        SASSERT(0 <= offset && offset < modulus);
+        return insert_parity(least_idx, row, offset, modulus);
     }
 
     void int_gcd_test::reset_test() {
@@ -306,7 +306,11 @@ namespace lp {
 
         // incomplete parity check.
         for (auto const& p : m_parities[j]) {            
-            if (p.m_modulo == modulo && offset != p.m_parity) {
+            if (p.m_modulo != modulo)
+                continue;
+            if (p.m_offset == offset) 
+                return true;
+            else {
                 fill_explanation_from_fixed_columns(r);
                 fill_explanation_from_fixed_columns(*p.m_row);
                 return false;
diff --git a/src/math/lp/int_gcd_test.h b/src/math/lp/int_gcd_test.h
index 7aa4a1151..28ac2f7b3 100644
--- a/src/math/lp/int_gcd_test.h
+++ b/src/math/lp/int_gcd_test.h
@@ -34,11 +34,11 @@ namespace lp {
     class int_gcd_test {
 
         struct parity {
-            mpq m_parity;
+            mpq m_offset;
             mpq m_modulo;
             const row_strip<mpq>* m_row = nullptr;
             parity(mpq const& p, mpq const& m, row_strip<mpq> const& r):
-                m_parity(p),
+                m_offset(p),
                 m_modulo(m),
                 m_row(&r)
             {}