The standby pump nobody started¶

A wet well with two pumps in it. Level rises, a pump runs, level falls, the pump stops. Duty-standby means one runs at a time so the other stays in reserve, and alternation means duty changes hands each cycle so that both pumps get used. Skip the alternation and you own a standby pump nobody has started since commissioning, which is the pump you find out about on the night the duty one fails.

This is also the first benchmark in this part that the checker cannot finish.

The rungs¶

Call := (Call OR LevelHigh) AND NOT LevelLow. Duty := (Duty AND NOT LevelLow) OR (NOT Duty AND LevelLow). PumpA := Call AND NOT Duty, PumpB := Call AND Duty. The Duty rung is an exclusive or against LevelLow, so the selector flips every time the well empties.

file	what it is	size	sha256
`program.xml`	ladder program, PLCopen XML	4.6 KB	`8987780ce8bd`
`stuck_duty.xml`	ladder program, PLCopen XML	4.2 KB	`249cfc022e01`
`props.yaml`	property file	0.2 KB	`e07405d45fbc`
`alternation_check.props.yaml`	property file	0.5 KB	`cf5d60e99918`

The property everyone writes¶

benchmarks/water_treatment/g_pump_alternation/props.yaml

format_version: "0.1"
properties:
  - id: P1
    kind: mutual_exclusion
    variables: [PumpA, PumpB]
    justification: "Duty-standby: one pump runs at a time, so the standby stays available and the rising main is not over-pressured."

Recorded 2026-09-04T23:41:00Z. Every build ran the same command.

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

Recorded 2026-09-04T23:41:00Z.

v8.4

cp benchmarks/water_treatment/g_pump_alternation/program.xml benchmarks/water_treatment/g_pump_alternation/program.ld
esbmc benchmarks/water_treatment/g_pump_alternation/program.ld --ld-props benchmarks/water_treatment/g_pump_alternation/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.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 LevelHigh=NONDET(_Bool);
        ASSIGN LevelLow=NONDET(_Bool);
        ASSIGN PumpB=1 && Call && Duty;
        ASSIGN PumpA=1 && Call && !Duty;
        ASSIGN Call=1 && Call && !LevelLow;
        ASSIGN Call=1 && LevelHigh && !LevelLow;
        ASSIGN Duty=1 && Duty && !LevelLow;
        ASSIGN Duty=1 && !Duty && LevelLow;
        GOTO 1
     2:

Now the defect, and it is a real one rather than an invented one. Somebody wires the toggle's set branch in series instead of in parallel, so the rung reads Duty := Duty AND LevelLow. Duty starts at zero and stays there for the life of the installation.

Predict the verdict

Duty never leaves the lead pump. Do the two pumps still exclude each other?

Answer

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

They do, and more strictly than before, because one of them never runs at all. A station that has quietly become single-pump satisfies every mutual-exclusion property you can write about it.

The discriminator, and where it stops¶

Ask about the selector rather than about pump B.

benchmarks/water_treatment/g_pump_alternation/alternation_check.props.yaml

# Discriminator, not a safety requirement. Alternation exists so both pumps wear evenly.
# A toggle wired in series rather than parallel never moves duty off pump A, and the
# standby becomes a pump nobody has started in months. Asking about the selector rather
# than about pump B keeps the question inductive: the stuck variant proves it at k = 1.
format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!Duty"
    justification: "The duty selector never moves to the second pump. Working alternation must refute this."

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

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

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

master

cp benchmarks/water_treatment/g_pump_alternation/program.xml benchmarks/water_treatment/g_pump_alternation/program.ld
esbmc benchmarks/water_treatment/g_pump_alternation/program.ld --ld-props benchmarks/water_treatment/g_pump_alternation/alternation_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 28
        ASSIGN LevelHigh=NONDET(_Bool);
        ASSIGN LevelLow=NONDET(_Bool);
        ASSIGN Call__prev=1 && Call;
        ASSIGN Duty__prev=1 && Duty;
        IF !1 THEN GOTO 2
        ASSIGN pf15=0;
     2: IF !(1 && Call__prev) THEN GOTO 3
        ASSIGN pf15=1;
     3: IF !1 THEN GOTO 4
        ASSIGN pf16=0;
     4: IF !(1 && pf15 && Duty__prev) THEN GOTO 5
        ASSIGN pf16=1;
     5: ASSIGN PumpB=1 && pf16;
        IF !1 THEN GOTO 6
        ASSIGN pf12=0;
     6: IF !(1 && Call__prev) THEN GOTO 7
        ASSIGN pf12=1;
     7: IF !1 THEN GOTO 8
        ASSIGN pf13=0;
     8: IF !(1 && pf12 && !Duty__prev) THEN GOTO 9
        ASSIGN pf13=1;
     9: ASSIGN PumpA=1 && pf13;
        IF !1 THEN GOTO 10
        ASSIGN pf4=0;
    10: IF !(1 && LevelHigh) THEN GOTO 11
        ASSIGN pf4=1;
    11: IF !1 THEN GOTO 12
        ASSIGN pf3=0;
    12: IF !(1 && Call__prev) THEN GOTO 13
        ASSIGN pf3=1;
    13: IF !1 THEN GOTO 14
        ASSIGN pf5=0;
    14: IF !(1 && pf4 && !LevelLow) THEN GOTO 15
        ASSIGN pf5=1;
    15: IF !(1 && pf3 && !LevelLow) THEN GOTO 16
        ASSIGN pf5=1;
    16: ASSIGN Call=1 && pf5;
        IF !1 THEN GOTO 17
        ASSIGN pf9=0;
    17: IF !(1 && !Duty__prev) THEN GOTO 18
        ASSIGN pf9=1;
    18: IF !1 THEN GOTO 19
        ASSIGN pf10=0;
    19: IF !(1 && pf9 && LevelLow) THEN GOTO 20
        ASSIGN pf10=1;
    20: IF !1 THEN GOTO 21
        ASSIGN pf7=0;
    21: IF !(1 && Duty__prev) THEN GOTO 22
        ASSIGN pf7=1;
    22: IF !1 THEN GOTO 23
        ASSIGN pf8=0;
    23: IF !(1 && pf7 && !LevelLow) THEN GOTO 24
        ASSIGN pf8=1;
    24: IF !1 THEN GOTO 25
        ASSIGN Duty__pf0=0;
    25: IF !(1 && pf10) THEN GOTO 26
        ASSIGN Duty__pf0=1;
    26: IF !(1 && pf8) THEN GOTO 27
        ASSIGN Duty__pf0=1;
    27: ASSIGN Duty=1 && Duty__pf0;
        GOTO 1
    28:

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

