1 files changed, 11 insertions, 2 deletions
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 9ae7cd1c2..4ee176cf1 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -19,6 +19,7 @@
 
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/arith_static_learner.h"
+#include "theory/arith/options.h"
 
 #include "util/propositional_query.h"
 
@@ -61,6 +62,13 @@ ArithStaticLearner::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_avgNumMiplibtrickValues);
 }
 
+void ArithStaticLearner::miplibTrickInsert(Node key, Node value){
+  if(options::arithMLTrick()){
+    d_miplibTrick.insert(key, value);
+  }
+}
+
+
 void ArithStaticLearner::staticLearning(TNode n, NodeBuilder<>& learned){
 
   vector<TNode> workList;
@@ -138,7 +146,8 @@ void ArithStaticLearner::process(TNode n, NodeBuilder<>& learned, const TNodeSet
         TNode var = n[1][0];
         Node current = (d_miplibTrick.find(var)  == d_miplibTrick.end()) ?
           mkBoolNode(false) : d_miplibTrick[var];
-        d_miplibTrick.insert(var, n.orNode(current));
+
+        miplibTrickInsert(var, n.orNode(current));
         Debug("arith::miplib") << "insert " << var  << " const " << n << endl;
       }
     }
@@ -338,7 +347,7 @@ void ArithStaticLearner::postProcess(NodeBuilder<>& learned){
     Result isTaut = PropositionalQuery::isTautology(possibleTaut);
     if(isTaut == Result(Result::VALID)){
       miplibTrick(var, values, learned);
-      d_miplibTrick.insert(var, mkBoolNode(false));
+      miplibTrickInsert(var, mkBoolNode(false));
     }
     ++keyIter;
   }