diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp
index a078b9af0..158a55d02 100644
--- a/src/sat/smt/xor_gaussian.cpp
+++ b/src/sat/smt/xor_gaussian.cpp
@@ -763,6 +763,19 @@ inline void EGaussian::update_cols_vals_set(literal lit) {
 // In case the argument is false it only updates the recently added variables. If true, it recalculates all
 void EGaussian::update_cols_vals_set(bool force) {
     SASSERT(initialized);
+    
+    auto output_rows = [this]() {
+        std::cout << "Col-Unassigned: ";
+        for (int i = 0; i < 64 * m_cols_unset->size; ++i) {
+            std::cout << (*m_cols_unset)[i];
+        }
+        std::cout << "\n";
+        std::cout << "Col-Values:     ";
+        for (int i = 0; i < 64 * m_cols_vals->size; ++i) {
+            std::cout << (*m_cols_vals)[i];
+        }
+        std::cout << std::endl;
+    };
 
     if (recalculate_values || force) {
         m_cols_vals->setZero();
@@ -779,6 +792,7 @@ void EGaussian::update_cols_vals_set(bool force) {
         last_val_update = m_solver.s().trail_size();
         recalculate_values = false;
         TRACE("xor", tout << "last val update set to " << last_val_update << "\n");         
+        output_rows();
         return;
     }
 
@@ -797,17 +811,7 @@ void EGaussian::update_cols_vals_set(bool force) {
         }
     }
     last_val_update = m_solver.s().trail_size();
-
-    std::cout << "Col-Unassigned: ";
-    for (int i = 0; i < 64 * m_cols_unset->size; ++i) {
-        std::cout << (*m_cols_unset)[i];
-    }
-    std::cout << "\n";
-    std::cout << "Col-Values:     ";
-    for (int i = 0; i < 64 * m_cols_vals->size; ++i) {
-        std::cout << (*m_cols_vals)[i];
-    }
-    std::cout << std::endl;
+    output_rows();
 }
 
 void EGaussian::prop_lit(const gauss_data& gqd, unsigned row_i, literal ret_lit_prop) {
diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp
index 3b09c9edb..0a46a99ad 100644
--- a/src/sat/smt/xor_solver.cpp
+++ b/src/sat/smt/xor_solver.cpp
@@ -280,13 +280,13 @@ namespace xr {
         }
         m_justifications_lim.shrink(old_sz);
         m_justifications.shrink(old_sz);*/
+        
+        check_need_gauss_jordan_disable(); // Do this before enforcing recalcultion!
 
         for (unsigned i = 0; i < m_gmatrices.size(); i++)
             if (m_gmatrices[i] && !m_gqueuedata[i].disabled)
                 m_gmatrices[i]->enforce_recalculate();
         
-        check_need_gauss_jordan_disable();
-        
         if (m_region)
             m_region->pop_scope(num_scopes);
     }
@@ -408,7 +408,7 @@ namespace xr {
         }
     }
     
-    // disables matrixes if applicable
+    // disables matrices if applicable
     void solver::check_need_gauss_jordan_disable() {
         for (unsigned i = 0; i < m_gqueuedata.size(); i++) {
             auto& gqd = m_gqueuedata[i];
@@ -423,7 +423,7 @@ namespace xr {
             }*/
     
             gqd.reset();
-            m_gmatrices[i]->update_cols_vals_set(false);
+            m_gmatrices[i]->update_cols_vals_set(false); // TODO: Probably we don't need this as we reset it anyway afterwards everywhere we call this function. Remove?
         }
     }