Z3.jl icon indicating copy to clipboard operation
Z3.jl copied to clipboard

Segfault with jemalloc

Open remysucre opened this issue 8 months ago • 0 comments

When using LD_PRELOAD to use jemalloc as the memory allocator, Z3 calls malloc_usable_size from glibc instead of jemalloc, triggering a segfault. To reproduce on linux, run LD_PRELOAD=$JEMALLOC_LIB julia --project where $JEMALLOC_LIB is the path to jemalloc, then run the following in the REPL:

malloc_usable_size(ptr::Ptr{Cvoid}) = ccall(:malloc_usable_size, Csize_t, (Ptr{Cvoid},), ptr)
ptr = ccall(:malloc, Ptr{Cvoid}, (Csize_t,), 1024)
size = malloc_usable_size(ptr)
println("Usable size of allocated memory: ", size)

Z3 is known to not work well with third party allocators, and one workaround is to disable HAS_MALLOC_USABLE_SIZE to remove the calls to malloc_usable_size.

remysucre avatar Jun 12 '24 22:06 remysucre