Profiling

When a proof is slow, guessing at the cause wastes time. Add @BmcProfile and the engine prints a per-stage breakdown alongside the verdict, so you can tune the part that actually matters.

@BmcProof
@BmcProfile
fun `the slow one`() { ... }

It is read from output the engine already produces, so it costs nothing and never changes the verdict. It is most useful on a proof that times out: the breakdown is parsed from whatever ran before the kill, which tells you how far it got.

Phase timing

The engine runs in three phases, in order:

• Symex (symbolic execution) runs the bytecode and unwinds loops. Time here means lots of paths or iterations.
• Convert SSA turns that into the logic formula. Time here means the formula is big to build.
• Solver is the SAT or SMT search. Time here means the formula is hard to solve.

The single most useful signal, especially on a timeout, is which phase it stopped in, in other words whether the solver was ever reached. A proof killed during Symex never got near the solver, so a faster solver won’t help; the loops are the problem.

Loop unwinding by method

A top-offenders list of which methods’ loops were unwound and how many times, with a per-loop breakdown down to the source line (recursion is listed the same way). The method at the top is the hot one. That is where a tighter unwind bound or domain splitting pays off.

Formula size

• Program expression size is how big the unrolled program got.
• VCCs generated, and how many remain after simplification, are the checks the engine has to discharge.
• SAT variables and clauses are the size of what the solver actually worked on (only shown once the solver is reached).

Watching these climb as you raise the unwind bound is the usual sign that the formula, not the code, is what got away from you.