The false alarm¶

A verifier that misses a defect has failed once, and one that condemns a correct program has failed twice over: the engineer loses an afternoon to a program that was never broken, and the next red result gets rather less attention than it deserves.

Both came from the same defect here, and both are gone. Like lesson 6.1, this page records behavior that esbmc#7354 removed on 28 August 2026. The reactor is worth keeping because the false alarm it produced is the harder half of that bug to argue about, and because the table at the end is the reason this site records an encoding beside every verdict.

Two out of three¶

A pressure vessel with three switches on it. One switch reading high could be a fault, so tripping on one is how a plant learns to bypass its own protection, while waiting for all three means a genuine overpressure with a single dead switch never trips the vessel at all. The industry answer is a vote: any two agreeing trip the reactor.

Three AND blocks, one per pair, into an OR.

benchmarks/chemical_batch/fbd_reactor_2oo3/props.yaml

format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!((ps1 && ps2) || (ps2 && ps3) || (ps1 && ps3)) || trip"
    justification: "Any two pressure switches agreeing high must trip the reactor, or the vessel stays pressurised behind a closed relief path."
  - id: P2
    kind: invariant
    expression: "!trip || ((ps1 && ps2) || (ps2 && ps3) || (ps1 && ps3))"
    justification: "A single stuck-high switch must not trip: spurious trips on a batch plant cost a charge and train operators to bypass the vote."

Two properties, and they pull against each other on purpose. P1 says any two agreeing must trip. P2 says nothing less than two may trip. A vote is exactly the logic that satisfies both, which is why the pair is worth writing down.

The defect¶

file	what it is	size	sha256
`clean.xml`	ladder program, PLCopen XML	6.8 KB	`72a1205e72e1`
`bomb.xml`	ladder program, PLCopen XML	5.6 KB	`bf03536740e2`
`props.yaml`	property file	0.5 KB	`de519b56ea30`

The bombed file drops the ps1 AND ps3 leg. Two of three pairs still vote, so the vessel trips whenever the middle switch agrees with either neighbour, and the plant behaves normally through commissioning. Only the outer pair is deaf: ps1=1, ps2=0, ps3=1 leaves trip low with two switches calling for it.

The correct program, refuted¶

Predict the verdict

The vote above is correct and satisfies both properties. What does the ladder front end say about it now?

Answer

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

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

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

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

v8.4

cp benchmarks/chemical_batch/fbd_reactor_2oo3/clean.xml benchmarks/chemical_batch/fbd_reactor_2oo3/clean.ld
esbmc benchmarks/chemical_batch/fbd_reactor_2oo3/clean.ld --ld-props benchmarks/chemical_batch/fbd_reactor_2oo3/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	`VIOLATION`	`SAFE`	wrong	fail	0.014 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 ps1=NONDET(_Bool);
        ASSIGN ps2=NONDET(_Bool);
        ASSIGN ps3=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.

v8.4

State 1  thread 0
----------------------------------------------------
  ps1 = 0

State 2  thread 0
----------------------------------------------------
  ps2 = 1

State 3  thread 0
----------------------------------------------------
  ps3 = 1

State 4 file benchmarks/chemical_batch/fbd_reactor_2oo3/clean.ld thread 0
----------------------------------------------------
Violated property:
  file benchmarks/chemical_batch/fbd_reactor_2oo3/clean.ld
  P1
  !(ps1 && ps2 || ps2 && ps3 || ps1 && ps3) || trip

ERROR: UnsupportedConstruct(FBD body of POU 'trip_logic', tier=2)

Today it refuses the file. Until #7354 was fixed it answered VIOLATION with status: wrong, and the counterexample looked entirely plausible:

ps1 = 0
ps2 = 1
ps3 = 1

Two switches high, no trip, P1 broken. The program does trip on that input. The scan body was the giveaway:

1: IF !1 THEN GOTO 2
   ASSIGN ps1=NONDET(_Bool);
   ASSIGN ps2=NONDET(_Bool);
   ASSIGN ps3=NONDET(_Bool);
   GOTO 1
2:

Three inputs and nothing else. trip was never assigned, so it held its initial value of false forever, and a property demanding that it rise was broken by construction. The gate said fail and named trip as the one variable no statement in the body drove.

The C route¶

Recorded 2026-08-27T19:16:31Z. Every build ran the same command.

runner/record_via_c.py benchmarks/chemical_batch/fbd_reactor_2oo3/clean.xml benchmarks/chemical_batch/fbd_reactor_2oo3/props.yaml true --tool master=<path-to-esbmc>

which generates the C below and hands it to ESBMC as:

esbmc <generated>/harness.c -I $PLC_TOOLS/matiec/lib/C -I <generated> --k-induction --timeout 30s

Translated by Beremiz df4370c and MatIEC 7949c0b.

build	ESBMC	verdict	expected	outcome	cpu
master	8.4.0 `d88a9fa4`	`SAFE`	`SAFE`	correct	2.843 s

master found its solution by the forward condition; all states are reachable (k = 9).

What ESBMC was given. The harness the adapter generated, with the property written over the variables MatIEC emitted.

#include "iec_std_lib.h"
#include "POUS.h"
#include "POUS.c"

int main(void) {
  TRIP_LOGIC_data__ d = {0};
  TRIP_LOGIC_init__(&d, 0);
  for (int scan = 0; scan < 8; scan++) {
    __SET_VAR(d., PS1, , nondet_bool());
    __SET_VAR(d., PS2, , nondet_bool());
    __SET_VAR(d., PS3, , nondet_bool());
    TRIP_LOGIC_body__(&d);
    __ESBMC_assert(!((__GET_VAR(d.PS1,) && __GET_VAR(d.PS2,)) || (__GET_VAR(d.PS2,) && __GET_VAR(d.PS3,)) || (__GET_VAR(d.PS1,) && __GET_VAR(d.PS3,))) || __GET_VAR(d.TRIP,), "P1");
    __ESBMC_assert(!__GET_VAR(d.TRIP,) || ((__GET_VAR(d.PS1,) && __GET_VAR(d.PS2,)) || (__GET_VAR(d.PS2,) && __GET_VAR(d.PS3,)) || (__GET_VAR(d.PS1,) && __GET_VAR(d.PS3,))), "P2");
  }
  return 0;
}

SAFE, found by the forward condition at k = 9. The vote is correct and provably so.

Both answers were wrong for one reason¶

The bombed twin was refuted on the ladder route as well, and that row read correct.

That is the part worth sitting with. The same front end returned VIOLATION for the working reactor and VIOLATION for the broken one, because it read neither program. One of those rows counts as a pass in any table that compares verdict against expectation, and it was right by accident.

	ladder route, before #7354	ladder route, now	via-C	truth
clean	`VIOLATION`, gate fails	refused by name	`SAFE`	correct program
bomb	`VIOLATION`, gate fails	refused by name	`VIOLATION`	broken program

An accuracy score over the first column reports fifty percent and tells you nothing. The gate reported four failures out of four, and told you everything: no verdict there rested on the program in the file.

That is the argument for recording the encoding next to the verdict rather than the verdict alone, and it is not retired by the fix. The gate is what made this page writable in the first place, a year before the front end learned to say UnsupportedConstruct, and it is what still catches lesson 7.9, where the tool is confident and wrong today.