Kontrol Prove Flags
-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.
Last updated