test/regress/regress2/arith/arith-int-098.cvc


1
2
3
4
5
6
7
8

% EXPECT: not_entailed
x0, x1, x2, x3 : INT;
ASSERT  (-28 * x0) + (12 * x1) + (-19 * x2) + (10 * x3) = 16 ;
ASSERT  (19 * x0) + (-25 * x1) + (-8 * x2) + (-32 * x3) = 12;
ASSERT (18 * x0) + (21 * x1) + (5 * x2) + (-14 * x3) < -12 ;
ASSERT  (-13 * x0) + (32 * x1) + (-5 * x2) + (-13 * x3) <= -15 ;
ASSERT  (30 * x0) + (-19 * x1) + (28 * x2) + (-27 * x3) <= -18 ;
QUERY FALSE;