There is a reference count bug in the simple backend runtime.
In the _sym_push_path_constraint function, refcount of newConstraint is increased but never decreased.
I believe this leads to a memory leak. When I try to generate large path constraints, it eventually causes segmentation faults and significant performance degradation.
/* Assert the actual path constraint */
Z3_ast newConstraint = (taken ? constraint : not_constraint);
Z3_inc_ref(g_context, newConstraint); // refcount increase for newConstraint
Z3_solver_assert(g_context, g_solver, newConstraint);
assert((Z3_solver_check(g_context, g_solver) == Z3_L_TRUE) &&
"Asserting infeasible path constraint");
Z3_dec_ref(g_context, constraint);
Z3_dec_ref(g_context, not_constraint);
// no 'Z3_dec_ref(g_context, newConstraint);'p.s. symcc-rt is a submodule of this repository, but since this repository appears to manage symcc-rt as a whole, I decided to report the issue here. If this causes any problems, I can move it to the symcc-rt repository.
There is a reference count bug in the simple backend runtime.
In the
_sym_push_path_constraintfunction, refcount ofnewConstraintis increased but never decreased.I believe this leads to a memory leak. When I try to generate large path constraints, it eventually causes segmentation faults and significant performance degradation.
p.s. symcc-rt is a submodule of this repository, but since this repository appears to manage symcc-rt as a whole, I decided to report the issue here. If this causes any problems, I can move it to the symcc-rt repository.