[sv-ac] Question on vacuous success

Dmitry,
If I have the following (attached file)
 logic a=1, b=0, c;
  ap_abc: assert property(@ (posedge clk) a|-> b |-> c);
  ap_bc: assert property(@ (posedge clk) b |-> c);

We agree that the property (b |-> c) succeeds vacuously.
Question: If a vendor states the following in the assertion report, is he in
error, per LRM in claiming ap_abc as a PASS,
yet ap_bc as NO pass? I understand that if b==0 the property b |-> c is
vacuously true, which in essence is true.
But in my mind, it is not a true success, thus, a PASS count of 1 is
misleading.
I guess we need the cover of the sequence a ##0 b ##0 c
ASSERTION RESULTS:
-------------------------------------------------------
Name File(Line) Failure Pass
                                          Count Count
-------------------------------------------------------
/top/m1/ap_abc test_if.sv(25) 0 500
/top/m1/ap_bc test_if.sv(26) 0 0

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.