diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 2566e1be9..e2dcee7c7 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -2789,10 +2789,11 @@ namespace sat {
         return idx;
     }
 
-    void solver::process_antecedent(literal antecedent, unsigned & num_marks) {
+    void solver::process_antecedent(literal antecedent, unsigned & num_marks) {        
         bool_var var     = antecedent.var();
         unsigned var_lvl = lvl(var);
         SASSERT(var < num_vars());
+        SASSERT(value(antecedent) == l_true);
         TRACE("sat_verbose", tout << "process " << var << "@" << var_lvl << " marked " << is_marked(var) << " conflict " << m_conflict_lvl << "\n";);
         if (!is_marked(var) && var_lvl > 0) {
             mark(var);
@@ -2823,6 +2824,7 @@ namespace sat {
         auto idx = js.get_ext_justification_idx();
         m_ext_antecedents.reset();
         m_ext->get_antecedents(consequent, idx, m_ext_antecedents, probing);
+        DEBUG_CODE(for (auto lit : m_ext_antecedents) SASSERT(value(lit) == l_true););
     }
 
     bool solver::is_two_phase() const {
diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp
index 6aabd3246..d2da78d4b 100644
--- a/src/sat/smt/xor_gaussian.cpp
+++ b/src/sat/smt/xor_gaussian.cpp
@@ -54,7 +54,7 @@ unsigned PackedRow::population_cnt(
 }
 
 // Gets the reason why the literal "prop" was propagated
-void PackedRow::get_reason(literal_vector& tmp_clause, const unsigned_vector& column_to_var, PackedRow& cols_vals, PackedRow& tmp_col2, literal prop) {
+void PackedRow::get_reason(literal_vector& antecedents, const unsigned_vector& column_to_var, PackedRow& cols_vals, PackedRow& tmp_col2, literal prop) {
 
     tmp_col2.set_and(*this, cols_vals);
     for (int i = 0; i < size; i++) {
@@ -69,11 +69,11 @@ void PackedRow::get_reason(literal_vector& tmp_clause, const unsigned_vector& co
             SASSERT((*this)[col] == 1);
             unsigned var = column_to_var[col];
             if (var == prop.var()) {
-                tmp_clause.push_back(~prop); // TODO: Why not negated?
-                std::swap(tmp_clause[0], tmp_clause.back());
+                antecedents.push_back(prop); 
+                std::swap(antecedents[0], antecedents.back());
             }
-            else
-                tmp_clause.push_back(literal(var, tmp_col2[col])); // NSB: double check if z3 use of sign is compatible
+            else 
+                antecedents.push_back(literal(var, !tmp_col2[col]));
 
             extra += at;
             if (extra == 64)
@@ -416,10 +416,10 @@ void EGaussian::eliminate() {
     std::cout << "-------------" << std::endl;
 }
 
-literal_vector* EGaussian::get_reason(unsigned row, int& out_ID) {
+literal_vector& EGaussian::get_reason(unsigned row, int& out_ID) {
     if (!xor_reasons[row].m_must_recalc) {
         out_ID = xor_reasons[row].m_ID;
-        return &(xor_reasons[row].m_reason);
+        return xor_reasons[row].m_reason;
     }
 
     // Clean up previous one
@@ -436,7 +436,7 @@ literal_vector* EGaussian::get_reason(unsigned row, int& out_ID) {
     
     xor_reasons[row].m_must_recalc = false;
     xor_reasons[row].m_ID = out_ID;
-    return &to_fill;
+    return to_fill;
 }
 
 // Creates binary clauses, assigns variables, adds conflicts based on the (reduced) gaussian-matrix. Also sets up the gaussian watchlist
@@ -556,12 +556,12 @@ void EGaussian::delete_gausswatch(unsigned row_n) {
 
 unsigned EGaussian::get_max_level(const gauss_data& gqd, unsigned row_n) {
     int ID;
-    literal_vector* cl = get_reason(row_n, ID);
+    literal_vector& ante = get_reason(row_n, ID);
     unsigned nMaxLevel = gqd.currLevel;
     unsigned nMaxInd = 1;
 
-    for (unsigned i = 1; i < cl->size(); i++) {
-        literal l = (*cl)[i];
+    for (unsigned i = ante.size(); i-- > 0; ) {
+        literal l = ante[i];
         unsigned nLevel = m_solver.s().lvl(l);
         if (nLevel > nMaxLevel) {
             nMaxLevel = nLevel;
@@ -571,7 +571,7 @@ unsigned EGaussian::get_max_level(const gauss_data& gqd, unsigned row_n) {
 
     //should we??
     if (nMaxInd != 1) 
-        std::swap((*cl)[1], (*cl)[nMaxInd]);
+        std::swap(ante[1], ante[nMaxInd]);
     
     return nMaxLevel;
 }
diff --git a/src/sat/smt/xor_gaussian.h b/src/sat/smt/xor_gaussian.h
index 2b6f4be08..1635feec8 100644
--- a/src/sat/smt/xor_gaussian.h
+++ b/src/sat/smt/xor_gaussian.h
@@ -574,7 +574,7 @@ namespace xr {
             gauss_data& gqd
         );
     
-        literal_vector* get_reason(unsigned row, int& out_ID);
+        literal_vector& get_reason(unsigned row, int& out_ID);
     
         // when basic variable is touched , eliminate one col
         void eliminate_column(
@@ -590,21 +590,21 @@ namespace xr {
         void check_watchlist_sanity();
         void move_back_xor_clauses();
 
-        void output_variable_assignment(std::ostream& out, sat::solver* s) {
+        void display_assignment(std::ostream& out, sat::solver& s) {
             for (unsigned i = 0; i < m_num_cols; i++) {
-                out << "v" << m_column_to_var[i] << "=" << (s->value(m_column_to_var[i]) == l_undef ? "?" : (s->value(m_column_to_var[i]) == l_true ? "1" : "0")) << " ";
+                out << "v" << m_column_to_var[i] << "=" << (s.value(m_column_to_var[i]) == l_undef ? "?" : (s.value(m_column_to_var[i]) == l_true ? "1" : "0")) << " ";
             }
             out << std::endl;
             for (unsigned i = 0; i < m_num_cols; i++) {
                 out << "v" << m_column_to_var[i] << "=";
-                if (s->get_justification(m_column_to_var[i]).is_none())
+                if (s.get_justification(m_column_to_var[i]).is_none())
                     out << "d";
-                else if (s->get_justification(m_column_to_var[i]).is_binary_clause())
+                else if (s.get_justification(m_column_to_var[i]).is_binary_clause())
                     out << "b";
-                else if (s->get_justification(m_column_to_var[i]).is_clause())
+                else if (s.get_justification(m_column_to_var[i]).is_clause())
                     out << "c";
                 else
-                    out << "j" << s->get_justification(m_column_to_var[i]).get_ext_justification_idx();
+                    out << "j" << s.get_justification(m_column_to_var[i]).get_ext_justification_idx();
                 out << " ";
             }
             out << std::endl;
diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp
index bbbbdcd7e..9e3f8a9e2 100644
--- a/src/sat/smt/xor_solver.cpp
+++ b/src/sat/smt/xor_solver.cpp
@@ -233,17 +233,16 @@ namespace xr {
         auto& j = justification::from_index(idx);
 
         int32_t ID;
-        literal_vector* cl = m_gmatrices[j.get_matrix_idx()]->get_reason(j.get_row_idx(), ID);
+        literal_vector const& ante = m_gmatrices[j.get_matrix_idx()]->get_reason(j.get_row_idx(), ID);
         std::cout << "Justification from matrix " << j.get_matrix_idx() << " on row " << j.get_row_idx() << " (ID: " << ID << "):\n";
-        for (unsigned i = 0; i < cl->size(); i++) {
-            std::cout << (*cl)[i] << "(" << s().value((*cl)[i]) << ") ";
-        }
+        for (auto lit : ante) 
+            std::cout << lit << "(" << s().value(lit) << ") ";
         std::cout << std::endl;
 
-        r.append(*cl);
+        r.append(ante);
 
         std::cout << "Overall assignments: ";
-        m_gmatrices[j.get_matrix_idx()]->output_variable_assignment(std::cout, &s());
+        m_gmatrices[j.get_matrix_idx()]->display_assignment(std::cout, s());
     }
     
     sat::check_result solver::check() {