summaryrefslogtreecommitdiff
path: root/test/regress/regress0/uf/simple.03.cvc
blob: 15fe5907ce5c76cf8c50620e07f73a50264d9a07 (plain)
1
2
3
4
5
6
7
8
9
10
11
% EXPECT: entailed
A: TYPE;
B: TYPE;
x, y: A;
a, b: A;

f: A -> B;

ASSERT (x = a AND y = a) OR (x = b AND y = b);
QUERY (f(x) = f(y));

generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback