SVA, counter with features and formal verification

SystemVerilog
5

In reply to ben@SystemVerilog.us:

Thanks Ben. I have not yet had the time to trial your mehtod, but there’s one interesting part:

ap_min_load: assume property(@(posedge clk) disable iff (!rst_n) 
            ld |-> not(data_in not(data_in > MAX_COUNT))
            cover_count++; else fail_count++ ;

What is this else part? I have been trying to if/else inside my properties but me and the tools seem to have a different understanding about what I want to achieve.