summaryrefslogtreecommitdiff
path: root/test/regress/regress0/arrays/constarr.cvc
blob: 406a1ce2b1ff30629f855fe6e07b377c61410e9f (plain) 
1
2
3
4
5
6
7

% EXPECT: unsat
all1 : ARRAY INT OF INT;
a, i : INT;
ASSERT all1 = ARRAY(INT OF INT) : 1;
ASSERT a = all1[i];
ASSERT a /= 1;
CHECKSAT TRUE;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback