The block the checker stops reading¶

Nobody writes a two-hand control from contacts twice. Certified safety libraries ship it as a block, you drop the block in, wire the two palm buttons, and the anti-tie-down logic is somebody else's tested code. That is the shape safety logic actually arrives in.

Update: released ESBMC 8.6.0

The runs on this page were recorded against the builds named beside them. For comparison, in the paper's evaluation (evidence/variants_302.csv in the release):

g_two_hand_fb: the released ESBMC 8.6.0 passes the ingestion gate and returns SAFE; 8.4.0 fails the gate.
The expected verdict is unchanged in every case.

So here is lesson 7.2's press again, with the identical Type II body moved into a function block. Same machine, same properties, same expected answers. The ladder twin verifies, and has since 7.2.

The block¶

BothOff := NOT LH AND NOT RH;
Armed := (Armed OR BothOff) AND NOT Stroke;
Stroke := (Stroke OR Armed) AND LH AND RH;

BothOff and Armed are the block's own locals, which is what makes the instance stateful and the anti-tie-down work.

file	what it is	size	sha256
`program.xml`	ladder program, PLCopen XML	3.7 KB	`d2d99912ea21`
`type_i.xml`	ladder program, PLCopen XML	3.6 KB	`fda94b735538`
`props.yaml`	property file	0.2 KB	`01c905820f28`

Both builds fail the gate¶

Recorded 2026-09-04T23:40:49Z. Every build ran the same command.

cp benchmarks/manufacturing/g_two_hand_fb/program.xml benchmarks/manufacturing/g_two_hand_fb/program.ld
esbmc benchmarks/manufacturing/g_two_hand_fb/program.ld --ld-props benchmarks/manufacturing/g_two_hand_fb/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

Recorded 2026-09-04T23:40:49Z.

v8.4

cp benchmarks/manufacturing/g_two_hand_fb/program.xml benchmarks/manufacturing/g_two_hand_fb/program.ld
esbmc benchmarks/manufacturing/g_two_hand_fb/program.ld --ld-props benchmarks/manufacturing/g_two_hand_fb/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	`SAFE`	`SAFE`	correct	fail	0.015 s

v8.4 found its solution by the inductive step (k = 2).

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN LH=NONDET(_Bool);
        ASSIGN RH=NONDET(_Bool);
        ASSIGN LH=NONDET(_Bool);
        ASSIGN RH=NONDET(_Bool);
        GOTO 1
     2:

SAFE on both, and the gate fails on both, with Stroke never driven. Here is the whole scan body, from either build:

ASSIGN LH=NONDET(_Bool);
ASSIGN RH=NONDET(_Bool);
ASSIGN LH=NONDET(_Bool);
ASSIGN RH=NONDET(_Bool);

The block is not in it. Two proofs about a press with no logic in it at all.

And the correct variant is condemned¶

Put the Type I body in the block instead, Stroke := LH AND RH, which is the program lesson 7.2 proves safe. This time the gate passes.

Predict the verdict

The block body is now the plain conjunction, and its ladder twin satisfies the property. What happens here?

Answer

build	verdict	expected	ingestion gate
v8.4	`VIOLATION`	`SAFE`	pass

Both builds refute a property that holds. The encoding says why:

ASSIGN THC0__LH=NONDET(_Bool);
ASSIGN THC0__RH=NONDET(_Bool);
ASSIGN THC0__Stroke=THC0__LH;
ASSIGN Stroke=THC0__Stroke;

Two separate defects, in one four-line block.

The block's inputs are havocked rather than bound. THC0__LH is a fresh unconstrained value, not the program's LH, so the wiring from the call site is gone. Then the body itself loses an operand: Stroke := LH AND RH arrives as Stroke := LH. We checked the direction, and it keeps the first operand rather than a particular name: B AND A becomes B, and A OR B becomes A. Arithmetic survives, so this looks specific to boolean operators.

What this does not mean¶

It would be easy to read that as "function blocks do not work", and it is narrower than that. The eight g_tank_* benchmarks in Part 5 are function-block programs, they pass their gates, and their verdicts are right, because their bombs are constant assignments sitting inside the block bodies rather than functions of the block inputs, which means an unbound parameter never changes the answer they give. Going back and reading their recorded encoding, the same NONDET on every formal parameter is sitting there and has been all along.

That is the uncomfortable part. This is not a new regression: it is behavior the corpus has been carrying since the tank programs were imported, invisible the whole time because nothing in it had ever asked a question whose answer depended on what a block does with the arguments handed to it. Two rungs of ISO 13851 logic asked. The answer came back about a different program.

The discriminator from 7.2 still runs here, for completeness, and inherits the same problem.

Recorded 2026-08-28T18:37:10Z. Every build ran the same command.

cp benchmarks/manufacturing/g_two_hand_fb/program.xml benchmarks/manufacturing/g_two_hand_fb/program.ld
esbmc benchmarks/manufacturing/g_two_hand_fb/program.ld --ld-props benchmarks/manufacturing/g_two_hand_fb/tiedown_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

Recorded 2026-08-28T18:37:10Z.

master

cp benchmarks/manufacturing/g_two_hand_fb/program.xml benchmarks/manufacturing/g_two_hand_fb/program.ld
esbmc benchmarks/manufacturing/g_two_hand_fb/program.ld --ld-props benchmarks/manufacturing/g_two_hand_fb/tiedown_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
master	8.4.0 `0064c4ac`	`VIOLATION`	`VIOLATION`	correct	fail	0.011 s

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

master

     1: IF !1 THEN GOTO 2
        ASSIGN LH=NONDET(_Bool);
        ASSIGN RH=NONDET(_Bool);
        ASSIGN LH=NONDET(_Bool);
        ASSIGN RH=NONDET(_Bool);
        GOTO 1
     2:

Counterexample. ESBMC's own output. A trace long enough to need it is elided in the middle, and the omission is marked and counted where it happens.

master

State 1  thread 0
----------------------------------------------------
  LH = 1

State 2  thread 0
----------------------------------------------------
  RH = 1

State 3 file benchmarks/manufacturing/g_two_hand_fb/program.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/manufacturing/g_two_hand_fb/program.ld
  P1
  !(LH && RH) || Stroke


** Results:
benchmarks/manufacturing/g_two_hand_fb/program.ld
  FAILED       [global.assertion.1]  line 0  P1

** 1 of 1 properties failed

Recorded 2026-08-28T18:37:10Z. Every build ran the same command.

cp benchmarks/manufacturing/g_two_hand_fb/type_i.xml benchmarks/manufacturing/g_two_hand_fb/type_i.ld
esbmc benchmarks/manufacturing/g_two_hand_fb/type_i.ld --ld-props benchmarks/manufacturing/g_two_hand_fb/tiedown_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

Recorded 2026-08-28T18:37:10Z.

master

cp benchmarks/manufacturing/g_two_hand_fb/type_i.xml benchmarks/manufacturing/g_two_hand_fb/type_i.ld
esbmc benchmarks/manufacturing/g_two_hand_fb/type_i.ld --ld-props benchmarks/manufacturing/g_two_hand_fb/tiedown_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
master	8.4.0 `0064c4ac`	`VIOLATION`	`SAFE`	wrong	pass	0.012 s

What the front end encoded. The scan body as the solver receives it, branch guards kept. An assignment-only view hides the guards and makes a guarded accumulator read as a constant.

master

     1: IF !1 THEN GOTO 2
        ASSIGN LH=NONDET(_Bool);
        ASSIGN RH=NONDET(_Bool);
        ASSIGN LH=NONDET(_Bool);
        ASSIGN RH=NONDET(_Bool);
        ASSIGN THC0__LH=NONDET(_Bool);
        ASSIGN THC0__RH=NONDET(_Bool);
        ASSIGN THC0__Stroke=THC0__LH;
        ASSIGN Stroke=THC0__Stroke;
        GOTO 1
     2:

Counterexample. ESBMC's own output. A trace long enough to need it is elided in the middle, and the omission is marked and counted where it happens.

master

State 1  thread 0
----------------------------------------------------
  LH = 1

State 2  thread 0
----------------------------------------------------
  RH = 1

State 3  thread 0
----------------------------------------------------
  THC0__LH = 0

State 4  thread 0
----------------------------------------------------
  THC0__Stroke = 0

State 5  thread 0
----------------------------------------------------
  Stroke = 0

State 6 file benchmarks/manufacturing/g_two_hand_fb/type_i.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/manufacturing/g_two_hand_fb/type_i.ld
  P1
  !(LH && RH) || Stroke


** Results:
benchmarks/manufacturing/g_two_hand_fb/type_i.ld
  FAILED       [global.assertion.1]  line 0  P1

** 1 of 1 properties failed

Where this leaves the part¶

Eight machines in this part carry a discriminator that separates a correct program from a plausible wrong one. This one cannot, because the checker is not reading the program. That makes it the odd lesson out here and a natural neighbour of Part 6, where the same thing happens to function block diagrams and sequential function charts.

The suite shipped it anyway, with the ladder twin as its expected verdict. A gap you can point at is worth more than a benchmark quietly dropped for answering wrong. The gap was fixed upstream in esbmc#8034, and the task is now marked validated.