BMC Task Recipes

Use these recipes after completing Your First Bounded Model Check. Start in an empty working directory and download the task model there. Save each task’s short FBMCQ block under the filename shown by its command, then run that command from the same directory. The model is small on purpose:

bmc_tasks.fcstm

def int x = 0;

state Root {
    event Go;

    state Idle {
        during abstract Tick;
    }

    state Done;

    [*] -> Idle;
    Idle -> Done : Go;
}

It has one persistent variable, one event, one abstract during action, and one event-driven transition. The examples below show the direct CLI command first, then the complete short .fbmcq text to save, then the explanation, expected output, and failure boundary. A block that compares alternatives labels each alternative as a separate file.

How to choose a property kind

SAT has different meaning for witness properties and counterexample properties. Pick the query kind from the user question first, then read the solver status through that polarity.

BMC property selection guide
Kind	User intent	Quantification	SAT meaning	Use when
`reach`	Find at least one bounded execution where a predicate becomes true.	Existential over traces and frames.	A witness was found; property holds for the search goal.	You want a concrete path to a state, value, call, or event condition.
`forbid`	Reject any bounded execution that reaches a bad predicate.	Universal safety check encoded as counterexample search.	A counterexample was found; property is violated.	You know the unsafe condition and want CI to fail when it is reachable.
`invariant`	Require a predicate on every searched frame.	Universal over frames in every bounded trace.	A counterexample frame was found; property is violated.	You need a bounded safety condition, such as `x >= 0` always.
`must_reach`	Require every bounded execution to reach a predicate.	Universal over traces, existential over frames per trace.	A trace that never reaches the predicate was found; property is violated.	You need guaranteed bounded progress rather than one successful example.
`exists_always`	Find one execution where a predicate stays true for the whole bound.	Existential over traces, universal over frames on that trace.	A witness trace was found; property holds for the search goal.	You want to prove a stable scenario is possible, not mandatory.
`response`	Check that every trigger is followed by a response within a window.	Universal over trigger steps and bounded successor-frame windows.	A violating trigger was found; property is violated.	You need request/acknowledge, command/effect, or alarm/clear behavior.
`cover`	Hit a named transition case label.	Existential over traces and case labels.	A witness hit the case label.	You need coverage for a specific generated transition branch.

How to handle inconclusive outcomes

Use this table when the CLI exits 3 or when a JSON report has an outcome that is neither property_satisfied nor property_violated.

Timeout, unknown, and incomplete handling
Outcome	Where it appears	Meaning	First response
`timeout`	`result.status` and `result.outcome` can both be `timeout`.	Z3 did not finish a single `check()` within `--timeout-ms`.	Raise `--timeout-ms`, simplify assumptions, or reduce the bound; do not treat it as safe.
`unknown`	`result.status` may be `unknown` when the backend cannot decide.	The solver returned an indeterminate answer that is not SAT or UNSAT.	Inspect diagnostics, simplify the query, or lower the bound; do not use it as proof.
`incomplete`	`result.outcome` is `incomplete` and `result.incomplete` is true.	The primary objective was UNSAT, but the separate response-horizon check was SAT, `unknown`, `timeout`, or not run.	Inspect `result.incomplete_status`. Increase the bound for SAT; diagnose the solver or timeout for `unknown`/`timeout`.

How to read the task cards

Each task card includes a direct CLI command, the relevant query snippet, a short explanation, expected output, side effects, failure boundary, and a link to the reference page for exhaustive syntax or result facts. Solver verdicts are reports, including expected nonzero verdicts. Controlled input errors write a short message to stderr and do not create a partial report.

1. Run the chosen property kind

CLI. Replace reach.fbmcq with the query file for the property you chose.

python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q reach.fbmcq --json

FBMCQ. These are seven separate query files, not seven check clauses in one file. Every file starts with init state("Root.Idle"); and contains exactly one row from this table:

One `check` clause per property file
File	Clause after the common `init` line
`reach.fbmcq`	`check reach <= 1: active("Root.Idle");`
`forbid.fbmcq`	`check forbid <= 1: active("Root.Done");`
`invariant.fbmcq`	`check invariant <= 1: x == 0;`
`must_reach.fbmcq`	`check must_reach <= 1: active("Root.Idle");`
`exists_always.fbmcq`	`check exists_always <= 1: x == 0;`
`response.fbmcq`	`check response <= 1: trigger false -> within 1 active("Root.Done");`
`cover.fbmcq`	`check cover <= 1: case("Root.Idle::transition::Root.Done::0");`

