summaryrefslogtreecommitdiff
path: root/test/regress/regress0/uflra/simple.02.cvc
blob: a14ca8a1f7f24fe1e29924495866c13df579e7ca (plain) 
1
2
3
4
5
6
7
8
9
10

% EXPECT: unsat
% EXIT: 20
x, y: REAL;
f: REAL -> REAL;

ASSERT (x <= y);
ASSERT (y <= x);
ASSERT NOT (f(x) = f(y));

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