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

1 files changed, 13 insertions, 0 deletions

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;