Hi, I am running z3 4.14.1 via the Java API (using https://github.com/tudo-aqua/z3-turnkey). It worked fine for contexts over 4GB until the moment I've added non-linear constraints. Now, when z3 reaches "max memory" to be approximately 4GB, I get:

error: max. memory exceeded

This happens on a local 64-bit Linux machine equipped 128GB of memory. There is definitely plenty of resident memory left. I tried to track it down, and it seems to me that this line does not convert the default value of 4294967295 to megabytes, as the other modules do:

Can it be that the default max memory is limited to 4GB in nlsat?