diff --git a/src/ast/sls/sat_ddfw.h b/src/ast/sls/sat_ddfw.h
index f7cfb2dca..0e930635e 100644
--- a/src/ast/sls/sat_ddfw.h
+++ b/src/ast/sls/sat_ddfw.h
@@ -72,7 +72,7 @@ namespace sat {
             double   m_reward = 0;
             double   m_last_reward = 0;
             unsigned m_make_count = 0;
-            unsigned m_timestamp = 0;
+            uint64_t m_timestamp = 0;
             int      m_bias = 0;
             ema      m_reward_avg = 1e-5;
         };
@@ -282,7 +282,7 @@ namespace sat {
 
         inline int& bias(bool_var v) { return m_vars[v].m_bias; }
 
-        unsigned timestamp(bool_var v) { return m_vars[v].m_timestamp; }
+        uint64_t timestamp(bool_var v) { return m_vars[v].m_timestamp; }
 
         void reserve_vars(unsigned n);
         
diff --git a/src/ast/sls/sls_context.h b/src/ast/sls/sls_context.h
index 4260d4690..fae5447eb 100644
--- a/src/ast/sls/sls_context.h
+++ b/src/ast/sls/sls_context.h
@@ -86,7 +86,7 @@ namespace sls {
         virtual void force_restart() = 0;
         virtual std::ostream& display(std::ostream& out) = 0;
         virtual reslimit& rlimit() = 0;
-        virtual unsigned timestamp(sat::bool_var v) = 0;
+        virtual uint64_t timestamp(sat::bool_var v) = 0;
     };
     
     class context {
@@ -196,7 +196,7 @@ namespace sls {
         void shift_weights() { s.shift_weights(); }
         bool try_rotate(sat::bool_var v, sat::bool_var_set& rotated, unsigned& budget) { return s.try_rotate(v, rotated, budget); }
         double reward(sat::bool_var v) { return s.reward(v); }
-        unsigned timestamp(sat::bool_var v) { return s.timestamp(v); }
+        uint64_t timestamp(sat::bool_var v) { return s.timestamp(v); }
         indexed_uint_set const& unsat() const { return s.unsat(); }
         indexed_uint_set const& unsat_vars() const { return s.unsat_vars(); }
         unsigned num_external_in_unsat_vars() const { return s.num_external_in_unsat_vars(); }
diff --git a/src/ast/sls/sls_smt_plugin.h b/src/ast/sls/sls_smt_plugin.h
index d3a1077ea..574bdaaad 100644
--- a/src/ast/sls/sls_smt_plugin.h
+++ b/src/ast/sls/sls_smt_plugin.h
@@ -186,6 +186,6 @@ namespace sls {
             m_new_clause_added = true;
         }
         void force_restart() override { m_ddfw->force_restart(); }
-        unsigned timestamp(sat::bool_var v) override { return m_ddfw->timestamp(v); }
+        uint64_t timestamp(sat::bool_var v) override { return m_ddfw->timestamp(v); }
     };
 }
diff --git a/src/ast/sls/sls_smt_solver.cpp b/src/ast/sls/sls_smt_solver.cpp
index d92970a04..cd41f3f12 100644
--- a/src/ast/sls/sls_smt_solver.cpp
+++ b/src/ast/sls/sls_smt_solver.cpp
@@ -102,7 +102,7 @@ namespace sls {
         void add_input_assertion(expr* f) { m_context.add_input_assertion(f); }
         reslimit& rlimit() override { return m_ddfw.rlimit(); }
         void shift_weights() override { m_ddfw.shift_weights(); }
-        unsigned timestamp(sat::bool_var v) override { return m_ddfw.timestamp(v); }
+        uint64_t timestamp(sat::bool_var v) override { return m_ddfw.timestamp(v); }
 
         void force_restart() override { m_ddfw.force_restart(); }
 
diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp
index b11b1ecde..f590cf3b1 100644
--- a/src/math/polynomial/upolynomial.cpp
+++ b/src/math/polynomial/upolynomial.cpp
@@ -301,7 +301,8 @@ namespace upolynomial {
 
     void core_manager::sub(unsigned sz1, numeral const * p1, unsigned sz2, numeral const * p2, numeral_vector & buffer) {
         sub_core(sz1, p1, sz2, p2, m_basic_tmp);
-        buffer = std::move(m_basic_tmp);
+        // buffer = std::move(m_basic_tmp);
+        buffer.swap(m_basic_tmp);
     }
 
     // buffer := p1 * p2
@@ -342,7 +343,8 @@ namespace upolynomial {
 
     void core_manager::mul(unsigned sz1, numeral const * p1, unsigned sz2, numeral const * p2, numeral_vector & buffer) {
         mul_core(sz1, p1, sz2, p2, m_basic_tmp);
-        buffer = std::move(m_basic_tmp);
+        // buffer = std::move(m_basic_tmp);
+        buffer.swap(m_basic_tmp);
     }
 
     // buffer := dp/dx
diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp
index 1a6583c9f..c88f15e0f 100644
--- a/src/nlsat/levelwise.cpp
+++ b/src/nlsat/levelwise.cpp
@@ -155,7 +155,7 @@ namespace nlsat {
         // Every root function on each side must be connected to the boundary through edges.
         bool relation_invariant() const {
             auto const& rfs = m_rel.m_rfunc;
-            unsigned n = rfs.size();
+            auto n = rfs.size();
             if (n == 0) return true;
 
             // Build adjacency list from pairs (using ps_idx)
@@ -602,7 +602,7 @@ namespace nlsat {
 
         void fill_relation_pairs_for_section_biggest_cell() {
             auto const& rfs = m_rel.m_rfunc;
-            unsigned n = rfs.size();
+            auto n = rfs.size();
             if (n == 0)
                 return;
             SASSERT(is_set(m_l_rf));
@@ -624,7 +624,7 @@ namespace nlsat {
         // K = lower rfunc positions, f = upper rfunc positions
         void build_both_side_spanning_tree() {
             auto const& rfs = m_rel.m_rfunc;
-            unsigned n = rfs.size();
+            auto n = rfs.size();
             SASSERT(n > 0 && is_set(m_l_rf) && is_set(m_u_rf));
             SASSERT(!is_section());
             SASSERT(!same_boundary_poly());
@@ -695,7 +695,7 @@ namespace nlsat {
             
             // Check arborescence invariants (used in debug via SASSERT)
             DEBUG_CODE(
-            unsigned lower_root_idx = both.size() - 1;
+            auto lower_root_idx = both.size() - 1;
             auto arb_invariant = [&]() {
                 // Reconstruct parent[] from the algorithm logic
                 std_vector<unsigned> parent(both.size(), UINT_MAX);