test/regress/regress0/datatypes/tuple-record-bug.cvc

   1 % EXPECT: invalid
   2
   3 Mem_0 : TYPE = ARRAY INT OF INT;
   4
   5 MEMORY : TYPE = [# int : Mem_0, queries : Mem_0 #];
   6
   7 x : INT;
   8
   9 foo : MEMORY -> MEMORY
  10     = LAMBDA (x : MEMORY) : LET y = x WITH .int := x.int IN y;
  11
  12 m : MEMORY;
  13
  14 w : [MEMORY,INT] =
  15         IF x = 0
  16         THEN (foo(m),0)
  17         ELSE (m, 0)
  18         ENDIF;
  19
  20 QUERY w.1 = 1;