mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

operator= checks this equality before moving (#5265)

Browse source
This commit is contained in:
Zachary Wimer 2021-05-12 13:10:14 -07:00 committed by GitHub
parent 7869cdbbc8
commit f942c3df91
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/api/c++/z3++.h
View file

@ -511,9 +511,11 @@ namespace z3 {
return *this; return *this;
} }
ast & operator=(ast && s) noexcept { ast & operator=(ast && s) noexcept {
object::operator=(std::forward<object>(s)); if (this != &s) {
m_ast = s.m_ast; object::operator=(std::forward<object>(s));
s.m_ast = nullptr; m_ast = s.m_ast;
s.m_ast = nullptr;
}
return *this; return *this;
} }
Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; } Z3_ast_kind kind() const { Z3_ast_kind r = Z3_get_ast_kind(ctx(), m_ast); check_error(); return r; }