Per-context, per-solver, or per-thread memory limit

[rhelmot]

I'm looking to assert one of the above memory limits on z3, so that I can explore a state space and prune the states that take too much memory to solve. I found that solver can take a max_memory parameter, but it seems to set a per-process memory limit rather than any of the scopes I'm looking for. Is such a thing implemented? Is such a thing compatible with z3's architecture?

[NikolajBjorner]

The memory manager module handles the interface to memory footprints.
It does not have a per-thread memory allocation interface.
Given that the memory manager has issues with 16 byte architectures as well, the proper approach seems to be to replace the underlying implementation under memory_manager with something more consequential.
Mimalloc may have the appropriate interfaces and be a good allocator and OS portable for these purposes.
Some amount of tuning went into avoiding contention when keeping track of global memory footprint.
Mimalloc should be next level around such things.