External solver

Every proof ends in a solver. The default is the engine’s built-in MiniSat, which is fine for most things. A few proofs solve much faster on a different backend, and you can pick one per proof with @BmcProof(solver = "...") or project-wide in the plugin config.

The options

• "kissat" is a fast SAT solver bundled with the engine, so there’s nothing to install. It applies only to numeric and boolean proofs with no text, where it is typically several times faster. bmc4j checks a proof is text-free before using it and falls back to the default solver otherwise, because it can’t reason about strings soundly.
• "z3", "cvc5", "boolector", "cvc4" are SMT solvers. They must be on your PATH (or point at them with solverPath). They can win on proofs heavy in arrays or bit-level arithmetic.

String proofs stay on the default solver

The fast and external SAT solvers are single-shot: they take one formula and solve it. String refinement, the default for string proofs, doesn’t work that way. It solves in a loop, adding constraints as it goes, which a single-shot external solver can’t take part in. So while string refinement is on, a proof that uses strings runs on the engine’s default solver, not the external one. If you want the fast solver on code that pushes string data around, switch that proof to the char-array string mode, which turns refinement off.

Before you reach for it

A faster solver helps, but it rarely fixes a proof that is hard because of its input space. Narrowing what the proof has to consider, with domain splitting or a tighter unwind bound, usually beats swapping the backend. Use profiling to confirm the solver is actually where the time goes first.