# How can I reuse SMT solver results across runs?

Reuse Z3 results across processes and restarts with Sail’s persistent SMT-LIB cache.

Author: Jeffrey Kent
Canonical: https://jeffreykent.dev/answers/reuse-smt-results/
Published: 2026-11-01
Updated: 2026-11-01
Source: https://github.com/Chelis-Lang/sail/blob/main/docs/runtime.md
Source revision: b7666c37d305efdb2a3ed34af6f3dd41d9539495

If your application keeps sending Z3 the same SMT-LIB scripts, run those queries through [Sail](/software/sail/). When a script and its execution settings match a cached run, Sail returns the stored solver output. A cache hit avoids another Z3 run.

The cache lives on disk, so reuse works across separate processes and application restarts. Results retain any model or unsat core you requested. Use Sail from the CLI or as a shared service, without keeping one solver session open. The [SMT runtime guide](https://github.com/Chelis-Lang/sail/blob/main/docs/runtime.md) shows how to submit queries.