> For the complete documentation index, see [llms.txt](https://docs.runtimeverification.com/kontrol/llms.txt). Markdown versions of documentation pages are available by appending `.md` to page URLs; this page is available as [Markdown](https://docs.runtimeverification.com/kontrol/glossary/kontrol-prove-flags.md).

# Kontrol Prove Flags

| Flag                                     | Description                                                                                                                                                                                                                                      |
| ---------------------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ |
| `-h`, `--help`                           | Show this help message and exit                                                                                                                                                                                                                  |
| `--verbose`, `-v`                        | Verbose output.                                                                                                                                                                                                                                  |
| `--debug`                                | Debug output.                                                                                                                                                                                                                                    |
| `--workers WORKERS`, `-j WORKERS`        | Number of processes to run in parallel.                                                                                                                                                                                                          |
| `-I INCLUDES`                            | Directories to lookup **K** definitions in.                                                                                                                                                                                                      |
| `--main-module MAIN_MODULE`              | Name of the main module.                                                                                                                                                                                                                         |
| `--syntax-module SYNTAX_MODULE`          | Name of the syntax module.                                                                                                                                                                                                                       |
| `--md-selector MD_SELECTOR`              | Code selector expression to use when reading markdown.                                                                                                                                                                                           |
| `--depth DEPTH`                          | Maximum depth to execute to.                                                                                                                                                                                                                     |
| `--definition DEFINITION_DIR`            | Path to definition to use.                                                                                                                                                                                                                       |
| `--debug-equations DEBUG_EQUATIONS`      | Comma-separate list of equations to debug.                                                                                                                                                                                                       |
| `--always-check-subsumption`             | Check subsumption even on non-terminal nodes (default, experimental).                                                                                                                                                                            |
| `--no-always-check-subsumption`          | Do not check subsumption on non-terminal nodes (experimental).                                                                                                                                                                                   |
| `--fast-check-subsumption`               | Use fast-check on k-cell to determine subsumption (experimental).                                                                                                                                                                                |
| `--smt-timeout SMT_TIMEOUT`              | Timeout in ms to use for SMT queries.                                                                                                                                                                                                            |
| `--smt-retry-limit SMT_RETRY_LIMIT`      | Number of times to retry SMT queries with scaling timeouts.                                                                                                                                                                                      |
| `--smt-tactic SMT_TACTIC`                | Z3 tactic to use when checking satisfiability. Example: (check-sat-using smt)                                                                                                                                                                    |
| `--trace-rewrites`                       | Log traces of all simplification and rewrite rule applications.                                                                                                                                                                                  |
| `--kore-rpc-command KORE_RPC_COMMAND`    | Custom command to start RPC server.                                                                                                                                                                                                              |
| `--use-booster`                          | Use the booster RPC server instead of kore-rpc (default).                                                                                                                                                                                        |
| `--no-use-booster`                       | Do not use the booster RPC server instead of kore-rpc.                                                                                                                                                                                           |
| `--port PORT`                            | Use existing RPC server on named port.                                                                                                                                                                                                           |
| `--maude-port MAUDE_PORT`                | Use existing Maude RPC server on named port.                                                                                                                                                                                                     |
| `--bug-report BUG_REPORT`                | Generate bug report with given name                                                                                                                                                                                                              |
| `--break-every-step`                     | Store a node for every EVM opcode step (expensive).                                                                                                                                                                                              |
| `--break-on-jumpi`                       | Store a node for every EVM jump opcode.                                                                                                                                                                                                          |
| `--break-on-calls`                       | Store a node for every EVM call made.                                                                                                                                                                                                            |
| `--no-break-on-calls`                    | Do not store a node for every EVM call made (default).                                                                                                                                                                                           |
| `--break-on-storage`                     | Store a node for every EVM SSTORE/SLOAD made.                                                                                                                                                                                                    |
| `--break-on-basic-blocks`                | Store a node for every EVM basic block (implies --break-on-calls).                                                                                                                                                                               |
| `--max-depth MAX_DEPTH`                  | Maximum number of K steps before the state is saved in a new node in the CFG. Branching will cause this to happen earlier.                                                                                                                       |
| `--max-iterations MAX_ITERATIONS`        | Number of times to expand the next pending node in the CFG.                                                                                                                                                                                      |
| `--failure-information`                  | Show failure summary for all failing tests (default).                                                                                                                                                                                            |
| `--no-failure-information`               | Do not show failure summary for failing tests.                                                                                                                                                                                                   |
| `--auto-abstract-gas`                    | Automatically extract gas cell when infinite gas is enabled.                                                                                                                                                                                     |
| `--counterexample-information`           | Show models for failing nodes (default).                                                                                                                                                                                                         |
| `--fail-fast`                            | Stop execution on other branches if a failing node is detected (default).                                                                                                                                                                        |
| `--no-fail-fast`                         | Continue execution on other branches if a failing node is detected.                                                                                                                                                                              |
| `--foundry-project-root FOUNDRY_ROOT`    | Path to Foundry project root directory.                                                                                                                                                                                                          |
| `--match-test TESTS`                     | Specify contract function(s) to test using a regular expression. This will match functions based on their full signature, e.g., 'ERC20Test.testTransfer(address,uint256)'. This option can be used multiple times to add more functions to test. |
| `--reinit`                               | Reinitialize CFGs even if they already exist.                                                                                                                                                                                                    |
| `--bmc-depth BMC_DEPTH`                  | Enables bounded model checking. Specifies the maximum depth to unroll all loops to.                                                                                                                                                              |
| `--run-constructor`                      | Include the contract constructor in the test execution.                                                                                                                                                                                          |
| `--use-gas`                              | Enables gas computation in KEVM.                                                                                                                                                                                                                 |
| `--break-on-cheatcodes`                  | Break on all Foundry rules.                                                                                                                                                                                                                      |
| `--init-node-from DEPLOYMENT_STATE_PATH` | Path to JSON file containing the deployment state of the deployment process used for the project.                                                                                                                                                |
| `--include-summary INCLUDE_SUMMARIES`    | Specify a summary to include as a lemma.                                                                                                                                                                                                         |
| `--with-non-general-state`               | Flag used by Simbolik to initialise the state of a non test function as if it was a test function.                                                                                                                                               |
| `--xml-test-report`                      | Generate a JUnit XML report                                                                                                                                                                                                                      |
| `--cse`                                  | Use Compositional Symbolic Execution                                                                                                                                                                                                             |
| `--hevm`                                 | Use hevm success predicate instead of foundry to determine if a test is passing.                                                                                                                                                                 |