summaryrefslogtreecommitdiff
path: root/test/regress/regress0/arith/miplib2.cvc
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/arith/miplib2.cvc')
-rw-r--r--test/regress/regress0/arith/miplib2.cvc32
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback