Exception counterexample

[Fuhj-better]

Is there an issue with the tool's verification of |-> and |=>?
When I was validating the following code, I discovered a problem.

module counter(clk, reset, load, en, value);
    input clk;
    input reset;
    input load;
    input en;

    parameter WIDTH = 8;
    output[WIDTH-1:0] value;

    reg [WIDTH-1:0] value;
   
    always @(posedge clk or posedge reset)
       if (reset)	 
          value <= 0;
       else begin
         if (load) 
               value <= 0;
         else if (en)
            value <= value + 1;
      end

      assert property (@(posedge clk) (reset |-> value == 0));
      assert property (@(posedge clk) (!reset && load |-> value == 0));
      assert property (@(posedge clk) (!reset && !load && en && value<255 |-> value == $past(value) + 1));
      assert property (@(posedge clk) (!reset && !load && !en |-> value == $past(value)));
      assert property (@(posedge clk) (!reset && !load && en && value == 255 |-> value == 0));

endmodule

All the assertions were refuted, yet the simulation did not trigger any assertion failures. However, when I changed |-> to |=>, all the assertions were confirmed. This is because I observed that the counterexamples provided were based on the judgment of the next cycle, which clearly does not align with the logic of the code. Moreover, running the simulation under these circumstances would result in assertion failures. Why does this situation occur?