Fix to miplib trick to make it less "cautious" and apply in more cases

3 files changed, 49 insertions, 0 deletions

diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index b0cdc5b91..40f04b239 100644
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -41,6 +41,8 @@ TESTS =	\
 	bug443.delta01.smt \
 	miplib.cvc \
 	miplib2.cvc \
+	miplib3.cvc \
+	miplib4.cvc \
 	miplibtrick.smt
 #	problem__003.smt2
 
diff --git a/test/regress/regress0/arith/miplib3.cvc b/test/regress/regress0/arith/miplib3.cvc
new file mode 100644
index 000000000..009effb74
--- /dev/null
+++ b/test/regress/regress0/arith/miplib3.cvc
@@ -0,0 +1,34 @@
+% COMMAND-LINE: --enable-miplib-trick
+% EXPECT: sat
+% EXIT: 10
+
+tmp1, tmp2, tmp3, tmp4 : 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;
+
+ASSERT NOT x AND (NOT y AND TRUE) => tmp4 = 0;
+ASSERT     x AND (NOT y AND TRUE) => tmp4 = 4;
+ASSERT NOT x AND (    y AND TRUE) => tmp4 = 6;
+ASSERT     x AND (    y AND TRUE) => tmp4 = 10;
+
+CHECKSAT;
diff --git a/test/regress/regress0/arith/miplib4.cvc b/test/regress/regress0/arith/miplib4.cvc
new file mode 100644
index 000000000..d56015222
--- /dev/null
+++ b/test/regress/regress0/arith/miplib4.cvc
@@ -0,0 +1,13 @@
+% 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;