Counters, and a pin that is not read¶

Counters are timers with the clock replaced by an event: a CTU counts rising edges on its CU pin until the count reaches PV and then raises Q, while a CTD counts the other way and raises Q when it hits zero. Both keep state across scans. That is what puts them here, in the half of Part 1 where the order of things starts to matter.

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_ctd_load: the released ESBMC 8.6.0 passes the ingestion gate and returns SAFE; 8.4.0 fails the gate.
g_ctu_saturate: 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.

Counting up, with a reset¶

file	what it is	size	sha256
`program.xml`	ladder program, PLCopen XML	3.2 KB	`3863a4a3c74d`
`props.yaml`	property file	0.2 KB	`71301ff6f8f1`

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

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

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

master

cp benchmarks/packaging/g_ctu_saturate/program.xml benchmarks/packaging/g_ctu_saturate/program.ld
esbmc benchmarks/packaging/g_ctu_saturate/program.ld --ld-props benchmarks/packaging/g_ctu_saturate/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`	`SAFE`	`SAFE`	correct	pass	0.016 s

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

master

     1: IF !1 THEN GOTO 6
        ASSIGN Pulse=NONDET(_Bool);
        ASSIGN Reset=NONDET(_Bool);
        IF !1 THEN GOTO 2
        ASSIGN pf3=0;
     2: IF !(1 && Pulse) THEN GOTO 3
        ASSIGN pf3=1;
     3: ASSIGN CTU0__CU=1 && pf3;
        IF !(CTU0__CU && !__ctr_prev_CTU0 && CTU0__CV < 2147483647) THEN GOTO 4
        ASSIGN CTU0__CV=CTU0__CV + 1;
     4: IF !Reset THEN GOTO 5
        ASSIGN CTU0__CV=0;
     5: ASSIGN __ctr_prev_CTU0=CTU0__CU;
        ASSIGN CTU0__Q=CTU0__CV >= CTU0__PV;
        ASSIGN Done=1 && CTU0__Q;
        GOTO 1
     6:

Done and Reset never hold together, proved, with the gate passing and CTU0__CV visible in the scan body. The counter is there, which is the precondition for the verdict meaning anything.

The R pin is wired to a contact here, and the front end reads that contact's variable straight through. Wire R to a chain of contacts instead and it prints a warning and models no reset at all, which is the honest thing to do and worth knowing before you draw one that way.

Counting down, and a pin that is not read¶

The IEC count-down block reloads its preset through the LD pin. This program wires it:

file	what it is	size	sha256
`g_ctd_load_program.xml`	ladder program, PLCopen XML	3.2 KB	`cea534618ccf`
`g_ctd_load_props.yaml`	property file	0.2 KB	`3223ae0dbc67`

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

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

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

master

cp benchmarks/elevator/g_ctd_load/program.xml benchmarks/elevator/g_ctd_load/program.ld
esbmc benchmarks/elevator/g_ctd_load/program.ld --ld-props benchmarks/elevator/g_ctd_load/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.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 5
        ASSIGN Pulse=NONDET(_Bool);
        ASSIGN Load=NONDET(_Bool);
        IF !1 THEN GOTO 2
        ASSIGN pf3=0;
     2: IF !(1 && Pulse) THEN GOTO 3
        ASSIGN pf3=1;
     3: ASSIGN CTD0__CD=1 && pf3;
        IF !(CTD0__CD && !__ctr_prev_CTD0 && CTD0__CV > -2147483648) THEN GOTO 4
        ASSIGN CTD0__CV=CTD0__CV + -1;
     4: ASSIGN __ctr_prev_CTD0=CTD0__CD;
        ASSIGN CTD0__Q=CTD0__CV <= 0;
        ASSIGN Empty=1 && CTD0__Q;
        GOTO 1
     5:

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
----------------------------------------------------
  Pulse = 0

State 2  thread 0
----------------------------------------------------
  Load = 1

State 3  thread 0
----------------------------------------------------
  CTD0__CD = 0

State 4  thread 0
----------------------------------------------------
  CTD0__Q = 1

State 5  thread 0
----------------------------------------------------
  Empty = 1

State 6 file benchmarks/elevator/g_ctd_load/program.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/elevator/g_ctd_load/program.ld
  P1
  !(Empty && Load)


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

** 1 of 1 properties failed

master reports a violation. It is right about the program it built, and the encoding says why in three lines:

ASSIGN CTD0__CD=1 && pf3;
ASSIGN CTD0__CV=CTD0__CV + -1;
ASSIGN CTD0__Q=CTD0__CV <= 0;

Load appears once, as a nondeterministic input, and never again. The graphical block reader looks for a pin named R and nothing else, so the LD wire is dropped on the floor, and what remains is a counter that decrements every time its input conducts and has no way back: CV runs negative, Q latches true, and Empty ends up true whatever Load does. The load pin might as well not be there.

Under IEC semantics the requirement holds: a load restores the preset, CV is positive again, and Empty goes low. The expected verdict stays SAFE and the task stays candidate, because no tool has confirmed it and the one tool available here cannot.

What to take from this¶

A wired pin that the tool ignores looks exactly like a wired pin that works. There is no diagnostic, the file is schema-valid, and the verdict comes back with the confidence of a proof. Only the encoding distinguishes them, which is why every panel on this site prints it.