What it does. The command asks one bounded question about the model. The query kind controls whether SAT means a positive witness or a counterexample. The shared hot-start line makes frame zero Root.Idle; it is required for the bound-one forbid and cover results shown below.

Expected output. For the direct reach command, JSON contains "kind": "reach", "status": "sat", "outcome": "witness_found", and "exit_code": 0. The verified fixture matrix is:

reach sat witness_found exit=0
forbid sat property_violated exit=1
invariant unsat property_satisfied exit=0
must_reach unsat property_satisfied exit=0
exists_always sat witness_found exit=0
response unsat property_satisfied exit=0
cover sat witness_found exit=0

File side effect. None unless you add -o.

Failure boundary. cover accepts only a naked, known, coverable case("...") label. A bounded result says nothing beyond the selected bound.

Reference. See FBMCQ Language Reference for exact property forms and Property Objectives, Definedness, and Bounds for their objectives.

2. Set a state and replace selected initializers

CLI.

python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q init_havoc_where.fbmcq --json

FBMCQ.

init state("Root.Idle") havoc { x } where x == 7;
check reach <= 1: x == 7;

What it does. The query starts from Root.Idle, removes only x from the initializer constraints, and constrains frame zero to x == 7.

Expected output. JSON contains "kind": "reach", "outcome": "witness_found", and a witness frame whose vars.x is 7; the exit status is 0.

File side effect. None; the report goes to stdout.

Failure boundary. where constrains initialization; it does not override an initializer. Without havoc { x }, this model’s x = 0 and where x == 7 make the trace formula UNSAT. havoc * removes every persistent initializer, so prefer a named set when possible.

Reference. See FBMCQ Language Reference for cold, state(...), terminated, havoc, and where legality.

3. Constrain frames and event inputs

CLI.

python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q assumptions.fbmcq --json \
    -o /tmp/bmc-assumptions.json

FBMCQ.

init state("Root.Idle");
assume always: x == 0;
assume event("Root.Go", 0) == false;
assume events cardinality at_most_one {"Root.Go"};
check invariant <= 1: x == 0;

What it does. The assumptions constrain x on every frame, disable Root.Go at step zero, and require at most one event from the selected event set.

Expected output. The payload reports invariant, unsat, property_satisfied, and exit 0. witness and replay are null because no counterexample exists under these assumptions.

File side effect. /tmp/bmc-assumptions.json is atomically created or replaced.

Failure boundary. Assumptions restrict the searched environment and can make an otherwise possible behavior disappear. Event paths are fully qualified; an unknown path is a binding error, not an UNSAT verdict.

Reference. See FBMCQ Language Reference for always, at, event selectors, ranges, and cardinality.

4. Match abstract calls and snapshots

CLI.

python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q calls.fbmcq --json \
    -o /tmp/bmc-calls.json

FBMCQ.

init state("Root.Idle");
check reach <= 1:
    called("Root.Idle.Tick", step=0, role="leaf_during", where x == 0)
    && call_count("Root.Idle.Tick", step=*) == 1;

What it does. The query selects the Root.Idle.Tick call at step zero, requires its runtime role, checks the call-time x snapshot, and counts the call within the one-step bound.

Expected output. Exit 0 with outcome equal to witness_found. The first witness step contains one abstract_calls record with action_name Root.Idle.Tick, role leaf_during, and snapshot.x equal to 0.

File side effect. /tmp/bmc-calls.json is atomically created or replaced.

Failure boundary. A call where expression sees the captured call-time variables; it cannot use frame atoms such as active() or nested call_count(). The CLI replay records abstract calls but installs no user handler that could mutate runtime state.

Reference. See FBMCQ Language Reference for every call filter key and allowed where expression.

5. Audit a human witness and replay

CLI.

python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q calls.fbmcq

FBMCQ.

init state("Root.Idle");
check reach <= 1:
    called("Root.Idle.Tick", step=0, role="leaf_during", where x == 0)
    && call_count("Root.Idle.Tick", step=*) == 1;

What it does. Human mode prints the same witness in a compact form and runs the mandatory replay trust gate before reporting success.

