Laurel User Guide

9.3. Useful verification flags🔗

laurelAnalyze and laurelAnalyzeBinary share the verification flag set. strata laurelAnalyze --help is the authoritative list; the ones that come up most are:

Flag

Effect

--keep-all-files DIR

Write every Laurel and Core pipeline stage under DIR.

--vc-directory DIR

Keep the generated SMT-LIB files in DIR.

--no-solve

Generate SMT-LIB without invoking a solver. Requires --vc-directory.

--solver NAME

Choose the solver executable. Defaults to cvc5.

--solver-timeout SECONDS

Per-invocation solver timeout. Defaults to 10.

--stop-on-first-error

Stop after the first failing obligation instead of reporting all of them.

--profile

Print elapsed time per pipeline step — the first thing to try when a run is slow.

--check-mode MODE

deductive (default), bugFinding, or bugFindingAssumingCompleteSpec.

--check-level LEVEL

minimal (default), minimalVerbose, or full; controls how many checks are emitted.

--overflow-checks LIST

Comma-separated signed, unsigned, float64, all, none.

--parallel N

Run N solver workers concurrently.

--set-option NAME=VALUE

Pass a solver-specific SMT option through verbatim. Repeatable.

Note that supplying --overflow-checks starts from all checks disabled and then applies the listed tokens left to right, so --overflow-checks unsigned turns the default signed check off.

The interpreter commands deliberately accept none of these — they never invoke a solver — and take only --fuel N (a step limit), --entry PROC (run one named procedure instead of the ones marked entry), and --keep-all-files.