test/regress/regress0/bug585.cvc

   1 % EXPECT: sat
   2
   3 Cache: TYPE = ARRAY [0..100] OF [# addr: INT, data: REAL #];
   4 State: TYPE = [# pc: INT, cache: Cache #];
   5
   6 s0: State;
   7 s1: State = s0 WITH .cache[10].data := 2/3;
   8
   9 CHECKSAT;