From 5327e90479ef29452130fac4e906f4b95342c6fa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Aurea=20B=C3=ADl=C3=A1?= Date: Tue, 29 Sep 2026 15:13:26 +0200 Subject: [PATCH] add @prover annotation --- src/language-annotations.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/language-annotations.md b/src/language-annotations.md index 4d2a0e0..37549ed 100644 --- a/src/language-annotations.md +++ b/src/language-annotations.md @@ -52,6 +52,7 @@ Various other annotations serve as hints to a specific verification backend; bac * `@exhaleMode("n")` on a method: overrides the exhale mode used to verify this method (corresponding to the `--exhaleMode` command-line option). * `@moreJoins("n")` on a method: joins verification paths after branches instead of exploring them separately (corresponding to `--moreJoins`), which can speed up verification of methods with many branches. -* `@stateConsolidationMode("n")` on a method: selects the state consolidation mode used for this method (corresponding to `--stateConsolidationMode`). +* `@prover("name")` on a method: restricts the prover(s) used to verify this method (corresponding to the `--prover` command-line option). * `@proverConfigArgs("key=value")` on a method: passes additional configuration options to the SMT solver while verifying this method (corresponding to `--proverConfigArgs`). +* `@stateConsolidationMode("n")` on a method: selects the state consolidation mode used for this method (corresponding to `--stateConsolidationMode`). * `@weight("n")` on a quantifier: sets the weight of the quantifier in the SMT encoding, which influences how eagerly the SMT solver instantiates it (higher weights mean fewer instantiations).