Expected output. The first line is BMC reach <= 1: PROPERTY HOLDS WITHIN BOUND; WITNESS FOUND. Solver: SAT follows as diagnostic evidence, Replay: verified reports the runtime trust gate, and the compact Trace lists source, target, selected case, events, and calls. The process exits 0. Use --color always to force ANSI terminal decoration or --color never for a stable plain-text transcript.

File side effect. None; the human summary goes to stdout. Use --json for the complete witness and replay records.

Failure boundary. A SAT decode or replay exception is an internal failure: it retains a traceback and exit 1 instead of emitting a partial report. A successfully constructed replay mismatch emits the complete report and exit 4. Replay checks runtime alignment; it is not an unbounded proof.

Reference. See BMC CLI and Result Protocol Reference for report sections, witness columns, replay mismatches, and exit precedence.

6. Gate CI with JSON and exit status

CLI.

python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q forbid.fbmcq --json \
    -o /tmp/bmc-ci.json

FBMCQ.

init state("Root.Idle");
check forbid <= 1: active("Root.Done");

What it does. This valid query intentionally finds a forbidden-state counterexample. It demonstrates a machine-readable report whose process exit is nonzero because the property is violated.

Expected output. The command exits 1 and still creates JSON containing "status": "sat", "outcome": "property_violated", and "exit_code": 1. CI should fail or allow that verdict according to project policy, but it must not confuse it with a CLI input error.

File side effect. /tmp/bmc-ci.json is created even though the verdict exit is 1.

Failure boundary. Exit 0 means a satisfied property or positive witness; 1 also covers controlled errors, distinguishable because those have stderr and no report; 2 is Click usage; 3 is inconclusive; 4 is a structured replay mismatch. Always inspect JSON when a report exists.

Reference. See BMC CLI and Result Protocol Reference for the full branch matrix and stable JSON schema.

7. Write a completed report atomically

CLI.

mkdir -p /tmp/pyfcstm-bmc
python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q invariant.fbmcq \
    --json -o /tmp/pyfcstm-bmc/result.json

FBMCQ.

init state("Root.Idle");
check invariant <= 1: x == 0;

What it does. The CLI writes a complete JSON payload through a same-directory temporary file, then replaces the target path.

Expected output. No stdout; the file contains "exit_code": 0.

File side effect. The target is atomically created or replaced. The parent directory must already exist.

Failure boundary. Parent directories are not created by pyfcstm bmc. If reading, compiling, solving internally, or writing fails before a complete payload exists, the command must not claim a successful output file.

Reference. See BMC CLI and Result Protocol Reference for overwrite, stdout, stderr, and UTF-8 rules.

8. Enforce a maximum bound policy

CLI.

python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q reach_bound_2.fbmcq \
    --max-bound 1

FBMCQ.

check reach <= 2: active("Root.Idle");

What it does. The query requests bound 2, while the command-line policy allows at most 1.

Expected output. stderr contains Failed to compile BMC query, query_bound=2, and max_bound=1; the command exits 1.

File side effect. None. With -o, no report would be created or modified because policy rejection happens before report construction.

Failure boundary. --max-bound is a pre-construction policy gate, not a request to silently clamp or truncate the query. Values below 1 are Click usage errors with exit 2.

Reference. See BMC CLI and Result Protocol Reference for CLI option and error classification details.

9. Apply a per-check solver timeout

CLI.

python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q reach_bound_2.fbmcq \
    --timeout-ms 1 --json -o /tmp/bmc-timeout.json

FBMCQ.

check reach <= 2: active("Root.Idle");

What it does. The command passes a one-millisecond timeout to each solver check(). This fixture normally reports a timeout on a loaded development machine, but very fast machines may produce a decisive result before the limit.

Expected output. On the verified run, the command exited 3 and JSON contained "timeout_ms": 1, "status": "timeout", and "outcome": "timeout". If the solve finishes first, the JSON still records "timeout_ms": 1 and uses the ordinary decisive exit.

File side effect. /tmp/bmc-timeout.json contains the completed verdict.

Failure boundary. The timeout is not a wall-clock budget for parsing, expansion, formula construction, or the whole CLI. response may execute a second incomplete-horizon check, also with the full timeout.

Reference. See BMC CLI and Result Protocol Reference for timeout fields and BMC solving, witnesses, and replay boundaries for the solve sequence.

