# 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. | --- # Agent Instructions: Querying This Documentation If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question. Perform an HTTP GET request on the current page URL with the `ask` query parameter: ``` GET https://docs.runtimeverification.com/kontrol/glossary/kontrol-prove-flags.md?ask= ``` The question should be specific, self-contained, and written in natural language. The response will contain a direct answer to the question and relevant excerpts and sources from the documentation. Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.