diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
index d7ce8e703..d61a831d3 100644
--- a/src/ast/sls/bv_sls_eval.cpp
+++ b/src/ast/sls/bv_sls_eval.cpp
@@ -924,15 +924,15 @@ namespace bv {
             bool try_above = m_rand(2) == 0;
             if (try_above) {
                 a.set_add(m_tmp, b.bits(), m_one);
-                if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand))
+                if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp,  m_rand))
                     return true;
             }
             a.set_sub(m_tmp, b.bits(), m_one);
-            if (!a.is_zero(m_tmp) && a.set_random_at_most(m_tmp, m_tmp2, m_rand))
+            if (!a.is_zero(m_tmp) && a.set_random_at_most(m_tmp, m_rand))
                 return true;
             if (!try_above) {
                 a.set_add(m_tmp, b.bits(), m_one);
-                if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_tmp2, m_rand))
+                if (!a.is_zero(m_tmp) && a.set_random_at_least(m_tmp, m_rand))
                     return true;
             }
             return false;
@@ -1007,7 +1007,6 @@ namespace bv {
     bool sls_eval::try_repair_bxor(bvect const& e, bvval& a, bvval const& b) {
         for (unsigned i = 0; i < a.nw; ++i)
             m_tmp[i] = e[i] ^ b.bits()[i];
-        a.clear_overflow_bits(m_tmp);
         return a.set_repair(random_bool(), m_tmp);
     }
 
@@ -1149,7 +1148,7 @@ namespace bv {
 
     bool sls_eval::try_repair_bnot(bvect const& e, bvval& a) {
         for (unsigned i = 0; i < a.nw; ++i)
-            m_tmp[i] = ~e[i];
+            m_tmp[i] = ~e[i];        
         a.clear_overflow_bits(m_tmp);
         return a.try_set(m_tmp);
     }
@@ -1230,14 +1229,14 @@ namespace bv {
         if (b < p2) {
             bool coin = m_rand(2) == 0;
             if (coin)
-                r = a.set_random_at_least(p2, m_tmp3, m_rand);
+                r = a.set_random_at_least(p2, m_rand);
             if (!r)
-                r = a.set_random_at_most(b, m_tmp3, m_rand);
+                r = a.set_random_at_most(b, m_rand);
             if (!coin && !r)
-                r = a.set_random_at_least(p2, m_tmp3, m_rand);
+                r = a.set_random_at_least(p2, m_rand);
         }
         else 
-            r = a.set_random_in_range(p2, b, m_tmp3, m_rand);
+            r = a.set_random_in_range(p2, b, m_rand);
         return r;
     }
 
@@ -1257,16 +1256,16 @@ namespace bv {
         bool r = false;
         if (p2 < b) 
             // random b <= x < p2 
-            r = a.set_random_in_range(b, p2_1, m_tmp3, m_rand);        
+            r = a.set_random_in_range(b, p2_1, m_rand);        
         else {
             // random b <= x or x < p2
             bool coin = m_rand(2) == 0;
             if (coin)
-                r = a.set_random_at_most(p2_1, m_tmp3, m_rand);
+                r = a.set_random_at_most(p2_1,m_rand);
             if (!r)
-                r = a.set_random_at_least(b, m_tmp3, m_rand);
+                r = a.set_random_at_least(b,  m_rand);
             if (!r && !coin)
-                r = a.set_random_at_most(p2_1, m_tmp3, m_rand);
+                r = a.set_random_at_most(p2_1,  m_rand);
         }
         p2_1.set_bw(0);
         return r;
@@ -1282,28 +1281,28 @@ namespace bv {
     bool sls_eval::try_repair_ule(bool e, bvval& a, bvval const& b) {
         if (e) {
             // a <= t
-            return a.set_random_at_most(b.bits(), m_tmp, m_rand);
+            return a.set_random_at_most(b.bits(),  m_rand);
         }
         else {
             // a > t
             a.set_add(m_tmp, b.bits(), m_one);
             if (a.is_zero(m_tmp))
                 return false;   
-            return a.set_random_at_least(m_tmp, m_tmp2, m_rand);
+            return a.set_random_at_least(m_tmp, m_rand);
         }           
     }
 
     bool sls_eval::try_repair_uge(bool e, bvval& a, bvval const& b) {
         if (e) {
             // a >= t
-            return a.set_random_at_least(b.bits(), m_tmp, m_rand);
+            return a.set_random_at_least(b.bits(), m_rand);
         }
         else {
             // a < t
             if (b.is_zero())
                 return false;
             a.set_sub(m_tmp, b.bits(), m_one);
-            return a.set_random_at_most(m_tmp, m_tmp2, m_rand);
+            return a.set_random_at_most(m_tmp, m_rand);
         }    
     }
 
@@ -1377,7 +1376,6 @@ namespace bv {
             unsigned n = b.bits().to_nat(e.bw);
             for (unsigned i = e.bw; i-- > e.bw - n;) 
                 t.set(i, a.get_bit(i)); 
-            a.clear_overflow_bits(t);
             if (a.set_repair(random_bool(), t))
                 return true;                      
         }
@@ -1527,7 +1525,6 @@ namespace bv {
                     t[i] = a.bits()[i];
                 t.set(b.bw - 1, a.is_ones(e));
             }   
-            a.clear_overflow_bits(t);
             if (a.set_repair(random_bool(), t))
                 return true;
         }
@@ -1541,13 +1538,10 @@ namespace bv {
                 a.get_variant(t, m_rand);
                 t.set(b.bw - 1, a.is_ones(e));
             }
-            a.clear_overflow_bits(t);
             if (a.set_repair(random_bool(), t))
                 return true;
         }            
-
-        a.get_variant(t, m_rand);
-        return a.set_repair(random_bool(), t);
+        return a.set_random(m_rand);
     }
 
     /*
@@ -1645,7 +1639,6 @@ namespace bv {
                 m_tmp2.set(b.msb(m_tmp2), false);
             while (a.set_add(m_tmp3, m_tmp, m_tmp2)) 
                 m_tmp2.set(b.msb(m_tmp2), false);       
-            a.clear_overflow_bits(m_tmp3);
             return a.set_repair(true, m_tmp3);
         }
         else {
@@ -1723,7 +1716,6 @@ namespace bv {
                 m_tmp[i] = random_bits();
             a.set_sub(m_tmp2, a.bits(), e);
             set_div(m_tmp2, m_tmp, a.bw, m_tmp3, m_tmp4);
-            a.clear_overflow_bits(m_tmp3);
             return b.set_repair(random_bool(), m_tmp3);
         }
     }
diff --git a/src/ast/sls/sls_valuation.cpp b/src/ast/sls/sls_valuation.cpp
index 68143e7b7..c46b2ef77 100644
--- a/src/ast/sls/sls_valuation.cpp
+++ b/src/ast/sls/sls_valuation.cpp
@@ -244,34 +244,35 @@ namespace bv {
         return true;
     }
 
-    bool sls_valuation::set_random_at_most(bvect const& src, bvect& tmp, random_gen& r) {
-        if (!get_at_most(src, tmp))
+    bool sls_valuation::set_random_at_most(bvect const& src, random_gen& r) {
+        if (!get_at_most(src, m_tmp))
             return false;
 
-        if (is_zero(tmp) || (0 != r(10)))
-            return try_set(tmp);
+        if (is_zero(m_tmp) || (0 != r(10)))
+            return try_set(m_tmp);
 
         // random value below tmp
-        set_random_below(tmp, r);
+        set_random_below(m_tmp, r);
         
-        return (can_set(tmp) || get_at_most(src, tmp)) && try_set(tmp);
+        return (can_set(m_tmp) || get_at_most(src, m_tmp)) && try_set(m_tmp);
     }
 
-    bool sls_valuation::set_random_at_least(bvect const& src, bvect& tmp, random_gen& r) {
-        if (!get_at_least(src, tmp))
+    bool sls_valuation::set_random_at_least(bvect const& src, random_gen& r) {
+        if (!get_at_least(src, m_tmp))
             return false;
 
-        if (is_ones(tmp) || (0 != r(10)))
-            return try_set(tmp);
+        if (is_ones(m_tmp) || (0 != r(10)))
+            return try_set(m_tmp);
 
         // random value at least tmp
-        set_random_above(tmp, r);
+        set_random_above(m_tmp, r);
 
-        return (can_set(tmp) || get_at_least(src, tmp)) && try_set(tmp);
+        return (can_set(m_tmp) || get_at_least(src, m_tmp)) && try_set(m_tmp);
     }
 
-    bool sls_valuation::set_random_in_range(bvect const& lo, bvect const& hi, bvect& tmp, random_gen& r) {
-        if (0 == r() % 2) {
+    bool sls_valuation::set_random_in_range(bvect const& lo, bvect const& hi, random_gen& r) {
+        bvect& tmp = m_tmp;
+        if (0 == r(2)) {
             if (!get_at_least(lo, tmp))
                 return false;
             SASSERT(in_range(tmp));
@@ -342,7 +343,7 @@ namespace bv {
     bool sls_valuation::set_repair(bool try_down, bvect& dst) {
         for (unsigned i = 0; i < nw; ++i)
             dst[i] = (~fixed[i] & dst[i]) | (fixed[i] & m_bits[i]);
-
+        clear_overflow_bits(dst);
         repair_sign_bits(dst);
         if (in_range(dst)) {
             set(eval, dst);
@@ -674,6 +675,4 @@ namespace bv {
             c += get_num_1bits(src[i]);
         return c == 1;
     }
-
-
 }
diff --git a/src/ast/sls/sls_valuation.h b/src/ast/sls/sls_valuation.h
index e4828302e..66d7e0281 100644
--- a/src/ast/sls/sls_valuation.h
+++ b/src/ast/sls/sls_valuation.h
@@ -226,9 +226,9 @@ namespace bv {
         bool get_at_most(bvect const& src, bvect& dst) const;
         bool get_at_least(bvect const& src, bvect& dst) const;
 
-        bool set_random_at_most(bvect const& src, bvect& tmp, random_gen& r);
-        bool set_random_at_least(bvect const& src, bvect& tmp, random_gen& r);
-        bool set_random_in_range(bvect const& lo, bvect const& hi, bvect& tmp, random_gen& r);
+        bool set_random_at_most(bvect const& src, random_gen& r);
+        bool set_random_at_least(bvect const& src, random_gen& r);
+        bool set_random_in_range(bvect const& lo, bvect const& hi, random_gen& r);
 
         bool set_repair(bool try_down, bvect& dst);
         void set_random_above(bvect& dst, random_gen& r);