10. Distinguish response violations from an incomplete horizon

CLI. Run the missing-response case first; use response_incomplete.fbmcq with the same command shape when you need the short-horizon case.

python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q response_missing.fbmcq --json \
    -o /tmp/bmc-response.json

FBMCQ file: response_missing.fbmcq

check response <= 1: trigger true -> within 1 false;

FBMCQ file: response_incomplete.fbmcq

check response <= 1: trigger true -> within 2 false;

What it does. The first query is a decisive violation: a trigger exists and no response can satisfy the one-step window. The second shape is inconclusive at bound 1 because a two-successor response window extends beyond the checked suffix.

Expected output. response_missing.fbmcq exits 1 with status sat and outcome property_violated. response_incomplete.fbmcq exits 3 with primary status unsat, outcome incomplete, incomplete true, and incomplete_status sat; witness and replay are null.

File side effect. The selected output file under /tmp is atomically created or replaced.

Failure boundary. Current outcome and witness schemas do not classify whether a decisive response counterexample came from an undefined trigger or from a defined trigger with no response; inspect the query and trace manually. Do not interpret primary UNSAT as satisfied until the suffix is closed. Raise the query bound for horizon coverage; timeout does not repair a short horizon.

Reference. See Property Objectives, Definedness, and Bounds for strict successor windows and BMC CLI and Result Protocol Reference for incomplete fields.

11. Diagnose parse, binding, and unsupported input

CLI.

python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q invalid_state.fbmcq

FBMCQ.

check reach <= 1: active("Root.Missing");

What it does. The query is syntactically valid but names a state that the model does not contain.

Expected output. stderr starts with Failed to compile BMC query and identifies Root.Missing; exit 1. stdout is empty.

File side effect. None. Adding -o /tmp/invalid.json still must not create a partial payload.

Failure boundary. A malformed .fbmcq fails during parsing; an unknown model object path fails during binding; a parsed but unsupported expression reports an unsupported query. These are controlled user-input errors. A traceback with an internal BMC sentinel is an implementation failure and should be reported as a bug rather than rewritten until it becomes UNSAT.

Reference. See FBMCQ Language Reference for legal and illegal forms and BMC CLI and Result Protocol Reference for error streams.

12. Choose an explanation depth

CLI.

python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q infeasible_two_values.fbmcq \
    --explain-infeasibility formal --color never

FBMCQ.

assume at 1: var("x") == 1;
assume at 1: var("x") == 2;
check reach <= 2: active("Root.Done");

What it does. --explain-infeasibility asks why an infeasible scenario is infeasible. none (the default) does no extra solver work. formal adds a classification and a source core. proof additionally builds a checked step-by-step derivation. The depth never changes the verdict, so raising it cannot turn an inconclusive run into a conclusive one – it only adds diagnosis.

Expected output. formal reports COMPLETE FORMAL DOMAIN EXPLANATION with the classification, the core members and their source positions. Re-running the same query with --explain-infeasibility proof reports COMPLETE VERIFIED DOMAIN PROOF and a numbered derivation. Both exit 3.

The headline names the depth and how complete it is, so COMPLETE at formal depth means the formal explanation produced everything it promises – not that a proof was found. The four headlines are listed in BMC CLI and Result Protocol Reference.

File side effect. None without -o.

Failure boundary. proof costs extra solver checks: each input node is verified in both directions and each derived step is re-derived independently. On this fixture the explanation took roughly 10 ms, but a large core with many members will cost more. Use none in a CI gate that only needs the verdict, formal when a human will read the failure, and proof when the reasoning itself has to be auditable.

Next diagnostic step. If proof returns achieved_mode as formal, go to task 15.

Reference. See BMC CLI and Result Protocol Reference for the option contract and the block layouts.

13. Read a conflict core and act on it

CLI.

python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q infeasible_cross_step.fbmcq \
    --explain-infeasibility formal --color never

FBMCQ.

init state("Root.Idle") where x == 0;
assume at 1: var("x") == 3;
check reach <= 2: active("Root.Done");

What it does. The core is the set of clauses that together make the scenario infeasible, each with the position it was written at.

Expected output. On the verified run:

Classification: assumptions conflict with the feasible prefix

