diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp
index 91e29b6d7..189ab1d2b 100644
--- a/src/sat/smt/xor_gaussian.cpp
+++ b/src/sat/smt/xor_gaussian.cpp
@@ -98,11 +98,12 @@ gret PackedRow::propGause(
     PackedRow& tmp_col2,
     PackedRow& cols_vals,
     PackedRow& cols_unset,
-    sat::literal& ret_lit_prop) {
+    literal& ret_lit_prop) {
     
     unsigned pop = tmp_col.set_and_until_popcnt_atleast2(*this, cols_unset);
     
-    //Find new watch
+    // There are still at least 2 unassigned elements in the matrix row
+    // Find new watch ==> a variable not yet having a row responsible for it
     if (pop >= 2) {
         for (int i = 0; i < size; i++) {
             if (!tmp_col.mp[i]) 
@@ -130,7 +131,7 @@ gret PackedRow::propGause(
         }
     }
 
-    //Calc value of row
+    // Calc value of row by bitwise-anding the current model and the row
     tmp_col2.set_and(*this, cols_vals);
     unsigned pop_t = tmp_col2.popcnt() + (unsigned)rhs();
 
@@ -153,7 +154,7 @@ gret PackedRow::propGause(
         unsigned col = (at - 1) + i * 64;
         SASSERT(tmp_col[col] == 1);
         unsigned var = column_to_var[col];
-        ret_lit_prop = literal(var,pop_t % 2);
+        ret_lit_prop = literal(var, !(pop_t % 2));
         return gret::prop;
     }
 
@@ -1049,7 +1050,7 @@ bool EGaussian::check_row_satisfied(unsigned row) {
     bool fin = m_mat[row].rhs();
     for (unsigned i = 0; i < m_num_cols; i++) {
         if (m_mat[row][i]) {
-            unsigned var = m_column_to_var[i];
+            bool_var var = m_column_to_var[i];
             auto val = m_solver.s().value(var);
             if (val == l_undef) {
                 TRACE("xor", tout << "Var " << var+1 << " col: " << i << " is undef!\n";);
diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp
index a423c7034..b45f346ad 100644
--- a/src/sat/smt/xor_solver.cpp
+++ b/src/sat/smt/xor_solver.cpp
@@ -22,11 +22,14 @@ Abstract:
 namespace xr {
     
     solver::solver(euf::solver& ctx) :
-        solver(ctx.get_manager(), ctx.get_manager().mk_family_id("xor")) {
-        m_ctx = &ctx;
-    }
+        euf::th_solver(
+                ctx.get_manager(), symbol("xor"),
+                ctx.get_manager().mk_family_id("xor")),
+        m_ctx(&ctx), m_region() { }
 
-    solver::solver(ast_manager& m, euf::theory_id id) : euf::th_solver(m, symbol("xor"), id) { }
+    solver::solver(ast_manager& m, euf::theory_id id) :
+        euf::th_solver(m, symbol("xor"), id),
+        m_ctx(nullptr), m_region(region()) { }
     
     solver::~solver() {
         /*for (justification* j : m_justifications) {
@@ -551,8 +554,8 @@ namespace xr {
         }
     }
     
-    sat::justification solver::mk_justification(const int level, const unsigned int matrix_no, const unsigned int row_i) {
-        void* mem = m_ctx->get_region().allocate(justification::get_obj_size());
+    sat::justification solver::mk_justification(int level, unsigned matrix_no, unsigned row_i) {
+        void* mem = get_region().allocate(justification::get_obj_size());
         sat::constraint_base::initialize(mem, this);
         auto* constraint = new (sat::constraint_base::ptr2mem(mem)) justification(matrix_no, row_i);
         return sat::justification::mk_ext_justification(level, constraint->to_index()); 
diff --git a/src/sat/smt/xor_solver.h b/src/sat/smt/xor_solver.h
index d5324e89e..c7a988485 100644
--- a/src/sat/smt/xor_solver.h
+++ b/src/sat/smt/xor_solver.h
@@ -37,6 +37,8 @@ namespace xr {
         // ptr_vector<justification> m_justifications;
         // unsigned_vector           m_justifications_lim;
 
+        optional<region>          m_region;
+
         bool_var_vector                m_tmp_xor_clash_vars;
              
         vector<xor_clause>             m_xorclauses;
@@ -52,7 +54,7 @@ namespace xr {
         svector<gauss_data>            m_gqueuedata;
         
         visit_helper                   m_visited;
-        
+
         // tmp
         bool_var_vector m_occurrences;
         // unfortunately, we cannot use generic "m_visited" here, 
@@ -66,6 +68,10 @@ namespace xr {
         void push_core();
         void pop_core(unsigned num_scopes);
 
+        region& get_region() {
+            return m_ctx != nullptr ? m_ctx->get_region() : *m_region;
+        }
+
         bool xor_has_interesting_var(const xor_clause& x);
         
         void clean_xor_no_prop(literal_vector& ps, bool& rhs);
@@ -125,7 +131,7 @@ namespace xr {
         
         bool xor_together_xors(vector<xor_clause>& xors);
         
-        sat::justification mk_justification(const int level, const unsigned int matrix_no, const unsigned int row_i);
+        sat::justification mk_justification(int level, unsigned matrix_no, unsigned row_i);
         
         std::ostream& display(std::ostream& out) const override;
         std::ostream& display_justification(std::ostream& out, sat::ext_justification_idx idx) const override;