diff --git a/src/tactic/sls/sls_compilation_settings.h b/src/tactic/sls/sls_compilation_settings.h
index 9add78daa..a649bc9ed 100644
--- a/src/tactic/sls/sls_compilation_settings.h
+++ b/src/tactic/sls/sls_compilation_settings.h
@@ -23,7 +23,7 @@ Notes:
 #define _SLS_COMPILATION_SETTINGS_H_
 
 // shall we use addition/subtraction?
-#define _USE_ADDSUB_ 0
+#define _USE_ADDSUB_ 1
 
 // should we use unsat-structures as done in SLS 4 SAT instead for random or bfs selection?
 #define _REAL_RS_ 0
diff --git a/src/tactic/sls/sls_engine.cpp b/src/tactic/sls/sls_engine.cpp
index c240a0c51..af8ae1df2 100644
--- a/src/tactic/sls/sls_engine.cpp
+++ b/src/tactic/sls/sls_engine.cpp
@@ -68,6 +68,12 @@ void sls_engine::updt_params(params_ref const & _p) {
     m_restart_base = p.restart_base();
     m_restart_next = m_restart_base;
     m_restart_init = p.restart_init();
+
+    // Andreas: Would cause trouble because repick requires an assertion being picked before which is not the case in GSAT.
+    if (m_walksat_repick && !m_walksat)
+        NOT_IMPLEMENTED_YET();
+    if (m_vns_repick && !m_walksat)
+        NOT_IMPLEMENTED_YET();
 }
 
 void sls_engine::checkpoint() {
@@ -435,19 +441,25 @@ lbool sls_engine::search() {
         if (m_vns_mc && (new_const == static_cast<unsigned>(-1)))
             score = find_best_move_mc(to_evaluate, score, new_const, new_value);
    
-        /*if (m_vns_repick && (new_const == static_cast<unsigned>(-1)))
+        if (m_vns_repick && (new_const == static_cast<unsigned>(-1)))
         {
-            expr * q = m_tracker.get_new_unsat_assertion(m_assertions, e);
+            expr * q = m_tracker.get_new_unsat_assertion(m_assertions);
             if (q)
             {
-                ptr_vector<func_decl> & to_evaluate2 = m_tracker.get_unsat_constants_walksat(e);
+                ptr_vector<func_decl> & to_evaluate2 = m_tracker.get_unsat_constants_walksat(q);
                 score = find_best_move(to_evaluate2, score, new_const, new_value, new_bit, move);
+
+                if (new_const != static_cast<unsigned>(-1)) {
+                    func_decl * fd = to_evaluate2[new_const];
+                    score = serious_score(fd, new_value);
+                    continue;
+                }
             }
-        }*/
+        }
 
         if (new_const == static_cast<unsigned>(-1)) {
             score = old_score;
-            if (m_walksat && m_walksat_repick)
+            if (m_walksat_repick)
                 m_evaluator.randomize_local(m_assertions);
             else
                 m_evaluator.randomize_local(to_evaluate);
diff --git a/src/tactic/sls/sls_tracker.h b/src/tactic/sls/sls_tracker.h
index 65011dc8d..7b48057d4 100644
--- a/src/tactic/sls/sls_tracker.h
+++ b/src/tactic/sls/sls_tracker.h
@@ -76,7 +76,7 @@ private:
     ptr_vector<func_decl> m_constants;
     ptr_vector<func_decl> m_temp_constants;
     occ_type              m_constants_occ;
-
+    unsigned              m_last_pos;
     unsigned              m_walksat;
     unsigned              m_ucb;
     double                m_ucb_constant;
@@ -1082,6 +1082,7 @@ public:
                 return 0;
         }
         
+        m_last_pos = pos;
         return as[pos];
 #if _REAL_RS_
         //unsigned pos = m_false_list[get_random_uint(16) % m_cnt_false];
@@ -1093,7 +1094,7 @@ public:
 #endif
     }
 
-    expr * get_new_unsat_assertion(ptr_vector<expr> const & as, expr * e) {
+    expr * get_new_unsat_assertion(ptr_vector<expr> const & as) {
         unsigned sz = as.size();
         if (sz == 1)
             return 0;
@@ -1101,7 +1102,7 @@ public:
         
         unsigned cnt_unsat = 0, pos = -1;
         for (unsigned i = 0; i < sz; i++)
-            if (m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0) && (as[i] != e)) pos = i;	
+            if ((i != m_last_pos) && m_mpz_manager.neq(get_value(as[i]), m_one) && (get_random_uint(16) % ++cnt_unsat == 0)) pos = i;	
 
         if (pos == static_cast<unsigned>(-1))
             return 0;