search

Z3Prover / z3

The Z3 Theorem Prover
Other
9.96k stars 1.46k forks source link

conflicts with libgc #7253

Closed KuiWei004 closed 2 weeks ago

KuiWei004 commented 3 weeks ago

I use z3-solver as a library in my c++ project, but it crashed occasionally. The crash point is always the destructor in z3-ast or z3-solver. I think the reason may be that before the destructor works, the libgc has collected the corresponding mem, so when the destructor works, it will delete a null pointer.

KuiWei004 commented 2 weeks ago

Is there any way to disable the mem-manager of z3? I'd like to let z3 use the malloc function overrided by libgc.

NikolajBjorner commented 2 weeks ago

memory manager code is here:

https://github.com/Z3Prover/z3/blob/master/src/util/memory_manager.cpp

it uses different libraries depending on compilation flags.