diff --git a/src/sat/smt/xor_gaussian.cpp b/src/sat/smt/xor_gaussian.cpp
index 699fb9679..99648b89a 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();
@@ -401,7 +401,7 @@ static void print_matrix(ostream& out, PackedMatrix& mat) {
 
 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;
@@ -444,7 +444,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);
@@ -479,7 +479,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) {
 
@@ -567,7 +567,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]];
 
@@ -581,7 +581,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;
@@ -607,8 +607,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);
@@ -811,7 +811,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;
@@ -826,8 +826,8 @@ bool EGaussian::inconsistent() const {
 }
 
 void EGaussian::eliminate_col(unsigned p, gauss_data& gqd) {
-    const unsigned new_resp_row_n = gqd.new_resp_row;
-    const unsigned new_resp_col = var_to_col[gqd.new_resp_var];
+    unsigned new_resp_row_n = gqd.new_resp_row;
+    unsigned new_resp_col = var_to_col[gqd.new_resp_var];
     unsigned row_size = mat.num_rows();
     unsigned row_i = 0;
 
@@ -970,7 +970,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 493b7f218..7dc47a669 100644
--- a/src/sat/smt/xor_gaussian.h
+++ b/src/sat/smt/xor_gaussian.h
@@ -279,7 +279,6 @@ namespace xr {
         
         PackedRow() = delete;
         
-        // NSB review: why not mp[i] = b.mp[i]?
         PackedRow& operator=(const PackedRow& b) {
             //start from -1, because that's where RHS is
             for (int i = -1; i < size; i++) 
@@ -429,7 +428,6 @@ namespace xr {
     public:
         PackedMatrix() { }
     
-        // NSB: rewview - are special memory allocations required?
         ~PackedMatrix() {
             #ifdef _WIN32
             _aligned_free((void*)mp);
@@ -478,11 +476,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));
         }
     
@@ -490,7 +488,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;
@@ -504,7 +502,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;
@@ -554,7 +552,7 @@ namespace xr {
     public:
         EGaussian(
             solver& solver,
-            const unsigned matrix_no,
+            unsigned matrix_no,
             const vector<xor_clause>& xorclauses
         );
         ~EGaussian();
@@ -565,12 +563,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(
@@ -590,20 +588,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();
@@ -612,7 +610,7 @@ namespace xr {
         gret init_adjust_matrix(); // adjust matrix, include watch, check row is zero, etc.
     
         //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 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 9283a43be..270297b2b 100644
--- a/src/sat/smt/xor_matrix_finder.cpp
+++ b/src/sat/smt/xor_matrix_finder.cpp
@@ -99,7 +99,7 @@ namespace xr {
                     newSet.push_back(v);
             }
             if (to_merge.num_elems() == 1) {
-                const unsigned into = *to_merge.begin();
+                unsigned into = *to_merge.begin();
                 unsigned_vector& intoReverse = m_reverseTable[into];
                 for (unsigned i = 0; i < newSet.size(); i++) {
                     intoReverse.push_back(newSet[i]);
@@ -109,9 +109,8 @@ namespace xr {
             }
     
             for (unsigned v: to_merge) {
-                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)
@@ -137,7 +136,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 < matrix_no);
     
             //for stats
diff --git a/src/sat/smt/xor_solver.cpp b/src/sat/smt/xor_solver.cpp
index 5032a1ed7..aa8206b9a 100644
--- a/src/sat/smt/xor_solver.cpp
+++ b/src/sat/smt/xor_solver.cpp
@@ -639,11 +639,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()) {
     
@@ -655,16 +653,18 @@ 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
                 for (unsigned i = 0; i < ws.size(); i++) {
                     const sat::watched& w = ws[i];
-                    if (!w.is_ext_constraint()) {
+                    if (!w.is_ext_constraint())
                         // 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();
diff --git a/src/sat/smt/xor_solver.h b/src/sat/smt/xor_solver.h
index 3923fd27f..ec4418dc1 100644
--- a/src/sat/smt/xor_solver.h
+++ b/src/sat/smt/xor_solver.h
@@ -102,22 +102,6 @@ namespace xr {
             watch_neg_literal(s().get_wlist(lit), idx);
         }
 
-        static std::string toString(literal l) {
-            return (std::stringstream() << l).str();
-        }
-
-        static std::string toString(const literal& l) {
-            return (std::stringstream() << l).str();
-        }
-
-        static std::string toString(const literal_vector& l) {
-            return (std::stringstream() << l).str();
-        }
-
-        static std::string toString(const bool_var_vector & l) {
-            return (std::stringstream() << l).str();
-        }
-
     public:
         solver(euf::solver& ctx);
         solver(ast_manager& m, euf::theory_id id);