[SwayamInSync]

Lean export runs no solver, yet --backend=lean, --lean-out, and --lean-project accepted every solver budget and ignored it. On main, each of --timeout, --collection-timeout, --certify-timeout, --function-timeout, --solver-rlimit, and --max-query-nodes leaves the output and the .lean file byte-identical, even --max-query-nodes=1, which on a solver backend rejects every module. A user who sets a budget for a Lean run gets no sign that it does nothing.

The change: resolveOptions (clang/tools/cpp-verify/Main.cpp) rejects any of these, and --int-encoding, which it already rejected, under the Lean backend, for source verification and archive replay alike. The error names the first one given:

$ cpp-verify --lean-out=goal.lean --timeout=60000 file.cpp --
error: --timeout requires a backend that runs an SMT solver

--lean-fallback runs Z3 or the strict portfolio first and accepts them all, as before.

Docs: the tooling page's table of options a run would not use gets the case, with a sentence listing every solver option. Each budget's entry in the options table says it is not accepted with Lean. The time-limits section says Lean runs no solver and that Lean certification gives each lake step 300 seconds, past which every result is Unresolved with reason lean.export-failed. The release notes' entry on unused options names the case.

Testing: backend_options.cpp adds each of the six budgets under --lean-out, --lean-project, --backend=lean, and Lean replay. It checks that no project or .lean file is written, and that Z3 and --lean-fallback accept the budgets. On main, exactly the nine new lines fail and the old ones pass. lean_backend_failure.cpp passed --timeout=1 to show that Lean export runs no solver; that is now the error itself, so the test drops the option and still checks that the export says Exported and contains no Z3 check. A matrix of all seven options under the four Lean modes gives the error, and under --backend=z3, cvc5, portfolio, race, bmc, --unroll, --lean-fallback, --lower-only, and Z3 replay gives the same verdicts as main.

Checked: Verify suite 423 passed, 1 unsupported. The change is in option checking only, so no verdict can change and no differential was run. After the rebase onto #39, the documentation examples pass and the site builds with -W.

With #48, --max-query-nodes bounds what is built for a function under every backend, Lean included, and --memory-limit is a new solver option. The two conflict in Main.cpp and tooling.rst. Whichever lands second gets rebased: --max-query-nodes leaves the list of solver-only options and --memory-limit joins it. The test line --lean-out ... --max-query-nodes becomes --memory-limit.