mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-09 23:53:25 +00:00
Code Activity

fix #5795

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-01-27 10:45:38 -08:00
parent 461e71017d
commit a621041308
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2627,7 +2627,8 @@ namespace z3 {
Z3_solver m_solver; Z3_solver m_solver;
void init(Z3_solver s) { void init(Z3_solver s) {
m_solver = s; m_solver = s;
Z3_solver_inc_ref(ctx(), s); if (s)
Z3_solver_inc_ref(ctx(), s);
} }
public: public:
struct simple {}; struct simple {};
@ -2636,7 +2637,7 @@ namespace z3 {
solver(context & c, simple):object(c) { init(Z3_mk_simple_solver(c)); } 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, 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, 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(solver const & s):object(s) { init(s.m_solver); }
~solver() { Z3_solver_dec_ref(ctx(), m_solver); } ~solver() { Z3_solver_dec_ref(ctx(), m_solver); }
operator Z3_solver() const { return m_solver; } operator Z3_solver() const { return m_solver; }