Impact: every verifier JVM leaves about 30 MB in the temp directory if it does not exit normally. On a shared VM this filled the 61 GB disk on 2026-09-30, when 1,277 folders had built up. Even shell output then failed with ENOSPC. Today (2026-11-11) there were 16 leftover folders again (466 MB). Not urgent for the study, but it builds up for anyone who runs the language server or the verifier often.

Cause: the verifier gets Z3 from tools.aqua:z3-turnkey 4.8.17 (version.z3 in liquidjava-verifier/pom.xml). When it loads, com.microsoft.z3.Z3Loader.loadZ3():

1. creates Files.createTempDirectory("z3-turnkey"), i.e. ${java.io.tmpdir}/z3-turnkey<random>;
2. unpacks libz3.so and libz3java.so (~30 MB) into it;
3. marks the folder and both files with File.deleteOnExit(), then System.loads them.

deleteOnExit runs only on a normal JVM exit, so a JVM that is killed (SIGKILL, a timeout, a closed VS Code window, an MCP server whose session ends, a killed test run) leaves the folder behind. Each JVM unpacks a fresh copy, so nothing is ever reused.

Where it happens: any process that loads the verifier: the VS Code language server, the MCP server, CLI/batch runs (ljverify), and Maven test runs that time out.

Ideas to check:

• On Linux/macOS, delete the unpacked files right after System.load: the library stays mapped, so nothing is left even on SIGKILL. This needs either our own loader or a check that newer z3-turnkey versions do it.
• Reuse one unpacked copy per Z3 version and user (e.g. ~/.cache/liquidjava/z3-<version>/) instead of a fresh temp folder per JVM.
• At startup, delete stale z3-turnkey* folders whose libraries no live process has mapped. This is fragile and a last resort.
• In the language server, handle LSP shutdown/exit so that a normal close runs the deleteOnExit hooks.

Workaround until then: rm -rf /tmp/z3-turnkey* while no verifier is running, or give each JVM its own -Djava.io.tmpdir and delete it afterwards (as ljverify.py does).