Some cleanup of miplib regressions and options

9 files changed, 16 insertions, 13 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 73e2b84c4..4104c0916 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2202,7 +2202,6 @@ void SmtEnginePrivate::doMiplibTrick() {
           Debug("miplib") << "  -- INELIGIBLE " << (*j).first << " -- (insufficiently marked, got " << (*j).second << " for " << numVars << " vars, expected " << expected << endl;
         } else {
           if(false) { //checks[(*j).first] != coef[(*j).first][0] + coef[(*j).first][1]) {
-#warning fixme
             Debug("miplib") << "  -- INELIGIBLE " << (*j).first << " -- (not linear combination)" << endl;
           } else {
             Debug("miplib") << "  -- ELIGIBLE " << *i << " , " << (*j).first << " --" << endl;
@@ -2252,7 +2251,7 @@ void SmtEnginePrivate::doMiplibTrick() {
               //Warning() << "REPLACE         " << newAssertion[1] << endl;
               //Warning() << "ORIG            " << d_topLevelSubstitutions.getSubstitution(newAssertion[0]) << endl;
               Assert(d_topLevelSubstitutions.getSubstitution(newAssertion[0]) == newAssertion[1]);
-            } else if(arithMLTrickSubstitutions) {
+            } else if(options::arithMLTrickSubstitutions()) {
               d_topLevelSubstitutions.addSubstitution(newAssertion[0], newAssertion[1]);
             }
             Debug("miplib") << "addSubs: " << newAssertion[0] << " to " << newAssertion[1] << endl;
diff --git a/src/theory/arith/options b/src/theory/arith/options
index 2a745a608..e12120f33 100644
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -51,11 +51,11 @@ option arithRewriteEq --enable-arith-rewrite-equalities/--disable-arith-rewrite-
  turns on the preprocessing rewrite turning equalities into a conjunction of inequalities
 /turns off the preprocessing rewrite turning equalities into a conjunction of inequalities
 
-option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bool :default true
+option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bool :default false
  turns on the preprocessing step of attempting to infer bounds on miplib problems
 /turns off the preprocessing step of attempting to infer bounds on miplib problems
 
-option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs :default true
+option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs bool :default true
  does top-level substitution for miplib 'tmp' vars
 
 option doCutAllBounded --enable-cut-all-bounded/--disable-cut-all-bounded bool :default false :read-write
diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am
index 1510b15ad..b0cdc5b91 100644
--- a/test/regress/regress0/arith/Makefile.am
+++ b/test/regress/regress0/arith/Makefile.am
@@ -41,14 +41,16 @@ TESTS =	\
 	bug443.delta01.smt \
 	miplib.cvc \
 	miplib2.cvc \
-	miplibtrick.smt \
+	miplibtrick.smt
+#	problem__003.smt2
+
+EXTRA_DIST = $(TESTS) \
 	miplib-opt1217--27.smt \
 	miplib-opt1217--27.smt2 \
 	miplib-pp08a-3000.smt \
-	miplib-pp08a-3000.smt2
-#	problem__003.smt2
-
-EXTRA_DIST = $(TESTS)
+	miplib-pp08a-3000.smt2 \
+	miplib-opt1217--27.smt.expect \
+	miplib-pp08a-3000.smt.expect
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
diff --git a/test/regress/regress0/arith/miplib-opt1217--27.smt.expect b/test/regress/regress0/arith/miplib-opt1217--27.smt.expect
index 04a3504d7..f6ae1d85b 100644
--- a/test/regress/regress0/arith/miplib-opt1217--27.smt.expect
+++ b/test/regress/regress0/arith/miplib-opt1217--27.smt.expect
@@ -1,3 +1,3 @@
-% COMMAND-LINE: --tlimit 5000
+% COMMAND-LINE: --enable-miplib-trick
 % EXPECT: unsat
 % EXIT: 20
diff --git a/test/regress/regress0/arith/miplib-opt1217--27.smt2 b/test/regress/regress0/arith/miplib-opt1217--27.smt2
index 49d652d80..e6ac8e69e 100644
--- a/test/regress/regress0/arith/miplib-opt1217--27.smt2
+++ b/test/regress/regress0/arith/miplib-opt1217--27.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --tlimit 5000
+; COMMAND-LINE: --enable-miplib-trick
 ; EXPECT: unsat
 ; EXIT: 20
 (set-logic QF_LRA)
diff --git a/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect b/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect
index 04a3504d7..f6ae1d85b 100644
--- a/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect
+++ b/test/regress/regress0/arith/miplib-pp08a-3000.smt.expect
@@ -1,3 +1,3 @@
-% COMMAND-LINE: --tlimit 5000
+% COMMAND-LINE: --enable-miplib-trick
 % EXPECT: unsat
 % EXIT: 20
diff --git a/test/regress/regress0/arith/miplib-pp08a-3000.smt2 b/test/regress/regress0/arith/miplib-pp08a-3000.smt2
index 5bbf0a758..e94506a23 100644
--- a/test/regress/regress0/arith/miplib-pp08a-3000.smt2
+++ b/test/regress/regress0/arith/miplib-pp08a-3000.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --tlimit 5000
+; COMMAND-LINE: --enable-miplib-trick
 ; EXPECT: unsat
 ; EXIT: 10
 (set-logic QF_LRA)
diff --git a/test/regress/regress0/arith/miplib.cvc b/test/regress/regress0/arith/miplib.cvc
index 4cd4b25b5..db2aa2ac5 100644
--- a/test/regress/regress0/arith/miplib.cvc
+++ b/test/regress/regress0/arith/miplib.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --enable-miplib-trick
 % EXPECT: sat
 % EXIT: 10
 
diff --git a/test/regress/regress0/arith/miplib2.cvc b/test/regress/regress0/arith/miplib2.cvc
index 6fbfcab0f..84f17e848 100644
--- a/test/regress/regress0/arith/miplib2.cvc
+++ b/test/regress/regress0/arith/miplib2.cvc
@@ -1,3 +1,4 @@
+% COMMAND-LINE: --enable-miplib-trick
 % EXPECT: sat
 % EXIT: 10