IFV PSL , using VHDL comparison operator

Hi ,

  I have an assertion in my PSL file -

 Assert1 : assert always ( { {R_seq} &&  {T /= A and (Z  = '0' ) } }  |=>  { D = ADDBUS }  ) @ (rising_edge(CLK)  ;  

 where  R_Seq is defined as - 

   sequence  R_Seq = { A1 and B1 } ;

 The assertion passed .

 Now , out of curiosity I have written a negative check -

 Assert2: assert always( { {R_seq} && { T/=A and (Z = '0' ) } }   |=>  {  D /= ADDBUS } ) @(rising_edge(CLK) ;

  This assertion also passed !!! .

  From my understanding , since the LHS are same and RHS are contradicting , either Assert1 or Assert2 should surely fail .

  Please explain to me , if my understanding is correct .

  I was using IFV version 8.20 .

 Also , would like to mention that trigger for both Assert1 and Assert2 passed .