new option for doing top-level miplib substitutions (or not)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5c55adc7a394022eefcd5fd3f17a91840bcaccf5..73e2b84c4b06b2eac354975dd3cff0f059c9e836 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2252,7 +2252,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 {
+            } else if(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 d21ccc0eedc5f7ad376e50670abc7c586d3f580a..2a745a608dbe12a8408a506e06dff289f87723a8 100644 (file)
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -55,6 +55,9 @@ option arithMLTrick miplib-trick --enable-miplib-trick/--disable-miplib-trick bo
  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
+ does top-level substitution for miplib 'tmp' vars
+
 option doCutAllBounded --enable-cut-all-bounded/--disable-cut-all-bounded bool :default false :read-write
  turns on the integer solving step of periodically cutting all integer variables that have both upper and lower bounds
 / turns off the integer solving step of periodically cutting all integer variables that have both upper and lower bounds