path: root/test/regress/regress0/arith/miplib4.cvc

% COMMAND-LINE: --enable-miplib-trick
% EXPECT: sat
% EXIT: 10

tmp1 : INT;
x, y : BOOLEAN;

ASSERT NOT x AND (NOT y AND TRUE) => tmp1 = 0;
ASSERT     x AND (NOT y AND TRUE) => tmp1 = 4;
ASSERT NOT x AND (    y AND TRUE) => tmp1 = 6;
ASSERT     x AND (    y AND TRUE) => tmp1 = 12;

CHECKSAT;