diff --git a/src/ast/sls/sls_bv_tracker.h b/src/ast/sls/sls_bv_tracker.h
index 7c9b02a46..37ef91480 100644
--- a/src/ast/sls/sls_bv_tracker.h
+++ b/src/ast/sls/sls_bv_tracker.h
@@ -42,8 +42,37 @@ class sls_tracker {
     struct value_score {
         value_score() : value(unsynch_mpz_manager::mk_z(0)) {};
         value_score(value_score&&) noexcept = default;
+        value_score(const value_score &other) {
+            m = other.m;
+            if (other.m && !unsynch_mpz_manager::is_zero(other.value)) {
+                m->set(value, other.value);
+            }
+            score = other.score;
+            score_prune = other.score_prune;
+            has_pos_occ = other.has_pos_occ;
+            has_neg_occ = other.has_neg_occ;
+            distance = other.distance;
+            touched = other.touched;
+        }
         ~value_score() { if (m) m->del(value); }
         value_score& operator=(value_score&&) = default;
+        value_score &operator=(const value_score &other) {
+            if (this != &other) {
+                if (m)
+                    m->del(value);
+                m = other.m;
+                if (other.m && !unsynch_mpz_manager::is_zero(other.value)) {
+                    m->set(value, other.value);
+                }
+                score = other.score;
+                score_prune = other.score_prune;
+                has_pos_occ = other.has_pos_occ;
+                has_neg_occ = other.has_neg_occ;
+                distance = other.distance;
+                touched = other.touched;
+            }
+            return *this;
+        }
         unsynch_mpz_manager * m = nullptr;
         mpz value;
         double score = 0.0;
diff --git a/src/util/obj_hashtable.h b/src/util/obj_hashtable.h
index c59f87696..cf7cdff05 100644
--- a/src/util/obj_hashtable.h
+++ b/src/util/obj_hashtable.h
@@ -61,6 +61,10 @@ public:
         key_data() {}
         key_data(Key *key) : m_key(key) {}
         key_data(Key *k, Value const &v) : m_key(k), m_value(v) {}
+        key_data(key_data &&kd) noexcept = default;
+        key_data(key_data const &kd) noexcept = default;
+        key_data &operator=(key_data const &kd)  = default;
+        key_data &operator=(key_data &&kd) = default;
         Value const & get_value() const { return m_value; }
         Key & get_key () const { return *m_key; }
         unsigned hash() const { return m_key->hash(); }