Skip to content

Commit

Permalink
remove likely culprit for Z3Prover#5493
Browse files Browse the repository at this point in the history
@zwimer: I had to remove a different move constructor before in the same API due to a different bug that the coverage tool exposed. I was unable to reproduce the bug reported in Z3Prover#5493 in my environment, but the interaction with reference counting and move constructors is sufficiently opaque that I rather not have to fix more bugs introduced with move constructors in the API. I am therefore removing also this use of && and maybe this fixes Z3Prover#5493
  • Loading branch information
NikolajBjorner committed Aug 20, 2021
1 parent d0e2108 commit 15e3e81
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion src/api/c++/z3++.h
Original file line number Diff line number Diff line change
Expand Up @@ -507,7 +507,6 @@ namespace z3 {
ast(context & c):object(c), m_ast(0) {}
ast(context & c, Z3_ast n):object(c), m_ast(n) { Z3_inc_ref(ctx(), m_ast); }
ast(ast const & s) :object(s), m_ast(s.m_ast) { Z3_inc_ref(ctx(), m_ast); }
ast(ast && s) noexcept : object(std::forward<object>(s)), m_ast(s.m_ast) { s.m_ast = nullptr; }
~ast() { if (m_ast) Z3_dec_ref(*m_ctx, m_ast); }
operator Z3_ast() const { return m_ast; }
operator bool() const { return m_ast != 0; }
Expand Down

0 comments on commit 15e3e81

Please sign in to comment.