An air handler whose name promises a timer¶

This benchmark is called g_hvac_fan_delay. There is no delay in it. That is worth a lesson of its own, because a benchmark id is a label somebody chose, and the only trustworthy description of a program is the program.

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_tof_hold: the released ESBMC 8.6.0 returns SAFE, which matches the expected verdict; 8.4.0 reports a false VIOLATION.
The expected verdict is unchanged in every case.

The machine¶

An air handling unit: a heating coil, a cooling coil and a supply fan, with an enable that says the unit is commissioned to run. Zone controls raise a heat call or a cool call.

Driving both coils at once is a fault every control specification forbids. The two fight each other, the unit never reaches setpoint, and the energy goes on being spent for as long as nobody notices. It is not the kind of hazard that hurts somebody in the next second, which is exactly why it can run for a season before anyone looks.

benchmarks/hvac/g_hvac_fan_delay/props.yaml

format_version: "0.1"
properties:
  - id: P1
    kind: mutual_exclusion
    variables: [heat, cool]
    justification: "Heating and cooling must never drive the plant simultaneously."

The program¶

heat := NOT cool_call AND heat_call AND enable
cool := cool_call AND enable
fan  := enable

Cooling wins ties. The interlock is the normally closed cool_call contact in the heat rung, and nothing else prevents the conflict.

file	what it is	size	sha256
`clean.xml`	ladder program, PLCopen XML	3.4 KB	`8ffc7e5fdaa8`
`bomb.xml`	ladder program, PLCopen XML	3.8 KB	`3242c8dd20d2`
`props.yaml`	property file	0.2 KB	`98a952136967`

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

cp benchmarks/hvac/g_hvac_fan_delay/clean.xml benchmarks/hvac/g_hvac_fan_delay/clean.ld
esbmc benchmarks/hvac/g_hvac_fan_delay/clean.ld --ld-props benchmarks/hvac/g_hvac_fan_delay/props.yaml --k-induction --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

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

v8.4

cp benchmarks/hvac/g_hvac_fan_delay/clean.xml benchmarks/hvac/g_hvac_fan_delay/clean.ld
esbmc benchmarks/hvac/g_hvac_fan_delay/clean.ld --ld-props benchmarks/hvac/g_hvac_fan_delay/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.018 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 heat_call=NONDET(_Bool);
        ASSIGN cool_call=NONDET(_Bool);
        ASSIGN enable=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN cool=1 && cool_call && enable;
        ASSIGN heat=1 && !cool_call && heat_call && enable;
        ASSIGN fan=1 && enable;
        GOTO 1
     2:

The bombed variant is the branch this part has now shown five times, and the checker refute it:

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

cp benchmarks/hvac/g_hvac_fan_delay/bomb.xml benchmarks/hvac/g_hvac_fan_delay/bomb.ld
esbmc benchmarks/hvac/g_hvac_fan_delay/bomb.ld --ld-props benchmarks/hvac/g_hvac_fan_delay/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

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

v8.4

cp benchmarks/hvac/g_hvac_fan_delay/bomb.xml benchmarks/hvac/g_hvac_fan_delay/bomb.ld
esbmc benchmarks/hvac/g_hvac_fan_delay/bomb.ld --ld-props benchmarks/hvac/g_hvac_fan_delay/props.yaml --incremental-bmc --unwind 20 --ld-scan-watchdog --ld-scan-budget 8 --timeout 20s

build	ESBMC	verdict	expected	outcome	ingestion gate	cpu
v8.4	8.4.0	`VIOLATION`	`VIOLATION`	correct	pass	0.013 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.

v8.4

     1: IF !1 THEN GOTO 2
        ASSIGN heat_call=NONDET(_Bool);
        ASSIGN cool_call=NONDET(_Bool);
        ASSIGN enable=NONDET(_Bool);
        ASSIGN maint=NONDET(_Bool);
        ASSIGN fan=1 && enable;
        ASSIGN heat=1 && !cool_call && heat_call && enable;
        ASSIGN heat=1 && cool_call && maint && heat_call && enable;
        ASSIGN cool=1 && cool_call && enable;
        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.

v8.4

State 1  thread 0
----------------------------------------------------
  heat_call = 1

State 2  thread 0
----------------------------------------------------
  cool_call = 1

State 3  thread 0
----------------------------------------------------
  enable = 1

State 4  thread 0
----------------------------------------------------
  maint = 1

State 5  thread 0
----------------------------------------------------
  heat = 1

State 6  thread 0
----------------------------------------------------
  cool = 1

State 7 file benchmarks/hvac/g_hvac_fan_delay/bomb.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/hvac/g_hvac_fan_delay/bomb.ld
  P1
  !(heat && cool)

heat_call = 1   cool_call = 1   enable = 1   maint = 1   ->   heat = 1   and   cool = 1

Now look at the third rung¶

fan := enable. The fan runs whenever the unit is enabled and stops the instant it is not. There is no timer in this program. Not a badly configured one: none.

$ grep -c '<block' clean.xml
0

The benchmark's own metadata says so plainly, features: [contacts, coils], so nothing here is being hidden. The name promises a delay and the description does not, which means somebody reading the catalog by id would form an expectation the file never had.

What a fan delay is actually for¶

An electric heating element carries heat after its contactor drops. If the fan stops at the same instant, that heat has nowhere to go: the element cooks, the thermal cutout trips, and on a bad day the cutout is the only thing between you and a duct fire. So the fan runs on for a fixed period after the heat call clears. That period is the purge, and it is why real AHU logic has a timer that this program does not.

Written properly it is an off-delay, which is exactly lesson 1.6's TOF: IN falls, Q holds for PT, then drops. The suite has that block exercised in g_tof_hold and the requirement to go with it.

Why it is not simply added here¶

Because time in this model is counted in scans. PT is a number of scan cycles, not seconds, so a thirty second purge on a ten millisecond task is three thousand scans. A bounded search will not reach the end of that purge, and proving anything about it means k-induction over the counter or an abstraction that replaces the count with a bound.

That is a real cost, and it is the honest reason the timer benchmarks in this suite are small and separate from the machine benchmarks. Combining them would produce a task that is realistic and unverifiable, which helps nobody.

What to take from this¶

Read the program. The id told you there was a delay, the property said nothing about fans at all, and the only place the truth was written down was the ladder and the features list beside it.

Two habits follow. Check that the feature a benchmark is named for is present before you count it as coverage of that feature. And when you write a suite, let the metadata carry the claim, because a name gets copied into a paper and a features list gets checked by a script.