path: root/test/regress/regress0/arith/integers/arith-interval.cvc

% EXPECT: valid
x: INT;
P: INT -> BOOLEAN;

ASSERT 1 <= x AND x <= 2;
ASSERT P(1) AND P(2);
QUERY P(x);