diff options
Diffstat (limited to 'test/regress/regress0/arith/miplib2.cvc')
-rw-r--r-- | test/regress/regress0/arith/miplib2.cvc | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/test/regress/regress0/arith/miplib2.cvc b/test/regress/regress0/arith/miplib2.cvc deleted file mode 100644 index ce2e9712e..000000000 --- a/test/regress/regress0/arith/miplib2.cvc +++ /dev/null @@ -1,32 +0,0 @@ -% COMMAND-LINE: --miplib-trick -% EXPECT: sat - -tmp1, tmp2, tmp3 : INT; -x, y, z : BOOLEAN; - -% x = {0, 1}, (NOT x) = 1 - x -% i*Nx + j*Ny + k = 0 -% i*x + j*Ny + k = 4 -% i*Nx + j*y + k = 6 -% i*x + j*y + k = 10 - -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 = 10; - -ASSERT NOT x AND (NOT z AND TRUE) => tmp2 = 0; -ASSERT x AND (NOT z AND TRUE) => tmp2 = 2; -ASSERT NOT x AND ( z AND TRUE) => tmp2 = 9; -ASSERT x AND ( z AND TRUE) => tmp2 = 11; - -ASSERT NOT y AND (NOT z AND TRUE) => tmp3 = 0; -ASSERT y AND (NOT z AND TRUE) => tmp3 = 5; -ASSERT NOT y AND ( z AND TRUE) => tmp3 = 16; -ASSERT y AND ( z AND TRUE) => tmp3 = 21; - -% miplib trick does not apply to blocks 1 and 2, x occurs outside -% of the tmp definitions -ASSERT x; - -CHECKSAT; |