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.