test/regress/regress0/cvc3.userdoc.03.cvc

   1 bv : BITVECTOR(10);
   2 a : BOOLEAN;
   3
   4 % EXPECT: valid
   5 QUERY
   6  0bin01100000[5:3]=(0bin1111001@bv[0:0])[4:2]
   7  AND
   8  0bin1@(IF a THEN 0bin0 ELSE 0bin1 ENDIF) = (IF a THEN 0bin110 ELSE 0bin011 ENDIF)[1:0] ;