diff --git a/src/tactic/sls/sls_evaluator.h b/src/tactic/sls/sls_evaluator.h
index 696d7664a..97860e3a2 100644
--- a/src/tactic/sls/sls_evaluator.h
+++ b/src/tactic/sls/sls_evaluator.h
@@ -586,7 +586,7 @@ public:
 #else
                 m_tracker.set_score(cur, m_tracker.score(cur));
 #endif
-#endif			
+#endif            
                 if (m_tracker.has_uplinks(cur)) {
                     ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
                     for (unsigned j = 0; j < ups.size(); j++) {
@@ -645,7 +645,7 @@ public:
 #else
                 m_tracker.set_score(cur, m_tracker.score(cur));
 #endif
-#endif			
+#endif            
                 if (m_tracker.has_uplinks(cur)) {
                     ptr_vector<expr> & ups = m_tracker.get_uplinks(cur);
                     for (unsigned j = 0; j < ups.size(); j++) {
diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index ada0ec359..743ad00bc 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -518,7 +518,6 @@ class sls_tactic : public tactic {
         void mk_random_move(ptr_vector<func_decl> & unsat_constants)
         {
             unsigned rnd_mv = 0;
-
             unsigned ucc = unsat_constants.size(); 
             unsigned rc = (m_tracker.get_random_uint((ucc < 16) ? 4 : (ucc < 256) ? 8 : (ucc < 4096) ? 12 : (ucc < 65536) ? 16 : 32)) % ucc;
             func_decl * fd = unsat_constants[rc];
diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h
index 0aca1f59c..4d9c078b6 100644
--- a/src/tactic/sls/sls_tracker.h
+++ b/src/tactic/sls/sls_tracker.h
@@ -1147,11 +1147,12 @@ public:
 #if _PROBABILISTIC_UCT_
             double sum_score = 0.0;
             unsigned start_index = get_random_uint(16) % sz;
-            
+
             for (unsigned i = start_index; i < sz; i++)
             {
                 expr * e = g->form(i);
                 vscore = m_scores.find(e);
+
 #if _PROBABILISTIC_UCT_ == 2
                 double q = vscore.score * vscore.score; 
 #else