-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. |