merlin

Glad it helped!

@NikolajBjorner Thank you for the response. The full stack trace is quite long, so I’ve attached it here for your convenience. The Z3 commit in use is: https://github.com/Z3Prover/z3/commit/423930dbadb68540ee18681e76f249b0774fedcc. [stack.txt](https://github.com/user-attachments/files/20805894/stack.txt)

Thanks for looking into this! I was able to trigger the memory leak on https://github.com/Z3Prover/z3/commit/a3c8bbb461b80bc6d35499b8224585aa330ed678 using the following configuration: ``` CFLAGS+="-fsanitize=address -fsanitize-recover=address -U_FORTIFY_SOURCE -fno-omit-frame-pointer -fno-common" LDFLAGS+="-fsanitize=address" python3 scripts/mk_make.py -d ```...

Cool!

Hi, @snova-nathanz I believe Nikolaj was referring specifically to the memory leak fix. The inconsistency issue still appears to be unresolved.

I've just realized that this case involves non-linear arithmetic. If that makes the report out of scope, please feel free to close it.