Address or state predicates to discard before further exploration.

Call-handling policy.

Maximum visits allowed at the same address. Zero means unlimited.

Maximum instructions to execute per path. Zero means unlimited.

Maximum number of states to expand. Zero means unlimited.

Enable solver-backed infeasible path pruning.

Query to answer.

Symbolic values to extract for satisfiability queries.

Maximum milliseconds to spend in Run. Zero means unlimited.

Solver backend used for path queries and optional pruning.

Stop exploration as soon as the first query answer is found.

Half-open address ranges [start, finish) to pre-lift before Run. Empty means no pre-lifting.

Adds one avoid condition.

Adds one address to the avoid set.

Adds addresses to the avoid set.

Adds one state predicate to the avoid conditions.

Adds all symbolic bytes of the given buffer to value extraction.

Adds all symbolic bytes of the given buffers to value extraction.

Adds one symbolic value to solver value extraction.

Adds symbolic values to solver value extraction.

Disables solver-backed infeasible path pruning.

Continues exploration after finding a query answer.

Enables solver-backed infeasible path pruning.

Stops exploration as soon as the first query answer is found.

Follows direct internal calls without using external-call hooks.

Registers a call hook and enables hook-based call handling.

Registers call hooks and enables hook-based call handling.

Stops before evaluating call instructions.

Uses the given avoid condition.

Replaces the avoid set.

Uses a prepared call hook registry for external-call dispatch.

Uses the given query expression for solver value extraction.

Uses the given symbolic values for solver value extraction.

Uses the given solver backend.

Uses the given half-open address ranges for pre-lifting.