MAZE 1.2.3

MAZE 1.2.3 preserves the time reserved for generating tests from unfinished symbolic paths. Expensive solver queries now stop at the exploration deadline so finalization can use the remaining budget.

Downloads

• Linux ARM64: maze-1.2.3-linux-arm64.tar.gz
• Linux x86-64: maze-1.2.3-linux-amd64.tar.gz
• Each archive has a .sha256 checksum file.

Packages include MAZE, its Java dependencies, Z3 4.13.3 native libraries, a launcher, and extension examples. They require Linux with glibc and Java 21 or newer; use a JDK to compile subjects or extensions. No Maven or separate Z3 installation is needed.

Unpack and run ./maze --help. On macOS or Windows, use a Java Docker container with Linux-container mode.

Changes

• Enforce the symbolic exploration deadline during constraint solving and candidate replay, protecting the existing 30% finalization reserve.
• Preserve the active symbolic candidate when exploration runs out of time and generate tests from pending paths within the remaining overall budget.
• Remove the search-time extension that could consume the finalization reserve.
• Keep concrete-driven execution's deadline behavior and unlimited runs unchanged.

Updating CLI scripts

Existing commands and options remain valid. Time-limited symbolic runs can produce different suites because exploration now yields to finalization at the intended boundary. Protecting finalization time can reduce coverage on subjects that benefit more from continued exploration, especially with short budgets. The overall search budget is unchanged. Initialization and final output still add wall time, and the solver timeout does not replace an external watchdog for arbitrary subject execution.

Validation

The full test suite passed: 1,178 tests, zero failures/errors, 31 skipped. Regression checks exercise solver deadlines and verify the transition to unfinished-path test generation while retaining tests completed earlier in the run.

Both downloadable archives passed generation, extension, generated-suite and failure-reporting checks in fresh, network-disabled Java containers without a separate Z3 installation. Linux ARM64 was checked natively on Apple Silicon; Linux x86-64 was checked under emulation.

Six formerly empty HeapSort/DFS cases (three at 10 seconds and three at 60 seconds, retaining their seeds and inputs) all produced executable suites covering 26/26 branches. Six other subject checks completed successfully; five matched their original branch coverage. A separate comparison found TriangleClassifier/DFS covering 47/66 branches with 1.2.2 versus 45/66 with 1.2.3 in each of three 10-second cases; both versions reached 66/66 at 60 seconds. These checks illustrate the budget-allocation tradeoff and are release validation, not paper observations.