mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

add explicit move constructor to deal with unit test regression test-z3 algebraic on Windows/debug -

Browse source 
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.
This commit is contained in:
Nikolaj Bjorner 2024-01-20 12:59:32 -08:00
parent a2993f7457
commit 548be4c1f9
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/util/scoped_numeral.h
View file

@ -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; }