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

% EXPECT: unsat
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