commented out SimplifyAssertions Pass, will refactor in the future

3 files changed, 514 insertions, 89 deletions

diff --git a/src/preproc/preprocessing_passes_core.cpp b/src/preproc/preprocessing_passes_core.cpp
index 25bca94b5..5abf8ce68 100644
--- a/src/preproc/preprocessing_passes_core.cpp
+++ b/src/preproc/preprocessing_passes_core.cpp
@@ -4,6 +4,8 @@
 #include <string>
 #include <stack>
 #include "expr/node_manager_attributes.h"
+#include "expr/node_self_iterator.h"
+#include "smt_util/boolean_simplification.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/fun_def_process.h"
@@ -17,11 +19,15 @@
 #include "options/bv_options.h"
 #include "options/uf_options.h"
 #include "options/proof_options.h"
+#include "options/arith_options.h"
 #include "util/ntuple.h"
 
 using namespace std;
 
 namespace CVC4 {
+
+using namespace theory;
+
 namespace preproc {
 
 ExpandingDefinitionsPass::ExpandingDefinitionsPass(ResourceManager* resourceManager, SmtEngine* smt, TimerStat definitionExpansionTime) : PreprocessingPass(resourceManager), d_smt(smt), d_definitionExpansionTime(definitionExpansionTime){
@@ -1045,7 +1051,6 @@ PreprocessingPassResult CNFPass::apply(AssertionPipeline* assertionsToPreprocess
   return PreprocessingPassResult(true);
 }
 
-/**
 RepeatSimpPass::RepeatSimpPass(ResourceManager* resourceManager, 
     theory::SubstitutionMap* topLevelSubstitutions,
     unsigned simplifyAssertionsDepth, bool* noConflict, 
@@ -1057,15 +1062,9 @@ RepeatSimpPass::RepeatSimpPass(ResourceManager* resourceManager,
     d_realAssertionsEnd(realAssertionsEnd){
 }
 
-<<<<<<< HEAD
 bool RepeatSimpPass::checkForBadSkolems(TNode n, TNode skolem, unordered_map<Node, bool, NodeHashFunction>& cache)
 {
   unordered_map<Node, bool, NodeHashFunction>::iterator it;
-=======
-bool RepeatSimpPass::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache)
-{
-  hash_map<Node, bool, NodeHashFunction>::iterator it;
->>>>>>> 93c2bbb764e34cd5285607dcb2bc4872bbe92456
   it = cache.find(n);
   if (it != cache.end()) {
     return (*it).second;
@@ -1096,15 +1095,9 @@ bool RepeatSimpPass::checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bo
   return false;
 }
 
-<<<<<<< HEAD
 void RepeatSimpPass::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache)
 {
   unordered_map<Node, bool, NodeHashFunction>::iterator it;
-=======
-void RepeatSimpPass::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Node, bool, NodeHashFunction>& cache)
-{
-  hash_map<Node, bool, NodeHashFunction>::iterator it;
->>>>>>> 93c2bbb764e34cd5285607dcb2bc4872bbe92456
   it = cache.find(n);
   if (it != cache.end()) {
     return;
@@ -1129,10 +1122,6 @@ void RepeatSimpPass::collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Nod
 
 
 PreprocessingPassResult RepeatSimpPass::apply(AssertionPipeline* assertionsToPreprocess){
-    Chat() << "re-simplifying assertions..." << std::endl;
-    ScopeCounter depth(d_simplifyAssertionsDepth);
-  //  *noConflict &= simplifyAssertions();
-    if (*noConflict) {
       // Need to fix up assertion list to maintain invariants:
       // Let Sk be the set of Skolem variables introduced by ITE's.  Let <_sk be the order in which these variables were introduced
       // during ite removal.
@@ -1187,32 +1176,29 @@ PreprocessingPassResult RepeatSimpPass::apply(AssertionPipeline* assertionsToPre
         }
         (*assertionsToPreprocess)[d_realAssertionsEnd - 1] = theory::Rewriter::rewrite(Node(builder));
        }
-      // For some reason this is needed for some benchmarks, such as
-      // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
-      // Figure it out later
-      removeITEs();
-      //      Assert(iteRewriteAssertionsEnd == d_assertions.size());
-    }
-  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << std::endl;
  return PreprocessingPassResult(true);
 }
-
+/*
 SimplifyAssertionsPass::SimplifyAssertionsPass(
    ResourceManager* resourceManager, unsigned simplifyAssertionsDepth, 
    SmtEngine* smt, bool propagatorNeedsFinish, 
-   theory::booleans::CircuitPropagator propagator,
-   context::CDO<unsigned> substitutionsIndex,
-   std::vector<Node> nonClausalLearnedLiterals, Node dtrue, 
-   TimerStat nonclausalSimplificationTime) : 
+   theory::booleans::CircuitPropagator* propagator,
+   context::CDO<unsigned>* substitutionsIndex,
+   std::vector<Node>* nonClausalLearnedLiterals, Node dtrue, 
+   TimerStat nonclausalSimplificationTime, unsigned realAssertionsEnd,
+   theory::SubstitutionMap* topLevelSubstitutions,
+   bool doConstantProp, std::vector<Node>* boolVars, context::Context* fakeContext) : 
    PreprocessingPass(resourceManager),
    d_simplifyAssertionsDepth(simplifyAssertionsDepth),
    d_smt(smt), d_propagatorNeedsFinish(propagatorNeedsFinish), 
    d_propagator(propagator), d_substitutionsIndex(substitutionsIndex), 
    d_nonClausalLearnedLiterals(nonClausalLearnedLiterals),
-   d_true(dtrue), d_nonclausalSimplificationTime(nonclausalSimplificationTime) {
+   d_true(dtrue), d_nonclausalSimplificationTime(nonclausalSimplificationTime),
+   d_realAssertionsEnd(realAssertionsEnd), 
+   d_topLevelSubstitutions(topLevelSubstitutions), d_doConstantProp(doConstantProp), d_boolVars(boolVars), d_fakeContext(fakeContext) {
 }
 
-void SimplifyAssertionsPass::addFormula(TNode n, bool inUnsatCore, bool inInput, AssertionPipeline d_assertions)
+void SimplifyAssertionsPass::addFormula(TNode n, bool inUnsatCore, AssertionPipeline &d_assertions, bool inInput)
   throw(TypeCheckingException, LogicException) {
 
   if (n == d_true) {
@@ -1264,10 +1250,10 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
   }
 
   if(d_propagatorNeedsFinish) {
-    d_propagator.finish();
+    d_propagator->finish();
     d_propagatorNeedsFinish = false;
   }
-  d_propagator.initialize();
+  d_propagator->initialize();
 
   // Assert all the assertions to the propagator
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
@@ -1275,40 +1261,40 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
   for (unsigned i = 0; i < d_assertions.size(); ++ i) {
     Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
     // Don't reprocess substitutions
-    if (d_substitutionsIndex > 0 && i == d_substitutionsIndex) {
+    if (*d_substitutionsIndex > 0 && i == *d_substitutionsIndex) {
       continue;
     }
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions[i] << endl;
     Debug("cores") << "d_propagator assertTrue: " << d_assertions[i] << std::endl;
-    d_propagator.assertTrue(d_assertions[i]);
+    d_propagator->assertTrue(d_assertions[i]);
   }
 
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                     << "propagating" << endl;
-  if (d_propagator.propagate()) {
+  if (d_propagator->propagate()) {
     // If in conflict, just return false
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                       << "conflict in non-clausal propagation" << endl;
     Node falseNode = NodeManager::currentNM()->mkConst<bool>(false);
     Assert(!options::unsatCores() && !options::fewerPreprocessingHoles());
     d_assertions.clear();
-    addFormula(falseNode, false, false, d_assertions);
+    addFormula(falseNode, false, d_assertions, false) ;
     d_propagatorNeedsFinish = true;
     return false;
   }
 
 
-  Trace("simplify") << "Iterate through " << d_nonClausalLearnedLiterals.size() << " learned literals." << std::endl;
+  Trace("simplify") << "Iterate through " << d_nonClausalLearnedLiterals->size() << " learned literals." << std::endl;
   // No conflict, go through the literals and solve them
   theory::SubstitutionMap constantPropagations(d_smt->d_context);
   theory::SubstitutionMap newSubstitutions(d_smt->d_context);
   theory::SubstitutionMap::iterator pos;
   unsigned j = 0;
-  for(unsigned i = 0, i_end = d_nonClausalLearnedLiterals.size(); i < i_end; ++ i) {
+  for(unsigned i = 0, i_end = d_nonClausalLearnedLiterals->size(); i < i_end; ++ i) {
     // Simplify the literal we learned wrt previous substitutions
-    Node learnedLiteral = d_nonClausalLearnedLiterals[i];
+    Node learnedLiteral = (*d_nonClausalLearnedLiterals)[i];
     Assert(theory::Rewriter::rewrite(learnedLiteral) == learnedLiteral);
-    Assert(d_topLevelSubstitutions.apply(learnedLiteral) == learnedLiteral);
+    Assert(d_topLevelSubstitutions->apply(learnedLiteral) == learnedLiteral);
     Trace("simplify") << "Process learnedLiteral : " << learnedLiteral << std::endl;
     Node learnedLiteralNew = newSubstitutions.apply(learnedLiteral);
     if (learnedLiteral != learnedLiteralNew) {
@@ -1333,10 +1319,10 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
         // If the learned literal simplifies to false, we're in conflict
         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                           << "conflict with "
-                          << d_nonClausalLearnedLiterals[i] << endl;
+                          << (*d_nonClausalLearnedLiterals)[i] << endl;
         Assert(!options::unsatCores());
         d_assertions.clear();
-        addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false, d_assertions);
+        addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, d_assertions, false);
         d_propagatorNeedsFinish = true;
         return false;
       }
@@ -1347,11 +1333,11 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                       << "solving " << learnedLiteral << endl;
 
-    Theory::PPAssertStatus solveStatus =
+    theory::Theory::PPAssertStatus solveStatus =
       d_smt->d_theoryEngine->solve(learnedLiteral, newSubstitutions);
 
     switch (solveStatus) {
-      case Theory::PP_ASSERT_STATUS_SOLVED: {
+      case theory::Theory::PP_ASSERT_STATUS_SOLVED: {
         // The literal should rewrite to true
         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                           << "solved " << learnedLiteral << endl;
@@ -1365,14 +1351,14 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
         // else fall through
         break;
       }
-      case Theory::PP_ASSERT_STATUS_CONFLICT:
+      case theory::Theory::PP_ASSERT_STATUS_CONFLICT:
         // If in conflict, we return false
         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                           << "conflict while solving "
                           << learnedLiteral << endl;
         Assert(!options::unsatCores());
         d_assertions.clear();
-        addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false, d_assertions);
+        addFormula(NodeManager::currentNM()->mkConst<bool>(false), false,d_assertions, false);
         d_propagatorNeedsFinish = true;
         return false;
       default:
@@ -1390,7 +1376,7 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
           }
           Assert(!t.isConst());
           Assert(constantPropagations.apply(t) == t);
-          Assert(d_topLevelSubstitutions.apply(t) == t);
+          Assert(d_topLevelSubstitutions->apply(t) == t);
           Assert(newSubstitutions.apply(t) == t);
           constantPropagations.addSubstitution(t, c);
           // vector<pair<Node,Node> > equations;
@@ -1405,7 +1391,7 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
         }
         else {
           // Keep the literal
-          d_nonClausalLearnedLiterals[j++] = d_nonClausalLearnedLiterals[i];
+          (*d_nonClausalLearnedLiterals)[j++] = (*d_nonClausalLearnedLiterals)[i];
         }
         break;
     }
@@ -1424,8 +1410,8 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
   // 4. each lhs of constantPropagations is different from each rhs
   for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) {
     Assert((*pos).first.isVar());
-    Assert(d_topLevelSubstitutions.apply((*pos).first) == (*pos).first);
-    Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second);
+    Assert(d_topLevelSubstitutions->apply((*pos).first) == (*pos).first);
+    Assert(d_topLevelSubstitutions->apply((*pos).second) == (*pos).second);
     Assert(newSubstitutions.apply(newSubstitutions.apply((*pos).second)) == newSubstitutions.apply((*pos).second));
   }
   for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
@@ -1445,13 +1431,13 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
     // }
     Assert(constantPropagations.apply((*pos).second) == (*pos).second);
   }
-//#endif  CVC4_ASSERTIONS 
+ #endif  //CVC4_ASSERTIONS 
 
   // Resize the learnt
   Trace("simplify") << "Resize non-clausal learned literals to " << j << std::endl;
-  d_nonClausalLearnedLiterals.resize(j);
+  d_nonClausalLearnedLiterals->resize(j);
 
-  hash_set<TNode, TNodeHashFunction> s;
+  unordered_set<TNode, TNodeHashFunction> s;
   Trace("debugging") << "NonClausal simplify pre-preprocess\n";
   for (unsigned i = 0; i < d_assertions.size(); ++ i) {
     Node assertion = d_assertions[i];
@@ -1482,9 +1468,9 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
   }
 
   // If in incremental mode, add substitutions to the list of assertions
-  if (d_substitutionsIndex > 0) {
+  if (*d_substitutionsIndex > 0) {
     NodeBuilder<> substitutionsBuilder(kind::AND);
-    substitutionsBuilder << d_assertions[d_substitutionsIndex];
+    substitutionsBuilder << d_assertions[*d_substitutionsIndex];
     pos = newSubstitutions.begin();
     for (; pos != newSubstitutions.end(); ++pos) {
       // Add back this substitution as an assertion
@@ -1494,12 +1480,12 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
       Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl;
     }
     if (substitutionsBuilder.getNumChildren() > 1) {
-      d_assertions.replace(d_substitutionsIndex,
+      d_assertions.replace(*d_substitutionsIndex,
         theory::Rewriter::rewrite(Node(substitutionsBuilder)));
     }
   } else {
     // If not in incremental mode, must add substitutions to model
-    TheoryModel* m = d_smt->d_theoryEngine->getModel();
+    theory::TheoryModel* m = d_smt->d_theoryEngine->getModel();
     if(m != NULL) {
       for(pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) {
         Node n = (*pos).first;
@@ -1514,9 +1500,9 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
   Assert(d_realAssertionsEnd <= d_assertions.size());
   learnedBuilder << d_assertions[d_realAssertionsEnd - 1];
 
-  for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) {
-    Node learned = d_nonClausalLearnedLiterals[i];
-    Assert(d_topLevelSubstitutions.apply(learned) == learned);
+  for (unsigned i = 0; i < d_nonClausalLearnedLiterals->size(); ++ i) {
+    Node learned = (*d_nonClausalLearnedLiterals)[i];
+    Assert(d_topLevelSubstitutions->apply(learned) == learned);
     Node learnedNew = newSubstitutions.apply(learned);
     if (learned != learnedNew) {
       learned = theory::Rewriter::rewrite(learnedNew);
@@ -1539,11 +1525,11 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
                       << "non-clausal learned : "
                       << learned << endl;
   }
-  d_nonClausalLearnedLiterals.clear();
+  d_nonClausalLearnedLiterals->clear();
 
   for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
     Node cProp = (*pos).first.eqNode((*pos).second);
-    Assert(d_topLevelSubstitutions.apply(cProp) == cProp);
+    Assert(d_topLevelSubstitutions->apply(cProp) == cProp);
     Node cPropNew = newSubstitutions.apply(cProp);
     if (cProp != cPropNew) {
       cProp = theory::Rewriter::rewrite(cPropNew);
@@ -1562,7 +1548,7 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
   // Add new substitutions to topLevelSubstitutions
   // Note that we don't have to keep rhs's in full solved form
   // because SubstitutionMap::apply does a fixed-point iteration when substituting
-  d_topLevelSubstitutions.addSubstitutions(newSubstitutions);
+  d_topLevelSubstitutions->addSubstitutions(newSubstitutions);
 
   if(learnedBuilder.getNumChildren() > 1) {
     d_assertions.replace(d_realAssertionsEnd - 1,
@@ -1573,6 +1559,420 @@ bool SimplifyAssertionsPass::nonClausalSimplify(AssertionPipeline &d_assertions)
   return true;
 }
 
+void SimplifyAssertionsPass::traceBackToAssertions(const std::vector<Node>& nodes, std::vector<TNode>& assertions) {
+  const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator->getBackEdges();
+  for(vector<Node>::const_iterator i = nodes.begin(); i != nodes.end(); ++i) {
+    booleans::CircuitPropagator::BackEdgesMap::const_iterator j = backEdges.find(*i);
+    // term must appear in map, otherwise how did we get here?!
+    Assert(j != backEdges.end());
+    // if term maps to empty, that means it's a top-level assertion
+    if(!(*j).second.empty()) {
+      traceBackToAssertions((*j).second, assertions);
+    } else {
+      assertions.push_back(*i);
+    }
+  }
+}
+
+size_t SimplifyAssertionsPass::removeFromConjunction(Node& n, const std::unordered_set<unsigned long>& toRemove) {
+  Assert(n.getKind() == kind::AND);
+  size_t removals = 0;
+  for(Node::iterator j = n.begin(); j != n.end(); ++j) {
+    size_t subremovals = 0;
+    Node sub = *j;
+    if(toRemove.find(sub.getId()) != toRemove.end() ||
+       (sub.getKind() == kind::AND && (subremovals = removeFromConjunction(sub, toRemove)) > 0)) {
+      NodeBuilder<> b(kind::AND);
+      b.append(n.begin(), j);
+      if(subremovals > 0) {
+        removals += subremovals;
+        b << sub;
+      } else {
+        ++removals;
+      }
+      for(++j; j != n.end(); ++j) {
+        if(toRemove.find((*j).getId()) != toRemove.end()) {
+          ++removals;
+        } else if((*j).getKind() == kind::AND) {
+          sub = *j;
+          if((subremovals = removeFromConjunction(sub, toRemove)) > 0) {
+            removals += subremovals;
+            b << sub;
+          } else {
+            b << *j;
+          }
+        } else {
+          b << *j;
+        }
+      }
+      if(b.getNumChildren() == 0) {
+        n = d_true;
+        b.clear();
+      } else if(b.getNumChildren() == 1) {
+        n = b[0];
+        b.clear();
+      } else {
+        n = b;
+      }
+      n = Rewriter::rewrite(n);
+      return removals;
+    }
+  }
+
+  Assert(removals == 0);
+  return 0;
+}
+
+void SimplifyAssertionsPass::doMiplibTrick(AssertionPipeline &d_assertions) {
+  Assert(d_realAssertionsEnd == d_assertions.size());
+  Assert(!options::incrementalSolving());
+
+  const theory::booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator->getBackEdges();
+  unordered_set<unsigned long> removeAssertions;
+
+  NodeManager* nm = NodeManager::currentNM();
+  Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1));
+
+  unordered_map<TNode, Node, TNodeHashFunction> intVars;
+  for(vector<Node>::const_iterator i = d_boolVars->begin(); i != d_boolVars->end(); ++i) {
+    if(d_propagator->isAssigned(*i)) {
+      Debug("miplib") << "ineligible: " << *i << " because assigned " << d_propagator->getAssignment(*i) << endl;
+      continue;
+    }
+
+    vector<TNode> assertions;
+    theory::booleans::CircuitPropagator::BackEdgesMap::const_iterator j = backEdges.find(*i);
+    // if not in back edges map, the bool var is unconstrained, showing up in no assertions.
+    // if maps to an empty vector, that means the bool var was asserted itself.
+    if(j != backEdges.end()) {
+      if(!(*j).second.empty()) {
+        traceBackToAssertions((*j).second, assertions);
+      } else {
+        assertions.push_back(*i);
+      }
+    }
+    Debug("miplib") << "for " << *i << endl;
+    bool eligible = true;
+    map<pair<Node, Node>, uint64_t> marks;
+    map<pair<Node, Node>, vector<Rational> > coef;
+    map<pair<Node, Node>, vector<Rational> > checks;
+    map<pair<Node, Node>, vector<TNode> > asserts;
+    for(vector<TNode>::const_iterator j = assertions.begin(); j != assertions.end(); ++j) {
+      Debug("miplib") << "  found: " << *j << endl;
+      if((*j).getKind() != kind::IMPLIES) {
+        eligible = false;
+        Debug("miplib") << "  -- INELIGIBLE -- (not =>)" << endl;
+        break;
+      }
+      Node conj = BooleanSimplification::simplify((*j)[0]);
+      if(conj.getKind() == kind::AND && conj.getNumChildren() > 6) {
+        eligible = false;
+        Debug("miplib") << "  -- INELIGIBLE -- (N-ary /\\ too big)" << endl;
+        break;
+      }
+      if(conj.getKind() != kind::AND && !conj.isVar() && !(conj.getKind() == kind::NOT && conj[0].isVar())) {
+        eligible = false;
+        Debug("miplib") << "  -- INELIGIBLE -- (not /\\ or literal)" << endl;
+        break;
+      }
+      if((*j)[1].getKind() != kind::EQUAL ||
+         !( ( (*j)[1][0].isVar() &&
+              (*j)[1][1].getKind() == kind::CONST_RATIONAL ) ||
+            ( (*j)[1][0].getKind() == kind::CONST_RATIONAL &&
+              (*j)[1][1].isVar() ) )) {
+        eligible = false;
+        Debug("miplib") << "  -- INELIGIBLE -- (=> (and X X) X)" << endl;
+        break;
+      }
+      if(conj.getKind() == kind::AND) {
+        vector<Node> posv;
+        bool found_x = false;
+        map<TNode, bool> neg;
+        for(Node::iterator ii = conj.begin(); ii != conj.end(); ++ii) {
+          if((*ii).isVar()) {
+            posv.push_back(*ii);
+            neg[*ii] = false;
+            found_x = found_x || *i == *ii;
+          } else if((*ii).getKind() == kind::NOT && (*ii)[0].isVar()) {
+            posv.push_back((*ii)[0]);
+            neg[(*ii)[0]] = true;
+            found_x = found_x || *i == (*ii)[0];
+          } else {
+            eligible = false;
+            Debug("miplib") << "  -- INELIGIBLE -- (non-var: " << *ii << ")" << endl;
+            break;
+          }
+          if(d_propagator->isAssigned(posv.back())) {
+            eligible = false;
+            Debug("miplib") << "  -- INELIGIBLE -- (" << posv.back() << " asserted)" << endl;
+            break;
+          }
+        }
+        if(!eligible) {
+          break;
+        }
+        if(!found_x) {
+          eligible = false;
+          Debug("miplib") << "  --INELIGIBLE -- (couldn't find " << *i << " in conjunction)" << endl;
+          break;
+        }
+        sort(posv.begin(), posv.end());
+        const Node pos = NodeManager::currentNM()->mkNode(kind::AND, posv);
+        const TNode var = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][1] : (*j)[1][0];
+        const pair<Node, Node> pos_var(pos, var);
+        const Rational& constant = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][0].getConst<Rational>() : (*j)[1][1].getConst<Rational>();
+        uint64_t mark = 0;
+        unsigned countneg = 0, thepos = 0;
+        for(unsigned ii = 0; ii < pos.getNumChildren(); ++ii) {
+          if(neg[pos[ii]]) {
+            ++countneg;
+          } else {
+            thepos = ii;
+            mark |= (0x1 << ii);
+          }
+        }
+        if((marks[pos_var] & (1lu << mark)) != 0) {
+          eligible = false;
+          Debug("miplib") << "  -- INELIGIBLE -- (remarked)" << endl;
+          break;
+        }
+        Debug("miplib") << "mark is " << mark << " -- " << (1lu << mark) << endl;
+        marks[pos_var] |= (1lu << mark);
+        Debug("miplib") << "marks[" << pos << "," << var << "] now " << marks[pos_var] << endl;
+        if(countneg == pos.getNumChildren()) {
+          if(constant != 0) {
+            eligible = false;
+            Debug("miplib") << "  -- INELIGIBLE -- (nonzero constant)" << endl;
+            break;
+          }
+        } else if(countneg == pos.getNumChildren() - 1) {
+          Assert(coef[pos_var].size() <= 6 && thepos < 6);
+          if(coef[pos_var].size() <= thepos) {
+            coef[pos_var].resize(thepos + 1);
+          }
+          coef[pos_var][thepos] = constant;
+        } else {
+          if(checks[pos_var].size() <= mark) {
+            checks[pos_var].resize(mark + 1);
+          }
+          checks[pos_var][mark] = constant;
+        }
+        asserts[pos_var].push_back(*j);
+      } else {
+        TNode x = conj;
+        if(x != *i && x != (*i).notNode()) {
+          eligible = false;
+          Debug("miplib") << "  -- INELIGIBLE -- (x not present where I expect it)" << endl;
+          break;
+        }
+        const bool xneg = (x.getKind() == kind::NOT);
+        x = xneg ? x[0] : x;
+        Debug("miplib") << "  x:" << x << "  " << xneg << endl;
+        const TNode var = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][1] : (*j)[1][0];
+        const pair<Node, Node> x_var(x, var);
+        const Rational& constant = ((*j)[1][0].getKind() == kind::CONST_RATIONAL) ? (*j)[1][0].getConst<Rational>() : (*j)[1][1].getConst<Rational>();
+        unsigned mark = (xneg ? 0 : 1);
+        if((marks[x_var] & (1u << mark)) != 0) {
+          eligible = false;
+          Debug("miplib") << "  -- INELIGIBLE -- (remarked)" << endl;
+          break;
+        }
+        marks[x_var] |= (1u << mark);
+        if(xneg) {
+          if(constant != 0) {
+            eligible = false;
+            Debug("miplib") << "  -- INELIGIBLE -- (nonzero constant)" << endl;
+            break;
+          }
+        } else {
+          Assert(coef[x_var].size() <= 6);
+          coef[x_var].resize(6);
+          coef[x_var][0] = constant;
+        }
+        asserts[x_var].push_back(*j);
+      }
+    }
+    if(eligible) {
+      for(map<pair<Node, Node>, uint64_t>::const_iterator j = marks.begin(); j != marks.end(); ++j) {
+        const TNode pos = (*j).first.first;
+        const TNode var = (*j).first.second;
+        const pair<Node, Node>& pos_var = (*j).first;
+        const uint64_t mark = (*j).second;
+        const unsigned numVars = pos.getKind() == kind::AND ? pos.getNumChildren() : 1;
+        uint64_t expected = (uint64_t(1) << (1 << numVars)) - 1;
+        expected = (expected == 0) ? -1 : expected; // fix for overflow
+        Debug("miplib") << "[" << pos << "] => " << hex << mark << " expect " << expected << dec << endl;
+        Assert(pos.getKind() == kind::AND || pos.isVar());
+        if(mark != expected) {
+          Debug("miplib") << "  -- INELIGIBLE " << pos << " -- (insufficiently marked, got " << mark << " for " << numVars << " vars, expected " << expected << endl;
+        } else {
+          if(mark != 3) { // exclude single-var case; nothing to check there
+            uint64_t sz = (uint64_t(1) << checks[pos_var].size()) - 1;
+            sz = (sz == 0) ? -1 : sz; // fix for overflow
+            Assert(sz == mark, "expected size %u == mark %u", sz, mark);
+            for(size_t k = 0; k < checks[pos_var].size(); ++k) {
+              if((k & (k - 1)) != 0) {
+                Rational sum = 0;
+                Debug("miplib") << k << " => " << checks[pos_var][k] << endl;
+                for(size_t v = 1, kk = k; kk != 0; ++v, kk >>= 1) {
+                  if((kk & 0x1) == 1) {
+                    Assert(pos.getKind() == kind::AND);
+                    Debug("miplib") << "var " << v << " : " << pos[v - 1] << " coef:" << coef[pos_var][v - 1] << endl;
+                    sum += coef[pos_var][v - 1];
+                  }
+                }
+                Debug("miplib") << "checkSum is " << sum << " input says " << checks[pos_var][k] << endl;
+                if(sum != checks[pos_var][k]) {
+                  eligible = false;
+                  Debug("miplib") << "  -- INELIGIBLE " << pos << " -- (nonlinear combination)" << endl;
+                  break;
+                }
+              } else {
+                Assert(checks[pos_var][k] == 0, "checks[(%s,%s)][%u] should be 0, but it's %s", pos.toString().c_str(), var.toString().c_str(), k, checks[pos_var][k].toString().c_str()); // we never set for single-positive-var
+              }
+            }
+          }
+          if(!eligible) {
+            eligible = true; // next is still eligible
+            continue;
+          }
+
+          Debug("miplib") << "  -- ELIGIBLE " << *i << " , " << pos << " --" << endl;
+          vector<Node> newVars;
+          expr::NodeSelfIterator ii, iiend;
+          if(pos.getKind() == kind::AND) {
+            ii = pos.begin();
+            iiend = pos.end();
+          } else {
+            ii = expr::NodeSelfIterator::self(pos);
+            iiend = expr::NodeSelfIterator::selfEnd(pos);
+          }
+          for(; ii != iiend; ++ii) {
+            Node& varRef = intVars[*ii];
+            if(varRef.isNull()) {
+              stringstream ss;
+              ss << "mipvar_" << *ii;
+              Node newVar = nm->mkSkolem(ss.str(), nm->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME);
+              Node geq = theory::Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero));
+              Node leq = theory::Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one));
+              addFormula(theory::Rewriter::rewrite(geq.andNode(leq)), false, d_assertions, false);
+              SubstitutionMap nullMap(d_fakeContext);
+              theory::Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions
+              status = d_smt->d_theoryEngine->solve(geq, nullMap); Assert(status == theory::Theory::PP_ASSERT_STATUS_UNSOLVED,
+                     "unexpected solution from arith's ppAssert()");
+              Assert(nullMap.empty(),
+                     "unexpected substitution from arith's ppAssert()");
+              status = d_smt->d_theoryEngine->solve(leq, nullMap);
+              Assert(status == theory::Theory::PP_ASSERT_STATUS_UNSOLVED,
+                     "unexpected solution from arith's ppAssert()");
+              Assert(nullMap.empty(),
+                     "unexpected substitution from arith's ppAssert()");
+              d_smt->d_theoryEngine->getModel()->addSubstitution(*ii, newVar.eqNode(one));
+              newVars.push_back(newVar);
+              varRef = newVar;
+            } else {
+              newVars.push_back(varRef);
+            }
+            if(!d_smt->d_logic.areIntegersUsed()) {
+              d_smt->d_logic = d_smt->d_logic.getUnlockedCopy();
+              d_smt->d_logic.enableIntegers();
+              d_smt->d_logic.lock();
+            }
+          }
+          Node sum;
+          if(pos.getKind() == kind::AND) {
+            NodeBuilder<> sumb(kind::PLUS);
+            for(size_t ii = 0; ii < pos.getNumChildren(); ++ii) {
+              sumb << nm->mkNode(kind::MULT, nm->mkConst(coef[pos_var][ii]), newVars[ii]);
+            }
+            sum = sumb;
+          } else {
+            sum = nm->mkNode(kind::MULT, nm->mkConst(coef[pos_var][0]), newVars[0]);
+          }
+          Debug("miplib") << "vars[] " << var << endl
+                          << "    eq " << theory::Rewriter::rewrite(sum) << endl;
+          Node newAssertion = var.eqNode(theory::Rewriter::rewrite(sum));
+          if(d_topLevelSubstitutions->hasSubstitution(newAssertion[0])) {
+            //Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl;
+            //Warning() << "REPLACE         " << newAssertion[1] << endl;
+            //Warning() << "ORIG            " << d_topLevelSubstitutions.getSubstitution(newAssertion[0]) << endl;
+            Assert(d_topLevelSubstitutions->getSubstitution(newAssertion[0]) == newAssertion[1]);
+          } else if(pos.getNumChildren() <= options::arithMLTrickSubstitutions()) {
+            d_topLevelSubstitutions->addSubstitution(newAssertion[0], newAssertion[1]);
+            Debug("miplib") << "addSubs: " << newAssertion[0] << " to " << newAssertion[1] << endl;
+          } else {
+            Debug("miplib") << "skipSubs: " << newAssertion[0] << " to " << newAssertion[1] << " (threshold is " << options::arithMLTrickSubstitutions() << ")" << endl;
+          }
+          newAssertion = theory::Rewriter::rewrite(newAssertion);
+          Debug("miplib") << "  " << newAssertion << endl;
+          addFormula(newAssertion, false, d_assertions, false);
+          Debug("miplib") << "  assertions to remove: " << endl;
+          for(vector<TNode>::const_iterator k = asserts[pos_var].begin(), k_end = asserts[pos_var].end(); k != k_end; ++k) {
+            Debug("miplib") << "    " << *k << endl;
+            removeAssertions.insert((*k).getId());
+          }
+        }
+      }
+    }
+  }
+  if(!removeAssertions.empty()) {
+    Debug("miplib") << "SmtEnginePrivate::simplify(): scrubbing miplib encoding..." << endl;
+    for(size_t i = 0; i < d_realAssertionsEnd; ++i) {
+      if(removeAssertions.find(d_assertions[i].getId()) != removeAssertions.end()) {
+        Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertions[i] << endl;
+        d_assertions[i] = d_true;
+        ++d_smt->d_stats->d_numMiplibAssertionsRemoved;
+      } else if(d_assertions[i].getKind() == kind::AND) {
+        size_t removals = removeFromConjunction(d_assertions[i], removeAssertions);
+        if(removals > 0) {
+          Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertions[i] << endl;
+          Debug("miplib") << "SmtEnginePrivate::simplify(): -      by " << removals << " conjuncts" << endl;
+          d_smt->d_stats->d_numMiplibAssertionsRemoved += removals;
+        }
+      }
+      Debug("miplib") << "had: " << d_assertions[i] << endl;
+      d_assertions[i] = theory::Rewriter::rewrite(d_topLevelSubstitutions->apply(d_assertions[i]));
+      Debug("miplib") << "now: " << d_assertions[i] << endl;
+    }
+  } else {
+    Debug("miplib") << "SmtEnginePrivate::simplify(): miplib pass found nothing." << endl;
+  }
+  d_realAssertionsEnd = d_assertions.size();
+}
+
+void SimplifyAssertionsPass::compressBeforeRealAssertions(size_t before, AssertionPipeline& d_assertions){
+  size_t curr = d_assertions.size();
+  if(before >= curr ||
+     d_realAssertionsEnd <= 0 ||
+     d_realAssertionsEnd >= curr){
+    return;
+  }
+}
+
+bool SimplifyAssertionsPass::simpITE(AssertionPipeline& d_assertions) {
+  TimerStat::CodeTimer simpITETimer(d_smt->d_stats->d_simpITETime);
+
+  spendResource(options::preprocessStep());
+
+  Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
+
+  unsigned numAssertionOnEntry = d_assertions.size();
+  for (unsigned i = 0; i < d_assertions.size(); ++i) {
+    spendResource(options::preprocessStep());
+    Node result = d_smt->d_theoryEngine->ppSimpITE(d_assertions[i]);
+    d_assertions.replace(i, result);
+    if(result.isConst() && !result.getConst<bool>()){
+      return false;
+    }
+  }
+  bool result = d_smt->d_theoryEngine->donePPSimpITE(d_assertions.ref());
+  if(numAssertionOnEntry < d_assertions.size()){
+    compressBeforeRealAssertions(numAssertionOnEntry, d_assertions);
+  }
+  return result;
+}
+
+
 // returns false if simplification led to "false"
 PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* assertionsToPreprocess)
   throw(TypeCheckingException, LogicException, UnsafeInterruptException) {
@@ -1613,7 +2013,7 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti
 
         TimerStat::CodeTimer miplibTimer(d_smt->d_stats->d_miplibPassTime);
 
-        doMiplibTrick();
+        doMiplibTrick(*assertionsToPreprocess);
       } else {
         Trace("simplify") << "SmtEnginePrivate::simplify(): "
                           << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl;
@@ -1650,7 +2050,7 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti
     if(options::doITESimp() &&
        (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) {
       Chat() << "...doing ITE simplification..." << endl;
-      bool noConflict = simpITE();
+      bool noConflict = simpITE(*assertionsToPreprocess);
       if(!noConflict){
         Chat() << "...ITE simplification found unsat..." << endl;
         return false;
@@ -1699,7 +2099,6 @@ PreprocessingPassResult SimplifyAssertionsPass::apply(AssertionPipeline* asserti
   }
   return PreprocessingPassResult(true); 
 }
-**/
-
+*/
 }  // namespace preproc
 }  // namespace CVC4
diff --git a/src/preproc/preprocessing_passes_core.h b/src/preproc/preprocessing_passes_core.h
index cff581894..429d44748 100644
--- a/src/preproc/preprocessing_passes_core.h
+++ b/src/preproc/preprocessing_passes_core.h
@@ -1,4 +1,4 @@
-#include "cvc4_public.h"
+#include "cvc4_private.h"
 
 #ifndef __CVC4__PREPROC__PREPROCESSING_PASSES_CORE_H
 #define __CVC4__PREPROC__PREPROCESSING_PASSES_CORE_H
@@ -12,6 +12,9 @@
 #include "decision/decision_engine.h"
 
 namespace CVC4 {
+
+using namespace theory;
+
 namespace preproc {
 
 typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
@@ -234,41 +237,52 @@ class CNFPass : public PreprocessingPass{
      TimerStat d_cnfConversionTime;
 };
 
-/* 
 class RepeatSimpPass : public PreprocessingPass {
   public:
      virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess);
      RepeatSimpPass(ResourceManager* resourceManager, theory::SubstitutionMap* topLevelSubstitutions, unsigned simplifyAssertionsDepth, bool* noConflict, IteSkolemMap iteSkolemMap, unsigned realAssertionsEnd);
   private: 
      theory::SubstitutionMap* d_topLevelSubstitutions;
-     void collectSkolems(TNode n, set<TNode>& skolemSet, hash_map<Node, bool, NodeHashFunction>& cache);
-     bool checkForBadSkolems(TNode n, TNode skolem, hash_map<Node, bool, NodeHashFunction>& cache);
-     bool simplifyAssertions();
+     void collectSkolems(TNode n, set<TNode>& skolemSet, unordered_map<Node, bool, NodeHashFunction>& cache);
+     bool checkForBadSkolems(TNode n, TNode skolem, unordered_map<Node, bool, NodeHashFunction>& cache);
      unsigned d_simplifyAssertionsDepth;
      bool* noConflict;
      IteSkolemMap d_iteSkolemMap;
      unsigned d_realAssertionsEnd;
 };     
 
-class SimplifyAssertionsPass : public PreprocessingPass {
+/*class SimplifyAssertionsPass : public PreprocessingPass {
   public:
      virtual PreprocessingPassResult apply(AssertionPipeline* assertionsToPreprocess) throw(TypeCheckingException, LogicException,
                                   UnsafeInterruptException);
-     SimplifyAssertionsPass(ResourceManager* resourceManager, unsigned simplifyAssertionsDepth, SmtEngine* smt, bool propagatorNeedsFinish, theory::booleans::CircuitPropagator propagator, context::CDO<unsigned> substitutionsIndex, std::vector<Node> nonClausalLearnedLiterals, Node dtrue, TimerStat nonclausalSimplificationTime);
+     SimplifyAssertionsPass(ResourceManager* resourceManager, unsigned simplifyAssertionsDepth, SmtEngine* smt, bool propagatorNeedsFinish, theory::booleans::CircuitPropagator* propagator, context::CDO<unsigned>* substitutionsIndex, std::vector<Node>* nonClausalLearnedLiterals, Node dtrue, TimerStat nonclausalSimplificationTime, unsigned realAssertionsEnd, theory::SubstitutionMap* topLevelSubstitutions, bool doConstantProp, std::vector<Node>* boolVars, context::Context* fakeContext );
   private:
    unsigned d_simplifyAssertionsDepth;
    SmtEngine* d_smt;
    bool d_propagatorNeedsFinish;
-   theory::booleans::CircuitPropagator d_propagator;
-   context::CDO<unsigned> d_substitutionsIndex;
-   std::vector<Node> d_nonClausalLearnedLiterals;
+   theory::booleans::CircuitPropagator* d_propagator;
+   context::CDO<unsigned>* d_substitutionsIndex;
+   std::vector<Node>* d_nonClausalLearnedLiterals;
    Node d_true;
    TimerStat d_nonclausalSimplificationTime;
+   unsigned d_realAssertionsEnd;
+   theory::SubstitutionMap* d_topLevelSubstitutions;
+   bool d_doConstantProp;
+   std::vector<Node>* d_boolVars;
+   context::Context* d_fakeContext;
+   
+   void traceBackToAssertions(const std::vector<Node>& nodes,
+                             std::vector<TNode>& assertions);
+   void doMiplibTrick(AssertionPipeline &d_assertions);
    bool nonClausalSimplify(AssertionPipeline &d_assertions);
-   void addFormula(TNode n, bool inUnsatCore, bool inInput = true, AssertionPipeline d_assertions)
+   void addFormula(TNode n, bool inUnsatCore, AssertionPipeline& d_assertions, bool inInput = true)
     throw(TypeCheckingException, LogicException);
-};
-*/
+   void compressBeforeRealAssertions(size_t before, AssertionPipeline &d_assertions);
+   bool simpITE(AssertionPipeline &d_assertions);
+   size_t removeFromConjunction(Node& n,
+                               const std::unordered_set<unsigned long>& toRemove);
+
+};*/
  
 }  // namespace preproc
 }  // namespace CVC4
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index cd2da586e..159201e71 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3560,7 +3560,8 @@ void SmtEnginePrivate::processAssertions() {
     preproc::RewritePass pass1(d_resourceManager);
     pass1.apply(&d_assertions);
  }