Conflict constraints:
  1. infeasible_cross_step.fbmcq:2:1-2:28
     assume at 1: var("x") == 3;
  2. infeasible_cross_step.fbmcq:1:1-1:38
     init state("Root.Idle") where x == 0;
  3. bmc_tasks.fcstm:1:1-1:15
     def int x = 0;
  4. generated transition constraint at step 0

Read it as: the classification says which file to open, and the members say which lines. Here the assumption at frame 1 disagrees with what the initializer and the declaration force, so either the assume value or the initial value has to change.

Member 4 has no source position because nobody wrote it: the builder generates the transition constraint that carries frame 0’s values forward. A generated member names its category and the step it constrains, and is not something you can edit – it tells you why the authored members conflict, not what to change.

File side effect. None without -o.

Failure boundary. A core is only guaranteed sufficient unless the report says otherwise. Check the Reduction: line: raw may include members that are not part of the conflict, partial_minimized was cut short, and only subset_minimal guarantees every listed member is load bearing. Editing a member of a raw core may change nothing.

Next diagnostic step. For the reasoning that links the members, raise the depth to proof and read task 14.

Reference. See BMC solving, witnesses, and replay boundaries for why sufficient is not minimal.

14. Read a proof and trace a sentence to a clause

CLI.

python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q infeasible_two_values.fbmcq \
    --explain-infeasibility proof --json -o /tmp/bmc-proof.json

What it does. At proof depth the narrative is the proof read in dependency order, and every sentence names the node behind it. The JSON keeps both, so a sentence and its checked step can be reached from each other.

Expected output. stdout carries the numbered derivation; the JSON at result.feasibility.explanation.proof carries the graph:

proof.input.0000   input          source_fact               core_binding
proof.input.0001   input          source_fact               core_binding
proof.step.0002    contradiction  incompatible_equalities   rule_checker

Two inputs, one per core member, each verified against the member it restates; one root, re-derived by an independent checker. root_id is proof.step.0002, input_minimality is subset_minimal, graph_minimality is dependency_pruned, and verification_status is verified.

File side effect. /tmp/bmc-proof.json contains the whole result.

Failure boundary. A verified proof says each step follows from the clauses named beside it. It does not say the encoding matches what you meant – that is the same boundary replay draws for a witness. And the closing sentence reports that the property was not evaluated; it is not a counterexample.

Next diagnostic step. If proof was requested but the block says achieved formal, read task 15.

Reference. See BMC CLI and Result Protocol Reference for the node vocabulary and what each verification method checks.

15. Handle a degraded or timed-out explanation

CLI.

python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q infeasible_cross_step.fbmcq \
    --explain-infeasibility proof --color never

What it does. The explanation reports the depth it reached, not the depth that was asked for. This query’s conflict only appears after accumulating across a step, so no rule in the catalog closes it.

Expected output. On the verified run:

Explanation: PARTIAL FORMAL DOMAIN EXPLANATION
Explanation depth: requested proof, achieved formal
Classification: assumptions conflict with the feasible prefix
...
Reason: the formal explanation is complete, but no rule in the catalog closes
this core.

In JSON, requested_mode is proof, achieved_mode is formal, status is partial, and proof is null.

File side effect. None without -o.

Failure boundary. Degradation is not an error and does not change the exit status, so a consumer must compare requested_mode with achieved_mode rather than assume proof is present. A missing proof key means the depth was not reached, not that the run failed. Note also that the formal narrative here names the initial state and both conflicting values – for cross-step conflicts it says more than a proof built without the intermediate facts could.

Next diagnostic step. Read reason. no rule in the catalog closes this core is a capability boundary and will not change by retrying. timeout or unknown in status is a budget problem: retry with a larger --timeout-ms, or drop to formal.

Reference. See BMC solving, witnesses, and replay boundaries for why some conflicts have no proof.

16. Gate CI on an explanation without scraping text

CLI.

# An infeasible scenario exits 3, which is a report and not a failure.  Under
# set -e -- which GitHub Actions uses for every run: step -- an unguarded
# invocation would abort the step here and never reach the inspection below.
python -m pyfcstm bmc \
    -i bmc_tasks.fcstm \
    -q infeasible_two_values.fbmcq \
    --explain-infeasibility proof --color never \
    --json -o /tmp/bmc-gate.json && status=0 || status=$?
test "$status" -eq 3

