I am trying to isolate a smaller smt file to post

I set a memory_high_watermark_mb to control how much memory usage from Python side. During solver.check(), i did encounter the watermark being passed but instead of a z3. instead of check() termiantes with unknown, process actually crash with this on output

libc++abi: terminating due to uncaught exception of type smt::cancel_exception: smt-canceled