Bound Z3 memory in testTimeout

Z3 only checks its `timeout` parameter at internal checkpoints. On the
quantified array query in this test it allocates roughly 400 MB/s of native
memory before reaching one, so the check grew to ~14 GB and the test JVM was
killed by the OS (`finished with non-zero exit value 137`). The test worker
runs with -Xmx512m, so none of that is heap.

On CI this consumed the whole runner - 16 GB plus swap - and GitHub reported
it as "The operation was canceled" on whichever task Gradle had last printed,
which made it look like an infrastructure problem rather than a test.

This is not specific to the recent Z3 upgrade: measured over 8 runs at
4 CPU / 6 GB, the previous Z3 dist failed 1/8 and the current one 2/8.

Bound Z3's memory for the duration of the check so it gives up cleanly with
UNKNOWN instead of taking the process down. The limit has to be the global
parameter: a solver parameter would not survive, because every check replaces
the solver parameters with the ones carrying the timeout.

12/12 runs pass at 4 CPU / 6 GB after this change.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>

Author: Saloed

ksmt-z3/ksmt-z3-core/src/test/kotlin/io/ksmt/solver/z3/IncrementalApiTest.kt

@@ -1,5 +1,6 @@
 package io.ksmt.solver.z3
 
+import com.microsoft.z3.Global
 import io.ksmt.KContext
 import io.ksmt.solver.KSolverStatus
 import io.ksmt.utils.mkConst
@@ -82,8 +83,43 @@ class IncrementalApiTest {
         val query = mkUniversalQuantifier(queryBody, listOf(x.decl))
         solver.assert(query)
 
-        val status = solver.checkWithAssumptions(emptyList(), timeout = 1.milliseconds)
+        val status = withZ3MemoryLimit(MEMORY_LIMIT_MB) {
+            solver.checkWithAssumptions(emptyList(), timeout = 1.milliseconds)
+        }
         assertEquals(KSolverStatus.UNKNOWN, status)
-        assertEquals("timeout", solver.reasonOfUnknown())
+
+        /**
+         * Normally Z3 reports the timeout. If it happens to reach the memory limit before
+         * its next timeout checkpoint it reports [Z3_OUT_OF_MEMORY_REASON] instead, which is
+         * an equally valid "gave up on the resource limit" outcome.
+         */
+        val reason = solver.reasonOfUnknown()
+        assertTrue(
+            reason == TIMEOUT_REASON || reason == Z3_OUT_OF_MEMORY_REASON,
+            "Unexpected reason of unknown: $reason"
+        )
+    }
+
+    /**
+     * Z3 only checks the [timeout] parameter at its internal checkpoints. On this query it
+     * allocates memory far faster than it reaches one, so without a memory limit the check
+     * grows to tens of gigabytes and the test process gets killed by the OS.
+     *
+     * The limit is a global Z3 parameter because a solver parameter would not survive:
+     * every check replaces the solver parameters with the ones holding the timeout.
+     */
+    private inline fun <T> withZ3MemoryLimit(limitMb: Int, body: () -> T): T = try {
+        Global.setParameter(Z3_MAX_MEMORY, limitMb.toString())
+        body()
+    } finally {
+        Global.setParameter(Z3_MAX_MEMORY, UNLIMITED_MEMORY)
+    }
+
+    companion object {
+        private const val Z3_MAX_MEMORY = "memory_max_size"
+        private const val UNLIMITED_MEMORY = "0"
+        private const val MEMORY_LIMIT_MB = 2048
+        private const val TIMEOUT_REASON = "timeout"
+        private const val Z3_OUT_OF_MEMORY_REASON = "out of memory"
     }
 }