diff --git a/src/sat/smt/xor_matrix_finder.cpp b/src/sat/smt/xor_matrix_finder.cpp
index d8f81a09d..2c1c3a14e 100644
--- a/src/sat/smt/xor_matrix_finder.cpp
+++ b/src/sat/smt/xor_matrix_finder.cpp
@@ -63,7 +63,7 @@ namespace xr {
     
         finder.move_xors_without_connecting_vars_to_unused();
         finder.clean_equivalent_xors(m_solver->xorclauses);
-        for(const auto& x: m_xor.xorclauses_unused)
+        for (const auto& x: m_xor.xorclauses_unused)
             clash_vars_unused.insert(x.clash_vars.begin(), x.clash_vars.end());
     
         if (m_xor.xorclauses.size() < m_sat.get_config().m_min_gauss_xor_clauses) {
@@ -73,9 +73,9 @@ namespace xr {
     
         //Just one giant matrix.
         // if (m_sat.get_config().m_xor_gauss_do_matrix_find)
-        if (!m_solver->conf.gaussconf.doMatrixFind) {
-            m_solver->gmatrices.push_back(new EGaussian(m_solver, 0, m_solver->xorclauses));
-            m_solver->gqueuedata.resize(m_solver->gmatrices.size());
+        if (!m_sat.get_config().m_xor_doMatrixFind) {
+            m_xor.gmatrices.push_back(new EGaussian(m_xor, 0, m_xor.xorclauses));
+            m_xor.gqueuedata.resize(m_xor.gmatrices.size());
             return true;
         }
     
diff --git a/src/sat/smt/xor_solver.h b/src/sat/smt/xor_solver.h
index c06ea0e52..91935ab61 100644
--- a/src/sat/smt/xor_solver.h
+++ b/src/sat/smt/xor_solver.h
@@ -20,7 +20,7 @@ namespace xr {
 
     class constraint {
         unsigned        m_size;
-        bool            m_detached;
+        bool            m_detached = false;
         size_t          m_obj_size;
         bool            m_rhs;
         sat::bool_var   m_vars[0];
@@ -28,7 +28,7 @@ namespace xr {
     public:
         static size_t get_obj_size(unsigned num_lits) { return sat::constraint_base::obj_size(sizeof(constraint) + num_lits * sizeof(sat::bool_var)); }
         
-        constraint(const svector<sat::bool_var>& ids, bool expected_result) : m_size(ids.size()), m_detached(false), m_obj_size(get_obj_size(ids.size())), m_rhs(expected_result) {
+        constraint(const svector<sat::bool_var>& ids, bool expected_result) : m_size(ids.size()), m_obj_size(get_obj_size(ids.size())), m_rhs(expected_result) {
             unsigned i = 0;
             for (auto v : ids)
                 m_vars[i++] = v;