diff --git a/src/util/scoped_numeral.h b/src/util/scoped_numeral.h
index b90ba640a..f70f5f185 100644
--- a/src/util/scoped_numeral.h
+++ b/src/util/scoped_numeral.h
@@ -28,8 +28,8 @@ private:
     numeral   m_num;
 public:
     _scoped_numeral(Manager & m):m_manager(m) {}
-    _scoped_numeral(_scoped_numeral const & n):m_manager(n.m_manager) { m().set(m_num, n.m_num); }
-    _scoped_numeral(_scoped_numeral &&) = default;
+    _scoped_numeral(_scoped_numeral const& n) :m_manager(n.m_manager) { m().set(m_num, n.m_num); }
+    _scoped_numeral(_scoped_numeral && n) noexcept: m_manager(n.m_manager) { m().swap(m_num, n.m_num); }
     ~_scoped_numeral() { m_manager.del(m_num); }
 
     Manager & m() const { return m_manager; }