The interlock that makes it wait¶

A reciprocating compressor on a receiver, with two pressure switches setting the band. Pressure falls to the cut-in, the compressor loads; pressure reaches the cut-out, it unloads. Every workshop has one.

The interlock that matters is not in that description. A compressor motor started too soon after stopping draws locked-rotor current into windings that have not cooled, and on a receiver with a leak the cycle can repeat every few seconds. So the load rung carries a minimum-off term, and the machine sits there for a while doing nothing while the pressure is already low.

The rung¶

Load := (Load OR (PressLow AND MinOffDone)) AND NOT PressHigh. One rung, one latch. MinOffDone gates the set branch only, so the compressor may always unload at once and may not always load at once. That asymmetry is the design.

file	what it is	size	sha256
`program.xml`	ladder program, PLCopen XML	2.4 KB	`6fc4e650e9b3`
`short_cycle.xml`	ladder program, PLCopen XML	2.2 KB	`57ac44247b5c`
`props.yaml`	property file	0.2 KB	`1aff1839ace5`
`mincycle_check.props.yaml`	property file	0.4 KB	`874b14eae58f`

The property everyone writes¶

benchmarks/manufacturing/g_compressor_cycle/props.yaml

format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!(Load && PressHigh)"
    justification: "The compressor never loads at or above the cut-out pressure."

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

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

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

v8.4

cp benchmarks/manufacturing/g_compressor_cycle/program.xml benchmarks/manufacturing/g_compressor_cycle/program.ld
esbmc benchmarks/manufacturing/g_compressor_cycle/program.ld --ld-props benchmarks/manufacturing/g_compressor_cycle/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	pass	0.017 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 PressLow=NONDET(_Bool);
        ASSIGN PressHigh=NONDET(_Bool);
        ASSIGN MinOffDone=NONDET(_Bool);
        ASSIGN Load=1 && Load && !PressHigh;
        ASSIGN Load=1 && PressLow && MinOffDone && !PressHigh;
        GOTO 1
     2:

Take MinOffDone out of the set branch and you have the short-cycling variant, which is what a hurried commissioning leaves behind when the timer is inconvenient during testing.

Predict the verdict

The minimum-off interlock is gone. Does the compressor still refuse to load above the cut-out?

Answer

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

NOT PressHigh is the tail of the rung in both files, so both prove it. The property constrains the top of the band and says nothing about the bottom, which is where the damage happens.

The discriminator¶

benchmarks/manufacturing/g_compressor_cycle/mincycle_check.props.yaml

# Discriminator, not a safety requirement. A minimum-off interlock makes the compressor
# wait before restarting, so a low pressure does not always load it at once. A program
# that proves this short-cycles the motor.
format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!PressLow || Load || PressHigh"
    justification: "A low pressure loads the compressor immediately. A minimum-off interlock must refute this."

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

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

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

master

cp benchmarks/manufacturing/g_compressor_cycle/program.xml benchmarks/manufacturing/g_compressor_cycle/program.ld
esbmc benchmarks/manufacturing/g_compressor_cycle/program.ld --ld-props benchmarks/manufacturing/g_compressor_cycle/mincycle_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	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 11
        ASSIGN PressLow=NONDET(_Bool);
        ASSIGN PressHigh=NONDET(_Bool);
        ASSIGN MinOffDone=NONDET(_Bool);
        ASSIGN Load__prev=1 && Load;
        IF !1 THEN GOTO 2
        ASSIGN pf3=0;
     2: IF !(1 && Load__prev) THEN GOTO 3
        ASSIGN pf3=1;
     3: IF !1 THEN GOTO 4
        ASSIGN pf4=0;
     4: IF !(1 && PressLow) THEN GOTO 5
        ASSIGN pf4=1;
     5: IF !1 THEN GOTO 6
        ASSIGN pf5=0;
     6: IF !(1 && pf4 && MinOffDone) THEN GOTO 7
        ASSIGN pf5=1;
     7: IF !1 THEN GOTO 8
        ASSIGN pf6=0;
     8: IF !(1 && pf3 && !PressHigh) THEN GOTO 9
        ASSIGN pf6=1;
     9: IF !(1 && pf5 && !PressHigh) THEN GOTO 10
        ASSIGN pf6=1;
    10: ASSIGN Load=1 && pf6;
        GOTO 1
    11:

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
----------------------------------------------------
  PressLow = 1

State 2  thread 0
----------------------------------------------------
  PressHigh = 0

State 3  thread 0
----------------------------------------------------
  MinOffDone = 0

State 4  thread 0
----------------------------------------------------
  Load = 0

State 5 file benchmarks/manufacturing/g_compressor_cycle/program.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/manufacturing/g_compressor_cycle/program.ld
  P1
  !PressLow || Load || PressHigh


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

** 1 of 1 properties failed

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

cp benchmarks/manufacturing/g_compressor_cycle/short_cycle.xml benchmarks/manufacturing/g_compressor_cycle/short_cycle.ld
esbmc benchmarks/manufacturing/g_compressor_cycle/short_cycle.ld --ld-props benchmarks/manufacturing/g_compressor_cycle/mincycle_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

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

master

cp benchmarks/manufacturing/g_compressor_cycle/short_cycle.xml benchmarks/manufacturing/g_compressor_cycle/short_cycle.ld
esbmc benchmarks/manufacturing/g_compressor_cycle/short_cycle.ld --ld-props benchmarks/manufacturing/g_compressor_cycle/mincycle_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`	`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 9
        ASSIGN PressLow=NONDET(_Bool);
        ASSIGN PressHigh=NONDET(_Bool);
        ASSIGN MinOffDone=NONDET(_Bool);
        ASSIGN Load__prev=1 && Load;
        IF !1 THEN GOTO 2
        ASSIGN pf4=0;
     2: IF !(1 && PressLow) THEN GOTO 3
        ASSIGN pf4=1;
     3: IF !1 THEN GOTO 4
        ASSIGN pf3=0;
     4: IF !(1 && Load__prev) THEN GOTO 5
        ASSIGN pf3=1;
     5: IF !1 THEN GOTO 6
        ASSIGN pf5=0;
     6: IF !(1 && pf4 && !PressHigh) THEN GOTO 7
        ASSIGN pf5=1;
     7: IF !(1 && pf3 && !PressHigh) THEN GOTO 8
        ASSIGN pf5=1;
     8: ASSIGN Load=1 && pf5;
        GOTO 1
     9:

The interlocked design refutes it: pressure is low, the machine is not loading, and that is the interlock doing its job. The short-cycling one proves it at k = 2. A proof, here, is the bad news.

Reading the whole part at once¶

Eight machines, and the same table in every one:

	the safety property	the discriminator
the correct program	`SAFE`	`VIOLATION`
the defective program	`SAFE`	`SAFE`

The left column is what gets written, reviewed, and reported. It is true of both programs in every pair. The right column is the one that carries information, and in every case it carries it by failing.

There is a habit buried in this. Engineers write properties that say the machine will not hurt anybody, and those properties are satisfied by a machine that does nothing at all. The interesting requirements are the ones about what the machine must still be able to do: hold the drive down until somebody resets it, refuse a taped button, leave a gap between two contactors, keep reversing after the beam clears, stay locked out, move duty to the other pump, wait before restarting. Every one of those is checked by asking for a counterexample and getting one.