diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp
index 40efb4b2a..49bcf4c76 100644
--- a/src/sat/smt/xor_gaussian.cpp
+++ b/src/sat/smt/xor_gaussian.cpp
@@ -76,7 +76,7 @@ void PackedRow::get_reason(
         while (at != 0) {
             unsigned col = extra + at - 1 + i * 64;
             SASSERT(operator[](col) == 1);
-            const unsigned var = col_to_var[col];
+            unsigned var = col_to_var[col];
             if (var == prop.var()) {
                 tmp_clause.push_back(prop);
                 std::swap(tmp_clause[0], tmp_clause.back());
@@ -117,7 +117,7 @@ gret PackedRow::propGause(
             int extra = 0;
             while (at != 0) {
                 unsigned col = extra + at-1 + i*64;
-                const unsigned var = col_to_var[col];
+                unsigned var = col_to_var[col];
                 // found new non-basic variable, let's watch it
                 if (!var_has_resp_row[var]) {
                     new_resp_var = var;
@@ -136,7 +136,7 @@ gret PackedRow::propGause(
 
     //Calc value of row
     tmp_col2.set_and(*this, cols_vals);
-    const unsigned pop_t = tmp_col2.popcnt() + (unsigned)rhs();
+    unsigned pop_t = tmp_col2.popcnt() + (unsigned)rhs();
 
     SASSERT(pop == 1 || pop == 0);
 
@@ -162,7 +162,7 @@ gret PackedRow::propGause(
     return gret::nothing_satisfied;
 }
 
-EGaussian::EGaussian(xr::solver& _solver, const unsigned _matrix_no, const vector<xor_clause>& _xorclauses) : 
+EGaussian::EGaussian(xr::solver& _solver, unsigned _matrix_no, const vector<xor_clause>& _xorclauses) : 
     m_xorclauses(_xorclauses), m_solver(_solver), matrix_no(_matrix_no) { }
 
 EGaussian::~EGaussian() {
@@ -201,7 +201,7 @@ public:
         }
     }
 
-    bool operator()(const unsigned a, const unsigned b) {
+    bool operator()(unsigned a, unsigned b) {
         SASSERT(m_solver.seen.size() > a);
         SASSERT(m_solver.seen.size() > b);
         if (m_solver.seen[b] && !m_solver.seen[a])
@@ -299,7 +299,7 @@ void EGaussian::delete_gauss_watch_this_matrix() {
         clear_gwatches(i);    
 }
 
-void EGaussian::clear_gwatches(const unsigned var) {
+void EGaussian::clear_gwatches(unsigned var) {
     //if there is only one matrix, don't check, just empty it
     if (m_solver.m_gmatrices.empty()) {
         m_solver.m_gwatches[var].clear();
@@ -391,7 +391,7 @@ bool EGaussian::full_init(bool& created) {
 
 void EGaussian::eliminate() {
     // TODO: Why twice? gauss_jordan_elim
-    const unsigned end_row = num_rows;
+    unsigned end_row = num_rows;
     unsigned rowI = 0;
     unsigned row_i = 0;
     unsigned col = 0;
@@ -431,7 +431,7 @@ void EGaussian::eliminate() {
     }
 }
 
-literal_vector* EGaussian::get_reason(const 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);
@@ -466,7 +466,7 @@ gret EGaussian::init_adjust_matrix() {
         if (row_i >= num_rows)
             break;
         unsigned non_resp_var;
-        const unsigned popcnt = row.find_watchVar(tmp_clause, col_to_var, var_has_resp_row, non_resp_var);
+        unsigned popcnt = row.find_watchVar(tmp_clause, col_to_var, var_has_resp_row, non_resp_var);
 
         switch (popcnt) {
 
@@ -555,7 +555,7 @@ gret EGaussian::init_adjust_matrix() {
 }
 
 // Delete this row because we have already add to xor clause, nothing to do anymore
-void EGaussian::delete_gausswatch(const unsigned row_n) {
+void EGaussian::delete_gausswatch(unsigned row_n) {
     // clear nonbasic value watch list
     svector<gauss_watched>& ws_t = m_solver.m_gwatches[row_to_var_non_resp[row_n]];
 
@@ -569,7 +569,7 @@ void EGaussian::delete_gausswatch(const unsigned row_n) {
     UNREACHABLE();
 }
 
-unsigned EGaussian::get_max_level(const gauss_data& gqd, const 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);
     unsigned nMaxLevel = gqd.currLevel;
@@ -595,8 +595,8 @@ bool EGaussian::find_truths(
     svector<gauss_watched>& ws,
     unsigned& i,
     unsigned& j,
-    const unsigned var,
-    const unsigned row_n,
+    unsigned var,
+    unsigned row_n,
     gauss_data& gqd) {
     SASSERT(gqd.status != gauss_res::confl);
     SASSERT(initialized);
@@ -800,7 +800,7 @@ void EGaussian::update_cols_vals_set(bool force) {
     last_val_update = m_solver.s().trail_size();
 }
 
-void EGaussian::prop_lit(const gauss_data& gqd, const unsigned row_i, const literal ret_lit_prop) {
+void EGaussian::prop_lit(const gauss_data& gqd, unsigned row_i, const literal ret_lit_prop) {
     unsigned level;
     if (gqd.currLevel == m_solver.m_num_scopes) 
         level = gqd.currLevel;
@@ -815,10 +815,10 @@ bool EGaussian::inconsistent() const {
 }
 
 void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) {
-    const unsigned new_resp_row_n = gqd.new_resp_row;
+    unsigned new_resp_row_n = gqd.new_resp_row;
     PackedMatrix::iterator rowI = mat.begin();
     PackedMatrix::iterator end = mat.end();
-    const unsigned new_resp_col = var_to_col[gqd.new_resp_var];
+    unsigned new_resp_col = var_to_col[gqd.new_resp_var];
     unsigned row_i = 0;
 
     elim_called++;
@@ -964,7 +964,7 @@ void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) {
 // Checking functions below
 //////////////////
 
-void EGaussian::check_row_not_in_watch(const unsigned v, const unsigned row_num) const {
+void EGaussian::check_row_not_in_watch(unsigned v, unsigned row_num) const {
     for (const auto& x: m_solver.m_gwatches[v]) 
         SASSERT(!(x.matrix_num == matrix_no && x.row_n == row_num));    
 }
diff --git a/src/sat/smt/xor_gaussian.h b/src/sat/smt/xor_gaussian.h
index 2598a7eb6..2be973b37 100644
--- a/src/sat/smt/xor_gaussian.h
+++ b/src/sat/smt/xor_gaussian.h
@@ -475,11 +475,11 @@ namespace xr {
             return *this;
         }
     
-        inline PackedRow operator[](const unsigned i) {
+        inline PackedRow operator[](unsigned i) {
             return PackedRow(numCols, mp+i*(numCols+1));
         }
     
-        inline PackedRow operator[](const unsigned i) const {
+        inline PackedRow operator[](unsigned i) const {
             return PackedRow(numCols, mp+i*(numCols+1));
         }
     
@@ -487,7 +487,7 @@ namespace xr {
             int64_t* mp;
             const unsigned numCols;
             
-            iterator(int64_t* _mp, const unsigned _numCols) : mp(_mp), numCols(_numCols) { }
+            iterator(int64_t* _mp, unsigned _numCols) : mp(_mp), numCols(_numCols) { }
                 
         public:
             friend class PackedMatrix;
@@ -501,7 +501,7 @@ namespace xr {
                 return *this;
             }
     
-            iterator operator+(const unsigned num) const {
+            iterator operator+(unsigned num) const {
                 iterator ret(*this);
                 ret.mp += (numCols + 1) * num;
                 return ret;
@@ -511,7 +511,7 @@ namespace xr {
                 return (unsigned)(mp - b.mp) / (numCols + 1);
             }
     
-            void operator+=(const unsigned num) {
+            void operator+=(unsigned num) {
                 mp += (numCols + 1) * num;  // add by f4
             }
     
@@ -543,7 +543,7 @@ namespace xr {
     public:
         EGaussian(
             solver& solver,
-            const unsigned matrix_no,
+            unsigned matrix_no,
             const vector<xor_clause>& xorclauses
         );
         ~EGaussian();
@@ -554,12 +554,12 @@ namespace xr {
             svector<gauss_watched>& ws,
             unsigned& i,
             unsigned& j,
-            const unsigned var,
-            const unsigned row_n,
+            unsigned var,
+            unsigned row_n,
             gauss_data& gqd
         );
     
-        literal_vector* get_reason(const unsigned row, int& out_ID);
+        literal_vector* get_reason(unsigned row, int& out_ID);
     
         // when basic variable is touched , eliminate one col
         void eliminate_col(
@@ -581,20 +581,20 @@ namespace xr {
         xr::solver& m_solver;   // original sat solver
     
         //Cleanup
-        void clear_gwatches(const unsigned var);
+        void clear_gwatches(unsigned var);
         void delete_gauss_watch_this_matrix();
-        void delete_gausswatch(const unsigned  row_n);
+        void delete_gausswatch(unsigned row_n);
     
         //Invariant checks, debug
         void check_no_prop_or_unsat_rows();
         void check_tracked_cols_only_one_set();
-        bool check_row_satisfied(const unsigned row);
-        void check_row_not_in_watch(const unsigned v, const unsigned row_num) const;
+        bool check_row_satisfied(unsigned row);
+        void check_row_not_in_watch(unsigned v, unsigned row_num) const;
     
         //Reason generation
         vector<reason> xor_reasons;
         sat::literal_vector tmp_clause;
-        unsigned get_max_level(const gauss_data& gqd, const unsigned row_n);
+        unsigned get_max_level(const gauss_data& gqd, unsigned row_n);
     
         //Initialisation
         void eliminate();
@@ -604,7 +604,7 @@ namespace xr {
         double get_density();
     
         //Helper functions
-        void prop_lit(const gauss_data& gqd, const unsigned row_i, const sat::literal ret_lit_prop);
+        void prop_lit(const gauss_data& gqd, unsigned row_i, const sat::literal ret_lit_prop);
         bool inconsistent() const;
 
         ///////////////
diff --git a/src/sat/smt/xor_matrix_finder.cpp b/src/sat/smt/xor_matrix_finder.cpp
index ecc9a77a0..3500b7f1a 100644
--- a/src/sat/smt/xor_matrix_finder.cpp
+++ b/src/sat/smt/xor_matrix_finder.cpp
@@ -94,7 +94,7 @@ namespace xr {
                     newSet.push_back(v);
             }
             if (tomerge.size() == 1) {
-                const unsigned into = *tomerge.begin();
+                unsigned into = *tomerge.begin();
                 unsigned_vector& intoReverse = m_reverseTable.find(into);
                 for (unsigned i = 0; i < newSet.size(); i++) {
                     intoReverse.push_back(newSet[i]);
@@ -104,9 +104,8 @@ namespace xr {
             }
     
             for (unsigned v: tomerge) {
-                for (const auto& v2 : m_reverseTable[v]) {
+                for (const auto& v2 : m_reverseTable[v]) 
                     newSet.insert(v2);
-                }
                 m_reverseTable.erase(v);
             }
             for (auto j : newSet)
@@ -133,7 +132,7 @@ namespace xr {
 
         for (xor_clause& x : m_xor.m_xorclauses) {
             // take 1st variable to check which matrix it's in.
-            const unsigned matrix = m_table[x[0]];
+            unsigned matrix = m_table[x[0]];
             SASSERT(matrix < m_matrix_no);
     
             //for stats
diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp
index 08bc872f4..b6ad2a3d9 100644
--- a/src/sat/smt/xor_solver.cpp
+++ b/src/sat/smt/xor_solver.cpp
@@ -606,11 +606,9 @@ namespace xr {
         while (changed) {
             changed = false;
             m_interesting.clear();
-            for (const bool_var l : m_occurrences) {
-                if (m_occ_cnt[l] == 2 && !s().is_visited(l)) {
+            for (const bool_var l : m_occurrences) 
+                if (m_occ_cnt[l] == 2 && !s().is_visited(l)) 
                     m_interesting.push_back(l);
-                }
-            }
     
             while (!m_interesting.empty()) {
     
@@ -622,7 +620,7 @@ namespace xr {
     
                 unsigned indexes[2];
                 unsigned at = 0;
-                size_t i2 = 0;
+                unsigned i2 = 0;
                 sat::watch_list& ws = s().get_wlist(literal(v, false));
     
                 //Remove the 2 indexes from the watchlist
@@ -632,6 +630,9 @@ namespace xr {
                         // TODO: Check!!! Is this fine?
                         ws[i2++] = ws[i];
                     } 
+                    // NSB code review get_ext_constraint_idx() is a pointer.
+                    // If it corresponds to an index in the watch list, use a helper function
+                    // to convert it.
                     else if (!xors[w.get_ext_constraint_idx()].empty()) {
                         SASSERT(at < 2);
                         indexes[at] = w.get_ext_constraint_idx();