State 2  thread 0
----------------------------------------------------
  Duty = 1

State 3 file benchmarks/water_treatment/g_pump_alternation/program.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/water_treatment/g_pump_alternation/program.ld
  P1
  !Duty


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

** 1 of 1 properties failed

One scan with LevelLow = 1 and duty has moved. Both builds find it.

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

cp benchmarks/water_treatment/g_pump_alternation/stuck_duty.xml benchmarks/water_treatment/g_pump_alternation/stuck_duty.ld
esbmc benchmarks/water_treatment/g_pump_alternation/stuck_duty.ld --ld-props benchmarks/water_treatment/g_pump_alternation/alternation_check.props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 30s

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

master

cp benchmarks/water_treatment/g_pump_alternation/stuck_duty.xml benchmarks/water_treatment/g_pump_alternation/stuck_duty.ld
esbmc benchmarks/water_treatment/g_pump_alternation/stuck_duty.ld --ld-props benchmarks/water_treatment/g_pump_alternation/alternation_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`	`unknown`	`SAFE`	unknown	pass	0.400 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 21
        ASSIGN LevelHigh=NONDET(_Bool);
        ASSIGN LevelLow=NONDET(_Bool);
        ASSIGN Call__prev=1 && Call;
        ASSIGN Duty__prev=1 && Duty;
        IF !1 THEN GOTO 2
        ASSIGN pf13=0;
     2: IF !(1 && Call__prev) THEN GOTO 3
        ASSIGN pf13=1;
     3: IF !1 THEN GOTO 4
        ASSIGN pf14=0;
     4: IF !(1 && pf13 && Duty__prev) THEN GOTO 5
        ASSIGN pf14=1;
     5: ASSIGN PumpB=1 && pf14;
        IF !1 THEN GOTO 6
        ASSIGN pf10=0;
     6: IF !(1 && Call__prev) THEN GOTO 7
        ASSIGN pf10=1;
     7: IF !1 THEN GOTO 8
        ASSIGN pf11=0;
     8: IF !(1 && pf10 && !Duty__prev) THEN GOTO 9
        ASSIGN pf11=1;
     9: ASSIGN PumpA=1 && pf11;
        IF !1 THEN GOTO 10
        ASSIGN pf7=0;
    10: IF !(1 && Duty__prev) THEN GOTO 11
        ASSIGN pf7=1;
    11: IF !1 THEN GOTO 12
        ASSIGN pf8=0;
    12: IF !(1 && pf7 && LevelLow) THEN GOTO 13
        ASSIGN pf8=1;
    13: ASSIGN Duty=1 && pf8;
        IF !1 THEN GOTO 14
        ASSIGN pf4=0;
    14: IF !(1 && LevelHigh) THEN GOTO 15
        ASSIGN pf4=1;
    15: IF !1 THEN GOTO 16
        ASSIGN pf3=0;
    16: IF !(1 && Call__prev) THEN GOTO 17
        ASSIGN pf3=1;
    17: IF !1 THEN GOTO 18
        ASSIGN pf5=0;
    18: IF !(1 && pf4 && !LevelLow) THEN GOTO 19
        ASSIGN pf5=1;
    19: IF !(1 && pf3 && !LevelLow) THEN GOTO 20
        ASSIGN pf5=1;
    20: ASSIGN Call=1 && pf5;
        GOTO 1
    21:

Neither build can discharge the same property on the stuck variant, and that is the recorded result. The property is inductive by inspection: assume Duty is false, and Duty AND LevelLow is false, so it stays false. k-induction should close it at k = 1.

We cut the program down to find out where the difficulty was, and it is not the program. One rung, one input, one coil is enough to reproduce it:

Duty ---| |---| |--- ( Duty )     Duty := Duty AND LevelLow
             LevelLow

Against !Duty, the checker reports The inductive step is unable to prove the property at every k from 2 to 50 and finish with VERIFICATION UNKNOWN. A bounded run to depth 20 finds no counterexample and fails only on the unwinding assertion, which is what an infinite scan loop always does. So there is no trace refuting the property within 20 scans, and no proof either.

What to take from it¶

Every pair before this one had a discriminator that refuted on one program and proved on the other. That symmetry is what makes the pair informative, and it depends on the checker being able to answer both halves. Here it answers one.

The pair is still worth shipping. It records what the tool did rather than what we wanted it to do, the working alternation is confirmed, and the gap has a five-line reproducer attached to it. An unknown that you can hand to somebody is a better artifact than a benchmark quietly reshaped until the checker agreed with it.