test/regress/regress0/arrays/constarr.cvc

   1 % EXPECT: unsat
   2 all1 : ARRAY INT OF INT;
   3 a, i : INT;
   4 ASSERT all1 = ARRAY(INT OF INT) : 1;
   5 ASSERT a = all1[i];
   6 ASSERT a /= 1;
   7 CHECKSAT TRUE;