1 2 3 4 5 6 7 8 9 10
%% This test borrowed from CVC3 regressions, bug15.cvc % 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