From a6210413086c7889dac7752dddbe38e7b172f785 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Jan 2022 10:45:38 -0800 Subject: [PATCH] fix #5795 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 80432450d..b7547b990 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -2627,7 +2627,8 @@ namespace z3 { Z3_solver m_solver; void init(Z3_solver s) { m_solver = s; - Z3_solver_inc_ref(ctx(), s); + if (s) + Z3_solver_inc_ref(ctx(), s); } public: struct simple {}; @@ -2636,7 +2637,7 @@ namespace z3 { solver(context & c, simple):object(c) { init(Z3_mk_simple_solver(c)); } solver(context & c, Z3_solver s):object(c) { init(s); } solver(context & c, char const * logic):object(c) { init(Z3_mk_solver_for_logic(c, c.str_symbol(logic))); } - solver(context & c, solver const& src, translate): object(c) { init(Z3_solver_translate(src.ctx(), src, c)); } + solver(context & c, solver const& src, translate): object(c) { Z3_solver s = Z3_solver_translate(src.ctx(), src, c); check_error(); init(s); } solver(solver const & s):object(s) { init(s.m_solver); } ~solver() { Z3_solver_dec_ref(ctx(), m_solver); } operator Z3_solver() const { return m_solver; }