summaryrefslogtreecommitdiff
path: root/test/regress/regress0/uflra/bug293.cvc
blob: 3bc91c7c5cf331a3a0e10f748f8bd3a9991ae165 (plain) 
1
2
3
4
5
6
7
8

% EXPECT: unsat
% EXIT: 20
x: REAL;
f: REAL -> REAL;
ASSERT NOT (f(1) = f(x));
ASSERT NOT (f(0) = f(x));
ASSERT (x = 0) XOR (x = 1);
CHECKSAT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback