summaryrefslogtreecommitdiff
path: root/test/regress/regress1/arith/arith-int-046.cvc
blob: d4d206c6edaa6872795ea55e2c8cd21bf1a3d2c1 (plain) 
1
2
3
4
5
6

% EXPECT: invalid
x0, x1, x2, x3 : INT;
ASSERT (2 * x0) + (-6 * x1) + (14 * x2) + (-24 * x3) > 4 ;
ASSERT  (-13 * x0) + (-2 * x1) + (-9 * x2) + (-7 * x3) >= 29 ;
ASSERT  (-11 * x0) + (28 * x1) + (-20 * x2) + (-2 * x3) >= 31;
QUERY FALSE;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback