Legal ways to specify the leading clock in SVA

In reply to ben@SystemVerilog.us:

Hi Ben,
I was trying a few variations of always block


  property  pr1;
    a ##2 b;
  endproperty

1) always  begin
     if ( bstate )  begin
       @( posedge clk );
       assert  property( pr1 )  $display("TIME:%2t  Assertion  pr1  PASS", $time );
                          else  $display("TIME:%2t  Assertion  pr1  Fails", $time );
     end 
    end 

2) always  begin
     @( posedge clk );
     if ( bstate )  begin
       
       assert  property( pr1 )  $display("TIME:%2t  Assertion  pr1  PASS", $time );
                          else  $display("TIME:%2t  Assertion  pr1  Fails", $time );
     end 
    end 

3)  always@(posedge clk)  begin
     if ( bstate )  begin
       @(negedge regcheck);
       assert  property( pr1 )  $display("TIME:%2t  Assertion  pr1  PASS", $time );
                          else  $display("TIME:%2t  Assertion  pr1  Fails", $time );
     end 
    end 

4)  always@(posedge clk)  begin
     #1;
     if ( bstate )  begin
       assert  property( pr1 )  $display("TIME:%2t  Assertion  pr1  PASS", $time );
                          else  $display("TIME:%2t  Assertion  pr1  Fails", $time );
     end 
    end  

I observe that although all tools unanimously throw compilation error for (1),(2) and (4).
Whereas some tools allow (3).

Would like to hear your thoughts/comments on the above four code ?