test/regress/regress1/arith/arith-int-100.cvc


1
2
3
4
5
6
7
8

% EXPECT: invalid
x0, x1, x2, x3 : INT;
ASSERT (27 * x0) + (-21 * x1) + (-6 * x2) + (-6 * x3) > -15 ;
ASSERT  (-5 * x0) + (-10 * x1) + (2 * x2) + (-16 * x3) <= -7 ;
ASSERT  (25 * x0) + (25 * x1) + (-15 * x2) + (-32 * x3) > -31 ;
ASSERT  (17 * x0) + (-26 * x1) + (9 * x2) + (-28 * x3) >= -29 ;
ASSERT  (-10 * x0) + (-18 * x1) + (15 * x2) + (0 * x3) <= 32;
QUERY FALSE;