test/regress/regress0/arith/miplib4.cvc


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15

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

tmp1 : INT;
x, y : BOOLEAN;

% nonlinear combination, not eligible for miplib trick replacement
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;

ASSERT tmp1 > 10;

CHECKSAT;