From 548be4c1f92447fa45e283c2903bb3ea939909bb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 20 Jan 2024 12:59:32 -0800 Subject: [PATCH] add explicit move constructor to deal with unit test regression test-z3 algebraic on Windows/debug - it uses copy constructor instead of move when returning a scoped_anum in functions such as power and root. This leads to freeing memory that gets passed as return value. The copy constructor for scoped_numeral is also suspicious because it doesn't ensure memory ownership. --- src/util/scoped_numeral.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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; }