`--liveness-to-safety` reports PROVED for a false liveness property with >=2 fairness assumptions

[tautschnig]

--liveness-to-safety reports PROVED for a false liveness property in the presence of ≥2 fairness assumptions

Summary

ebmc --liveness-to-safety reports PROVED for an s_eventually property that is
plainly false, when the module contains two or more assume property (always s_eventually …)
fairness assumptions. The --buechi engine and plain bounded model checking both correctly
report REFUTED on the same input. A single fairness assumption (or none) does not trigger
the problem, so the issue is specific to how --liveness-to-safety combines multiple liveness
assumptions.

Environment

• ebmc: hw-cbmc at commit 7b05b8d (built from source, make -C src)
• Spot: ltl2tgba (spot) 2.14.3 (for --buechi)
• OS: Ubuntu 24.04, x86_64

Minimal reproducer

// x is a register stuck at 0 forever, so "s_eventually x" is FALSE.
module min_fair2(input clk, input act);
  reg x; initial x = 1'b0;
  always @(posedge clk) x <= x;                 // x never changes
  assume property (always s_eventually act);    // fairness 1
  assume property (always s_eventually (!act));  // fairness 2
  p_live: assert property (s_eventually x);      // FALSE
endmodule

Observed vs expected

command	result	expected
ebmc min.v --systemverilog --top min_fair2 --liveness-to-safety --bdd	PROVED	REFUTED
ebmc min.v --systemverilog --top min_fair2 --liveness-to-safety --bound 40	PROVED up to bound 40	REFUTED
ebmc min.v --systemverilog --top min_fair2 --buechi	REFUTED	REFUTED
ebmc min.v --systemverilog --top min_fair2 --bound 40	REFUTED	REFUTED

x is initialized to 0 and never assigned anything else, so s_eventually x can never hold;
REFUTED is correct. --liveness-to-safety returning PROVED is unsound.

Minimization / trigger isolation

• No fairness assumption — correct:

  module min_stuck(input clk);
    reg x; initial x = 1'b0;
    always @(posedge clk) x <= x;
    p_live: assert property (s_eventually x);   // l2s, buechi, bmc all REFUTE (correct)
  endmodule

• One fairness assumption — correct:

  module min_fair1(input clk, input act);
    reg x; initial x = 1'b0;
    always @(posedge clk) x <= x;
    assume property (always s_eventually act);
    p_live: assert property (s_eventually x);   // l2s REFUTES (correct)
  endmodule

• Two fairness assumptions (min_fair2 above) — --liveness-to-safety wrongly PROVES.

So the trigger is ≥2 always s_eventually fairness assumptions.

Hypothesis

The liveness-to-safety translation appears to mis-combine multiple always s_eventually
fairness assumptions into its loop/acceptance condition, erroneously excluding the fair
counterexample lasso (the state where x stays 0 while act toggles — which satisfies both
s_eventually act and s_eventually !act). As a result the safety translation is vacuously
discharged and the false liveness property is reported PROVED.

Impact

Any --liveness-to-safety proof of a liveness property in a model with multiple fairness
assumptions cannot be trusted; it can report PROVED for false properties. --buechi is a
sound alternative.