python - <<'INSPECT'
import json
report = json.load(open("/tmp/bmc-gate.json"))
explanation = report["result"]["feasibility"]["explanation"]
print(explanation["requested_mode"], explanation["achieved_mode"])
print(explanation["status"], explanation["classification"])
INSPECT

What it does. Reads the explanation through the versioned JSON contract instead of the human report, which is what a gate should depend on.

Expected output. proof proof then complete assumptions_self_conflict.

File side effect. /tmp/bmc-gate.json is written atomically.

Failure boundary. The exit status is part of the contract a gate has to handle: 3 means the scenario was infeasible and the property was not evaluated, which for this query is the expected result rather than an error. A step that lets set -e abort on it never reads the explanation it asked for.

explanation is null at none depth, so a gate must handle that rather than index into it. Human wording and elapsed_ms are not contracts and must not be asserted on; the enumerated fields are. ANSI decoration never reaches JSON or --output files regardless of --color.

Next diagnostic step. To fail a build only on a specific conflict family, compare classification against the closed list rather than matching the printed phrase.

Reference. See BMC CLI and Result Protocol Reference for JSON nullability and the schema.

Choose and compare a solver profile

Use this page’s bmc_tasks.fcstm and reach.fbmcq from the same directory. Run each choice explicitly:

python -m pyfcstm bmc -i bmc_tasks.fcstm -q reach.fbmcq --solver-profile default --json
python -m pyfcstm bmc -i bmc_tasks.fcstm -q reach.fbmcq --solver-profile logic --json
python -m pyfcstm bmc -i bmc_tasks.fcstm -q reach.fbmcq --solver-profile tactic --json

Each command exits 0 and prints result.status="sat", result.property_satisfied=true and replay.ok=true. The requested choice appears in result.solver_profile. With no -o, only stdout is written; no file is created. Inspect result.solver_logic to distinguish fragment selection from a fallback after no probe matched.

Compare verdicts and replay before comparing cost. Different strategies can choose different valid witnesses. Context-wide counters in solver_statistics are not per-query work. To measure your own model, keep inputs and Python/Z3 versions fixed and repeat in fresh processes; one faster invocation is not enough to change a default. The repository’s benchmarks/bmc/solving/ supplies four comparison arms, immutable raw records and pre-registered performance thresholds.

--solver-profile fast exits 2; use one of the three lowercase choices. If an optional profile returns an inconclusive answer, rerun with default and inspect reason rather than counting it as a property pass. --explain-infeasibility formal or proof can accompany any profile; explanation checks still use the default solver.

See BMC CLI and Result Protocol Reference for fields, fallback and budget boundaries.

Try conservative slicing for one query

Slicing requires an explicit option:

python -m pyfcstm bmc -i bmc_tasks.fcstm -q reach.fbmcq --cone-slicing --json

Python compilation uses compile_bmc_query(model, query, options=BmcOptions(cone_slicing=True)); the file API accepts build_bmc_output(..., cone_slicing=True). Only bool values are accepted.

Slicing retains query references, guards, ordered operation conditions and their dependencies. Assignments whose evaluation is not known total remain, including division, modulo, powers, functions and floating-point arithmetic. An integer declaration does not justify removing calculations that depend on a temporary non-integer value inside an action. Any abstract action skips the whole model. Unread outputs therefore cannot erase a dangerous calculation and change scenario feasibility, including UNSAT results with no SAT witness to replay.

Initial values and all variable symbols remain intact. Decoding completes removed values through the original runtime, so every frame still contains all variables. Deterministic traces with fixed initial values and events stay equal; queries with multiple solutions may select another legal path. Both the primary witness and a response incomplete suffix are verified before solving returns. Verification failure retries the full model at most once using the same remaining solver budget. Verification and rebuilding consume that budget, but timeout does not forcibly interrupt those Python operations.

When enabled, inspect result.cone_slicing for removals, skip reasons and fallback. Disabled results omit this field. total_elapsed_ms includes internal verification and fallback; performance comparisons must also measure compilation and external decoding/replay rather than excluding completion cost.

The measured correctness gate passes, but the 6.09% formula reduction misses T3’s 20% requirement, so slicing remains disabled by default. A query regresses 131.73% in solve time; compare compilation, solving and external replay costs together. See Measured slicing costs for the measured results.