- The learned clauses from the miplib trick were being added twice. This was slowing...

diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 6fb538fac8eb92a36221f8aa5ce89d590a31b5f3..5486513587dcea75ecea9777f0a161b4e6bb7dc2 100644 (file)
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -212,13 +212,19 @@ void ArithStaticLearner::iteConstant(TNode n, NodeBuilder<>& learned){
 
 
 void ArithStaticLearner::postProcess(NodeBuilder<>& learned){
+  vector<TNode> keys;
+  VarToNodeSetMap::iterator mipIter = d_miplibTrick.begin();
+  VarToNodeSetMap::iterator endMipLibTrick = d_miplibTrick.end();
+  for(; mipIter != endMipLibTrick; ++mipIter){
+    keys.push_back(mipIter->first);
+  }
 
   // == 3-FINITE VALUE SET ==
-  VarToNodeSetMap::iterator i = d_miplibTrick.begin();
-  VarToNodeSetMap::iterator endMipLibTrick = d_miplibTrick.end();
-  for(; i != endMipLibTrick; ++i){
-    TNode var = i->first;
-    const set<Node>& imps = i->second;
+  vector<TNode>::iterator keyIter = keys.begin();
+  vector<TNode>::iterator endKeys = keys.end();
+  for(; keyIter != endKeys; ++keyIter){
+    TNode var = *keyIter;
+    const set<Node>& imps = d_miplibTrick[var];
 
     Assert(!imps.empty());
     vector<Node> conditions;
@@ -253,6 +259,7 @@ void ArithStaticLearner::postProcess(NodeBuilder<>& learned){
     Result isTaut = PropositionalQuery::isTautology(possibleTaut);
     if(isTaut == Result(Result::VALID)){
       miplibTrick(var, values, learned);
+      d_miplibTrick.erase(var);
     }
   }
 }