-
+ 
+ Debug("smt") << "d_assertions    :" << d_assertions.size() << endl;
  bool noConflict = true;
 
   // Unconstrained simplification
@@ -3679,12 +3680,23 @@ void SmtEnginePrivate::processAssertions() {
 
   dumpAssertions("pre-repeat-simplify", d_assertions);
   if(options::repeatSimp()) {
-/*     preproc::SimplifyAssertionsPass pass(d_resourceManager, d_simplifyAssertionsDepth, &d_smt, d_propagatorNeedsFinish, d_propagator, d_substitutionsIndex, d_nonClausalLearnedLiterals, d_true, d_smt.d_stats->d_nonclausalSimplificationTime);
-     noConflict &= pass.apply(&d_assertions).d_noConflict;
-
-     preproc::RepeatSimpPass pass1(d_resourceManager, &d_topLevelSubstitutions, d_simplifyAssertionsDepth, &noConflict, d_iteSkolemMap, d_realAssertionsEnd); 
-     pass1.apply(&d_assertions);*/
-    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl;
+    Chat() << "re-simplifying assertions..." << std::endl;
+    ScopeCounter depth(d_simplifyAssertionsDepth);
+    noConflict &= simplifyAssertions();
+   
+    if (noConflict) {
+      preproc::RepeatSimpPass pass1(d_resourceManager, &d_topLevelSubstitutions, d_simplifyAssertionsDepth, &noConflict, d_iteSkolemMap, d_realAssertionsEnd); 
+      pass1.apply(&d_assertions);
+      // For some reason this is needed for some benchmarks, such as
+      // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
+      // Figure it out later
+      preproc::RemoveITEPass pass2(d_resourceManager, &d_smt, &d_iteSkolemMap, &d_iteRemover);
+      pass2.apply(&d_assertions); 
+      //      Assert(iteRewriteAssertionsEnd == d_assertions.size());
+     }
+   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << std::endl;
+ 
+/*    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-repeat-simplify" << endl;
     Chat() << "re-simplifying assertions..." << endl;
     ScopeCounter depth(d_simplifyAssertionsDepth);
     noConflict &= simplifyAssertions();
@@ -3750,7 +3762,7 @@ void SmtEnginePrivate::processAssertions() {
       removeITEs();
       //      Assert(iteRewriteAssertionsEnd == d_assertions.size());
     }
-    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;
+    Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl;*/
   }
   dumpAssertions("post-repeat-simplify", d_assertions);