summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bug1.cvc
blob: 2b59638d1cb17ad4d1031378ff164cb3a34c3113 (plain)
1
2
3
4
5
6
7
8
9
% EXPECT: VALID
x : REAL;
y : REAL;
f : REAL -> REAL;
ASSERT ((x > y) => f(x) > f (y));
ASSERT (x = 3);
ASSERT (y = 2);
QUERY(f(x) > f (y));
% EXIT: 20
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback