diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp
index cb73c6b38..4666ea101 100644
--- a/src/sat/smt/xor_gaussian.cpp
+++ b/src/sat/smt/xor_gaussian.cpp
@@ -606,10 +606,10 @@ bool EGaussian::find_truths(
     // printf("dd Watch variable : %d  ,  Wathch row num %d    n", p , row_n);
 
     TRACE("xor", tout 
-        << "mat[" << matrix_no << "] find_truths\n"
-        << "-> row: " << row_n << "\n"
-        << "-> var: " << var+1 << "\n"
-        << "-> dec lev:" << m_solver.s().scope_lvl());
+          << "mat[" << matrix_no << "] find_truths\n"
+          << "-> row: " << row_n << "\n"
+          << "-> var: " << var+1 << "\n"
+          << "-> dec lev:" << m_solver.s().scope_lvl() << "\n");
     SASSERT(row_n < m_num_rows);
     SASSERT(satisfied_xors.size() > row_n);
 
@@ -654,7 +654,7 @@ bool EGaussian::find_truths(
             xor_reasons[row_n].m_propagated = sat::null_literal;
             gqd.conflict = m_solver.mk_justification(m_solver.s().scope_lvl(), matrix_no, row_n);
             gqd.status = gauss_res::confl;
-            TRACE("xor", tout << "--> conflict";);
+            TRACE("xor", tout << "--> conflict\n");
             
             if (was_resp_var) { // recover
                 var_has_resp_row[row_to_var_non_resp[row_n]] = false;
@@ -776,9 +776,11 @@ void EGaussian::update_cols_vals_set(bool force) {
         }
         last_val_update = m_solver.s().trail_size();
         cancelled_since_val_update = false;
+        TRACE("xor", tout << "last val update set to " << last_val_update << "\n");         
         return;
     }
 
+    TRACE("xor", tout << last_val_update << " " << m_solver.s().trail_size() << "\n");
     SASSERT(m_solver.s().trail_size() >= last_val_update);
     for (unsigned i = last_val_update; i < m_solver.s().trail_size(); i++) {
         bool_var var = m_solver.s().trail_literal(i).var();
diff --git a/src/sat/smt/xor_gaussian.h b/src/sat/smt/xor_gaussian.h
index 358b89fa7..7db7478e4 100644
--- a/src/sat/smt/xor_gaussian.h
+++ b/src/sat/smt/xor_gaussian.h
@@ -587,7 +587,7 @@ namespace xr {
         );
         void canceling();
         bool full_init(bool& created);
-        void update_cols_vals_set(bool force = false);
+        void update_cols_vals_set(bool force);
         bool must_disable(gauss_data& gqd);
         void check_invariants();
         void update_matrix_no(unsigned n);
diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp
index 06b601073..26f42d75d 100644
--- a/src/sat/smt/xor_solver.cpp
+++ b/src/sat/smt/xor_solver.cpp
@@ -139,7 +139,7 @@ namespace xr {
         force_push();
         for (; m_prop_queue_head < m_prop_queue.size() && !s().inconsistent(); ++m_prop_queue_head) {
             literal p = m_prop_queue[m_prop_queue_head];
-            std::cout << "Propagating: " << p.var() << " = " << !p.sign() << std::endl;
+            std::cout << "Propagating: " << p.var() << " := " << !p.sign() << std::endl;
             SASSERT(s().lvl(p) == s().scope_lvl());
             sat::justification conflict = gauss_jordan_elim(p);
             if (!conflict.is_none()) {
@@ -158,7 +158,7 @@ namespace xr {
         for (unsigned i = 0; i < m_gqueuedata.size(); i++) {
             if (m_gqueuedata[i].disabled || !m_gmatrices[i]->is_initialized()) continue;
             m_gqueuedata[i].reset();
-            m_gmatrices[i]->update_cols_vals_set();
+            m_gmatrices[i]->update_cols_vals_set(false);
         }
         
         bool confl_in_gauss = false;