Changes to the combination mechanism, lots of details. Not done yet, there are still the AUFBV wrong results, but it seems better.

http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5

38 files changed, 2368 insertions, 1007 deletions

diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index fb76c1857..74641513b 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -130,6 +130,7 @@ ${theory_enum}
 };
 
 const TheoryId THEORY_FIRST = static_cast<TheoryId>(0);
+const TheoryId THEORY_SAT_SOLVER = THEORY_LAST;
 
 inline TheoryId& operator ++ (TheoryId& id) {
   return id = static_cast<TheoryId>(((int)id) + 1);
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 65e409012..4ba4aeba5 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -319,33 +319,12 @@ bool TheoryArrays::propagate(TNode literal)
     return false;
   }
 
-  // See if the literal has been asserted already
-  Node normalized = Rewriter::rewrite(literal);
-  bool satValue = false;
-  bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue);
-
-  // If asserted, we're done or in conflict
-  if (isAsserted) {
-    if (!satValue) {
-      Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
-      std::vector<TNode> assumptions;
-      Node negatedLiteral;
-      negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
-      assumptions.push_back(negatedLiteral);
-      explain(literal, assumptions);
-      d_conflictNode = mkAnd(assumptions);
-      d_conflict = true;
-      return false;
-    }
-    // Propagate even if already known in SAT - could be a new equation between shared terms
-    // (terms that weren't shared when the literal was asserted!)
+  // Propagate away
+  bool ok = d_out->propagate(literal);
+  if (!ok) {
+    d_conflict = true;
   }
-
-  // Nothing, just enqueue it for propagation and mark it as asserted already
-  Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
-  d_literalsToPropagate.push_back(literal);
-
-  return true;
+  return ok;
 }/* TheoryArrays::propagate(TNode) */
 
 
@@ -479,29 +458,7 @@ void TheoryArrays::preRegisterTerm(TNode node)
 
 void TheoryArrays::propagate(Effort e)
 {
-  Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate()" << std::endl;
-  if (!d_conflict) {
-    for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
-      TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
-      Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): propagating " << literal << std::endl;
-      bool satValue;
-      Node normalized = Rewriter::rewrite(literal);
-      if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
-        d_out->propagate(literal);
-      } else {
-        Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl;
-        Node negatedLiteral;
-        std::vector<TNode> assumptions;
-        negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
-        assumptions.push_back(negatedLiteral);
-        explain(literal, assumptions);
-        d_conflictNode = mkAnd(assumptions);
-        d_conflict = true;
-        break;
-      }
-    }
-  }
-
+  // direct propagation now
 }
 
 
@@ -634,6 +591,7 @@ void TheoryArrays::computeCareGraph()
             break;
           case EQUALITY_FALSE_IN_MODEL:
             Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): false in model" << std::endl;
+            continue;
             break;
           default:
             break;
@@ -700,11 +658,21 @@ void TheoryArrays::check(Effort e) {
 
     Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): processing " << fact << std::endl;
 
-    // If the assertion doesn't have a literal, it's a shared equality
-    Assert(assertion.isPreregistered ||
-           ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) ||
-            (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL &&
-             d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1]))));
+    bool polarity = fact.getKind() != kind::NOT;
+    TNode atom = polarity ? fact : fact[0];
+
+    if (!assertion.isPreregistered) {
+      if (atom.getKind() == kind::EQUAL) {
+        if (!d_equalityEngine.hasTerm(atom[0])) {
+          Assert(atom[0].isConst());
+          d_equalityEngine.addTerm(atom[0]);
+        }
+        if (!d_equalityEngine.hasTerm(atom[1])) {
+          Assert(atom[1].isConst());
+          d_equalityEngine.addTerm(atom[1]);
+        }
+      }
+    }
 
     // Do the work
     switch (fact.getKind()) {
@@ -758,19 +726,10 @@ void TheoryArrays::check(Effort e) {
   }
 
   // If in conflict, output the conflict
-  if (d_conflict) {
-    Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::check(): conflict " << d_conflictNode << std::endl;
-    d_out->conflict(d_conflictNode);
-  }
-  else {
-    // Otherwise we propagate
-    propagate(e);
-
-    if(!d_eagerLemmas && fullEffort(e) && !d_conflict) {
-      // generate the lemmas on the worklist
-      Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
-      dischargeLemmas();
-    }
+  if(!d_eagerLemmas && fullEffort(e) && !d_conflict) {
+    // generate the lemmas on the worklist
+    Trace("arrays-lem")<<"Arrays::discharging lemmas: "<<d_RowQueue.size()<<"\n";
+    dischargeLemmas();
   }
 
   Trace("arrays") << spaces(getSatContext()->getLevel()) << "Arrays::check(): done" << endl;
@@ -1138,6 +1097,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   TNode b = lem.second;
   TNode i = lem.third;
   TNode j = lem.fourth;
+
   Assert(a.getType().isArray() && b.getType().isArray());
   if (d_equalityEngine.areEqual(a,b) ||
       d_equalityEngine.areEqual(i,j)) {
@@ -1345,6 +1305,16 @@ void TheoryArrays::dischargeLemmas()
   }
 }
 
+void TheoryArrays::conflict(TNode a, TNode b) {
+  if (Theory::theoryOf(a) == theory::THEORY_BOOL) {
+    d_conflictNode = explain(a.iffNode(b));
+  } else {
+    d_conflictNode = explain(a.eqNode(b));
+  }
+  d_out->conflict(d_conflictNode);
+  d_conflict = true;
+}
+
 
 }/* CVC4::theory::arrays namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index d17caba45..6592e86cf 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -261,11 +261,8 @@ class TheoryArrays : public Theory {
 
     bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
       Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
-      if (Theory::theoryOf(t1) == THEORY_BOOL) {
-        return d_arrays.propagate(t1.iffNode(t2));
-      } else {
-        return d_arrays.propagate(t1.eqNode(t2));
-      }
+      d_arrays.conflict(t1, t2);
+      return false;
     }
   };
 
@@ -275,9 +272,12 @@ class TheoryArrays : public Theory {
   /** Equaltity engine */
   eq::EqualityEngine d_equalityEngine;
 
-  // Are we in conflict?
+  /** Are we in conflict? */
   context::CDO<bool> d_conflict;
 
+  /** Conflict when merging constants */
+  void conflict(TNode a, TNode b);
+
   /** The conflict node */
   Node d_conflictNode;
 
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index 807d90137..98678a9b4 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -134,7 +134,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool v
 }
 
 bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value) {
-  BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+  BVDebug("bitvector::equality") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" ) << ")" << std::endl;
   if (value) {
     return d_bv->storePropagation(predicate, TheoryBV::SUB_EQUALITY);
   } else {
@@ -143,7 +143,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool
 }
 
 bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
-  Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl;
+  Debug("bitvector::equality") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
   if (value) {
     return d_bv->storePropagation(t1.eqNode(t2), TheoryBV::SUB_EQUALITY);
   } else {
@@ -152,7 +152,7 @@ bool EqualitySolver::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNod
 }
 
 bool EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-  Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
+  Debug("bitvector::equality") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
   if (Theory::theoryOf(t1) == THEORY_BOOL) {
     return d_bv->storePropagation(t1.iffNode(t2), TheoryBV::SUB_EQUALITY);
   }
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 251650bf2..30493737a 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -141,58 +141,9 @@ void TheoryBV::propagate(Effort e) {
   }
 
   // go through stored propagations
-  for (; d_literalsToPropagateIndex < d_literalsToPropagate.size();
-       d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1)
-  {
+  for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
     TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
-    Node normalized = Rewriter::rewrite(literal);
-
-    TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;  
-    bool isSharedLiteral = (atom.getKind() == kind::EQUAL &&
-                            (d_sharedTermsSet.find(atom[0]) != d_sharedTermsSet.end() &&
-                             d_sharedTermsSet.find(atom[1]) != d_sharedTermsSet.end()));
-
-    // Check if this is a SAT literal
-    if (d_valuation.isSatLiteral(normalized)) {
-      bool satValue = false;
-      if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
-        // check if we already propagated the negation
-        Node negLiteral = literal.getKind() == kind::NOT ? (Node)literal[0] : mkNot(literal);
-        if (d_alreadyPropagatedSet.find(negLiteral) != d_alreadyPropagatedSet.end()) {
-          Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict " << literal << " and its negation both propagated \n"; 
-          // we are in conflict
-          std::vector<TNode> assumptions;
-          explain(literal, assumptions);
-          explain(negLiteral, assumptions);
-          setConflict(mkAnd(assumptions)); 
-          return;
-        }
-        // If it's not a shared literal and hasn't already been set to true, we propagate the normalized version
-        // shared literals are handled below
-        if (!isSharedLiteral && !satValue) {
-          BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << normalized << std::endl;
-          d_out->propagate(normalized);
-          d_alreadyPropagatedSet.insert(normalized); 
-          return;
-        }
-      } else {
-        // 
-        Debug("bitvector") << indent() << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
-        Node negatedLiteral;
-        std::vector<TNode> assumptions;
-        negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
-        assumptions.push_back(negatedLiteral);
-        explain(literal, assumptions);
-        setConflict(mkAnd(assumptions));
-        return;
-      }
-    }
-    // Either it was not a SAT literal or it was but it is also shared - in that case we have to propagate the original literal (not the normalized one)
-    if (isSharedLiteral) {
-      BVDebug("bitvector") << indent() << "TheoryBV::propagate(): " << literal << std::endl;
-      d_out->propagate(literal);
-      d_alreadyPropagatedSet.insert(literal); 
-    }
+    d_out->propagate(literal);
   }
 }
 
@@ -269,16 +220,18 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
   // Ask the appropriate subtheory for the explanation 
   if (propagatedBy(literal, SUB_EQUALITY)) {
+    BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << "): EQUALITY" << std::endl;
     d_equalitySolver.explain(literal, assumptions); 
   } else {
     Assert(propagatedBy(literal, SUB_BITBLAST));
+    BVDebug("bitvector::explain") << "TheoryBV::explain(" << literal << ") : BITBLASTER" << std::endl;    
     d_bitblastSolver.explain(literal, assumptions); 
   }
 }
 
 
 Node TheoryBV::explain(TNode node) {
-  BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl;
+  BVDebug("bitvector::explain") << "TheoryBV::explain(" << node << ")" << std::endl;
   std::vector<TNode> assumptions;
 
   // Ask for the explanation
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 3736da639..c456ef73f 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -72,11 +72,26 @@ inline Node mkVar(unsigned size) {
 }
 
 inline Node mkAnd(std::vector<TNode>& children) {
-  if (children.size() > 1) {
-    return NodeManager::currentNM()->mkNode(kind::AND, children);
-  } else {
-    return children[0];
+  std::set<TNode> distinctChildren;
+  distinctChildren.insert(children.begin(), children.end());
+  
+  if (children.size() == 0) {
+    return mkTrue();
+  }
+  
+  if (children.size() == 1) {
+    return *children.begin();
   }
+  
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = distinctChildren.begin();
+  std::set<TNode>::const_iterator it_end = distinctChildren.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
+  }
+
+  return conjunction;
 }
 
 inline Node mkSortedNode(Kind kind, std::vector<Node>& children) {
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 71bbefb6a..5c2cedf5b 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -103,8 +103,9 @@ public:
    * Propagate a theory literal.
    *
    * @param n - a theory consequence at the current decision level
+   * @return false if an immediate conflict was encountered
    */
-  virtual void propagate(TNode n) throw(AssertionException) = 0;
+  virtual bool propagate(TNode n) throw(AssertionException) = 0;
 
   /**
    * Request that the core make a decision on this atom.  The decision
diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index 0c893482a..b081e27ef 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -15,25 +15,26 @@
  ** \todo document this file
  **/
 
+
 #include "theory/shared_terms_database.h"
+#include "theory/theory_engine.h"
 
 using namespace std;
 using namespace CVC4;
 using namespace theory;
 
-SharedTermsDatabase::SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context)
-  : ContextNotifyObj(context),
-    d_context(context), 
-    d_statSharedTerms("theory::shared_terms", 0),
-    d_addedSharedTermsSize(context, 0),
-    d_termsToTheories(context),
-    d_alreadyNotifiedMap(context),
-    d_sharedNotify(notify),
-    d_termToNotifyList(context),
-    d_allocatedNLSize(0),
-    d_allocatedNLNext(context, 0),
-    d_EENotify(*this),
-    d_equalityEngine(d_EENotify, context, "SharedTermsDatabase")
+SharedTermsDatabase::SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context)
+: ContextNotifyObj(context)
+, d_context(context)
+, d_statSharedTerms("theory::shared_terms", 0)
+, d_addedSharedTermsSize(context, 0)
+, d_termsToTheories(context)
+, d_alreadyNotifiedMap(context)
+, d_registeredEqualities(context)
+, d_EENotify(*this)
+, d_equalityEngine(d_EENotify, context, "SharedTermsDatabase")
+, d_theoryEngine(theoryEngine)
+, d_inConflict(context, false)
 {
   StatisticsRegistry::registerStat(&d_statSharedTerms);
 }
@@ -41,11 +42,15 @@ SharedTermsDatabase::SharedTermsDatabase(SharedTermsNotifyClass& notify, context
 SharedTermsDatabase::~SharedTermsDatabase() throw(AssertionException)
 {
   StatisticsRegistry::unregisterStat(&d_statSharedTerms);
-  for (unsigned i = 0; i < d_allocatedNLSize; ++i) {
-    d_allocatedNL[i]->deleteSelf();
-  }
 }
 
+void SharedTermsDatabase::addEqualityToPropagate(TNode equality) {
+  d_registeredEqualities.insert(equality);
+  d_equalityEngine.addTriggerEquality(equality);
+  checkForConflict();
+}
+
+
 void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theories) {
   Debug("register") << "SharedTermsDatabase::addSharedTerm(" << atom << ", " << term << ", " << Theory::setToString(theories) << ")" << std::endl; 
 
@@ -57,9 +62,6 @@ void SharedTermsDatabase::addSharedTerm(TNode atom, TNode term, Theory::Set theo
     d_addedSharedTerms.push_back(atom);
     d_addedSharedTermsSize = d_addedSharedTermsSize + 1;
     d_termsToTheories[search_pair] = theories;
-    if (!d_equalityEngine.hasTerm(term)) {
-      d_equalityEngine.addTriggerTerm(term, THEORY_UF);
-    }
   } else {
     Assert(theories != (*find).second);
     d_termsToTheories[search_pair] = Theory::setUnion(theories, (*find).second); 
@@ -120,104 +122,26 @@ Theory::Set SharedTermsDatabase::getNotifiedTheories(TNode term) const {
   }
 }
 
-
-SharedTermsDatabase::NotifyList* SharedTermsDatabase::getNewNotifyList()
+bool SharedTermsDatabase::propagateSharedEquality(TheoryId theory, TNode a, TNode b, bool value)
 {
-  NotifyList* retval;
-  if (d_allocatedNLSize == d_allocatedNLNext) {
-    retval = new (true) NotifyList(d_context);
-    d_allocatedNL.push_back(retval);
-    d_allocatedNLNext = ++d_allocatedNLSize;
-  }
-  else {
-    retval = d_allocatedNL[d_allocatedNLNext];
-    d_allocatedNLNext = d_allocatedNLNext + 1;
-  }
-  Assert(retval->empty());
-  return retval;
-}
+  Debug("shared-terms-database") << "SharedTermsDatabase::newEquality(" << theory << a << "," << b << ", " << (value ? "true" : "false") << ")" << endl;
 
-
-void SharedTermsDatabase::mergeSharedTerms(TNode a, TNode b)
-{
-  // Note: a is the new representative
-  Debug("shared-terms-database") << "SharedTermsDatabase::mergeSharedTerms(" << a << "," << b << ")" << endl;
-
-  NotifyList* pnlLeft = NULL;
-  NotifyList* pnlRight = NULL;
-
-  TermToNotifyList::iterator it = d_termToNotifyList.find(a);
-  if (it == d_termToNotifyList.end()) {
-    pnlLeft = getNewNotifyList();
-    d_termToNotifyList[a] = pnlLeft;
-  }
-  else {
-    pnlLeft = (*it).second;
-  }
-  it = d_termToNotifyList.find(b);
-  if (it != d_termToNotifyList.end()) {
-    pnlRight = (*it).second;
+  if (d_inConflict) {
+    return false;
   }
 
-  // Get theories interested in EC for lhs
-  Theory::Set lhsSet = getNotifiedTheories(a);
-  Theory::Set rhsSet = getNotifiedTheories(b);
-  NotifyList::iterator nit;
-  TNode left, right;
-
-  for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) {
-
-    if (Theory::setContains(currentTheory, rhsSet)) {
-      right = b;
-    }
-    else if (pnlRight != NULL &&
-             ((nit = pnlRight->find(currentTheory)) != pnlRight->end())) {
-      right = (*nit).second;
-    }
-    else {
-      // no match for right: continue
-      continue;
-    }
-
-    if (Theory::setContains(currentTheory, lhsSet)) {
-      left = a;
-    }
-    else if ((nit = pnlLeft->find(currentTheory)) != pnlLeft->end()) {
-      left = (*nit).second;
-    }
-    else {
-      // no match for left: insert right into left
-      (*pnlLeft)[currentTheory] = right;
-      continue;
-    }
-
-    // New shared equality: notify the client
-
-    // TODO: add propagation of disequalities?
-
-    assertEq(left.eqNode(right), currentTheory);
+  // Propagate away 
+  Node equality = a.eqNode(b);
+  if (value) {
+    d_theoryEngine->assertToTheory(equality, theory, THEORY_BUILTIN);
+  } else {
+    d_theoryEngine->assertToTheory(equality.notNode(), theory, THEORY_BUILTIN);
   }
 
-}
-  
-
-void SharedTermsDatabase::assertEq(TNode equality, TheoryId theory)
-{
-  Debug("shared-terms-database") << "SharedTermsDatabase::assertEq(" << equality << ") to theory " << theory << endl;
-  Node normalized = Rewriter::rewriteEquality(theory, equality);
-  if (normalized.getKind() != kind::CONST_BOOLEAN || !normalized.getConst<bool>()) {
-    // Notify client
-    d_sharedNotify.notify(normalized, equality, theory);
-  }
+  // As you were
+  return true;
 }
 
-
-// term was just part of an assertion that makes it shared for theories
-// Let's mark that the set theories has now been notified
-// In addition, we make sure the equivalence class containing term knows a
-// representative for each theory in theories.
-// Finally, if the EC already knows a rep for a theory that was just notified, we
-// have to tell the theory that these two terms are equal.
 void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) {
 
   // Find out if there are any new theories that were notified about this term
@@ -232,87 +156,46 @@ void SharedTermsDatabase::markNotified(TNode term, Theory::Set theories) {
   if (newlyNotified == 0) {
     return;
   }
-
+  
   Debug("shared-terms-database") << "SharedTermsDatabase::markNotified(" << term << ")" << endl;
 
   // First update the set of notified theories for this term
   d_alreadyNotifiedMap[term] = Theory::setUnion(newlyNotified, alreadyNotified);
 
-  // Now get the representative of the equivalence class and find out which theories it represents
-  TNode rep = d_equalityEngine.getRepresentative(term);
-  if (rep != term) {
-    alreadyNotified = 0;
-    theoriesFind = d_alreadyNotifiedMap.find(rep);
-    if (theoriesFind != d_alreadyNotifiedMap.end()) {
-      alreadyNotified = (*theoriesFind).second;
-    }
-  }
-
-  // For each theory that is newly notified
-  for (TheoryId theory = THEORY_FIRST; theory != THEORY_LAST; ++ theory) {
-    if (Theory::setContains(theory, newlyNotified)) {
-
-      Debug("shared-terms-database") << "SharedTermsDatabase::markNotified: processing theory " << theory << endl;
-
-      if (Theory::setContains(theory, alreadyNotified)) {
-        // rep represents this theory already, need to assert that term = rep
-        Assert(rep != term);
-        assertEq(rep.eqNode(term), theory);
-      }
-      else {
-        // Get the list of terms representing theories for this EC
-        TermToNotifyList::iterator it = d_termToNotifyList.find(rep);
-        if (it == d_termToNotifyList.end()) {
-          // No need to do anything - no list associated with this EC
-          Assert(term == rep);
-        }
-        else {
-          NotifyList* pnl = (*it).second;
-          Assert(pnl != NULL);
-
-          // Check if this theory is already represented
-          NotifyList::iterator nit = pnl->find(theory);
-          if (nit != pnl->end()) {
-            // Already have a representative for this theory, assert term equal to it
-            assertEq((*nit).second.eqNode(term), theory);
-          }
-          else {
-            // if term == rep, no need to do anything, as term will represent the theory via alreadyNotifiedMap
-            if (term != rep) {
-              // No term in this EC represents this theory, so add term as a new representative
-              Debug("shared-terms-database") << "SharedTermsDatabase::markNotified: adding " << term << " to representative " << rep << " for theory " << theory << endl;
-              (*pnl)[theory] = term;
-            }
-          }
-        }
-      }
-    }
+  // Mark the shared terms in the equality engine
+  theory::TheoryId currentTheory; 
+  while ((currentTheory = Theory::setPop(newlyNotified)) != THEORY_LAST) {
+    d_equalityEngine.addTriggerTerm(term, currentTheory);    
   }
+  
+  // Check for any conflits
+  checkForConflict();  
 }
 
-
-bool SharedTermsDatabase::areEqual(TNode a, TNode b) {
+bool SharedTermsDatabase::areEqual(TNode a, TNode b) const {
   return d_equalityEngine.areEqual(a,b);
 }
 
-
-bool SharedTermsDatabase::areDisequal(TNode a, TNode b) {
+bool SharedTermsDatabase::areDisequal(TNode a, TNode b) const {
   return d_equalityEngine.areDisequal(a,b,false);
 }
 
-void SharedTermsDatabase::processSharedLiteral(TNode literal, TNode reason)
+void SharedTermsDatabase::assertEquality(TNode equality, bool polarity, TNode reason)
 {
-  bool negated = literal.getKind() == kind::NOT;
-  TNode atom = negated ? literal[0] : literal;
-  if (negated) {
-    Assert(!d_equalityEngine.areDisequal(atom[0], atom[1],false));
-    d_equalityEngine.assertEquality(atom, false, reason);
-    //    !!! need to send this out
-  }
-  else {
-    Assert(!d_equalityEngine.areEqual(atom[0], atom[1]));
-    d_equalityEngine.assertEquality(atom, true, reason);
+  Debug("shared-terms-database::assert") << "SharedTermsDatabase::assertEquality(" << equality << ", " << (polarity ? "true" : "false") << ", " << reason << ")" << endl;
+  // Add it to the equality engine
+  d_equalityEngine.assertEquality(equality, polarity, reason);
+  // Check for conflict
+  checkForConflict();
+}
+
+bool SharedTermsDatabase::propagateEquality(TNode equality, bool polarity) {
+  if (polarity) {
+    d_theoryEngine->propagate(equality, THEORY_BUILTIN);
+  } else {
+    d_theoryEngine->propagate(equality.notNode(), THEORY_BUILTIN);
   }
+  return true;
 }
 
 static Node mkAnd(const std::vector<TNode>& conjunctions) {
@@ -335,18 +218,35 @@ static Node mkAnd(const std::vector<TNode>& conjunctions) {
   }
 
   return conjunction;
-}/* mkAnd() */
+}
 
+void SharedTermsDatabase::checkForConflict() {
+  if (d_inConflict) {
+    d_inConflict = false;
+    std::vector<TNode> assumptions;
+    d_equalityEngine.explainEquality(d_conflictLHS, d_conflictRHS, d_conflictPolarity, assumptions);
+    Node conflict = mkAnd(assumptions);
+    d_theoryEngine->conflict(conflict, THEORY_BUILTIN);    
+    d_conflictLHS = d_conflictRHS = Node::null();
+  }
+}
 
-Node SharedTermsDatabase::explain(TNode literal)
-{
-  std::vector<TNode> assumptions;
-  if (literal.getKind() == kind::NOT) {
-    Assert(literal[0].getKind() == kind::EQUAL);
-    d_equalityEngine.explainEquality(literal[0][0], literal[0][1], false, assumptions);
+bool SharedTermsDatabase::isKnown(TNode literal) const {
+  bool polarity = literal.getKind() != kind::NOT;
+  TNode equality = polarity ? literal : literal[0];
+  if (polarity) {
+    return d_equalityEngine.areEqual(equality[0], equality[1]);
   } else {
-    Assert(literal.getKind() == kind::EQUAL);
-    d_equalityEngine.explainEquality(literal[0], literal[1], true, assumptions);
+    return d_equalityEngine.areDisequal(equality[0], equality[1], false);
   }
-  return mkAnd(assumptions);
 }
+
+Node SharedTermsDatabase::explain(TNode literal) const {
+  bool polarity = literal.getKind() != kind::NOT;
+  TNode atom = polarity ? literal : literal[0];
+  Assert(atom.getKind() == kind::EQUAL);
+  std::vector<TNode> assumptions;
+  d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+  return mkAnd(assumptions);  
+}
+
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index c044097ff..1a38d7332 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -18,12 +18,14 @@
 
 #include "expr/node.h"
 #include "theory/theory.h"
-#include "context/context.h"
-#include "util/stats.h"
 #include "theory/uf/equality_engine.h"
+#include "util/stats.h"
+#include "context/cdhashset.h"
 
 namespace CVC4 {
 
+class TheoryEngine;
+
 class SharedTermsDatabase : public context::ContextNotifyObj {
 
 public:
@@ -54,51 +56,20 @@ private:
   /** Context-dependent size of the d_addedSharedTerms list */
   context::CDO<unsigned> d_addedSharedTermsSize;
   
-  typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap;
-
   /** A map from atoms and subterms to the theories that use it */
+  typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap;
   SharedTermsTheoriesMap d_termsToTheories;
 
-  typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap;
-
   /** Map from term to theories that have already been notified about the shared term */
+  typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap;
   AlreadyNotifiedMap d_alreadyNotifiedMap;
 
-public:
-
-  /** Class for notifications about new shared term equalities */
-  class SharedTermsNotifyClass {
-    public:
-      SharedTermsNotifyClass() {}
-      virtual ~SharedTermsNotifyClass() {}
-      virtual void notify(TNode literal, TNode original, theory::TheoryId theory) = 0;
-  };
+  /** The registered equalities for propagation */
+  typedef context::CDHashSet<TNode, TNodeHashFunction> RegisteredEqualitiesSet;
+  RegisteredEqualitiesSet d_registeredEqualities;
 
 private:
 
-  // Instance of class to send shared term notifications to
-  SharedTermsNotifyClass& d_sharedNotify;
-
-  // Type for list of theory, node pairs: theory is theory to be notified,
-  // node is the representative for this equivalence class known to the
-  // theory that will be notified
-  typedef context::CDHashMap<theory::TheoryId, TNode, __gnu_cxx::hash<unsigned> > NotifyList;
-  typedef context::CDHashMap<TNode, NotifyList*, TNodeHashFunction> TermToNotifyList;
-
-  // Map from terms (only valid for reps) to their notify lists
-  // Note that theory, term pairs only need to be in the notify list if the
-  // representative term is not a valid shared term for the theory.
-  TermToNotifyList d_termToNotifyList;
-
-  // List of allocated NotifyList* objects
-  std::vector<NotifyList*> d_allocatedNL;
-
-  // Total number of allocated NotifyList* objects
-  unsigned d_allocatedNLSize;
-
-  // Size of portion of d_allocatedNL that is currently in use
-  context::CDO<unsigned> d_allocatedNLNext;
-
   /** This method removes all the un-necessary stuff from the maps */
   void backtrack();
 
@@ -108,7 +79,7 @@ private:
   public:
     EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {}
     bool eqNotifyTriggerEquality(TNode equality, bool value) {
-      Unreachable();
+      d_sharedTerms.propagateEquality(equality, value);
       return true;
     }
 
@@ -118,14 +89,12 @@ private:
     }
 
     bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) {
-      if (value) {
-        d_sharedTerms.mergeSharedTerms(t1, t2);
-      }
-      return true;
+      return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value);
     }
 
     bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-      return true;
+      d_sharedTerms.conflict(t1, t2, true);
+      return false;
     }
   };
 
@@ -135,24 +104,83 @@ private:
   /** Equality engine */
   theory::eq::EqualityEngine d_equalityEngine;
 
-  /** Attach a new notify list to an equivalence class representative */
-  NotifyList* getNewNotifyList();
+  /**
+   * Method called by equalityEngine when a becomes (dis-)equal to b and a and b are shared with
+   * the theory. Returns false if there is a direct conflict (via rewrite for example).
+   */
+  bool propagateSharedEquality(theory::TheoryId theory, TNode a, TNode b, bool value);
+
+  /**
+   * Called from the equality engine when a trigger equality is deduced.
+   */
+  bool propagateEquality(TNode equality, bool polarity);
+
+  /** Theory engine */
+  TheoryEngine* d_theoryEngine;  
+
+  /** Are we in conflict */
+  context::CDO<bool> d_inConflict;
+  
+  /** Conflicting terms, if any */
+  Node d_conflictLHS, d_conflictRHS;
+  
+  /** Polarity of the conflict */
+  bool d_conflictPolarity;
+
+  /** Called by the equality engine notify to mark the conflict */
+  void conflict(TNode lhs, TNode rhs, bool polarity) {
+    if (!d_inConflict) {
+      // Only remember it if we're not already in conflict
+      d_inConflict = true;
+      d_conflictLHS = lhs;
+      d_conflictRHS = rhs;
+      d_conflictPolarity = polarity;
+    }
+  }
 
-  /** Method called by equalityEngine when a becomes equal to b */
-  void mergeSharedTerms(TNode a, TNode b);
+  /**
+   * Should be called before any public non-const method in order to
+   * enqueue the conflict to the theory engine.
+   */
+  void checkForConflict();
 
 public:
 
-  SharedTermsDatabase(SharedTermsNotifyClass& notify, context::Context* context);
+  SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context);
   ~SharedTermsDatabase() throw(AssertionException);
   
   /**
+   * Asserts the equality to the shared terms database,
+   */
+  void assertEquality(TNode equality, bool polarity, TNode reason);
+
+  /**
+   * Return whether the equality is alreday known to the engine
+   */
+  bool isKnown(TNode literal) const;
+
+  /** 
+   * Returns an explanation of the propagation that came from the database.
+   */
+  Node explain(TNode literal) const;
+
+  /**
+   * Add an equality to propagate.
+   */
+  void addEqualityToPropagate(TNode equality);
+  
+  /**
    * Add a shared term to the database. The shared term is a subterm of the atom and 
    * should be associated with the given theory. 
    */
   void addSharedTerm(TNode atom, TNode term, theory::Theory::Set theories);
 
   /**
+   * Mark that the given theories have been notified of the given shared term.
+   */
+  void markNotified(TNode term, theory::Theory::Set theories);
+
+  /**
    * Returns true if the atom contains any shared terms, false otherwise.
    */
   bool hasSharedTerms(TNode atom) const;
@@ -176,26 +204,32 @@ public:
    * Get the theories that share the term and have been notified already.
    */
   theory::Theory::Set getNotifiedTheories(TNode term) const;
-
-  // Notify theory about a new equality between shared terms
-  void assertEq(TNode equality, theory::TheoryId theory);
-
+   
   /**
-   * Mark that the given theories have been notified of the given shared term.
+   * Returns true if the term is currently registered as shared with some theory.
    */
-  void markNotified(TNode term, theory::Theory::Set theories);
-   
   bool isShared(TNode term) const {
-    return d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end();
+    return term.isConst() || d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end();
   }
 
-  bool areEqual(TNode a, TNode b);
-
-  bool areDisequal(TNode a, TNode b);
+  /**
+   * Returns true if the literal is an (dis-)equality with both sides registered as shared with
+   * some theory.
+   */
+  bool isSharedEquality(TNode literal) const {
+    TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
+    return atom.getKind() == kind::EQUAL && isShared(atom[0]) && isShared(atom[1]);
+  }
 
-  void processSharedLiteral(TNode literal, TNode reason);
+  /**
+   * Returns true if the shared terms a and b are known to be equal.
+   */
+  bool areEqual(TNode a, TNode b) const;
 
-  Node explain(TNode literal);
+  /**
+   * Retursn true if the shared terms a and b are known to be dis-equal.
+   */
+  bool areDisequal(TNode a, TNode b) const;
 
 protected:
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 3e1dc6fe4..ca2460805 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -45,22 +45,22 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_context(context),
   d_userContext(userContext),
   d_logicInfo(logicInfo),
-  d_notify(*this),
-  d_sharedTerms(d_notify, context),
+  d_sharedTerms(this, context),
   d_ppCache(),
   d_possiblePropagations(context),
   d_hasPropagated(context),
   d_inConflict(context, false),
   d_hasShutDown(false),
   d_incomplete(context, false),
-  d_sharedLiteralsIn(context),
-  d_assertedLiteralsOut(context),
+  d_propagationMap(context),
+  d_propagationMapTimestamp(context, 0),
   d_propagatedLiterals(context),
   d_propagatedLiteralsIndex(context, 0),
   d_decisionRequests(context),
   d_decisionRequestsIndex(context, 0),
   d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
   d_inPreregister(false),
+  d_factsAsserted(context, false),
   d_preRegistrationVisitor(this, context),
   d_sharedTermsVisitor(d_sharedTerms),
   d_unconstrainedSimp(context, logicInfo)
@@ -105,6 +105,11 @@ void TheoryEngine::preRegister(TNode preprocessed) {
       preprocessed = d_preregisterQueue.front();
       d_preregisterQueue.pop();
 
+      if (d_logicInfo.isSharingEnabled() && preprocessed.getKind() == kind::EQUAL) {
+        // When sharing is enabled, we propagate from the shared terms manager also
+        d_sharedTerms.addEqualityToPropagate(preprocessed);
+      }
+
       // Pre-register the terms in the atom
       bool multipleTheories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
       if (multipleTheories) {
@@ -148,6 +153,50 @@ void TheoryEngine::printAssertions(const char* tag) {
   }
 }
 
+void TheoryEngine::dumpAssertions(const char* tag) {
+  if (Dump.isOn(tag)) {
+    Dump(tag) << CommentCommand("Starting completeness check");
+    for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
+      Theory* theory = d_theoryTable[theoryId];
+      if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
+        Dump(tag) << CommentCommand("Completeness check");
+        Dump(tag) << PushCommand();
+
+        // Dump the shared terms 
+        if (d_logicInfo.isSharingEnabled()) {
+          Dump(tag) << CommentCommand("Shared terms");
+          context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
+          for (unsigned i = 0; it != it_end; ++ it, ++i) {
+              stringstream ss;
+              ss << (*it);
+              Dump(tag) << CommentCommand(ss.str());
+          }
+        }
+
+        // Dump the assertions 
+        Dump(tag) << CommentCommand("Assertions");
+        context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
+        for (; it != it_end; ++ it) {
+          // Get the assertion
+          Node assertionNode = (*it).assertion;
+          // Purify all the terms
+          
+          BoolExpr assertionExpr(assertionNode.toExpr());
+          if ((*it).isPreregistered) {
+            Dump(tag) << CommentCommand("Preregistered");
+          } else {
+            Dump(tag) << CommentCommand("Shared assertion");
+          }
+          Dump(tag) << AssertCommand(assertionExpr);
+        }
+        Dump(tag) << CheckSatCommand();
+        Dump(tag) << PopCommand();
+      }
+    }
+  }
+}
+
+
 template<typename T, bool doAssert>
 class scoped_vector_clear {
   vector<T>& d_v;
@@ -181,8 +230,6 @@ void TheoryEngine::check(Theory::Effort effort) {
        } \
     }
 
-  // make sure d_propagatedSharedLiterals is cleared on exit
-  scoped_vector_clear<SharedLiteral, true> clear_shared_literals(d_propagatedSharedLiterals);
 
   // Do the checking
   try {
@@ -194,15 +241,25 @@ void TheoryEngine::check(Theory::Effort effort) {
     // Mark the lemmas flag (no lemmas added)
     d_lemmasAdded = false;
 
-    while (true) {
+    Debug("theory") << "TheoryEngine::check(" << effort << "): d_factsAsserted = " << (d_factsAsserted ? "true" : "false") << std::endl;
+
+    // If in full effort, we have a fake new assertion just to jumpstart the checking
+    if (Theory::fullEffort(effort)) {
+      d_factsAsserted = true;
+    } 
+    
+    // Check until done
+    while (d_factsAsserted && !d_inConflict && !d_lemmasAdded) {
 
       Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl;
-      Assert(d_propagatedSharedLiterals.empty());
 
       if (Debug.isOn("theory::assertions")) {
         printAssertions("theory::assertions");
       }
 
+      // Note that we've discharged all the facts
+      d_factsAsserted = false;
+
       // Do the checking
       CVC4_FOR_EACH_THEORY;
 
@@ -217,34 +274,11 @@ void TheoryEngine::check(Theory::Effort effort) {
       // We are still satisfiable, propagate as much as possible
       propagate(effort);
 
-      // If we have any propagated shared literals, we enqueue them to the theories and re-check
-      if (d_propagatedSharedLiterals.size() > 0) {
-        Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared literals" << std::endl;
-        outputSharedLiterals();
-        continue;
-      }
-
-      // If we added any lemmas, we're done
-      if (d_lemmasAdded) {
-        Debug("theory") << "TheoryEngine::check(" << effort << "): lemmas added, done" << std::endl;
-        break;
-      }
-
-      // If in full check and no lemmas added, run the combination
-      if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled()) {
+      // We do combination if all has been processed and we are in fullcheck
+      if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled() && !d_factsAsserted && !d_lemmasAdded) {
         // Do the combination
         Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << std::endl;
         combineTheories();
-        // If we have any propagated shared literals, we enqueue them to the theories and re-check
-        if (d_propagatedSharedLiterals.size() > 0) {
-          Debug("theory") << "TheoryEngine::check(" << effort << "): distributing shared literals" << std::endl;
-          outputSharedLiterals();
-        } else {
-          // No propagated shared literals, we're either sat, or there are lemmas added
-          break;
-        }
-      } else {
-        break;
       }
     }
 
@@ -253,30 +287,15 @@ void TheoryEngine::check(Theory::Effort effort) {
   } catch(const theory::Interrupted&) {
     Trace("theory") << "TheoryEngine::check() => conflict" << endl;
   }
-}
-
-void TheoryEngine::outputSharedLiterals() {
-
-  scoped_vector_clear<SharedLiteral, false> clear_shared_literals(d_propagatedSharedLiterals);
-
-  // Assert all the shared literals
-  for (unsigned i = 0; i < d_propagatedSharedLiterals.size(); ++ i) {
-    const SharedLiteral& eq = d_propagatedSharedLiterals[i];
-    // Check if the theory already got this one
-    if (d_assertedLiteralsOut.find(eq.toAssert) == d_assertedLiteralsOut.end()) {
-      Debug("sharing") << "TheoryEngine::outputSharedLiterals(): asserting " << eq.toAssert.node << " to " << eq.toAssert.theory << std::endl;
-      Debug("sharing") << "TheoryEngine::outputSharedLiterals(): orignal " << eq.toExplain << std::endl;
-      d_assertedLiteralsOut[eq.toAssert] = eq.toExplain;
-      if (eq.toAssert.theory == theory::THEORY_LAST) {
-        d_propagatedLiterals.push_back(eq.toAssert.node);
-      } else {
-        theoryOf(eq.toAssert.theory)->assertFact(eq.toAssert.node, false);
-      }
+  
+  // If fulleffort, check all theories 
+  if(Dump.isOn("theory::fullcheck") && Theory::fullEffort(effort)) {
+    if (!d_inConflict && !d_lemmasAdded) {
+      dumpAssertions("theory::fullcheck");
     }
   }
 }
 
-
 void TheoryEngine::combineTheories() {
 
   Debug("sharing") << "TheoryEngine::combineTheories()" << std::endl;
@@ -305,44 +324,38 @@ void TheoryEngine::combineTheories() {
 
     Debug("sharing") << "TheoryEngine::combineTheories(): checking " << carePair.a << " = " << carePair.b << " from " << carePair.theory << std::endl;
 
-    if (d_sharedTerms.areEqual(carePair.a, carePair.b) ||
-        d_sharedTerms.areDisequal(carePair.a, carePair.b)) {
-      continue;
-    }
-
-    if (carePair.a.isConst() && carePair.b.isConst()) {
-      // TODO: equality engine should auto-detect these as disequal
-      d_sharedTerms.processSharedLiteral(carePair.a.eqNode(carePair.b).notNode(), d_true);
-      continue;
-    }
+    Assert(!d_sharedTerms.areEqual(carePair.a, carePair.b), "Please don't care about stuff you were notified about");
+    Assert(!d_sharedTerms.areDisequal(carePair.a, carePair.b), "Please don't care about stuff you were notified about");
 
+    // The equality in question
     Node equality = carePair.a.eqNode(carePair.b);
+
+    // Normalize the equality
     Node normalizedEquality = Rewriter::rewrite(equality);
-    bool isTrivial = normalizedEquality.getKind() == kind::CONST_BOOLEAN;
-    bool value;
-    if (isTrivial || (d_propEngine->isSatLiteral(normalizedEquality) && d_propEngine->hasValue(normalizedEquality, value))) {
-      // Missed propagation!
-      Debug("sharing") << "TheoryEngine::combineTheories(): has a literal or is trivial" << std::endl;
-      
-      if (isTrivial) {
-        value = normalizedEquality.getConst<bool>();
-        normalizedEquality = d_true;
-      }
-      else {
-        d_sharedLiteralsIn[normalizedEquality] = theory::THEORY_LAST;
-        if (!value) normalizedEquality = normalizedEquality.notNode();
-      }
-      if (!value) {
-        equality = equality.notNode();
+
+    // Check if the normalized equality already has a value (this also
+    // covers constants, since they always have values
+    if (d_propEngine->isSatLiteral(normalizedEquality)) {
+      bool value;
+      if (d_propEngine->hasValue(normalizedEquality, value)) {
+        Assert(equality != normalizedEquality);
+        Node literal = value ? equality : equality.notNode();
+        Node normalizedLiteral = value ? normalizedEquality : normalizedEquality.notNode();
+        // We're sending the original literal back, backed by the normalized one
+        if (markPropagation(literal, normalizedLiteral, /* to */ carePair.theory, /* from */ THEORY_SAT_SOLVER)) {        
+          // We assert it, and we know it's preregistereed if it's the same theory
+          bool preregistered = Theory::theoryOf(literal) == carePair.theory;
+          theoryOf(carePair.theory)->assertFact(literal, preregistered);
+          // Mark that we have more information
+          d_factsAsserted = true;
+          continue;
+        }
       }
-      d_sharedTerms.processSharedLiteral(equality, normalizedEquality);
-      continue;
     }
-
-    // There is no value, so we need to split on it
+        
+    // We need to split on it
     Debug("sharing") << "TheoryEngine::combineTheories(): requesting a split " << std::endl;
     lemma(equality.orNode(equality.notNode()), false, false);
-
   }
 }
 
@@ -363,7 +376,7 @@ void TheoryEngine::propagate(Theory::Effort effort) {
     for(unsigned i = 0; i < d_possiblePropagations.size(); ++ i) {
       Node atom = d_possiblePropagations[i];
       bool value;
-      if (d_propEngine->hasValue(atom, value)) continue;
+      if (!d_propEngine->hasValue(atom, value)) continue;
       // Doesn't have a value, check it (and the negation)
       if(d_hasPropagated.find(atom) == d_hasPropagated.end()) {
         Dump("missed-t-propagations")
@@ -662,24 +675,160 @@ Node TheoryEngine::preprocess(TNode assertion) {
   return d_ppCache[assertion];
 }
 
-void TheoryEngine::assertFact(TNode node)
-{
-  Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
-  // Trace("theory::assertions") << "TheoryEngine::assertFact(" << node << "): d_sharedTermsExist = " << (d_sharedTermsExist ? "true" : "false") << std::endl;
+bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
+
+  // What and where we are asserting
+  NodeTheoryPair toAssert(assertion, toTheoryId, d_propagationMapTimestamp);
+  // What and where it came from
+  NodeTheoryPair toExplain(originalAssertion, fromTheoryId, d_propagationMapTimestamp);
+
+  // See if the theory already got this literal  
+  PropagationMap::const_iterator find = d_propagationMap.find(toAssert);
+  if (find != d_propagationMap.end()) {
+    // The theory already knows this
+    Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): already there" << std::endl;
+    return false;
+  }
+
+  Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): marking [" << d_propagationMapTimestamp << "] " << assertion << ", " << toTheoryId << " from " << originalAssertion << ", " << fromTheoryId << std::endl;
+
+  // Mark the propagation
+  d_propagationMap[toAssert] = toExplain;
+  d_propagationMapTimestamp = d_propagationMapTimestamp + 1;
+
+  return true;
+}
+
+
+void TheoryEngine::assertToTheory(TNode assertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
+ 
+  Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << ")" << std::endl;
+  
+  Assert(toTheoryId != fromTheoryId);
+  
+  if (d_inConflict) {
+    return;
+  }
+
+  // If sharing is disabled, things are easy
+  if (!d_logicInfo.isSharingEnabled()) {
+    if (fromTheoryId == THEORY_SAT_SOLVER) {
+      // Send to the apropriate theory
+      theory::Theory* toTheory = theoryOf(toTheoryId);
+      // We assert it, and we know it's preregistereed
+      toTheory->assertFact(assertion, true);
+      // Mark that we have more information
+      d_factsAsserted = true;      
+    } else {
+      Assert(toTheoryId == THEORY_SAT_SOLVER);
+      // Enqueue for propagation to the SAT solver
+      d_propagatedLiterals.push_back(assertion);
+      // Check for propositional conflict
+      bool value;
+      if (d_propEngine->hasValue(assertion, value) && !value) {
+        d_inConflict = true;
+      }
+    }
+    return;
+  }
+  
+  // Polarity of the assertion
+  bool polarity = assertion.getKind() != kind::NOT;
+  
+  // Atom of the assertion
+  TNode atom = polarity ? assertion : assertion[0];
+  
+  // If sending to the shared terms database, it's also simple
+  if (toTheoryId == THEORY_BUILTIN) {
+    Assert(atom.getKind() == kind::EQUAL);
+    if (markPropagation(assertion, assertion, toTheoryId, fromTheoryId)) {
+      d_sharedTerms.assertEquality(atom, polarity, assertion);
+    }
+    return;
+  }
+  
+  // Things from the SAT solver are already normalized, so they go 
+  // directly to the apropriate theory
+  if (fromTheoryId == THEORY_SAT_SOLVER) {
+    // We know that this is normalized, so just send it off to the theory 
+    if (markPropagation(assertion, assertion, toTheoryId, fromTheoryId)) {
+      // We assert it, and we know it's preregistereed coming from the SAT solver directly
+      theoryOf(toTheoryId)->assertFact(assertion, true);
+      // Mark that we have more information
+      d_factsAsserted = true;
+    }
+    return;
+  }
+  
+  // Propagations to the SAT solver are just enqueued for pickup by
+  // the SAT solver later
+  if (toTheoryId == THEORY_SAT_SOLVER) {
+    if (markPropagation(assertion, assertion, toTheoryId, fromTheoryId)) {
+      // Enqueue for propagation to the SAT solver
+      d_propagatedLiterals.push_back(assertion);
+      // Check for propositional conflicts
+      bool value;
+      if (d_propEngine->hasValue(assertion, value) && !value) {
+        d_inConflict = true;
+      }
+    }
+    return;
+  }
+  
+  // We are left with internal distribution of shared literals
+  Assert(atom.getKind() == kind::EQUAL);
+  Node normalizedAtom = Rewriter::rewriteEquality(toTheoryId, atom);
+  Node normalizedAssertion = polarity ? normalizedAtom : normalizedAtom.notNode();
+  
+  // If we normalize to true or false, it's a special case
+  if (normalizedAtom.isConst()) {
+    if (polarity == normalizedAtom.getConst<bool>()) {
+      // Trivially true, just ignore
+      return;
+    } else {
+      // Mark the propagation for explanations
+      if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) {
+        // Get the explanation (conflict will figure out where it came from)
+        conflict(normalizedAssertion, toTheoryId);
+      } else {
+        Unreachable();
+      }
+      return;
+    }
+  }
+  
+  // Try and assert
+  if (markPropagation(normalizedAssertion, assertion, toTheoryId, fromTheoryId)) {
+    // Check if has been pre-registered with the theory
+    bool preregistered = d_propEngine->isSatLiteral(normalizedAssertion) && Theory::theoryOf(normalizedAtom) == toTheoryId;
+    // Assert away
+    theoryOf(toTheoryId)->assertFact(normalizedAssertion, preregistered);
+    d_factsAsserted = true;
+  } 
+
+  return;
+}
 
+void TheoryEngine::assertFact(TNode literal)
+{
+  Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << std::endl;
+  
   d_propEngine->checkTime();
 
+  // If we're in conflict, nothing to do
+  if (d_inConflict) {
+    return;
+  }
+
   // Get the atom
-  bool negated = node.getKind() == kind::NOT;
-  TNode atom = negated ? node[0] : node;
-  Theory* theory = theoryOf(atom);
+  bool polarity = literal.getKind() != kind::NOT;
+  TNode atom = polarity ? literal : literal[0];
 
   if (d_logicInfo.isSharingEnabled()) {
 
-    Trace("theory::assertions") << "TheoryEngine::assertFact(" << node << "): hasShared terms = " << (d_sharedTerms.hasSharedTerms(atom) ? "true" : "false") << std::endl;
-
-    // If any shared terms, notify the theories
+    // If any shared terms, it's time to do sharing work
     if (d_sharedTerms.hasSharedTerms(atom)) {
+      // Notify the theories the shared terms
       SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
       SharedTermsDatabase::shared_terms_iterator it_end = d_sharedTerms.end(atom);
       for (; it != it_end; ++ it) {
@@ -692,48 +841,27 @@ void TheoryEngine::assertFact(TNode node)
         }
         d_sharedTerms.markNotified(term, theories);
       }
-      if (d_propagatedSharedLiterals.size() > 0) {
-        Debug("theory") << "TheoryEngine::assertFact: distributing shared literals from new shared terms" << std::endl;
-        outputSharedLiterals();
-      }
     }
 
-    if (atom.getKind() == kind::EQUAL &&
-        d_sharedTerms.isShared(atom[0]) &&
-        d_sharedTerms.isShared(atom[1])) {
-      Debug("sharing") << "TheoryEngine::assertFact: asserting shared node: " << node << std::endl;
-      // Important: don't let facts through that are already known by the shared terms database or we can get into a loop in explain
-      if ((negated && d_sharedTerms.areDisequal(atom[0], atom[1])) ||
-          ((!negated) && d_sharedTerms.areEqual(atom[0], atom[1]))) {
-        Debug("sharing") << "TheoryEngine::assertFact: sharedLiteral already known(" << node << ")" << std::endl;
-        return;
-      }
-      d_sharedLiteralsIn[node] = THEORY_LAST;
-      d_sharedTerms.processSharedLiteral(node, node);
-      if (d_propagatedSharedLiterals.size() > 0) {
-        Debug("theory") << "TheoryEngine::assertFact: distributing shared literals from new assertion" << std::endl;
-        outputSharedLiterals();
-      }
-      // TODO: have processSharedLiteral propagate disequalities?
-      if (node.getKind() == kind::EQUAL) {
-        // Don't have to assert it - this will be taken care of by processSharedLiteral
-        Assert(d_logicInfo.isTheoryEnabled(theory->getId()));
-        return;
-      }
-    }
-    // If theory didn't already get this literal, add to the map
-    NodeTheoryPair ntp(node, theory->getId());
-    if (d_assertedLiteralsOut.find(ntp) == d_assertedLiteralsOut.end()) {
-      d_assertedLiteralsOut[ntp] = Node();
+    // If it's an equality, assert it to the shared term manager, even though the terms are not
+    // yet shared. As the terms become shared later, the shared terms manager will then add them
+    // to the assert the equality to the interested theories
+    if (atom.getKind() == kind::EQUAL) {
+      // Assert it to the the owning theory
+      assertToTheory(literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
+      // Shared terms manager will assert to interested theories directly, as the terms become shared
+      assertToTheory(literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER);
+    } else {
+      // Not an equality, just assert to the appropriate theory
+      assertToTheory(literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
     }
+  } else {
+    // Assert the fact to the appropriate theory directly
+    assertToTheory(literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
   }
-
-  // Assert the fact to the appropriate theory and mark it active
-  theory->assertFact(node, true);
-  Assert(d_logicInfo.isTheoryEnabled(theory->getId()));
 }
 
-void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
+bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
 
   Debug("theory") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << std::endl;
 
@@ -747,42 +875,26 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
     d_hasPropagated.insert(literal);
   }
 
-  bool negated = (literal.getKind() == kind::NOT);
-  TNode atom = negated ? literal[0] : literal;
-  bool value;
+  // Get the atom
+  bool polarity = literal.getKind() != kind::NOT;
+  TNode atom = polarity ? literal : literal[0];
 
-  if (!d_logicInfo.isSharingEnabled() || atom.getKind() != kind::EQUAL ||
-      !d_sharedTerms.isShared(atom[0]) || !d_sharedTerms.isShared(atom[1])) {
-    // If not an equality or if an equality between terms that are not both shared,
-    // it must be a SAT literal so we enqueue it
-    Assert(d_propEngine->isSatLiteral(literal));
-    if (d_propEngine->hasValue(literal, value)) {
-      // if we are propagting something that already has a sat value we better be the same
-      Debug("theory") << "literal " << literal << ") propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl;
-      Assert(value);
-    } else {
-      d_propagatedLiterals.push_back(literal);
+  if (d_logicInfo.isSharingEnabled() && atom.getKind() == kind::EQUAL) {
+    if (d_propEngine->isSatLiteral(literal)) {
+      // We propagate SAT literals to SAT
+      assertToTheory(literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
     }
-  } else {
-    // Important: don't let facts through that are already known by the shared terms database or we can get into a loop in explain
-    if ((negated && d_sharedTerms.areDisequal(atom[0], atom[1])) ||
-        ((!negated) && d_sharedTerms.areEqual(atom[0], atom[1]))) {
-      Debug("sharing") << "TheoryEngine::propagate: sharedLiteral already known(" << literal << ")" << std::endl;
-      return;
+    if (theory != THEORY_BUILTIN) {
+      // Assert to the shared terms database
+      assertToTheory(literal, /* to */ THEORY_BUILTIN, /* from */ theory);      
     }
-
-    // Otherwise it is a shared-term (dis-)equality
-    Node normalizedLiteral = Rewriter::rewrite(literal);
-    if (d_propEngine->isSatLiteral(normalizedLiteral)) {
-      // If there is a literal, propagate it to SAT
-      SharedLiteral sharedLiteral(normalizedLiteral, literal, theory::THEORY_LAST);
-      d_propagatedSharedLiterals.push_back(sharedLiteral);
-    }
-    // Assert to interested theories
-    Debug("shared-in") << "TheoryEngine::propagate: asserting shared node: " << literal << std::endl;
-    d_sharedLiteralsIn[literal] = theory;
-    d_sharedTerms.processSharedLiteral(literal, literal);
+  } else {
+    // Just send off to the SAT solver
+    Assert(d_propEngine->isSatLiteral(literal));
+    assertToTheory(literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
   }
+
+  return !d_inConflict;
 }
 
 
@@ -809,160 +921,112 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
   return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
 }
 
-Node TheoryEngine::getExplanation(TNode node) {
-  Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl;
+static Node mkExplanation(const std::vector<NodeTheoryPair>& explanation) {
 
-  TNode atom = node.getKind() == kind::NOT ? node[0] : node;
-
-  Node explanation;
-
-  // The theory that has explaining to do
-  Theory* theory;
-
-  //This is true if atom is a shared assertion
-  bool sharedLiteral = false;
-
-  AssertedLiteralsOutMap::iterator find;
-  // "find" will have a value when sharedAssertion is true
-  if (d_logicInfo.isSharingEnabled() && atom.getKind() == kind::EQUAL) {
-    find = d_assertedLiteralsOut.find(NodeTheoryPair(node, theory::THEORY_LAST));
-    sharedLiteral = (find != d_assertedLiteralsOut.end());
+  std::set<TNode> all;
+  for (unsigned i = 0; i < explanation.size(); ++ i) {
+    Assert(explanation[i].theory == THEORY_SAT_SOLVER);
+    all.insert(explanation[i].node);
   }
 
-  // Get the explanation
-  if(sharedLiteral) {
-    explanation = explain(ExplainTask((*find).second, SHARED_LITERAL_OUT));
-  } else {
-    theory = theoryOf(atom);
-    explanation = theory->explain(node);
-
-    // Explain any shared equalities that might be in the explanation
-    if (d_logicInfo.isSharingEnabled()) {
-      explanation = explain(ExplainTask(explanation, THEORY_EXPLANATION, theory->getId()));
-    }
+  if (all.size() == 0) {
+    // Normalize to true
+    return NodeManager::currentNM()->mkConst<bool>(true);
   }
 
-  Assert(!explanation.isNull());
-  if(Dump.isOn("t-explanations")) {
-    Dump("t-explanations") << CommentCommand(std::string("theory explanation from ") + theoryOf(atom)->identify() + ": expect valid")
-      << QueryCommand(explanation.impNode(node).toExpr());
+  if (all.size() == 1) {
+    // All the same, or just one
+    return explanation[0].node;
   }
-  Assert(properExplanation(node, explanation));
 
-  Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << std::endl;
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = all.begin();
+  std::set<TNode>::const_iterator it_end = all.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
+  }
 
-  return explanation;
+  return conjunction;
 }
 
-Node TheoryEngine::explain(ExplainTask toExplain)
-{
-  Debug("theory") << "TheoryEngine::explain(" << toExplain.node << ", " << toExplain.kind << ", " << toExplain.theory << ")" << std::endl;
-
-  std::set<TNode> satAssertions;
-  std::deque<ExplainTask> explainQueue;
-  // TODO: benchmark whether this helps
-  std::hash_set<ExplainTask, ExplainTaskHashFunction> explained;
 
-#ifdef CVC4_ASSERTIONS
-  bool value;
-#endif
-
-  // No need to explain "true"
-  explained.insert(ExplainTask(d_true, SHARED_DATABASE_EXPLANATION));
-
-  while (true) {
-
-    Debug("theory-explain") << "TheoryEngine::explain(" << toExplain.node << ", " << toExplain.kind << ", " << toExplain.theory << ")" << std::endl;
-
-    if (explained.find(toExplain) == explained.end()) {
+Node TheoryEngine::getExplanation(TNode node) {
+  Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl;
 
-      explained.insert(toExplain);
+  bool polarity = node.getKind() != kind::NOT;
+  TNode atom = polarity ? node : node[0];
 
-      if (toExplain.node.getKind() == kind::AND) {
-        for (unsigned i = 0, i_end = toExplain.node.getNumChildren(); i != i_end; ++ i) {
-          explainQueue.push_back(ExplainTask(toExplain.node[i], toExplain.kind, toExplain.theory));
-        }
-      }
-      else {
-
-        switch (toExplain.kind) {
-
-          // toExplain.node contains a shared literal sent out from theory engine (before being rewritten)
-          case SHARED_LITERAL_OUT: {
-            // Shortcut - see if this came directly from a theory
-            SharedLiteralsInMap::iterator it = d_sharedLiteralsIn.find(toExplain.node);
-            if (it != d_sharedLiteralsIn.end()) {
-              TheoryId id = (*it).second;
-              if (id == theory::THEORY_LAST) {
-                Assert(d_propEngine->isSatLiteral(toExplain.node));
-                Assert(d_propEngine->hasValue(toExplain.node, value) && value);
-                satAssertions.insert(toExplain.node);
-                break;
-              }
-              explainQueue.push_back(ExplainTask(theoryOf((*it).second)->explain(toExplain.node), THEORY_EXPLANATION, (*it).second));
-            }
-            // Otherwise, get explanation from shared terms database
-            else {
-              explainQueue.push_back(ExplainTask(d_sharedTerms.explain(toExplain.node), SHARED_DATABASE_EXPLANATION));
-            }
-            break;
-          }
+  // If we're not in shared mode, explanations are simple
+  if (!d_logicInfo.isSharingEnabled()) {
+    Node explanation = theoryOf(atom)->explain(node);
+    Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << std::endl;
+    return explanation;
+  }
 
-            // toExplain.node contains explanation from theory, toExplain.theory contains theory that produced explanation
-          case THEORY_EXPLANATION: {
-            AssertedLiteralsOutMap::iterator find = d_assertedLiteralsOut.find(NodeTheoryPair(toExplain.node, toExplain.theory));
-            if (find == d_assertedLiteralsOut.end() || (*find).second.isNull()) {
-              Assert(d_propEngine->isSatLiteral(toExplain.node));
-              Assert(d_propEngine->hasValue(toExplain.node, value) && value);
-              satAssertions.insert(toExplain.node);
-            }
-            else {
-              explainQueue.push_back(ExplainTask((*find).second, SHARED_LITERAL_OUT));
-            }
-            break;
-          }
+  // Initial thing to explain 
+  NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp);
+  Assert(d_propagationMap.find(toExplain) != d_propagationMap.end());
+  // Create the workplace for explanations
+  std::vector<NodeTheoryPair> explanationVector;
+  explanationVector.push_back(d_propagationMap[toExplain]);
+  // Process the explanation
+  getExplanation(explanationVector);
+  Node explanation = mkExplanation(explanationVector);
+  
+  Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => " << explanation << std::endl;
+ 
+  return explanation;
+}
 
-            // toExplain.node contains an explanation from the shared terms database
-            // Each literal in the explanation should be in the d_sharedLiteralsIn map
-          case SHARED_DATABASE_EXPLANATION: {
-            Assert(d_sharedLiteralsIn.find(toExplain.node) != d_sharedLiteralsIn.end());
-            TheoryId id = d_sharedLiteralsIn[toExplain.node];
-            if (id == theory::THEORY_LAST) {
-              Assert(d_propEngine->isSatLiteral(toExplain.node));
-              Assert(d_propEngine->hasValue(toExplain.node, value) && value);
-              satAssertions.insert(toExplain.node);
-            }
-            else {
-              explainQueue.push_back(ExplainTask(theoryOf(id)->explain(toExplain.node), THEORY_EXPLANATION, id));
-            }
-            break;
-          }        
-          default:
-            Unreachable();
-        }
-      }
-    }
+theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable) {
+  if(Dump.isOn("t-lemmas")) {
+    Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
+                     << QueryCommand(node.toExpr());
+  }
 
-    if (explainQueue.empty()) break;
+  // Share with other portfolio threads
+  if(Options::current()->lemmaOutputChannel != NULL) {
+    Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr());
+  }
 
-    toExplain = explainQueue.front();
-    explainQueue.pop_front();
+  // Remove the ITEs
+  std::vector<Node> additionalLemmas;
+  IteSkolemMap iteSkolemMap;
+  additionalLemmas.push_back(node);
+  RemoveITE::run(additionalLemmas, iteSkolemMap);
+  additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
+
+  // assert to prop engine
+  d_propEngine->assertLemma(additionalLemmas[0], negated, removable);
+  for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
+    additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
+    d_propEngine->assertLemma(additionalLemmas[i], false, removable);
   }
 
-  Assert(satAssertions.size() > 0);
-  if (satAssertions.size() == 1) {
-    return *(satAssertions.begin());
+  // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
+  // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
+  if(negated) {
+    // Can't we just get rid of passing around this 'negated' stuff?
+    // Is it that hard for the propEngine to figure that out itself?
+    // (I like the use of triple negation <evil laugh>.) --K
+    additionalLemmas[0] = additionalLemmas[0].notNode();
+    negated = false;
   }
+  // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
+  // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
 
-  // Now build the explanation
-  NodeBuilder<> conjunction(kind::AND);
-  std::set<TNode>::const_iterator it = satAssertions.begin();
-  std::set<TNode>::const_iterator it_end = satAssertions.end();
-  while (it != it_end) {
-    conjunction << *it;
-    ++ it;
+  // assert to decision engine
+  if(!removable) {
+    d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap);
   }
-  return conjunction;
+  
+  // Mark that we added some lemmas
+  d_lemmasAdded = true;
+
+  // Lemma analysis isn't online yet; this lemma may only live for this
+  // user level.
+  return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel());
 }
 
 void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
@@ -974,12 +1038,16 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
                         << CheckSatCommand(conflict.toExpr());
   }
-
+  
+  // In the multiple-theories case, we need to reconstruct the conflict
   if (d_logicInfo.isSharingEnabled()) {
-    // In the multiple-theories case, we need to reconstruct the conflict
-    Node fullConflict = explain(ExplainTask(conflict, THEORY_EXPLANATION, theoryId));
-    Assert(properConflict(fullConflict));
-    Debug("theory") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): " << fullConflict << std::endl;
+    // Create the workplace for explanations
+    std::vector<NodeTheoryPair> explanationVector;
+    explanationVector.push_back(NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
+    // Process the explanation
+    getExplanation(explanationVector);
+    Node fullConflict = mkExplanation(explanationVector);
+    Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << std::endl;
     lemma(fullConflict, true, false);
   } else {
     // When only one theory, the conflict should need no processing
@@ -988,24 +1056,6 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
   }
 }
 
-
-//Conflict from shared terms database
-void TheoryEngine::sharedConflict(TNode conflict) {
-  // Mark that we are in conflict
-  d_inConflict = true;
-
-  if(Dump.isOn("t-conflicts")) {
-    Dump("t-conflicts") << CommentCommand("theory conflict: expect unsat")
-                        << CheckSatCommand(conflict.toExpr());
-  }
-
-  Node fullConflict = explain(ExplainTask(d_sharedTerms.explain(conflict), SHARED_DATABASE_EXPLANATION));
-  Assert(properConflict(fullConflict));
-  Debug("theory") << "TheoryEngine::sharedConflict(" << conflict << "): " << fullConflict << std::endl;
-  lemma(fullConflict, true, false);
-}
-
-
 Node TheoryEngine::ppSimpITE(TNode assertion)
 {
   Node result = d_iteSimplifier.simpITE(assertion);
@@ -1014,6 +1064,77 @@ Node TheoryEngine::ppSimpITE(TNode assertion)
   return result;
 }
 
+void TheoryEngine::getExplanation(std::vector<NodeTheoryPair>& explanationVector)
+{
+  Assert(explanationVector.size() > 0);
+
+  unsigned i = 0; // Index of the current literal we are processing
+  unsigned j = 0; // Index of the last literal we are keeping
+    
+  while (i < explanationVector.size()) {
+  
+    // Get the current literal to explain
+    NodeTheoryPair toExplain = explanationVector[i];
+
+    Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << std::endl;
+
+    // If a treu constant or a negation of a false constant we can ignore it
+    if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) {
+      ++ i;
+      continue;
+    }    
+    if (toExplain.node.getKind() == kind::NOT && toExplain.node[0].isConst() && !toExplain.node[0].getConst<bool>()) {
+      ++ i;
+      continue;
+    }
+
+    // If from the SAT solver, keep it
+    if (toExplain.theory == THEORY_SAT_SOLVER) {
+      explanationVector[j++] = explanationVector[i++];
+      continue;
+    }
+
+    // If an and, expand it
+    if (toExplain.node.getKind() == kind::AND) {
+      Debug("theory::explain") << "TheoryEngine::explain(): expanding " << toExplain.node << " got from " << toExplain.theory << std::endl;
+      for (unsigned k = 0; k < toExplain.node.getNumChildren(); ++ k) {
+        NodeTheoryPair newExplain(toExplain.node[k], toExplain.theory, toExplain.timestamp);
+        explanationVector.push_back(newExplain);
+      }
+      ++ i;
+      continue;
+    }
+
+    // See if it was sent to the theory by another theory 
+    PropagationMap::const_iterator find = d_propagationMap.find(toExplain);
+    if (find != d_propagationMap.end()) {
+      // There is some propagation, check if its a timely one
+      if ((*find).second.timestamp < toExplain.timestamp) {
+        explanationVector.push_back((*find).second);
+        ++ i;
+        continue;
+      }
+    }
+
+    // It was produced by the theory, so ask for an explanation
+    Node explanation;
+    if (toExplain.theory == THEORY_BUILTIN) {
+      explanation = d_sharedTerms.explain(toExplain.node);
+    } else {
+      explanation = theoryOf(toExplain.theory)->explain(toExplain.node);
+    }
+    Assert(explanation != toExplain.node, "wansn't sent to you, so why are you explaining it trivially");
+    Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << std::endl;
+    // Mark the explanation
+    NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp);
+    explanationVector.push_back(newExplain);
+    ++ i;
+  }
+    
+  // Keep only the relevant literals
+  explanationVector.resize(j);
+}  
+
 
 void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
 {
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index bc9f4c889..ed95149b3 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -46,16 +46,19 @@
 
 namespace CVC4 {
 
-// In terms of abstraction, this is below (and provides services to)
-// PropEngine.
-
+/**
+ * A pair of a theory and a node. This is used to mark the flow of 
+ * propagations between theories.
+ */ 
 struct NodeTheoryPair {
   Node node;
   theory::TheoryId theory;
-  NodeTheoryPair(TNode node, theory::TheoryId theory)
-  : node(node), theory(theory) {}
+  size_t timestamp;
+  NodeTheoryPair(TNode node, theory::TheoryId theory, size_t timestamp)
+  : node(node), theory(theory), timestamp(timestamp) {}
   NodeTheoryPair()
   : theory(theory::THEORY_LAST) {}
+  // Comparison doesn't take into account the timestamp  
   bool operator == (const NodeTheoryPair& pair) const {
     return node == pair.node && theory == pair.theory;
   }
@@ -63,6 +66,7 @@ struct NodeTheoryPair {
 
 struct NodeTheoryPairHashFunction {
   NodeHashFunction hashFunction;
+  // Hash doesn't take into account the timestamp
   size_t operator()(const NodeTheoryPair& pair) const {
     return hashFunction(pair.node)*0x9e3779b9 + pair.theory;
   }
@@ -75,6 +79,9 @@ struct NodeTheoryPairHashFunction {
  * CVC4.
  */
 class TheoryEngine {
+  
+  /** Shared terms database can use the internals notify the theories */
+  friend class SharedTermsDatabase;
 
   /** Associated PropEngine engine */
   prop::PropEngine* d_propEngine;
@@ -103,21 +110,6 @@ class TheoryEngine {
    */
   const LogicInfo& d_logicInfo;
 
-  // NotifyClass: template helper class for Shared Terms Database
-  class NotifyClass :public SharedTermsDatabase::SharedTermsNotifyClass {
-    TheoryEngine& d_theoryEngine;
-  public:
-    NotifyClass(TheoryEngine& engine): d_theoryEngine(engine) {}
-    ~NotifyClass() {}
-
-    void notify(TNode literal, TNode original, theory::TheoryId theory) {
-      d_theoryEngine.propagateSharedLiteral(literal, original, theory);
-    }
-  };
-
-  // Instance of NotifyClass
-  NotifyClass d_notify;
-
   /**
    * The database of shared terms.
    */
@@ -221,11 +213,11 @@ class TheoryEngine {
       d_engine->conflict(conflictNode, d_theory);
     }
 
-    void propagate(TNode literal) throw(AssertionException) {
+    bool propagate(TNode literal) throw(AssertionException) {
       Trace("theory::propagate") << "EngineOutputChannel<" << d_theory << ">::propagate(" << literal << ")" << std::endl;
       ++ d_statistics.propagations;
       d_engine->d_outputChannelUsed = true;
-      d_engine->propagate(literal, d_theory);
+      return d_engine->propagate(literal, d_theory);
     }
 
     void propagateAsDecision(TNode literal) throw(AssertionException) {
@@ -263,28 +255,11 @@ class TheoryEngine {
   context::CDO<bool> d_inConflict;
 
   /**
-   * Explain the equality literals and push all the explaining literals
-   * into the builder. All the non-equality literals are pushed to the
-   * builder.
-   */
-  void explainEqualities(theory::TheoryId theoryId, TNode literals, NodeBuilder<>& builder);
-
-  /**
-   * Same as above, but just for single equalities.
-   */
-  void explainEquality(theory::TheoryId theoryId, TNode eqLiteral, NodeBuilder<>& builder);
-
-  /**
    * Called by the theories to notify of a conflict.
    */
   void conflict(TNode conflict, theory::TheoryId theoryId);
 
   /**
-   * Called by shared terms database to notify of a conflict.
-   */
-  void sharedConflict(TNode conflict);
-
-  /**
    * Debugging flag to ensure that shutdown() is called before the
    * destructor.
    */
@@ -310,63 +285,16 @@ class TheoryEngine {
     d_propEngine->spendResource();
   }
 
-  struct SharedLiteral {
-    /**
-     * The node/theory pair for the assertion. THEORY_LAST indicates this is a SAT
-     * literal and should be sent to the SAT solver
-     */
-    NodeTheoryPair toAssert;
-    /** This is the node that we will use to explain it */
-    Node toExplain;
-
-    SharedLiteral(TNode assertion, TNode original, theory::TheoryId receivingTheory)
-    : toAssert(assertion, receivingTheory),
-      toExplain(original)
-    { }
-  };
-
-  /**
-   * Map from nodes to theories.
-   */
-  typedef context::CDHashMap<Node, theory::TheoryId, NodeHashFunction> SharedLiteralsInMap;
-
   /**
-   * All shared literals asserted to theory engine.
-   * Maps from literal to the theory that sent the literal (THEORY_LAST means sent from SAT).
+   * Mapping of propagations from recievers to senders.
    */
-  SharedLiteralsInMap d_sharedLiteralsIn;
-
-  /**
-   * Map from literals asserted by theory engine to literal that can explain
-   */
-  typedef context::CDHashMap<NodeTheoryPair, Node, NodeTheoryPairHashFunction> AssertedLiteralsOutMap;
-
-  /**
-   * All literals asserted to theories from theory engine.
-   * Maps from literal/theory pair to literal that can explain this assertion.
-   */
-  AssertedLiteralsOutMap d_assertedLiteralsOut;
-
-  /**
-   * Shared literals queud up to be asserted to the individual theories.
-   */
-  std::vector<SharedLiteral> d_propagatedSharedLiterals;
-
-  void propagateSharedLiteral(TNode literal, TNode original, theory::TheoryId theory)
-  {
-    if (literal.getKind() == kind::CONST_BOOLEAN) {
-      Assert(!literal.getConst<bool>());
-      sharedConflict(original);
-    }
-    else {
-      d_propagatedSharedLiterals.push_back(SharedLiteral(literal, original, theory));
-    }
-  }
+  typedef context::CDHashMap<NodeTheoryPair, NodeTheoryPair, NodeTheoryPairHashFunction> PropagationMap;
+  PropagationMap d_propagationMap;
 
   /**
-   * Assert the shared literals that are queued up to the theories.
+   * Timestamp of propagations
    */
-  void outputSharedLiterals();
+  context::CDO<size_t> d_propagationMapTimestamp;
 
   /**
    * Literals that are propagated by the theory. Note that these are TNodes.
@@ -395,8 +323,9 @@ class TheoryEngine {
 
   /**
    * Called by the output channel to propagate literals and facts
+   * @return false if immediate conflict
    */
-  void propagate(TNode literal, theory::TheoryId theory);
+  bool propagate(TNode literal, theory::TheoryId theory);
 
   /**
    * Internal method to call the propagation routines and collect the
@@ -427,55 +356,8 @@ class TheoryEngine {
   /**
    * Adds a new lemma, returning its status.
    */
-  theory::LemmaStatus lemma(TNode node, bool negated, bool removable) {
-    if(Dump.isOn("t-lemmas")) {
-      Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
-                       << QueryCommand(node.toExpr());
-    }
-
-    // Share with other portfolio threads
-    if(Options::current()->lemmaOutputChannel != NULL) {
-      Options::current()->lemmaOutputChannel->notifyNewLemma(node.toExpr());
-    }
-
-    // Remove the ITEs
-    std::vector<Node> additionalLemmas;
-    IteSkolemMap iteSkolemMap;
-    additionalLemmas.push_back(node);
-    RemoveITE::run(additionalLemmas, iteSkolemMap);
-    additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
-
-    // assert to prop engine
-    d_propEngine->assertLemma(additionalLemmas[0], negated, removable);
-    for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
-      additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
-      d_propEngine->assertLemma(additionalLemmas[i], false, removable);
-    }
-
-    // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
-    // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
-    if(negated) {
-      // Can't we just get rid of passing around this 'negated' stuff?
-      // Is it that hard for the propEngine to figure that out itself?
-      // (I like the use of triple negation <evil laugh>.) --K
-      additionalLemmas[0] = additionalLemmas[0].notNode();
-      negated = false;
-    }
-    // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
-    // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
-
-    // assert to decision engine
-    if(!removable)
-      d_decisionEngine->addAssertions(additionalLemmas, 1, iteSkolemMap);
-
-    // Mark that we added some lemmas
-    d_lemmasAdded = true;
-
-    // Lemma analysis isn't online yet; this lemma may only live for this
-    // user level.
-    return theory::LemmaStatus(additionalLemmas[0], d_userContext->getLevel());
-  }
-
+  theory::LemmaStatus lemma(TNode node, bool negated, bool removable);
+  
   /** Time spent in theory combination */
   TimerStat d_combineTheoriesTime;
 
@@ -535,6 +417,45 @@ private:
    */
   bool d_inPreregister;
 
+  /**
+   * Did the theories get any new facts since the last time we called
+   * check()
+   */
+  context::CDO<bool> d_factsAsserted;
+
+  /**
+   * Assert the formula to the given theory.
+   * @param assertion the assertion to send (not necesserily normalized)
+   * @param original the assertion as it was sent in from the propagating theory
+   * @param toTheoryId the theory to assert to
+   * @param fromTheoryId the theory that sent it
+   */
+  void assertToTheory(TNode assertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId);
+
+  /**
+   * Marks a theory propagation from a theory to a theory where a 
+   * theory could be the THEORY_SAT_SOLVER for literals coming from
+   * or being propagated to the SAT solver. If the receiving theory
+   * already recieved the literal, the method returns false, otherwise
+   * it returns true.
+   * 
+   * @param assertion the normalized assertion being sent
+   * @param originalAssertion the actual assertion that was sent
+   * @param toTheoryId the theory that is on the receiving end
+   * @param fromTheoryId the theory that sent the assertino
+   * @return true if a new assertion, false if theory already got it
+   */
+  bool markPropagation(TNode assertion, TNode originalAssertions, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId);
+
+  /**
+   * Computes the explanation by travarsing the propagation graph and
+   * asking relevant theories to explain the propagations. Initially 
+   * the explanation vector should contain only the element (node, theory)
+   * where the node is the one to be explained, and the theory is the
+   * theory that sent the literal.
+   */
+  void getExplanation(std::vector<NodeTheoryPair>& explanationVector);
+
 public:
 
   /**
@@ -657,40 +578,14 @@ public:
   bool properPropagation(TNode lit) const;
   bool properExplanation(TNode node, TNode expl) const;
 
-  enum ExplainTaskKind {
-    // Literal sent out from the theory engine
-    SHARED_LITERAL_OUT,
-    // Explanation produced by a theory
-    THEORY_EXPLANATION,
-    // Explanation produced by the shared terms database
-    SHARED_DATABASE_EXPLANATION
-  };
-
-  struct ExplainTask {
-    Node node;
-    ExplainTaskKind kind;
-    theory::TheoryId theory;
-    ExplainTask(Node n, ExplainTaskKind k, theory::TheoryId tid = theory::THEORY_LAST) :
-      node(n), kind(k), theory(tid) {}
-    bool operator == (const ExplainTask& other) const {
-      return node == other.node && kind == other.kind && theory == other.theory;
-    }
-  };
-
-  struct ExplainTaskHashFunction {
-    size_t operator () (const ExplainTask& task) const {
-      size_t hash = 0;
-      hash = 0x9e3779b9 + NodeHashFunction().operator()(task.node);
-      hash ^= 0x9e3779b9 + task.kind + (hash << 6) + (hash >> 2);
-      hash ^= 0x9e3779b9 + task.theory + (hash << 6) + (hash >> 2);
-      return hash;
-    }
-  };
-
+  /**
+   * Returns an explanation of the node propagated to the SAT solver.
+   */
   Node getExplanation(TNode node);
 
-  Node explain(ExplainTask toExplain);
-
+  /**
+   * Returns the value of the given node.
+   */
   Node getValue(TNode node);
 
   /**
@@ -732,6 +627,9 @@ private:
   /** Prints the assertions to the debug stream */
   void printAssertions(const char* tag);
 
+  /** Dump the assertions to the dump */
+  void dumpAssertions(const char* tag);
+
   /** For preprocessing pass simplifying ITEs */
   ITESimplifier d_iteSimplifier;
 
@@ -739,6 +637,7 @@ private:
   UnconstrainedSimplifier d_unconstrainedSimp;
 
 public:
+
   Node ppSimpITE(TNode assertion);
   void ppUnconstrainedSimp(std::vector<Node>& assertions);
 
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index aaf47425b..bf1370090 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -78,9 +78,10 @@ public:
     push(CONFLICT, n);
   }
 
-  void propagate(TNode n)
+  bool propagate(TNode n)
     throw(AssertionException) {
     push(PROPAGATE, n);
+    return true;
   }
 
   void propagateAsDecision(TNode n)
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 5093e5a7b..4cd54a2bf 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -62,14 +62,14 @@ void EqualityEngine::init() {
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 
+  d_triggerDatabaseAllocatedSize = 100000;
+  d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize);
+
   addTerm(d_true);
   addTerm(d_false);
 
   d_trueId = getNodeId(d_true);
   d_falseId = getNodeId(d_false);  
-
-  d_triggerDatabaseAllocatedSize = 100000;
-  d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize);
 } 
 
 EqualityEngine::~EqualityEngine() throw(AssertionException) {
@@ -114,7 +114,8 @@ EqualityEngine::EqualityEngine(EqualityEngineNotify& notify, context::Context* c
 }
 
 void EqualityEngine::enqueue(const MergeCandidate& candidate) {
-    d_propagationQueue.push(candidate);
+  Debug("equality") << "EqualityEngine::enqueue(" << d_nodes[candidate.t1Id] << ", " << d_nodes[candidate.t2Id] << ", " << candidate.type << ")" << std::endl;
+  d_propagationQueue.push(candidate);
 }
 
 EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, bool isEquality) {
@@ -144,7 +145,15 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId
     if (isEquality && d_isConstant[t1ClassId] && d_isConstant[t2ClassId]) {
       if (t1ClassId != t2ClassId) {
         Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): got constants" << std::endl;
+        Assert(d_nodes[funId].getKind() == kind::EQUAL);
         enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+        // Also enqueue the symmetric one
+        TNode eq = d_nodes[funId];
+        Node symmetricEq = eq[1].eqNode(eq[0]);
+        if (hasTerm(symmetricEq)) {
+          EqualityNodeId symmFunId = getNodeId(symmetricEq);
+          enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));              
+        }
       }
     }
   } else {
@@ -154,8 +163,8 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId
   }
 
   // Add to the use lists
-  d_equalityNodes[t1ClassId].usedIn<USE_LIST_FUNCTIONS>(funId, d_useListNodes);
-  d_equalityNodes[t2ClassId].usedIn<USE_LIST_FUNCTIONS>(funId, d_useListNodes);
+  d_equalityNodes[t1].usedIn(funId, d_useListNodes);
+  d_equalityNodes[t2].usedIn(funId, d_useListNodes);
 
   // Return the new id
   Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ") => " << funId << std::endl;
@@ -238,6 +247,20 @@ void EqualityEngine::addTerm(TNode t) {
     // We set this here as this only applies to actual terms, not the
     // intermediate application terms
     d_isBoolean[result] = true;
+  } else if (t.isConst()) {
+    // Non-Boolean constants are trigger terms for all tags
+    EqualityNodeId tId = getNodeId(t);
+    d_newSetTags = 0;
+    d_newSetTriggersSize = THEORY_LAST;
+    for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST; ++ currentTheory) {
+      d_newSetTags = Theory::setInsert(currentTheory, d_newSetTags);
+      d_newSetTriggers[currentTheory] = tId;
+    } 
+    // Add it to the list for backtracking
+    d_triggerTermSetUpdates.push_back(TriggerSetUpdate(tId, null_set_id));
+    d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
+    // Mark the the new set as a trigger 
+    d_nodeIndividualTrigger[tId] = newTriggerTermSet();
   }
 
   propagate();
@@ -319,15 +342,20 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) {
     assertEqualityInternal(eq, d_false, reason);
     propagate();    
     assertEqualityInternal(eq[1].eqNode(eq[0]), d_false, reason);
-    propagate();
+    propagate();    
   
     if (d_done) {
       return;
     }
   
-    // If we are adding a disequality, notify of the shared term representatives
+    // If both have constant representatives, we don't notify anyone
     EqualityNodeId a = getNodeId(eq[0]);
     EqualityNodeId b = getNodeId(eq[1]);
+    if (isConstant(a) && isConstant(b)) {
+      return;
+    }    
+    
+    // If we are adding a disequality, notify of the shared term representatives
     EqualityNodeId eqId = getNodeId(eq);
     TriggerTermSetRef aTriggerRef = d_nodeIndividualTrigger[a];
     TriggerTermSetRef bTriggerRef = d_nodeIndividualTrigger[b];
@@ -356,6 +384,7 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) {
           d_deducedDisequalityReasons.push_back(EqualityPair(bSharedId, b));
           d_deducedDisequalityReasons.push_back(EqualityPair(eqId, d_falseId));
           storePropagatedDisequality(d_nodes[aSharedId], d_nodes[bSharedId], 3);
+
           // We notify even if the it's already been sent (they are not 
           // disequal at assertion, and we need to notify for each tag) 
           if (!d_notify.eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) {
@@ -383,7 +412,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
   Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl;
 
   Assert(triggersFired.empty());
-
+  
   ++ d_stats.mergesCount;
 
   EqualityNodeId class1Id = class1.getFind();
@@ -391,6 +420,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
 
   // Check for constant merges
   bool isConstant = d_isConstant[class1Id];
+  Assert(isConstant || !d_isConstant[class2Id]);
 
   // Update class2 representative information
   Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl;
@@ -438,13 +468,13 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
       Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl;
  
       // Go through the uselist and check for congruences
-      UseListNodeId currentUseId = currentNode.getUseList<USE_LIST_FUNCTIONS>();
+      UseListNodeId currentUseId = currentNode.getUseList();
       while (currentUseId != null_uselist_id) {
         // Get the node of the use list
         UseListNode& useNode = d_useListNodes[currentUseId];
         // Get the function application
         EqualityNodeId funId = useNode.getApplicationId();
-        Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl;
+        Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl;
         const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized;
         // Check if there is an application with find arguments
         EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
@@ -460,11 +490,16 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
           // There is no representative, so we can add one, we remove this when backtracking
           storeApplicationLookup(funNormalized, funId);
           // Now, if we're constant and it's an equality, check if the other guy is also a constant
-          if (isConstant && funNormalized.isEquality) {
-            if (d_isConstant[funNormalized.a] && d_isConstant[funNormalized.b]) {
-              // both constants
-              if (funNormalized.a != funNormalized.b) {
-                enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+          if (funNormalized.isEquality) {
+            if (d_isConstant[aNormalized] && d_isConstant[bNormalized] && aNormalized != bNormalized) {
+              Assert(d_nodes[funId].getKind() == kind::EQUAL);
+              enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
+              // Also enqueue the symmetric one
+              TNode eq = d_nodes[funId];
+              Node symmetricEq = eq[1].eqNode(eq[0]);
+              if (hasTerm(symmetricEq)) {
+                EqualityNodeId symmFunId = getNodeId(symmetricEq);
+                enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));              
               }
             }
           }          
@@ -482,6 +517,17 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
   // Now merge the lists
   class1.merge<true>(class2);
 
+  // Notify of the constants merge
+  bool constantMerge = false;
+  if (isConstant && d_isConstant[class2Id]) {
+    constantMerge = true;
+    if (d_performNotify) {
+      if (!d_notify.eqNotifyConstantTermMerge(d_nodes[class1Id], d_nodes[class2Id])) {
+        return false;
+      }
+    }
+  }
+
   // Go through the triggers and store the dis-equalities
   unsigned i = 0, j = 0;
   for (; i < triggersFired.size();) {
@@ -543,7 +589,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
           // copy tag1 
           EqualityNodeId tag1id = d_newSetTriggers[d_newSetTriggersSize++] = class1triggers.triggers[i1++];
           // since they are both tagged notify of merge
-          if (d_performNotify) {
+          if (d_performNotify && !constantMerge) {
             EqualityNodeId tag2id = class2triggers.triggers[i2++];
             if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) {
               return false;
@@ -566,15 +612,6 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
     }	
   }
 
-  // Notify of the constants merge
-  if (isConstant && d_isConstant[class2Id]) {
-    if (d_performNotify) {
-      if (!d_notify.eqNotifyConstantTermMerge(d_nodes[class1Id], d_nodes[class2Id])) {
-        return false;
-      }
-    }
-  }
-
   // Everything fine
   return true;
 }
@@ -680,12 +717,12 @@ void EqualityEngine::backtrack() {
       Debug("equality") << "EqualityEngine::backtrack(): removing node " << d_nodes[i] << std::endl;
       d_nodeIds.erase(d_nodes[i]);
 
-      const FunctionApplication& app = d_applications[i].normalized;
+      const FunctionApplication& app = d_applications[i].original;
       if (app.isApplication()) {
         // Remove b from use-list
-        getEqualityNode(app.b).removeTopFromUseList<USE_LIST_FUNCTIONS>(d_useListNodes);
+        getEqualityNode(app.b).removeTopFromUseList(d_useListNodes);
         // Remove a from use-list
-        getEqualityNode(app.a).removeTopFromUseList<USE_LIST_FUNCTIONS>(d_useListNodes);
+        getEqualityNode(app.a).removeTopFromUseList(d_useListNodes);
       }
     }
 
@@ -818,8 +855,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
 
     // Go through the equality edges of this node
     EqualityEdgeId currentEdge = d_equalityGraph[currentNode];
-    Debug("equality") << "EqualityEngine::getExplanation(): edgesId =  " << currentEdge << std::endl;
-    Debug("equality") << "EqualityEngine::getExplanation(): edges =  " << edgesToString(currentEdge) << std::endl;
+    if (Debug.isOn("equality")) {
+      Debug("equality") << "EqualityEngine::getExplanation(): edgesId =  " << currentEdge << std::endl;
+      Debug("equality") << "EqualityEngine::getExplanation(): edges =  " << edgesToString(currentEdge) << std::endl;
+    }
 
     while (currentEdge != null_edge) {
       // Get the edge
@@ -871,8 +910,10 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               
               Debug("equality") << push;
               // Explain why a is a constant
+              Assert(isConstant(eq.a));
               getExplanation(eq.a, getEqualityNode(eq.a).getFind(), equalities);
               // Explain why b is a constant
+              Assert(isConstant(eq.b));
               getExplanation(eq.b, getEqualityNode(eq.b).getFind(), equalities);
               Debug("equality") << pop;
             
@@ -1062,7 +1103,7 @@ void EqualityEngine::propagate() {
 
     // Depending on the merge preference (such as size, or being a constant), merge them
     std::vector<TriggerId> triggers;
-    if (node2.getSize() > node1.getSize() || d_isConstant[t2classId]) {
+    if ((node2.getSize() > node1.getSize() && !d_isConstant[t1classId]) || d_isConstant[t2classId]) {
       Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl;
       d_assertedEqualities.push_back(Equality(t2classId, t1classId));
       if (!merge(node2, node1, triggers)) {
@@ -1222,7 +1263,7 @@ size_t EqualityEngine::getSize(TNode t)
 
 void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
 {
-  Debug("equality::internal") << "EqualityEngine::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
+  Debug("equality::trigger") << "EqualityEngine::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
   Assert(tag != THEORY_LAST);
 
   if (d_done) {
@@ -1243,12 +1284,71 @@ void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
     // If the term already is in the equivalence class that a tagged representative, just notify
     if (d_performNotify) {
       EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag);
-      if (!d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) {
+      if (eqNodeId != triggerId && !d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) {
         d_done = true;
       }
     }
   } else {
 
+    // Check for disequalities by going through the equivalence class looking for equalities in the
+    // uselists that have been asserted to false. All the representatives appearing on the other
+    // side of such disequalities, that have the tag on, are put in a set.
+    std::set<EqualityNodeId> disequalSet;
+    EqualityNodeId currentId = classId;
+    do {
+      // Current node
+      EqualityNode& currentNode = getEqualityNode(currentId);
+      // Go through the uselist and look for disequalities
+      UseListNodeId currentUseId = currentNode.getUseList();
+      while (!d_done && currentUseId != null_uselist_id) {
+        // Get the normalized equality
+        UseListNode& useNode = d_useListNodes[currentUseId];
+        EqualityNodeId funId = useNode.getApplicationId();
+        const FunctionApplication& fun = d_applications[useNode.getApplicationId()].original;
+        // Check for asserted disequalities
+        if (fun.isEquality && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) {
+          // Get the other equality member
+          EqualityNodeId toCompare = fun.b;
+          if (toCompare == currentId) {
+            toCompare = fun.a;
+          }
+          // Representative of the other member
+          EqualityNodeId toCompareRep = getEqualityNode(toCompare).getFind();
+          Assert(toCompareRep != classId);
+          // Get the trigger set
+          TriggerTermSetRef toCompareTriggerSetRef = d_nodeIndividualTrigger[toCompareRep];
+          // Only notify if we're not both constants
+          if ((!d_isConstant[classId] || !d_isConstant[toCompareRep]) && toCompareTriggerSetRef != null_set_id) {
+            TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef);
+            if (Theory::setContains(tag, toCompareTriggerSet.tags)) {
+              // Get the tag representative
+              EqualityNodeId tagRep = toCompareTriggerSet.getTrigger(tag);
+              // Propagate the disequality if not already done
+              if (!disequalSet.count(tagRep) && d_performNotify) {
+                // Mark as propagated
+                disequalSet.insert(tagRep);
+                // Store the propagation
+                d_deducedDisequalityReasons.push_back(EqualityPair(eqNodeId, currentId));
+                d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep));
+                d_deducedDisequalityReasons.push_back(EqualityPair(funId, d_falseId));
+                storePropagatedDisequality(t, d_nodes[tagRep], 3);
+                // We don't check if it's been propagated already, as we need one per tag
+                if (d_performNotify) {
+                  if (!d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[tagRep], false)) {
+                    d_done = true;
+                  }
+                }
+              }
+            }
+          }
+        }
+        // Go to the next one in the use list
+        currentUseId = useNode.getNext();
+      }
+      // Next in equivalence class
+      currentId = currentNode.getNext();
+    } while (!d_done && currentId != classId);
+
     // Setup the data for the new set
     if (triggerSetRef != null_set_id) {
       // Get the existing set
@@ -1322,7 +1422,7 @@ void EqualityEngine::getUseListTerms(TNode t, std::set<TNode>& output) {
       // Get the current node
       EqualityNode& currentNode = getEqualityNode(currentId);
       // Go through the use-list
-      UseListNodeId currentUseId = currentNode.getUseList<USE_LIST_FUNCTIONS>();
+      UseListNodeId currentUseId = currentNode.getUseList();
       while (currentUseId != null_uselist_id) {
         // Get the node of the use list
         UseListNode& useNode = d_useListNodes[currentUseId];
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 5ff8ee4dc..f40c79df3 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -345,6 +345,13 @@ private:
   std::vector<bool> d_isConstant;
 
   /**
+   * Returns true if it's a constant
+   */
+  bool isConstant(EqualityNodeId id) const {
+    return d_isConstant[getEqualityNode(id).getFind()];
+  }
+
+  /**
    * Map from ids to wheather they are Boolean.
    */
   std::vector<bool> d_isBoolean;
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index 0baf70fcf..056ee0b84 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -94,8 +94,9 @@ struct MergeCandidate {
   EqualityNodeId t1Id, t2Id;
   MergeReasonType type;
   TNode reason;
-  MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason):
-    t1Id(x), t2Id(y), type(type), reason(reason) {}
+  MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason)
+  : t1Id(x), t2Id(y), type(type), reason(reason) 
+  {}
 };
 
 /**
@@ -145,15 +146,6 @@ public:
   }
 };
 
-/** Main types of uselists */
-enum UseListType {
-  /** Use list of functions where the term appears in */
-  USE_LIST_FUNCTIONS,
-  /** Use list of asserted disequalities */
-  USE_LIST_DISEQUALITIES
-};
-
-
 /**
  * Main class for representing nodes in the equivalence class. The 
  * nodes are a circular list, with the representative carrying the
@@ -178,9 +170,6 @@ private:
   /** The use list of this node */
   UseListNodeId d_useList;
 
-  /** The list of asserted disequalities that this node appears in */
-  UseListNodeId d_diseqList;
-
 public:
 
   /**
@@ -191,15 +180,13 @@ public:
   , d_findId(nodeId) 
   , d_nextId(nodeId)
   , d_useList(null_uselist_id)
-  , d_diseqList(null_uselist_id)
   {}
 
   /**
    * Returns the requested uselist.
    */
-  template<UseListType type>
   UseListNodeId getUseList() const {
-    return type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList;
+    return d_useList;
   }
 
   /**
@@ -244,22 +231,20 @@ public:
    * Note that this node is used in a function application funId, or
    * a negatively asserted equality (dis-equality) with funId. 
    */
-  template<UseListType type, typename memory_class>
+  template<typename memory_class>
   void usedIn(EqualityNodeId funId, memory_class& memory) {
-    UseListNodeId& useList = type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList;
     UseListNodeId newUseId = memory.size();
-    memory.push_back(UseListNode(funId, useList));
-    useList = newUseId;
+    memory.push_back(UseListNode(funId, d_useList));
+    d_useList = newUseId;
   }
 
   /**
    * For backtracking: remove the first element from the uselist and pop the memory.
    */
-  template<UseListType type, typename memory_class>
+  template<typename memory_class>
   void removeTopFromUseList(memory_class& memory) {
-    UseListNodeId& useList = type == USE_LIST_FUNCTIONS ? d_useList : d_diseqList;
-    Assert ((int) useList == (int)memory.size() - 1);
-    useList = memory.back().getNext();
+    Assert ((int) d_useList == (int)memory.size() - 1);
+    d_useList = memory.back().getNext();
     memory.pop_back();
   }
 };
@@ -288,7 +273,7 @@ struct FunctionApplication {
   FunctionApplication(bool isEquality = false, EqualityNodeId a = null_id, EqualityNodeId b = null_id)
   : isEquality(isEquality), a(a), b(b) {}
   bool operator == (const FunctionApplication& other) const {
-    return a == other.a && b == other.b;
+    return isEquality == other.isEquality && a == other.a && b == other.b;
   }
   bool isApplication() const {
     return a != null_id && b != null_id;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index ae8bdc8da..7583f8ee7 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -70,16 +70,6 @@ void TheoryUF::check(Effort level) {
 
     Debug("uf") << "TheoryUF::check(): processing " << fact << std::endl;
 
-    // If the assertion doesn't have a literal, it's a shared equality, so we set it up
-    if (!assertion.isPreregistered) {
-      Debug("uf") << "TheoryUF::check(): shared equality, setting up " << fact << std::endl;
-      if (fact.getKind() == kind::NOT) {
-        preRegisterTerm(fact[0]);
-      } else {
-        preRegisterTerm(fact);
-      }
-    }
-
     // Do the work
     bool polarity = fact.getKind() != kind::NOT;
     TNode atom = polarity ? fact : fact[0];
@@ -90,31 +80,8 @@ void TheoryUF::check(Effort level) {
     }
   }
 
-  // If in conflict, output the conflict
-  if (d_conflict) {
-    Debug("uf") << "TheoryUF::check(): conflict " << d_conflictNode << std::endl;
-    d_out->conflict(d_conflictNode);
-  }
-
-  // Otherwise we propagate in order to detect a weird conflict like
-  // p, x = y
-  // p -> f(x) != f(y) -- f(x) = f(y) gets added to the propagation list at preregistration time
-  // but when f(x) != f(y) is deduced by the sat solver, so it's asserted, and we don't detect the conflict
-  // until we go through the propagation list
-  propagate(level);
 }/* TheoryUF::check() */
 
-void TheoryUF::propagate(Effort level) {
-  Debug("uf") << "TheoryUF::propagate()" << std::endl;
-  if (!d_conflict) {
-    for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
-      TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
-      Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl;
-      d_out->propagate(literal);
-    }
-  }
-}/* TheoryUF::propagate(Effort) */
-
 void TheoryUF::preRegisterTerm(TNode node) {
   Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
 
@@ -143,37 +110,18 @@ void TheoryUF::preRegisterTerm(TNode node) {
 }/* TheoryUF::preRegisterTerm() */
 
 bool TheoryUF::propagate(TNode literal) {
-  Debug("uf") << "TheoryUF::propagate(" << literal  << ")" << std::endl;
-
+  Debug("uf::propagate") << "TheoryUF::propagate(" << literal  << ")" << std::endl;
   // If already in conflict, no more propagation
   if (d_conflict) {
-    Debug("uf") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
+    Debug("uf::propagate") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
     return false;
   }
-
-  // See if the literal has been asserted already
-  Node normalized = Rewriter::rewrite(literal);
-
-  // If asserted and is false, we're done or in conflict
-  // Note that even trivial equalities have a SAT value (i.e. 1 = 2 -> false)
-  bool satValue = false;
-  if (d_valuation.hasSatValue(normalized, satValue) && !satValue) {
-      Debug("uf") << "TheoryUF::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
-      std::vector<TNode> assumptions;
-      Node negatedLiteral;
-      negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
-      assumptions.push_back(negatedLiteral);
-      explain(literal, assumptions);
-      d_conflictNode = mkAnd(assumptions);
-      d_conflict = true;
-      return false;
+  // Propagate out
+  bool ok = d_out->propagate(literal);
+  if (!ok) {
+    d_conflict = true;
   }
-
-  // Nothing, just enqueue it for propagation and mark it as asserted already
-  Debug("uf") << "TheoryUF::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
-  d_literalsToPropagate.push_back(literal);
-
-  return true;
+  return ok;
 }/* TheoryUF::propagate(TNode) */
 
 void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
@@ -437,3 +385,13 @@ void TheoryUF::computeCareGraph() {
     }
   }
 }/* TheoryUF::computeCareGraph() */
+
+void TheoryUF::conflict(TNode a, TNode b) {
+  if (Theory::theoryOf(a) == theory::THEORY_BOOL) {
+    d_conflictNode = explain(a.iffNode(b));
+  } else {
+    d_conflictNode = explain(a.eqNode(b));
+  }
+  d_out->conflict(d_conflictNode);
+  d_conflict = true;
+}
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 1dfcb86f0..0d35d57d8 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -55,7 +55,7 @@ public:
     }
 
     bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
-      Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+      Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
       if (value) {
         return d_uf.propagate(predicate);
       } else {
@@ -64,7 +64,7 @@ public:
     }
 
     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
-      Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << std::endl;
+      Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
       if (value) {
         return d_uf.propagate(t1.eqNode(t2));
       } else {
@@ -73,12 +73,9 @@ public:
     }
 
     bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-      Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
-      if (Theory::theoryOf(t1) == THEORY_BOOL) {
-        return d_uf.propagate(t1.iffNode(t2));
-      } else {
-        return d_uf.propagate(t1.eqNode(t2));
-      }
+      Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
+      d_uf.conflict(t1, t2);
+      return false;
     }
   };
 
@@ -119,13 +116,15 @@ private:
   /** Symmetry analyzer */
   SymmetryBreaker d_symb;
 
+  /** Conflict when merging two constants */
+  void conflict(TNode a, TNode b);
+
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
   TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo);
 
   void check(Effort);
-  void propagate(Effort);
   void preRegisterTerm(TNode term);
   Node explain(TNode n);
 
@@ -135,6 +134,8 @@ public:
   void addSharedTerm(TNode n);
   void computeCareGraph();
 
+  void propagate(Effort effort) {}
+
   EqualityStatus getEqualityStatus(TNode a, TNode b);
 
   std::string identify() const {
diff --git a/src/util/options.cpp b/src/util/options.cpp
index e9ef7d959..e5d91e0d8 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -699,7 +699,8 @@ throw(OptionException) {
         } else if(!strcmp(optarg, "t-conflicts") ||
                   !strcmp(optarg, "t-lemmas") ||
                   !strcmp(optarg, "t-explanations") ||
-                  !strcmp(optarg, "bv-rewrites")) {
+                  !strcmp(optarg, "bv-rewrites") ||
+                  !strcmp(optarg, "theory::fullcheck")) {
           // These are "non-state-dumping" modes.  If state (SAT decisions,
           // propagations, etc.) is dumped, it will interfere with the validity
           // of these generated queries.
diff --git a/test/regress/regress0/aufbv/Makefile b/test/regress/regress0/aufbv/Makefile
new file mode 100644
index 000000000..7dd17882f
--- /dev/null
+++ b/test/regress/regress0/aufbv/Makefile
@@ -0,0 +1,8 @@
+topdir = ../../../..
+srcdir = test/regress/regress0/aufbv
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am
index f9ec6b474..9b9820258 100644
--- a/test/regress/regress0/aufbv/Makefile.am
+++ b/test/regress/regress0/aufbv/Makefile.am
@@ -9,7 +9,10 @@ endif
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =	\
-	bug00.smt
+	bug00.smt \
+	bug338.smt2 \
+	try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \
+	wchains010ue.delta01.smt 
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/aufbv/no_init_multi_delete14.smt b/test/regress/regress0/aufbv/no_init_multi_delete14.smt
new file mode 100644
index 000000000..06071cd32
--- /dev/null
+++ b/test/regress/regress0/aufbv/no_init_multi_delete14.smt
@@ -0,0 +1,670 @@
+(benchmark no_init_multi_delete14.smt
+  :source {
+The benchmarks come from Bounded Model Checking of software.
+Contributed by Lorenzo Platania (c1009@unige.it).
+}
+  :status unknown
+  :difficulty { unknown }
+  :category { industrial }
+  :logic QF_AUFBV
+  :extrafuns ((main_0_head_0 BitVec[32]))
+  :extrafuns ((main_0_head_1 BitVec[32]))
+  :assumption
+(= main_0_head_1 bv0[32])
+  :extrafuns ((arr_val_0 Array[32:32]))
+  :extrafuns ((arr_val_1 Array[32:32]))
+  :assumption
+(= arr_val_1 (store arr_val_0 main_0_head_1 bv0[32]))
+  :extrafuns ((arr_next_0 Array[32:32]))
+  :extrafuns ((arr_next_1 Array[32:32]))
+  :assumption
+(= arr_next_1 (store arr_next_0 main_0_head_1 (bvneg bv1[32])))
+  :extrafuns ((main_0_curr_0 BitVec[32]))
+  :extrafuns ((main_0_curr_1 BitVec[32]))
+  :assumption
+(= main_0_curr_1 main_0_head_1)
+  :extrafuns ((main_0_i_0 BitVec[32]))
+  :extrafuns ((main_0_i_1 BitVec[32]))
+  :assumption
+(= main_0_i_1 bv1[32])
+  :extrafuns ((main_0_tmp_0 BitVec[32]))
+  :extrafuns ((main_0_tmp_1 BitVec[32]))
+  :assumption
+(= main_0_tmp_1 (ite (bvult main_0_i_1 bv13[32]) bv1[32] main_0_tmp_0))
+  :extrafuns ((arr_val_2 Array[32:32]))
+  :assumption
+(= arr_val_2 (ite (bvult main_0_i_1 bv13[32]) (store arr_val_1 main_0_tmp_1 main_0_i_1) arr_val_1))
+  :extrafuns ((arr_next_2 Array[32:32]))
+  :assumption
+(= arr_next_2 (ite (bvult main_0_i_1 bv13[32]) (store arr_next_1 main_0_curr_1 main_0_tmp_1) arr_next_1))
+  :extrafuns ((main_0_curr_2 BitVec[32]))
+  :assumption
+(= main_0_curr_2 (ite (bvult main_0_i_1 bv13[32]) (select arr_next_2 main_0_curr_1) main_0_curr_1))
+  :extrafuns ((arr_next_3 Array[32:32]))
+  :assumption
+(= arr_next_3 (ite (bvult main_0_i_1 bv13[32]) (store arr_next_2 main_0_tmp_1 (bvneg bv1[32])) arr_next_2))
+  :extrafuns ((main_0_temp_i_0 BitVec[32]))
+  :extrafuns ((main_0_temp_i_1 BitVec[32]))
+  :assumption
+(= main_0_temp_i_1 (ite (bvult main_0_i_1 bv13[32]) main_0_i_1 main_0_temp_i_0))
+  :extrafuns ((main_0_i_2 BitVec[32]))
+  :assumption
+(= main_0_i_2 (ite (bvult main_0_i_1 bv13[32]) (bvadd main_0_i_1 bv1[32]) main_0_i_1))
+  :extrafuns ((main_0_tmp_2 BitVec[32]))
+  :assumption
+(= main_0_tmp_2 (ite (bvult main_0_i_2 bv13[32]) bv2[32] main_0_tmp_1))
+  :extrafuns ((arr_val_3 Array[32:32]))
+  :assumption
+(= arr_val_3 (ite (bvult main_0_i_2 bv13[32]) (store arr_val_2 main_0_tmp_2 main_0_i_2) arr_val_2))
+  :extrafuns ((arr_next_4 Array[32:32]))
+  :assumption
+(= arr_next_4 (ite (bvult main_0_i_2 bv13[32]) (store arr_next_3 main_0_curr_2 main_0_tmp_2) arr_next_3))
+  :extrafuns ((main_0_curr_3 BitVec[32]))
+  :assumption
+(= main_0_curr_3 (ite (bvult main_0_i_2 bv13[32]) (select arr_next_4 main_0_curr_2) main_0_curr_2))
+  :extrafuns ((arr_next_5 Array[32:32]))
+  :assumption
+(= arr_next_5 (ite (bvult main_0_i_2 bv13[32]) (store arr_next_4 main_0_tmp_2 (bvneg bv1[32])) arr_next_4))
+  :extrafuns ((main_0_temp_i_2 BitVec[32]))
+  :assumption
+(= main_0_temp_i_2 (ite (bvult main_0_i_2 bv13[32]) main_0_i_2 main_0_temp_i_1))
+  :extrafuns ((main_0_i_3 BitVec[32]))
+  :assumption
+(= main_0_i_3 (ite (bvult main_0_i_2 bv13[32]) (bvadd main_0_i_2 bv1[32]) main_0_i_2))
+  :extrafuns ((main_0_tmp_3 BitVec[32]))
+  :assumption
+(= main_0_tmp_3 (ite (bvult main_0_i_3 bv13[32]) bv3[32] main_0_tmp_2))
+  :extrafuns ((arr_val_4 Array[32:32]))
+  :assumption
+(= arr_val_4 (ite (bvult main_0_i_3 bv13[32]) (store arr_val_3 main_0_tmp_3 main_0_i_3) arr_val_3))
+  :extrafuns ((arr_next_6 Array[32:32]))
+  :assumption
+(= arr_next_6 (ite (bvult main_0_i_3 bv13[32]) (store arr_next_5 main_0_curr_3 main_0_tmp_3) arr_next_5))
+  :extrafuns ((main_0_curr_4 BitVec[32]))
+  :assumption
+(= main_0_curr_4 (ite (bvult main_0_i_3 bv13[32]) (select arr_next_6 main_0_curr_3) main_0_curr_3))
+  :extrafuns ((arr_next_7 Array[32:32]))
+  :assumption
+(= arr_next_7 (ite (bvult main_0_i_3 bv13[32]) (store arr_next_6 main_0_tmp_3 (bvneg bv1[32])) arr_next_6))
+  :extrafuns ((main_0_temp_i_3 BitVec[32]))
+  :assumption
+(= main_0_temp_i_3 (ite (bvult main_0_i_3 bv13[32]) main_0_i_3 main_0_temp_i_2))
+  :extrafuns ((main_0_i_4 BitVec[32]))
+  :assumption
+(= main_0_i_4 (ite (bvult main_0_i_3 bv13[32]) (bvadd main_0_i_3 bv1[32]) main_0_i_3))
+  :extrafuns ((main_0_tmp_4 BitVec[32]))
+  :assumption
+(= main_0_tmp_4 (ite (bvult main_0_i_4 bv13[32]) bv4[32] main_0_tmp_3))
+  :extrafuns ((arr_val_5 Array[32:32]))
+  :assumption
+(= arr_val_5 (ite (bvult main_0_i_4 bv13[32]) (store arr_val_4 main_0_tmp_4 main_0_i_4) arr_val_4))
+  :extrafuns ((arr_next_8 Array[32:32]))
+  :assumption
+(= arr_next_8 (ite (bvult main_0_i_4 bv13[32]) (store arr_next_7 main_0_curr_4 main_0_tmp_4) arr_next_7))
+  :extrafuns ((main_0_curr_5 BitVec[32]))
+  :assumption
+(= main_0_curr_5 (ite (bvult main_0_i_4 bv13[32]) (select arr_next_8 main_0_curr_4) main_0_curr_4))
+  :extrafuns ((arr_next_9 Array[32:32]))
+  :assumption
+(= arr_next_9 (ite (bvult main_0_i_4 bv13[32]) (store arr_next_8 main_0_tmp_4 (bvneg bv1[32])) arr_next_8))
+  :extrafuns ((main_0_temp_i_4 BitVec[32]))
+  :assumption
+(= main_0_temp_i_4 (ite (bvult main_0_i_4 bv13[32]) main_0_i_4 main_0_temp_i_3))
+  :extrafuns ((main_0_i_5 BitVec[32]))
+  :assumption
+(= main_0_i_5 (ite (bvult main_0_i_4 bv13[32]) (bvadd main_0_i_4 bv1[32]) main_0_i_4))
+  :extrafuns ((main_0_tmp_5 BitVec[32]))
+  :assumption
+(= main_0_tmp_5 (ite (bvult main_0_i_5 bv13[32]) bv5[32] main_0_tmp_4))
+  :extrafuns ((arr_val_6 Array[32:32]))
+  :assumption
+(= arr_val_6 (ite (bvult main_0_i_5 bv13[32]) (store arr_val_5 main_0_tmp_5 main_0_i_5) arr_val_5))
+  :extrafuns ((arr_next_10 Array[32:32]))
+  :assumption
+(= arr_next_10 (ite (bvult main_0_i_5 bv13[32]) (store arr_next_9 main_0_curr_5 main_0_tmp_5) arr_next_9))
+  :extrafuns ((main_0_curr_6 BitVec[32]))
+  :assumption
+(= main_0_curr_6 (ite (bvult main_0_i_5 bv13[32]) (select arr_next_10 main_0_curr_5) main_0_curr_5))
+  :extrafuns ((arr_next_11 Array[32:32]))
+  :assumption
+(= arr_next_11 (ite (bvult main_0_i_5 bv13[32]) (store arr_next_10 main_0_tmp_5 (bvneg bv1[32])) arr_next_10))
+  :extrafuns ((main_0_temp_i_5 BitVec[32]))
+  :assumption
+(= main_0_temp_i_5 (ite (bvult main_0_i_5 bv13[32]) main_0_i_5 main_0_temp_i_4))
+  :extrafuns ((main_0_i_6 BitVec[32]))
+  :assumption
+(= main_0_i_6 (ite (bvult main_0_i_5 bv13[32]) (bvadd main_0_i_5 bv1[32]) main_0_i_5))
+  :extrafuns ((main_0_tmp_6 BitVec[32]))
+  :assumption
+(= main_0_tmp_6 (ite (bvult main_0_i_6 bv13[32]) bv6[32] main_0_tmp_5))
+  :extrafuns ((arr_val_7 Array[32:32]))
+  :assumption
+(= arr_val_7 (ite (bvult main_0_i_6 bv13[32]) (store arr_val_6 main_0_tmp_6 main_0_i_6) arr_val_6))
+  :extrafuns ((arr_next_12 Array[32:32]))
+  :assumption
+(= arr_next_12 (ite (bvult main_0_i_6 bv13[32]) (store arr_next_11 main_0_curr_6 main_0_tmp_6) arr_next_11))
+  :extrafuns ((main_0_curr_7 BitVec[32]))
+  :assumption
+(= main_0_curr_7 (ite (bvult main_0_i_6 bv13[32]) (select arr_next_12 main_0_curr_6) main_0_curr_6))
+  :extrafuns ((arr_next_13 Array[32:32]))
+  :assumption
+(= arr_next_13 (ite (bvult main_0_i_6 bv13[32]) (store arr_next_12 main_0_tmp_6 (bvneg bv1[32])) arr_next_12))
+  :extrafuns ((main_0_temp_i_6 BitVec[32]))
+  :assumption
+(= main_0_temp_i_6 (ite (bvult main_0_i_6 bv13[32]) main_0_i_6 main_0_temp_i_5))
+  :extrafuns ((main_0_i_7 BitVec[32]))
+  :assumption
+(= main_0_i_7 (ite (bvult main_0_i_6 bv13[32]) (bvadd main_0_i_6 bv1[32]) main_0_i_6))
+  :extrafuns ((main_0_tmp_7 BitVec[32]))
+  :assumption
+(= main_0_tmp_7 (ite (bvult main_0_i_7 bv13[32]) bv7[32] main_0_tmp_6))
+  :extrafuns ((arr_val_8 Array[32:32]))
+  :assumption
+(= arr_val_8 (ite (bvult main_0_i_7 bv13[32]) (store arr_val_7 main_0_tmp_7 main_0_i_7) arr_val_7))
+  :extrafuns ((arr_next_14 Array[32:32]))
+  :assumption
+(= arr_next_14 (ite (bvult main_0_i_7 bv13[32]) (store arr_next_13 main_0_curr_7 main_0_tmp_7) arr_next_13))
+  :extrafuns ((main_0_curr_8 BitVec[32]))
+  :assumption
+(= main_0_curr_8 (ite (bvult main_0_i_7 bv13[32]) (select arr_next_14 main_0_curr_7) main_0_curr_7))
+  :extrafuns ((arr_next_15 Array[32:32]))
+  :assumption
+(= arr_next_15 (ite (bvult main_0_i_7 bv13[32]) (store arr_next_14 main_0_tmp_7 (bvneg bv1[32])) arr_next_14))
+  :extrafuns ((main_0_temp_i_7 BitVec[32]))
+  :assumption
+(= main_0_temp_i_7 (ite (bvult main_0_i_7 bv13[32]) main_0_i_7 main_0_temp_i_6))
+  :extrafuns ((main_0_i_8 BitVec[32]))
+  :assumption
+(= main_0_i_8 (ite (bvult main_0_i_7 bv13[32]) (bvadd main_0_i_7 bv1[32]) main_0_i_7))
+  :extrafuns ((main_0_tmp_8 BitVec[32]))
+  :assumption
+(= main_0_tmp_8 (ite (bvult main_0_i_8 bv13[32]) bv8[32] main_0_tmp_7))
+  :extrafuns ((arr_val_9 Array[32:32]))
+  :assumption
+(= arr_val_9 (ite (bvult main_0_i_8 bv13[32]) (store arr_val_8 main_0_tmp_8 main_0_i_8) arr_val_8))
+  :extrafuns ((arr_next_16 Array[32:32]))
+  :assumption
+(= arr_next_16 (ite (bvult main_0_i_8 bv13[32]) (store arr_next_15 main_0_curr_8 main_0_tmp_8) arr_next_15))
+  :extrafuns ((main_0_curr_9 BitVec[32]))
+  :assumption
+(= main_0_curr_9 (ite (bvult main_0_i_8 bv13[32]) (select arr_next_16 main_0_curr_8) main_0_curr_8))
+  :extrafuns ((arr_next_17 Array[32:32]))
+  :assumption
+(= arr_next_17 (ite (bvult main_0_i_8 bv13[32]) (store arr_next_16 main_0_tmp_8 (bvneg bv1[32])) arr_next_16))
+  :extrafuns ((main_0_temp_i_8 BitVec[32]))
+  :assumption
+(= main_0_temp_i_8 (ite (bvult main_0_i_8 bv13[32]) main_0_i_8 main_0_temp_i_7))
+  :extrafuns ((main_0_i_9 BitVec[32]))
+  :assumption
+(= main_0_i_9 (ite (bvult main_0_i_8 bv13[32]) (bvadd main_0_i_8 bv1[32]) main_0_i_8))
+  :extrafuns ((main_0_tmp_9 BitVec[32]))
+  :assumption
+(= main_0_tmp_9 (ite (bvult main_0_i_9 bv13[32]) bv9[32] main_0_tmp_8))
+  :extrafuns ((arr_val_10 Array[32:32]))
+  :assumption
+(= arr_val_10 (ite (bvult main_0_i_9 bv13[32]) (store arr_val_9 main_0_tmp_9 main_0_i_9) arr_val_9))
+  :extrafuns ((arr_next_18 Array[32:32]))
+  :assumption
+(= arr_next_18 (ite (bvult main_0_i_9 bv13[32]) (store arr_next_17 main_0_curr_9 main_0_tmp_9) arr_next_17))
+  :extrafuns ((main_0_curr_10 BitVec[32]))
+  :assumption
+(= main_0_curr_10 (ite (bvult main_0_i_9 bv13[32]) (select arr_next_18 main_0_curr_9) main_0_curr_9))
+  :extrafuns ((arr_next_19 Array[32:32]))
+  :assumption
+(= arr_next_19 (ite (bvult main_0_i_9 bv13[32]) (store arr_next_18 main_0_tmp_9 (bvneg bv1[32])) arr_next_18))
+  :extrafuns ((main_0_temp_i_9 BitVec[32]))
+  :assumption
+(= main_0_temp_i_9 (ite (bvult main_0_i_9 bv13[32]) main_0_i_9 main_0_temp_i_8))
+  :extrafuns ((main_0_i_10 BitVec[32]))
+  :assumption
+(= main_0_i_10 (ite (bvult main_0_i_9 bv13[32]) (bvadd main_0_i_9 bv1[32]) main_0_i_9))
+  :extrafuns ((main_0_tmp_10 BitVec[32]))
+  :assumption
+(= main_0_tmp_10 (ite (bvult main_0_i_10 bv13[32]) bv10[32] main_0_tmp_9))
+  :extrafuns ((arr_val_11 Array[32:32]))
+  :assumption
+(= arr_val_11 (ite (bvult main_0_i_10 bv13[32]) (store arr_val_10 main_0_tmp_10 main_0_i_10) arr_val_10))
+  :extrafuns ((arr_next_20 Array[32:32]))
+  :assumption
+(= arr_next_20 (ite (bvult main_0_i_10 bv13[32]) (store arr_next_19 main_0_curr_10 main_0_tmp_10) arr_next_19))
+  :extrafuns ((main_0_curr_11 BitVec[32]))
+  :assumption
+(= main_0_curr_11 (ite (bvult main_0_i_10 bv13[32]) (select arr_next_20 main_0_curr_10) main_0_curr_10))
+  :extrafuns ((arr_next_21 Array[32:32]))
+  :assumption
+(= arr_next_21 (ite (bvult main_0_i_10 bv13[32]) (store arr_next_20 main_0_tmp_10 (bvneg bv1[32])) arr_next_20))
+  :extrafuns ((main_0_temp_i_10 BitVec[32]))
+  :assumption
+(= main_0_temp_i_10 (ite (bvult main_0_i_10 bv13[32]) main_0_i_10 main_0_temp_i_9))
+  :extrafuns ((main_0_i_11 BitVec[32]))
+  :assumption
+(= main_0_i_11 (ite (bvult main_0_i_10 bv13[32]) (bvadd main_0_i_10 bv1[32]) main_0_i_10))
+  :extrafuns ((main_0_tmp_11 BitVec[32]))
+  :assumption
+(= main_0_tmp_11 (ite (bvult main_0_i_11 bv13[32]) bv11[32] main_0_tmp_10))
+  :extrafuns ((arr_val_12 Array[32:32]))
+  :assumption
+(= arr_val_12 (ite (bvult main_0_i_11 bv13[32]) (store arr_val_11 main_0_tmp_11 main_0_i_11) arr_val_11))
+  :extrafuns ((arr_next_22 Array[32:32]))
+  :assumption
+(= arr_next_22 (ite (bvult main_0_i_11 bv13[32]) (store arr_next_21 main_0_curr_11 main_0_tmp_11) arr_next_21))
+  :extrafuns ((main_0_curr_12 BitVec[32]))
+  :assumption
+(= main_0_curr_12 (ite (bvult main_0_i_11 bv13[32]) (select arr_next_22 main_0_curr_11) main_0_curr_11))
+  :extrafuns ((arr_next_23 Array[32:32]))
+  :assumption
+(= arr_next_23 (ite (bvult main_0_i_11 bv13[32]) (store arr_next_22 main_0_tmp_11 (bvneg bv1[32])) arr_next_22))
+  :extrafuns ((main_0_temp_i_11 BitVec[32]))
+  :assumption
+(= main_0_temp_i_11 (ite (bvult main_0_i_11 bv13[32]) main_0_i_11 main_0_temp_i_10))
+  :extrafuns ((main_0_i_12 BitVec[32]))
+  :assumption
+(= main_0_i_12 (ite (bvult main_0_i_11 bv13[32]) (bvadd main_0_i_11 bv1[32]) main_0_i_11))
+  :extrafuns ((main_0_tmp_12 BitVec[32]))
+  :assumption
+(= main_0_tmp_12 (ite (bvult main_0_i_12 bv13[32]) bv12[32] main_0_tmp_11))
+  :extrafuns ((arr_val_13 Array[32:32]))
+  :assumption
+(= arr_val_13 (ite (bvult main_0_i_12 bv13[32]) (store arr_val_12 main_0_tmp_12 main_0_i_12) arr_val_12))
+  :extrafuns ((arr_next_24 Array[32:32]))
+  :assumption
+(= arr_next_24 (ite (bvult main_0_i_12 bv13[32]) (store arr_next_23 main_0_curr_12 main_0_tmp_12) arr_next_23))
+  :extrafuns ((main_0_curr_13 BitVec[32]))
+  :assumption
+(= main_0_curr_13 (ite (bvult main_0_i_12 bv13[32]) (select arr_next_24 main_0_curr_12) main_0_curr_12))
+  :extrafuns ((arr_next_25 Array[32:32]))
+  :assumption
+(= arr_next_25 (ite (bvult main_0_i_12 bv13[32]) (store arr_next_24 main_0_tmp_12 (bvneg bv1[32])) arr_next_24))
+  :extrafuns ((main_0_temp_i_12 BitVec[32]))
+  :assumption
+(= main_0_temp_i_12 (ite (bvult main_0_i_12 bv13[32]) main_0_i_12 main_0_temp_i_11))
+  :extrafuns ((main_0_i_13 BitVec[32]))
+  :assumption
+(= main_0_i_13 (ite (bvult main_0_i_12 bv13[32]) (bvadd main_0_i_12 bv1[32]) main_0_i_12))
+  :extrafuns ((main_0_tmp_13 BitVec[32]))
+  :assumption
+(= main_0_tmp_13 (ite (bvult main_0_i_13 bv13[32]) bv13[32] main_0_tmp_12))
+  :extrafuns ((arr_val_14 Array[32:32]))
+  :assumption
+(= arr_val_14 (ite (bvult main_0_i_13 bv13[32]) (store arr_val_13 main_0_tmp_13 main_0_i_13) arr_val_13))
+  :extrafuns ((arr_next_26 Array[32:32]))
+  :assumption
+(= arr_next_26 (ite (bvult main_0_i_13 bv13[32]) (store arr_next_25 main_0_curr_13 main_0_tmp_13) arr_next_25))
+  :extrafuns ((main_0_curr_14 BitVec[32]))
+  :assumption
+(= main_0_curr_14 (ite (bvult main_0_i_13 bv13[32]) (select arr_next_26 main_0_curr_13) main_0_curr_13))
+  :extrafuns ((arr_next_27 Array[32:32]))
+  :assumption
+(= arr_next_27 (ite (bvult main_0_i_13 bv13[32]) (store arr_next_26 main_0_tmp_13 (bvneg bv1[32])) arr_next_26))
+  :extrafuns ((main_0_temp_i_13 BitVec[32]))
+  :assumption
+(= main_0_temp_i_13 (ite (bvult main_0_i_13 bv13[32]) main_0_i_13 main_0_temp_i_12))
+  :extrafuns ((main_0_i_14 BitVec[32]))
+  :assumption
+(= main_0_i_14 (ite (bvult main_0_i_13 bv13[32]) (bvadd main_0_i_13 bv1[32]) main_0_i_13))
+  :extrafuns ((main_0_tmp_14 BitVec[32]))
+  :assumption
+(= main_0_tmp_14 (ite (bvult main_0_i_14 bv13[32]) bv14[32] main_0_tmp_13))
+  :extrafuns ((arr_val_15 Array[32:32]))
+  :assumption
+(= arr_val_15 (ite (bvult main_0_i_14 bv13[32]) (store arr_val_14 main_0_tmp_14 main_0_i_14) arr_val_14))
+  :extrafuns ((arr_next_28 Array[32:32]))
+  :assumption
+(= arr_next_28 (ite (bvult main_0_i_14 bv13[32]) (store arr_next_27 main_0_curr_14 main_0_tmp_14) arr_next_27))
+  :extrafuns ((main_0_curr_15 BitVec[32]))
+  :assumption
+(= main_0_curr_15 (ite (bvult main_0_i_14 bv13[32]) (select arr_next_28 main_0_curr_14) main_0_curr_14))
+  :extrafuns ((arr_next_29 Array[32:32]))
+  :assumption
+(= arr_next_29 (ite (bvult main_0_i_14 bv13[32]) (store arr_next_28 main_0_tmp_14 (bvneg bv1[32])) arr_next_28))
+  :extrafuns ((main_0_temp_i_14 BitVec[32]))
+  :assumption
+(= main_0_temp_i_14 (ite (bvult main_0_i_14 bv13[32]) main_0_i_14 main_0_temp_i_13))
+  :extrafuns ((main_0_i_15 BitVec[32]))
+  :assumption
+(= main_0_i_15 (ite (bvult main_0_i_14 bv13[32]) (bvadd main_0_i_14 bv1[32]) main_0_i_14))
+  :extrafuns ((undefInt_1 BitVec[32]))
+  :extrafuns ((delete_0_val_0 BitVec[32]))
+  :extrafuns ((delete_0_val_1 BitVec[32]))
+  :assumption
+(= delete_0_val_1 undefInt_1)
+  :extrafuns ((delete_0_list_0 BitVec[32]))
+  :extrafuns ((delete_0_list_1 BitVec[32]))
+  :assumption
+(= delete_0_list_1 main_0_head_1)
+  :extrafuns ((delete_0_head_0 BitVec[32]))
+  :extrafuns ((delete_0_head_1 BitVec[32]))
+  :assumption
+(= delete_0_head_1 delete_0_list_1)
+  :extrafuns ((delete_0_head_2 BitVec[32]))
+  :assumption
+(let (?cvc_0 (select arr_next_29 delete_0_head_1)) (= delete_0_head_2 (ite (and (= (select arr_val_15 delete_0_head_1) delete_0_val_1) (not (= ?cvc_0 (bvneg bv1[32])))) ?cvc_0 delete_0_head_1)))
+  :extrafuns ((delete_0_head_3 BitVec[32]))
+  :assumption
+(= delete_0_head_3 (ite (and (= (select arr_val_15 delete_0_head_2) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_2) delete_0_head_2))
+  :extrafuns ((delete_0_head_4 BitVec[32]))
+  :assumption
+(= delete_0_head_4 (ite (and (= (select arr_val_15 delete_0_head_3) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_3) delete_0_head_3))
+  :extrafuns ((delete_0_head_5 BitVec[32]))
+  :assumption
+(= delete_0_head_5 (ite (and (= (select arr_val_15 delete_0_head_4) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_4) delete_0_head_4))
+  :extrafuns ((delete_0_head_6 BitVec[32]))
+  :assumption
+(= delete_0_head_6 (ite (and (= (select arr_val_15 delete_0_head_5) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_5) delete_0_head_5))
+  :extrafuns ((delete_0_head_7 BitVec[32]))
+  :assumption
+(= delete_0_head_7 (ite (and (= (select arr_val_15 delete_0_head_6) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_6) delete_0_head_6))
+  :extrafuns ((delete_0_head_8 BitVec[32]))
+  :assumption
+(= delete_0_head_8 (ite (and (= (select arr_val_15 delete_0_head_7) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_7) delete_0_head_7))
+  :extrafuns ((delete_0_head_9 BitVec[32]))
+  :assumption
+(= delete_0_head_9 (ite (and (= (select arr_val_15 delete_0_head_8) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_8) delete_0_head_8))
+  :extrafuns ((delete_0_head_10 BitVec[32]))
+  :assumption
+(= delete_0_head_10 (ite (and (= (select arr_val_15 delete_0_head_9) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_9) delete_0_head_9))
+  :extrafuns ((delete_0_head_11 BitVec[32]))
+  :assumption
+(= delete_0_head_11 (ite (and (= (select arr_val_15 delete_0_head_10) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_10) delete_0_head_10))
+  :extrafuns ((delete_0_head_12 BitVec[32]))
+  :assumption
+(= delete_0_head_12 (ite (and (= (select arr_val_15 delete_0_head_11) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_11) delete_0_head_11))
+  :extrafuns ((delete_0_head_13 BitVec[32]))
+  :assumption
+(= delete_0_head_13 (ite (and (= (select arr_val_15 delete_0_head_12) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_12) delete_0_head_12))
+  :extrafuns ((delete_0_head_14 BitVec[32]))
+  :assumption
+(= delete_0_head_14 (ite (and (= (select arr_val_15 delete_0_head_13) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_13) delete_0_head_13))
+  :extrafuns ((delete_0_head_15 BitVec[32]))
+  :assumption
+(= delete_0_head_15 (ite (and (= (select arr_val_15 delete_0_head_14) delete_0_val_1) (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32])))) (select arr_next_29 delete_0_head_14) delete_0_head_14))
+  :extrafuns ((delete_0_prev_0 BitVec[32]))
+  :extrafuns ((delete_0_prev_1 BitVec[32]))
+  :assumption
+(= delete_0_prev_1 (ite (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32]))) delete_0_head_15 delete_0_prev_0))
+  :extrafuns ((delete_0_curr_0 BitVec[32]))
+  :extrafuns ((delete_0_curr_1 BitVec[32]))
+  :assumption
+(= delete_0_curr_1 (ite (not (= (select arr_next_29 delete_0_head_1) (bvneg bv1[32]))) (select arr_next_29 delete_0_head_15) delete_0_curr_0))
+  :extrafuns ((arr_next_30 Array[32:32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= arr_next_30 (ite (and (and (not (= delete_0_curr_1 ?cvc_0)) (= (select arr_val_15 delete_0_curr_1) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_29 delete_0_prev_1 (select arr_next_29 delete_0_curr_1)) arr_next_29)))
+  :extrafuns ((delete_0_curr_2 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_2 (ite (and (and (not (= delete_0_curr_1 ?cvc_0)) (= (select arr_val_15 delete_0_curr_1) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_30 delete_0_curr_1) delete_0_curr_1)))
+  :extrafuns ((delete_0_prev_2 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_2 (ite (and (and (not (= delete_0_curr_1 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_1) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_2 delete_0_prev_1)))
+  :extrafuns ((delete_0_curr_3 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_3 (ite (and (and (not (= delete_0_curr_1 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_1) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_30 delete_0_curr_2) delete_0_curr_2)))
+  :extrafuns ((arr_next_31 Array[32:32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= arr_next_31 (ite (and (and (not (= delete_0_curr_3 ?cvc_0)) (= (select arr_val_15 delete_0_curr_3) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_30 delete_0_prev_2 (select arr_next_30 delete_0_curr_3)) arr_next_30)))
+  :extrafuns ((delete_0_curr_4 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_4 (ite (and (and (not (= delete_0_curr_3 ?cvc_0)) (= (select arr_val_15 delete_0_curr_3) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_31 delete_0_curr_3) delete_0_curr_3)))
+  :extrafuns ((delete_0_prev_3 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_3 (ite (and (and (not (= delete_0_curr_3 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_3) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_4 delete_0_prev_2)))
+  :extrafuns ((delete_0_curr_5 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_5 (ite (and (and (not (= delete_0_curr_3 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_3) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_31 delete_0_curr_4) delete_0_curr_4)))
+  :extrafuns ((arr_next_32 Array[32:32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= arr_next_32 (ite (and (and (not (= delete_0_curr_5 ?cvc_0)) (= (select arr_val_15 delete_0_curr_5) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_31 delete_0_prev_3 (select arr_next_31 delete_0_curr_5)) arr_next_31)))
+  :extrafuns ((delete_0_curr_6 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_6 (ite (and (and (not (= delete_0_curr_5 ?cvc_0)) (= (select arr_val_15 delete_0_curr_5) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_32 delete_0_curr_5) delete_0_curr_5)))
+  :extrafuns ((delete_0_prev_4 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_4 (ite (and (and (not (= delete_0_curr_5 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_5) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_6 delete_0_prev_3)))
+  :extrafuns ((delete_0_curr_7 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_7 (ite (and (and (not (= delete_0_curr_5 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_5) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_32 delete_0_curr_6) delete_0_curr_6)))
+  :extrafuns ((arr_next_33 Array[32:32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= arr_next_33 (ite (and (and (not (= delete_0_curr_7 ?cvc_0)) (= (select arr_val_15 delete_0_curr_7) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_32 delete_0_prev_4 (select arr_next_32 delete_0_curr_7)) arr_next_32)))
+  :extrafuns ((delete_0_curr_8 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_8 (ite (and (and (not (= delete_0_curr_7 ?cvc_0)) (= (select arr_val_15 delete_0_curr_7) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_33 delete_0_curr_7) delete_0_curr_7)))
+  :extrafuns ((delete_0_prev_5 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_5 (ite (and (and (not (= delete_0_curr_7 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_7) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_8 delete_0_prev_4)))
+  :extrafuns ((delete_0_curr_9 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_9 (ite (and (and (not (= delete_0_curr_7 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_7) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_33 delete_0_curr_8) delete_0_curr_8)))
+  :extrafuns ((arr_next_34 Array[32:32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= arr_next_34 (ite (and (and (not (= delete_0_curr_9 ?cvc_0)) (= (select arr_val_15 delete_0_curr_9) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_33 delete_0_prev_5 (select arr_next_33 delete_0_curr_9)) arr_next_33)))
+  :extrafuns ((delete_0_curr_10 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_10 (ite (and (and (not (= delete_0_curr_9 ?cvc_0)) (= (select arr_val_15 delete_0_curr_9) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_34 delete_0_curr_9) delete_0_curr_9)))
+  :extrafuns ((delete_0_prev_6 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_6 (ite (and (and (not (= delete_0_curr_9 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_9) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_10 delete_0_prev_5)))
+  :extrafuns ((delete_0_curr_11 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_11 (ite (and (and (not (= delete_0_curr_9 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_9) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_34 delete_0_curr_10) delete_0_curr_10)))
+  :extrafuns ((arr_next_35 Array[32:32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= arr_next_35 (ite (and (and (not (= delete_0_curr_11 ?cvc_0)) (= (select arr_val_15 delete_0_curr_11) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_34 delete_0_prev_6 (select arr_next_34 delete_0_curr_11)) arr_next_34)))
+  :extrafuns ((delete_0_curr_12 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_12 (ite (and (and (not (= delete_0_curr_11 ?cvc_0)) (= (select arr_val_15 delete_0_curr_11) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_35 delete_0_curr_11) delete_0_curr_11)))
+  :extrafuns ((delete_0_prev_7 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_7 (ite (and (and (not (= delete_0_curr_11 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_11) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_12 delete_0_prev_6)))
+  :extrafuns ((delete_0_curr_13 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_13 (ite (and (and (not (= delete_0_curr_11 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_11) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_35 delete_0_curr_12) delete_0_curr_12)))
+  :extrafuns ((arr_next_36 Array[32:32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= arr_next_36 (ite (and (and (not (= delete_0_curr_13 ?cvc_0)) (= (select arr_val_15 delete_0_curr_13) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_35 delete_0_prev_7 (select arr_next_35 delete_0_curr_13)) arr_next_35)))
+  :extrafuns ((delete_0_curr_14 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_14 (ite (and (and (not (= delete_0_curr_13 ?cvc_0)) (= (select arr_val_15 delete_0_curr_13) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_36 delete_0_curr_13) delete_0_curr_13)))
+  :extrafuns ((delete_0_prev_8 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_8 (ite (and (and (not (= delete_0_curr_13 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_13) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_14 delete_0_prev_7)))
+  :extrafuns ((delete_0_curr_15 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_15 (ite (and (and (not (= delete_0_curr_13 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_13) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_36 delete_0_curr_14) delete_0_curr_14)))
+  :extrafuns ((arr_next_37 Array[32:32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= arr_next_37 (ite (and (and (not (= delete_0_curr_15 ?cvc_0)) (= (select arr_val_15 delete_0_curr_15) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_36 delete_0_prev_8 (select arr_next_36 delete_0_curr_15)) arr_next_36)))
+  :extrafuns ((delete_0_curr_16 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_16 (ite (and (and (not (= delete_0_curr_15 ?cvc_0)) (= (select arr_val_15 delete_0_curr_15) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_37 delete_0_curr_15) delete_0_curr_15)))
+  :extrafuns ((delete_0_prev_9 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_9 (ite (and (and (not (= delete_0_curr_15 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_15) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_16 delete_0_prev_8)))
+  :extrafuns ((delete_0_curr_17 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_17 (ite (and (and (not (= delete_0_curr_15 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_15) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_37 delete_0_curr_16) delete_0_curr_16)))
+  :extrafuns ((arr_next_38 Array[32:32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= arr_next_38 (ite (and (and (not (= delete_0_curr_17 ?cvc_0)) (= (select arr_val_15 delete_0_curr_17) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_37 delete_0_prev_9 (select arr_next_37 delete_0_curr_17)) arr_next_37)))
+  :extrafuns ((delete_0_curr_18 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_18 (ite (and (and (not (= delete_0_curr_17 ?cvc_0)) (= (select arr_val_15 delete_0_curr_17) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_38 delete_0_curr_17) delete_0_curr_17)))
+  :extrafuns ((delete_0_prev_10 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_10 (ite (and (and (not (= delete_0_curr_17 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_17) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_18 delete_0_prev_9)))
+  :extrafuns ((delete_0_curr_19 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_19 (ite (and (and (not (= delete_0_curr_17 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_17) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_38 delete_0_curr_18) delete_0_curr_18)))
+  :extrafuns ((arr_next_39 Array[32:32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= arr_next_39 (ite (and (and (not (= delete_0_curr_19 ?cvc_0)) (= (select arr_val_15 delete_0_curr_19) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_38 delete_0_prev_10 (select arr_next_38 delete_0_curr_19)) arr_next_38)))
+  :extrafuns ((delete_0_curr_20 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_20 (ite (and (and (not (= delete_0_curr_19 ?cvc_0)) (= (select arr_val_15 delete_0_curr_19) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_39 delete_0_curr_19) delete_0_curr_19)))
+  :extrafuns ((delete_0_prev_11 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_11 (ite (and (and (not (= delete_0_curr_19 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_19) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_20 delete_0_prev_10)))
+  :extrafuns ((delete_0_curr_21 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_21 (ite (and (and (not (= delete_0_curr_19 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_19) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_39 delete_0_curr_20) delete_0_curr_20)))
+  :extrafuns ((arr_next_40 Array[32:32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= arr_next_40 (ite (and (and (not (= delete_0_curr_21 ?cvc_0)) (= (select arr_val_15 delete_0_curr_21) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_39 delete_0_prev_11 (select arr_next_39 delete_0_curr_21)) arr_next_39)))
+  :extrafuns ((delete_0_curr_22 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_22 (ite (and (and (not (= delete_0_curr_21 ?cvc_0)) (= (select arr_val_15 delete_0_curr_21) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_40 delete_0_curr_21) delete_0_curr_21)))
+  :extrafuns ((delete_0_prev_12 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_12 (ite (and (and (not (= delete_0_curr_21 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_21) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_22 delete_0_prev_11)))
+  :extrafuns ((delete_0_curr_23 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_23 (ite (and (and (not (= delete_0_curr_21 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_21) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_40 delete_0_curr_22) delete_0_curr_22)))
+  :extrafuns ((arr_next_41 Array[32:32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= arr_next_41 (ite (and (and (not (= delete_0_curr_23 ?cvc_0)) (= (select arr_val_15 delete_0_curr_23) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_40 delete_0_prev_12 (select arr_next_40 delete_0_curr_23)) arr_next_40)))
+  :extrafuns ((delete_0_curr_24 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_24 (ite (and (and (not (= delete_0_curr_23 ?cvc_0)) (= (select arr_val_15 delete_0_curr_23) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_41 delete_0_curr_23) delete_0_curr_23)))
+  :extrafuns ((delete_0_prev_13 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_13 (ite (and (and (not (= delete_0_curr_23 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_23) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_24 delete_0_prev_12)))
+  :extrafuns ((delete_0_curr_25 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_25 (ite (and (and (not (= delete_0_curr_23 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_23) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_41 delete_0_curr_24) delete_0_curr_24)))
+  :extrafuns ((arr_next_42 Array[32:32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= arr_next_42 (ite (and (and (not (= delete_0_curr_25 ?cvc_0)) (= (select arr_val_15 delete_0_curr_25) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_41 delete_0_prev_13 (select arr_next_41 delete_0_curr_25)) arr_next_41)))
+  :extrafuns ((delete_0_curr_26 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_26 (ite (and (and (not (= delete_0_curr_25 ?cvc_0)) (= (select arr_val_15 delete_0_curr_25) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_42 delete_0_curr_25) delete_0_curr_25)))
+  :extrafuns ((delete_0_prev_14 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_14 (ite (and (and (not (= delete_0_curr_25 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_25) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_26 delete_0_prev_13)))
+  :extrafuns ((delete_0_curr_27 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_27 (ite (and (and (not (= delete_0_curr_25 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_25) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_42 delete_0_curr_26) delete_0_curr_26)))
+  :extrafuns ((arr_next_43 Array[32:32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= arr_next_43 (ite (and (and (not (= delete_0_curr_27 ?cvc_0)) (= (select arr_val_15 delete_0_curr_27) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (store arr_next_42 delete_0_prev_14 (select arr_next_42 delete_0_curr_27)) arr_next_42)))
+  :extrafuns ((delete_0_curr_28 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_28 (ite (and (and (not (= delete_0_curr_27 ?cvc_0)) (= (select arr_val_15 delete_0_curr_27) delete_0_val_1)) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_43 delete_0_curr_27) delete_0_curr_27)))
+  :extrafuns ((delete_0_prev_15 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_prev_15 (ite (and (and (not (= delete_0_curr_27 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_27) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) delete_0_curr_28 delete_0_prev_14)))
+  :extrafuns ((delete_0_curr_29 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= delete_0_curr_29 (ite (and (and (not (= delete_0_curr_27 ?cvc_0)) (not (= (select arr_val_15 delete_0_curr_27) delete_0_val_1))) (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (select arr_next_43 delete_0_curr_28) delete_0_curr_28)))
+  :extrafuns ((delete_return_0 BitVec[32]))
+  :extrafuns ((delete_return_1 BitVec[32]))
+  :assumption
+(= delete_return_1 delete_0_head_15)
+  :extrafuns ((main_0_head_2 BitVec[32]))
+  :assumption
+(= main_0_head_2 delete_return_1)
+  :extrafuns ((main_0_x_0 BitVec[32]))
+  :extrafuns ((member_0_val_0 BitVec[32]))
+  :extrafuns ((member_0_val_1 BitVec[32]))
+  :assumption
+(= member_0_val_1 bv0[32])
+  :extrafuns ((member_0_head_0 BitVec[32]))
+  :extrafuns ((member_0_head_1 BitVec[32]))
+  :assumption
+(= member_0_head_1 main_0_head_2)
+  :extrafuns ((member_0_curr_0 BitVec[32]))
+  :extrafuns ((member_0_curr_1 BitVec[32]))
+  :assumption
+(= member_0_curr_1 member_0_head_1)
+  :extrafuns ((member_0_result_0 BitVec[32]))
+  :extrafuns ((member_0_result_1 BitVec[32]))
+  :assumption
+(= member_0_result_1 (ite (and (not (= member_0_curr_1 (bvneg bv1[32]))) (= (select arr_val_15 member_0_curr_1) member_0_val_1)) bv1[32] member_0_result_0))
+  :extrafuns ((member_0_curr_2 BitVec[32]))
+  :assumption
+(flet ($cvc_0 (not (= member_0_curr_1 (bvneg bv1[32])))) (= member_0_curr_2 (ite (and (not (and $cvc_0 (= (select arr_val_15 member_0_curr_1) member_0_val_1))) $cvc_0) (select arr_next_43 member_0_curr_1) member_0_curr_1)))
+  :extrafuns ((member_0_result_2 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_2 (ite (and (and (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1))) (not (= member_0_curr_2 ?cvc_0))) (= (select arr_val_15 member_0_curr_2) member_0_val_1)) bv1[32] member_0_result_1)))
+  :extrafuns ((member_0_curr_3 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_2 ?cvc_0))) (= member_0_curr_3 (ite (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_2) member_0_val_1))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_2) member_0_curr_2))))
+  :extrafuns ((member_0_result_3 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_3 (ite (and (and (and (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_3 ?cvc_0))) (= (select arr_val_15 member_0_curr_3) member_0_val_1)) bv1[32] member_0_result_2)))
+  :extrafuns ((member_0_curr_4 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_3 ?cvc_0))) (= member_0_curr_4 (ite (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_3) member_0_val_1))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_3) member_0_curr_3))))
+  :extrafuns ((member_0_result_4 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_4 (ite (and (and (and (and (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_4 ?cvc_0))) (= (select arr_val_15 member_0_curr_4) member_0_val_1)) bv1[32] member_0_result_3)))
+  :extrafuns ((member_0_curr_5 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_4 ?cvc_0))) (= member_0_curr_5 (ite (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_4) member_0_val_1))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_4) member_0_curr_4))))
+  :extrafuns ((member_0_result_5 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_5 (ite (and (and (and (and (and (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_5 ?cvc_0))) (= (select arr_val_15 member_0_curr_5) member_0_val_1)) bv1[32] member_0_result_4)))
+  :extrafuns ((member_0_curr_6 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_5 ?cvc_0))) (= member_0_curr_6 (ite (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_5) member_0_val_1))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_5) member_0_curr_5))))
+  :extrafuns ((member_0_result_6 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_6 (ite (and (and (and (and (and (and (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_6 ?cvc_0))) (= (select arr_val_15 member_0_curr_6) member_0_val_1)) bv1[32] member_0_result_5)))
+  :extrafuns ((member_0_curr_7 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_6 ?cvc_0))) (= member_0_curr_7 (ite (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_6) member_0_val_1))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_6) member_0_curr_6))))
+  :extrafuns ((member_0_result_7 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_7 (ite (and (and (and (and (and (and (and (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_7 ?cvc_0))) (= (select arr_val_15 member_0_curr_7) member_0_val_1)) bv1[32] member_0_result_6)))
+  :extrafuns ((member_0_curr_8 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_7 ?cvc_0))) (= member_0_curr_8 (ite (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_7) member_0_val_1))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_7) member_0_curr_7))))
+  :extrafuns ((member_0_result_8 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_8 (ite (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_8 ?cvc_0))) (= (select arr_val_15 member_0_curr_8) member_0_val_1)) bv1[32] member_0_result_7)))
+  :extrafuns ((member_0_curr_9 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_8 ?cvc_0))) (= member_0_curr_9 (ite (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_8) member_0_val_1))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_8) member_0_curr_8))))
+  :extrafuns ((member_0_result_9 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_9 (ite (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_9 ?cvc_0))) (= (select arr_val_15 member_0_curr_9) member_0_val_1)) bv1[32] member_0_result_8)))
+  :extrafuns ((member_0_curr_10 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_9 ?cvc_0))) (= member_0_curr_10 (ite (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_9) member_0_val_1))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_9) member_0_curr_9))))
+  :extrafuns ((member_0_result_10 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_10 (ite (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_10 ?cvc_0))) (= (select arr_val_15 member_0_curr_10) member_0_val_1)) bv1[32] member_0_result_9)))
+  :extrafuns ((member_0_curr_11 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_10 ?cvc_0))) (= member_0_curr_11 (ite (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_10) member_0_val_1))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_10) member_0_curr_10))))
+  :extrafuns ((member_0_result_11 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_11 (ite (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_11 ?cvc_0))) (= (select arr_val_15 member_0_curr_11) member_0_val_1)) bv1[32] member_0_result_10)))
+  :extrafuns ((member_0_curr_12 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_11 ?cvc_0))) (= member_0_curr_12 (ite (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_11) member_0_val_1))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_11) member_0_curr_11))))
+  :extrafuns ((member_0_result_12 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_12 (ite (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_12 ?cvc_0))) (= (select arr_val_15 member_0_curr_12) member_0_val_1)) bv1[32] member_0_result_11)))
+  :extrafuns ((member_0_curr_13 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_12 ?cvc_0))) (= member_0_curr_13 (ite (and (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_12) member_0_val_1))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_12) member_0_curr_12))))
+  :extrafuns ((member_0_result_13 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_13 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_13 ?cvc_0))) (= (select arr_val_15 member_0_curr_13) member_0_val_1)) bv1[32] member_0_result_12)))
+  :extrafuns ((member_0_curr_14 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_13 ?cvc_0))) (= member_0_curr_14 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_13) member_0_val_1))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_13) member_0_curr_13))))
+  :extrafuns ((member_0_result_14 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_14 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_13 ?cvc_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) (not (= member_0_curr_14 ?cvc_0))) (= (select arr_val_15 member_0_curr_14) member_0_val_1)) bv1[32] member_0_result_13)))
+  :extrafuns ((member_0_curr_15 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= member_0_curr_14 ?cvc_0))) (= member_0_curr_15 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_1 (= (select arr_val_15 member_0_curr_14) member_0_val_1))) (not (and (not (= member_0_curr_13 ?cvc_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1)))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_1) (select arr_next_43 member_0_curr_14) member_0_curr_14))))
+  :extrafuns ((member_0_result_15 BitVec[32]))
+  :assumption
+(let (?cvc_0 (bvneg bv1[32])) (= member_0_result_15 (ite (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and (not (= member_0_curr_14 ?cvc_0)) (= (select arr_val_15 member_0_curr_14) member_0_val_1))) (not (and (not (= member_0_curr_13 ?cvc_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1)))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) bv0[32] member_0_result_14)))
+  :extrafuns ((main_0_x_1 BitVec[32]))
+  :assumption
+(= main_0_x_1 member_0_result_15)
+  :formula
+(let (?cvc_0 (bvneg bv1[32])) (flet ($cvc_1 (not (= (select arr_next_29 delete_0_head_1) ?cvc_0))) (flet ($cvc_2 (not (= member_0_curr_14 ?cvc_0))) (not (and (and (and (and (implies (bvult main_0_i_14 bv13[32]) (not (bvult main_0_i_15 bv13[32]))) (implies (and (= (select arr_val_15 delete_0_head_14) delete_0_val_1) $cvc_1) (not (= (select arr_val_15 delete_0_head_15) delete_0_val_1)))) (implies (and (not (= delete_0_curr_27 ?cvc_0)) $cvc_1) (not (not (= delete_0_curr_29 ?cvc_0))))) (implies (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (and $cvc_2 (= (select arr_val_15 member_0_curr_14) member_0_val_1))) (not (and (not (= member_0_curr_13 ?cvc_0)) (= (select arr_val_15 member_0_curr_13) member_0_val_1)))) (not (and (not (= member_0_curr_12 ?cvc_0)) (= (select arr_val_15 member_0_curr_12) member_0_val_1)))) (not (and (not (= member_0_curr_11 ?cvc_0)) (= (select arr_val_15 member_0_curr_11) member_0_val_1)))) (not (and (not (= member_0_curr_10 ?cvc_0)) (= (select arr_val_15 member_0_curr_10) member_0_val_1)))) (not (and (not (= member_0_curr_9 ?cvc_0)) (= (select arr_val_15 member_0_curr_9) member_0_val_1)))) (not (and (not (= member_0_curr_8 ?cvc_0)) (= (select arr_val_15 member_0_curr_8) member_0_val_1)))) (not (and (not (= member_0_curr_7 ?cvc_0)) (= (select arr_val_15 member_0_curr_7) member_0_val_1)))) (not (and (not (= member_0_curr_6 ?cvc_0)) (= (select arr_val_15 member_0_curr_6) member_0_val_1)))) (not (and (not (= member_0_curr_5 ?cvc_0)) (= (select arr_val_15 member_0_curr_5) member_0_val_1)))) (not (and (not (= member_0_curr_4 ?cvc_0)) (= (select arr_val_15 member_0_curr_4) member_0_val_1)))) (not (and (not (= member_0_curr_3 ?cvc_0)) (= (select arr_val_15 member_0_curr_3) member_0_val_1)))) (not (and (not (= member_0_curr_2 ?cvc_0)) (= (select arr_val_15 member_0_curr_2) member_0_val_1)))) (not (and (not (= member_0_curr_1 ?cvc_0)) (= (select arr_val_15 member_0_curr_1) member_0_val_1)))) $cvc_2) (not (not (= member_0_curr_15 ?cvc_0))))) (= main_0_x_1 bv0[32]))))))
+)
diff --git a/test/regress/regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt b/test/regress/regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt
new file mode 100644
index 000000000..028427acc
--- /dev/null
+++ b/test/regress/regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt
@@ -0,0 +1,28 @@
+(benchmark B_
+:logic QF_AUFBV
+:extrafuns ((R_ESP_1_58 BitVec[32]))
+:extrafuns ((mem_35_197 Array[32:8]))
+:status sat
+:formula
+(let (?n1 bv0[32])
+(let (?n2 bv0[24])
+(let (?n3 bv1[32])
+(let (?n4 (bvadd ?n3 R_ESP_1_58))
+(let (?n5 bv0[8])
+(let (?n6 (store mem_35_197 ?n4 ?n5))
+(let (?n7 (bvadd ?n3 ?n4))
+(let (?n8 (store ?n6 ?n7 ?n5))
+(let (?n9 (store ?n8 ?n1 ?n5))
+(let (?n10 (select ?n6 R_ESP_1_58))
+(let (?n11 (concat ?n2 ?n10))
+(let (?n12 (bvadd ?n3 ?n11))
+(let (?n13 (select ?n9 ?n12))
+(let (?n14 (concat ?n2 ?n13))
+(let (?n15 (bvxor ?n3 ?n14))
+(let (?n16 (extract[7:0] ?n15))
+(let (?n17 (store ?n9 ?n12 ?n16))
+(let (?n18 (select ?n17 ?n1))
+(let (?n19 (concat ?n2 ?n18))
+(flet ($n20 (= ?n1 ?n19))
+$n20
+)))))))))))))))))))))
diff --git a/test/regress/regress0/aufbv/wchains010ue.delta01.smt b/test/regress/regress0/aufbv/wchains010ue.delta01.smt
new file mode 100644
index 000000000..28a892e8d
--- /dev/null
+++ b/test/regress/regress0/aufbv/wchains010ue.delta01.smt
@@ -0,0 +1,36 @@
+(benchmark wchains010ue.smt
+:logic QF_AUFBV
+:extrafuns ((v6 BitVec[32]))
+:extrafuns ((a1 Array[32:8]))
+:extrafuns ((v15 BitVec[32]))
+:status sat
+:formula
+(let (?n1 bv0[1])
+(let (?n2 (extract[1:0] v6))
+(let (?n3 bv0[2])
+(flet ($n4 (= ?n2 ?n3))
+(let (?n5 bv1[1])
+(let (?n6 (ite $n4 ?n5 ?n1))
+(let (?n7 bv0[8])
+(let (?n8 (store a1 v15 ?n7))
+(let (?n9 bv1[32])
+(let (?n10 (bvadd ?n9 v15))
+(let (?n11 (store ?n8 ?n10 ?n7))
+(let (?n12 bv3[32])
+(let (?n13 (bvadd ?n12 v15))
+(let (?n14 (store ?n11 ?n13 ?n7))
+(let (?n15 (extract[7:0] v6))
+(let (?n16 (store a1 v6 ?n15))
+(let (?n17 (bvadd ?n9 v6))
+(let (?n18 bv1[8])
+(let (?n19 (store ?n16 ?n17 ?n18))
+(let (?n20 (bvadd ?n12 v6))
+(let (?n21 (store ?n19 ?n20 ?n18))
+(flet ($n22 (= ?n14 ?n21))
+(let (?n23 (ite $n22 ?n5 ?n1))
+(let (?n24 (bvnot ?n23))
+(let (?n25 (bvand ?n6 ?n24))
+(flet ($n26 (= ?n1 ?n25))
+(flet ($n27 (not $n26))
+$n27
+))))))))))))))))))))))))))))
diff --git a/test/regress/regress0/aufbv/wchains010ue.delta02.smt b/test/regress/regress0/aufbv/wchains010ue.delta02.smt
new file mode 100644
index 000000000..d5ddf6446
--- /dev/null
+++ b/test/regress/regress0/aufbv/wchains010ue.delta02.smt
@@ -0,0 +1,35 @@
+(benchmark wchains010ue.smt
+:logic QF_AUFBV
+:extrafuns ((v6 BitVec[32]))
+:extrafuns ((v7 BitVec[32]))
+:extrafuns ((a1 Array[32:8]))
+:status unsat
+:formula
+(let (?n1 bv0[1])
+(let (?n2 bv0[2])
+(let (?n3 (extract[1:0] v6))
+(flet ($n4 (= ?n2 ?n3))
+(let (?n5 bv1[1])
+(let (?n6 (ite $n4 ?n5 ?n1))
+(let (?n7 (extract[23:16] v6))
+(let (?n8 (store a1 v6 ?n7))
+(let (?n9 bv0[32])
+(let (?n10 bv0[8])
+(let (?n11 (store ?n8 ?n9 ?n10))
+(let (?n12 (extract[23:16] v7))
+(let (?n13 (store ?n11 v7 ?n12))
+(let (?n14 bv1[32])
+(let (?n15 (store ?n13 ?n14 ?n10))
+(let (?n16 (store ?n15 ?n9 ?n10))
+(let (?n17 (store a1 ?n9 ?n10))
+(let (?n18 (store ?n17 v7 ?n12))
+(let (?n19 (store ?n18 ?n14 ?n10))
+(let (?n20 (store ?n19 v6 ?n7))
+(flet ($n21 (= ?n16 ?n20))
+(let (?n22 (ite $n21 ?n5 ?n1))
+(let (?n23 (bvnot ?n22))
+(let (?n24 (bvand ?n6 ?n23))
+(flet ($n25 (= ?n1 ?n24))
+(flet ($n26 (not $n25))
+$n26
+)))))))))))))))))))))))))))
diff --git a/test/regress/regress0/aufbv/wchains010ue.smt b/test/regress/regress0/aufbv/wchains010ue.smt
new file mode 100644
index 000000000..a4d0f1ddb
--- /dev/null
+++ b/test/regress/regress0/aufbv/wchains010ue.smt
@@ -0,0 +1,221 @@
+(benchmark wchains010ue.smt
+:source {
+This benchmark generates write chain permutations and tries to show
+via extensionality that they are equal.
+
+Contributed by Armin Biere (armin.biere@jku.at).
+}
+:status unsat
+:category { crafted }
+:logic QF_AUFBV
+:difficulty { 2 }
+:extrafuns ((a1 Array[32:8]))
+:extrafuns ((v6 BitVec[32]))
+:extrafuns ((v7 BitVec[32]))
+:extrafuns ((v8 BitVec[32]))
+:extrafuns ((v9 BitVec[32]))
+:extrafuns ((v10 BitVec[32]))
+:extrafuns ((v11 BitVec[32]))
+:extrafuns ((v12 BitVec[32]))
+:extrafuns ((v13 BitVec[32]))
+:extrafuns ((v14 BitVec[32]))
+:extrafuns ((v15 BitVec[32]))
+:formula
+(let (?e2 bv0[32])
+(let (?e3 bv1[32])
+(let (?e4 bv2[32])
+(let (?e5 bv3[32])
+(let (?e16 (bvadd ?e2 v6))
+(let (?e17 (extract[7:0] v6))
+(let (?e18 (store a1 ?e16 ?e17))
+(let (?e19 (bvadd ?e3 v6))
+(let (?e20 (extract[15:8] v6))
+(let (?e21 (store ?e18 ?e19 ?e20))
+(let (?e22 (bvadd ?e4 v6))
+(let (?e23 (extract[23:16] v6))
+(let (?e24 (store ?e21 ?e22 ?e23))
+(let (?e25 (bvadd ?e5 v6))
+(let (?e26 (extract[31:24] v6))
+(let (?e27 (store ?e24 ?e25 ?e26))
+(let (?e28 (bvadd ?e2 v7))
+(let (?e29 (extract[7:0] v7))
+(let (?e30 (store ?e27 ?e28 ?e29))
+(let (?e31 (bvadd ?e3 v7))
+(let (?e32 (extract[15:8] v7))
+(let (?e33 (store ?e30 ?e31 ?e32))
+(let (?e34 (bvadd ?e4 v7))
+(let (?e35 (extract[23:16] v7))
+(let (?e36 (store ?e33 ?e34 ?e35))
+(let (?e37 (bvadd ?e5 v7))
+(let (?e38 (extract[31:24] v7))
+(let (?e39 (store ?e36 ?e37 ?e38))
+(let (?e40 (bvadd ?e2 v8))
+(let (?e41 (extract[7:0] v8))
+(let (?e42 (store ?e39 ?e40 ?e41))
+(let (?e43 (bvadd ?e3 v8))
+(let (?e44 (extract[15:8] v8))
+(let (?e45 (store ?e42 ?e43 ?e44))
+(let (?e46 (bvadd ?e4 v8))
+(let (?e47 (extract[23:16] v8))
+(let (?e48 (store ?e45 ?e46 ?e47))
+(let (?e49 (bvadd ?e5 v8))
+(let (?e50 (extract[31:24] v8))
+(let (?e51 (store ?e48 ?e49 ?e50))
+(let (?e52 (bvadd ?e2 v9))
+(let (?e53 (extract[7:0] v9))
+(let (?e54 (store ?e51 ?e52 ?e53))
+(let (?e55 (bvadd ?e3 v9))
+(let (?e56 (extract[15:8] v9))
+(let (?e57 (store ?e54 ?e55 ?e56))
+(let (?e58 (bvadd ?e4 v9))
+(let (?e59 (extract[23:16] v9))
+(let (?e60 (store ?e57 ?e58 ?e59))
+(let (?e61 (bvadd ?e5 v9))
+(let (?e62 (extract[31:24] v9))
+(let (?e63 (store ?e60 ?e61 ?e62))
+(let (?e64 (bvadd ?e2 v10))
+(let (?e65 (extract[7:0] v10))
+(let (?e66 (store ?e63 ?e64 ?e65))
+(let (?e67 (bvadd ?e3 v10))
+(let (?e68 (extract[15:8] v10))
+(let (?e69 (store ?e66 ?e67 ?e68))
+(let (?e70 (bvadd ?e4 v10))
+(let (?e71 (extract[23:16] v10))
+(let (?e72 (store ?e69 ?e70 ?e71))
+(let (?e73 (bvadd ?e5 v10))
+(let (?e74 (extract[31:24] v10))
+(let (?e75 (store ?e72 ?e73 ?e74))
+(let (?e76 (bvadd ?e2 v11))
+(let (?e77 (extract[7:0] v11))
+(let (?e78 (store ?e75 ?e76 ?e77))
+(let (?e79 (bvadd ?e3 v11))
+(let (?e80 (extract[15:8] v11))
+(let (?e81 (store ?e78 ?e79 ?e80))
+(let (?e82 (bvadd ?e4 v11))
+(let (?e83 (extract[23:16] v11))
+(let (?e84 (store ?e81 ?e82 ?e83))
+(let (?e85 (bvadd ?e5 v11))
+(let (?e86 (extract[31:24] v11))
+(let (?e87 (store ?e84 ?e85 ?e86))
+(let (?e88 (bvadd ?e2 v12))
+(let (?e89 (extract[7:0] v12))
+(let (?e90 (store ?e87 ?e88 ?e89))
+(let (?e91 (bvadd ?e3 v12))
+(let (?e92 (extract[15:8] v12))
+(let (?e93 (store ?e90 ?e91 ?e92))
+(let (?e94 (bvadd ?e4 v12))
+(let (?e95 (extract[23:16] v12))
+(let (?e96 (store ?e93 ?e94 ?e95))
+(let (?e97 (bvadd ?e5 v12))
+(let (?e98 (extract[31:24] v12))
+(let (?e99 (store ?e96 ?e97 ?e98))
+(let (?e100 (bvadd ?e2 v13))
+(let (?e101 (extract[7:0] v13))
+(let (?e102 (store ?e99 ?e100 ?e101))
+(let (?e103 (bvadd ?e3 v13))
+(let (?e104 (extract[15:8] v13))
+(let (?e105 (store ?e102 ?e103 ?e104))
+(let (?e106 (bvadd ?e4 v13))
+(let (?e107 (extract[23:16] v13))
+(let (?e108 (store ?e105 ?e106 ?e107))
+(let (?e109 (bvadd ?e5 v13))
+(let (?e110 (extract[31:24] v13))
+(let (?e111 (store ?e108 ?e109 ?e110))
+(let (?e112 (bvadd ?e2 v14))
+(let (?e113 (extract[7:0] v14))
+(let (?e114 (store ?e111 ?e112 ?e113))
+(let (?e115 (bvadd ?e3 v14))
+(let (?e116 (extract[15:8] v14))
+(let (?e117 (store ?e114 ?e115 ?e116))
+(let (?e118 (bvadd ?e4 v14))
+(let (?e119 (extract[23:16] v14))
+(let (?e120 (store ?e117 ?e118 ?e119))
+(let (?e121 (bvadd ?e5 v14))
+(let (?e122 (extract[31:24] v14))
+(let (?e123 (store ?e120 ?e121 ?e122))
+(let (?e124 (bvadd ?e2 v15))
+(let (?e125 (extract[7:0] v15))
+(let (?e126 (store ?e123 ?e124 ?e125))
+(let (?e127 (bvadd ?e3 v15))
+(let (?e128 (extract[15:8] v15))
+(let (?e129 (store ?e126 ?e127 ?e128))
+(let (?e130 (bvadd ?e4 v15))
+(let (?e131 (extract[23:16] v15))
+(let (?e132 (store ?e129 ?e130 ?e131))
+(let (?e133 (bvadd ?e5 v15))
+(let (?e134 (extract[31:24] v15))
+(let (?e135 (store ?e132 ?e133 ?e134))
+(let (?e136 (store a1 ?e124 ?e125))
+(let (?e137 (store ?e136 ?e127 ?e128))
+(let (?e138 (store ?e137 ?e130 ?e131))
+(let (?e139 (store ?e138 ?e133 ?e134))
+(let (?e140 (store ?e139 ?e112 ?e113))
+(let (?e141 (store ?e140 ?e115 ?e116))
+(let (?e142 (store ?e141 ?e118 ?e119))
+(let (?e143 (store ?e142 ?e121 ?e122))
+(let (?e144 (store ?e143 ?e100 ?e101))
+(let (?e145 (store ?e144 ?e103 ?e104))
+(let (?e146 (store ?e145 ?e106 ?e107))
+(let (?e147 (store ?e146 ?e109 ?e110))
+(let (?e148 (store ?e147 ?e88 ?e89))
+(let (?e149 (store ?e148 ?e91 ?e92))
+(let (?e150 (store ?e149 ?e94 ?e95))
+(let (?e151 (store ?e150 ?e97 ?e98))
+(let (?e152 (store ?e151 ?e76 ?e77))
+(let (?e153 (store ?e152 ?e79 ?e80))
+(let (?e154 (store ?e153 ?e82 ?e83))
+(let (?e155 (store ?e154 ?e85 ?e86))
+(let (?e156 (store ?e155 ?e64 ?e65))
+(let (?e157 (store ?e156 ?e67 ?e68))
+(let (?e158 (store ?e157 ?e70 ?e71))
+(let (?e159 (store ?e158 ?e73 ?e74))
+(let (?e160 (store ?e159 ?e52 ?e53))
+(let (?e161 (store ?e160 ?e55 ?e56))
+(let (?e162 (store ?e161 ?e58 ?e59))
+(let (?e163 (store ?e162 ?e61 ?e62))
+(let (?e164 (store ?e163 ?e40 ?e41))
+(let (?e165 (store ?e164 ?e43 ?e44))
+(let (?e166 (store ?e165 ?e46 ?e47))
+(let (?e167 (store ?e166 ?e49 ?e50))
+(let (?e168 (store ?e167 ?e28 ?e29))
+(let (?e169 (store ?e168 ?e31 ?e32))
+(let (?e170 (store ?e169 ?e34 ?e35))
+(let (?e171 (store ?e170 ?e37 ?e38))
+(let (?e172 (store ?e171 ?e16 ?e17))
+(let (?e173 (store ?e172 ?e19 ?e20))
+(let (?e174 (store ?e173 ?e22 ?e23))
+(let (?e175 (store ?e174 ?e25 ?e26))
+(let (?e176 (ite (= ?e135 ?e175) bv1[1] bv0[1]))
+(let (?e177 (extract[1:0] v6))
+(let (?e178 bv0[2])
+(let (?e179 (ite (= ?e177 ?e178) bv1[1] bv0[1]))
+(let (?e180 (bvand (bvnot ?e176) ?e179))
+(let (?e181 (extract[1:0] v7))
+(let (?e182 (ite (= ?e178 ?e181) bv1[1] bv0[1]))
+(let (?e183 (bvand ?e180 ?e182))
+(let (?e184 (extract[1:0] v8))
+(let (?e185 (ite (= ?e178 ?e184) bv1[1] bv0[1]))
+(let (?e186 (bvand ?e183 ?e185))
+(let (?e187 (extract[1:0] v9))
+(let (?e188 (ite (= ?e178 ?e187) bv1[1] bv0[1]))
+(let (?e189 (bvand ?e186 ?e188))
+(let (?e190 (extract[1:0] v10))
+(let (?e191 (ite (= ?e178 ?e190) bv1[1] bv0[1]))
+(let (?e192 (bvand ?e189 ?e191))
+(let (?e193 (extract[1:0] v11))
+(let (?e194 (ite (= ?e178 ?e193) bv1[1] bv0[1]))
+(let (?e195 (bvand ?e192 ?e194))
+(let (?e196 (extract[1:0] v12))
+(let (?e197 (ite (= ?e178 ?e196) bv1[1] bv0[1]))
+(let (?e198 (bvand ?e195 ?e197))
+(let (?e199 (extract[1:0] v13))
+(let (?e200 (ite (= ?e178 ?e199) bv1[1] bv0[1]))
+(let (?e201 (bvand ?e198 ?e200))
+(let (?e202 (extract[1:0] v14))
+(let (?e203 (ite (= ?e178 ?e202) bv1[1] bv0[1]))
+(let (?e204 (bvand ?e201 ?e203))
+(let (?e205 (extract[1:0] v15))
+(let (?e206 (ite (= ?e178 ?e205) bv1[1] bv0[1]))
+(let (?e207 (bvand ?e204 ?e206))
+(not (= ?e207 bv0[1]))
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am
index 314566f87..f4f5c57b4 100644
--- a/test/regress/regress0/auflia/Makefile.am
+++ b/test/regress/regress0/auflia/Makefile.am
@@ -9,7 +9,8 @@ endif
 # If a test shouldn't be run in e.g. competition mode,
 # put it below in "TESTS +="
 TESTS =	\
-	bug336.smt2
+        bug330.smt2 \
+	bug336.smt2 
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 5048ca680..07619b965 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -28,7 +28,8 @@ SMT_TESTS = \
 	fuzz11.smt \
 	fuzz12.smt \
 	fuzz13.smt \
-	fuzz14.smt
+	fuzz14.smt \
+	calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt
 
 # Regression tests for SMT2 inputs
 SMT2_TESTS =
diff --git a/test/regress/regress0/bv/bug345.smt b/test/regress/regress0/bv/bug345.smt
new file mode 100644
index 000000000..b836cba2c
--- /dev/null
+++ b/test/regress/regress0/bv/bug345.smt
@@ -0,0 +1,46 @@
+(benchmark B_
+:logic QF_AUFBV
+:extrafuns ((mem_35_197 Array[32:8]))
+:status unknown
+:formula
+(let (?n1 bv1[1])
+(let (?n2 bv0[31])
+(let (?n3 bv0[32])
+(let (?n4 bv0[24])
+(let (?n5 (select mem_35_197 ?n3))
+(let (?n6 (concat ?n4 ?n5))
+(flet ($n7 (= ?n3 ?n6))
+(let (?n8 bv0[1])
+(let (?n9 (ite $n7 ?n1 ?n8))
+(let (?n10 (concat ?n2 ?n9))
+(let (?n11 (extract[0:0] ?n10))
+(let (?n12 bv0[8])
+(let (?n13 bv1[32])
+(let (?n14 (select mem_35_197 ?n13))
+(let (?n15 (concat ?n4 ?n14))
+(let (?n16 (extract[7:0] ?n15))
+(flet ($n17 (= ?n12 ?n16))
+(let (?n18 bv1[8])
+(flet ($n19 (= ?n16 ?n18))
+(let (?n20 bv3[8])
+(flet ($n21 (= ?n16 ?n20))
+(let (?n22 (ite $n21 ?n13 ?n3))
+(let (?n23 (ite $n19 ?n3 ?n22))
+(let (?n24 (ite $n17 ?n13 ?n23))
+(let (?n25 (extract[7:0] ?n24))
+(let (?n26 (store mem_35_197 ?n3 ?n25))
+(let (?n27 (concat ?n4 ?n16))
+(let (?n28 (extract[7:0] ?n27))
+(let (?n29 (concat ?n4 ?n28))
+(let (?n30 (extract[7:0] ?n29))
+(let (?n31 (concat ?n4 ?n30))
+(let (?n32 (bvadd ?n6 ?n31))
+(let (?n33 (store ?n26 ?n32 ?n12))
+(let (?n34 (select ?n33 ?n3))
+(let (?n35 (concat ?n4 ?n34))
+(flet ($n36 (= ?n3 ?n35))
+(let (?n37 (ite $n36 ?n1 ?n8))
+(let (?n38 (bvor ?n11 ?n37))
+(flet ($n39 (= ?n1 ?n38))
+$n39
+))))))))))))))))))))))))))))))))))))))))
diff --git a/test/regress/regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt b/test/regress/regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt
new file mode 100644
index 000000000..467f10c39
--- /dev/null
+++ b/test/regress/regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt
@@ -0,0 +1,80 @@
+(benchmark B_
+:logic QF_BV
+:extrapreds ((UCL_p16))
+:extrapreds ((UCL_p34))
+:status sat
+:formula
+(let (?n1 bv1[1])
+(let (?n2 bv0[2])
+(let (?n3 bv1[5])
+(let (?n4 bv0[5])
+(let (?n5 bv0[4])
+(let (?n6 bv1[4])
+(let (?n7 (ite UCL_p16 ?n6 ?n5))
+(flet ($n8 (= ?n5 ?n7))
+(let (?n9 bv1[2])
+(let (?n10 (ite $n8 ?n9 ?n2))
+(flet ($n11 (= ?n2 ?n10))
+(flet ($n12 (= ?n9 ?n10))
+(flet ($n13 (or $n11 $n12))
+(let (?n14 (ite $n13 ?n3 ?n4))
+(flet ($n15 (= ?n4 ?n14))
+(let (?n16 (ite $n15 ?n3 ?n4))
+(flet ($n17 (= ?n4 ?n16))
+(let (?n18 (ite UCL_p34 ?n2 ?n9))
+(flet ($n19 (= ?n9 ?n18))
+(let (?n20 (ite $n19 ?n6 ?n5))
+(flet ($n21 (= ?n5 ?n20))
+(let (?n22 (ite $n21 ?n3 ?n4))
+(let (?n23 (bvadd ?n22 ?n16))
+(let (?n24 (bvadd ?n3 ?n23))
+(let (?n25 (ite $n17 ?n24 ?n23))
+(flet ($n26 (= ?n3 ?n25))
+(let (?n27 bv1[6])
+(let (?n28 (concat ?n27 ?n9))
+(let (?n29 bv0[32])
+(let (?n30 (concat ?n28 ?n29))
+(let (?n31 (concat ?n30 ?n29))
+(let (?n32 bv0[72])
+(let (?n33 (ite $n26 ?n31 ?n32))
+(let (?n34 (extract[67:64] ?n33))
+(let (?n35 (extract[3:2] ?n34))
+(flet ($n36 (= ?n2 ?n35))
+(let (?n37 (ite $n36 ?n9 ?n2))
+(flet ($n38 (= ?n2 ?n37))
+(let (?n39 bv0[3])
+(let (?n40 bv1[3])
+(let (?n41 (ite $n38 ?n39 ?n40))
+(let (?n42 (extract[0:0] ?n41))
+(flet ($n43 (= ?n1 ?n42))
+(let (?n44 (ite $n43 ?n9 ?n2))
+(let (?n45 (ite $n12 ?n3 ?n4))
+(flet ($n46 (= ?n4 ?n45))
+(let (?n47 (ite $n8 ?n3 ?n4))
+(flet ($n48 (= ?n4 ?n47))
+(let (?n49 (ite $n48 ?n14 ?n4))
+(flet ($n50 (= ?n4 ?n49))
+(let (?n51 (bvsub ?n4 ?n3))
+(let (?n52 (ite $n50 ?n4 ?n51))
+(flet ($n53 (= ?n4 ?n52))
+(let (?n54 (ite $n53 ?n3 ?n52))
+(let (?n55 (ite $n46 ?n4 ?n54))
+(flet ($n56 (= ?n3 ?n55))
+(let (?n57 (concat ?n6 ?n9))
+(let (?n58 (concat ?n57 ?n2))
+(let (?n59 (concat ?n58 ?n29))
+(let (?n60 (concat ?n59 ?n29))
+(let (?n61 (bvadd ?n45 ?n52))
+(flet ($n62 (= ?n3 ?n61))
+(let (?n63 (ite $n62 ?n32 ?n31))
+(let (?n64 (ite $n56 ?n60 ?n63))
+(let (?n65 (extract[67:64] ?n64))
+(let (?n66 (extract[3:2] ?n65))
+(flet ($n67 (= ?n2 ?n66))
+(let (?n68 (extract[71:68] ?n64))
+(flet ($n69 (= ?n5 ?n68))
+(let (?n70 (ite $n69 ?n2 ?n9))
+(let (?n71 (ite $n67 ?n70 ?n2))
+(flet ($n72 (= ?n44 ?n71))
+$n72
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am
index 0244d768e..5b095b500 100644
--- a/test/regress/regress0/uflia/Makefile.am
+++ b/test/regress/regress0/uflia/Makefile.am
@@ -14,7 +14,12 @@ MAKEFLAGS = -k
 # Regression tests for SMT inputs
 SMT_TESTS = \
 	xs-09-16-3-4-1-5.smt \
+	xs-09-16-3-4-1-5.delta01.smt \
+	xs-09-16-3-4-1-5.delta02.smt \
+	xs-09-16-3-4-1-5.delta03.smt \
+	xs-09-16-3-4-1-5.delta04.smt \
 	error0.smt2 \
+	error0.delta01.smt \
 	simple_cyclic2.smt2
 
 # Regression tests for SMT2 inputs
diff --git a/test/regress/regress0/uflia/error0.delta01.smt b/test/regress/regress0/uflia/error0.delta01.smt
new file mode 100644
index 000000000..cc205063c
--- /dev/null
+++ b/test/regress/regress0/uflia/error0.delta01.smt
@@ -0,0 +1,78 @@
+(benchmark B_
+:logic QF_UFLIA
+:extrafuns ((format Int Int))
+:extrafuns ((arg1 Int))
+:extrafuns ((fmt1 Int))
+:extrafuns ((s_count Int Int))
+:extrafuns ((fmt0 Int))
+:extrafuns ((x_count Int Int))
+:status sat
+:formula
+(flet ($n1 true)
+(let (?n2 1)
+(let (?n3 (~ ?n2))
+(let (?n4 (* ?n3 fmt1))
+(let (?n5 (+ ?n4 fmt0))
+(let (?n6 8)
+(let (?n7 (~ ?n6))
+(flet ($n8 (>= ?n5 ?n7))
+(let (?n9 6)
+(let (?n10 (x_count ?n9))
+(let (?n11 7)
+(let (?n12 (x_count ?n11))
+(let (?n13 (* ?n3 ?n12))
+(let (?n14 (+ ?n10 ?n13))
+(let (?n15 0)
+(flet ($n16 (>= ?n14 ?n15))
+(flet ($n17 (>= fmt1 ?n11))
+(flet ($n18 (<= arg1 ?n9))
+(let (?n19 2)
+(let (?n20 (~ ?n19))
+(let (?n21 (* ?n3 fmt0))
+(let (?n22 (+ fmt1 ?n20 ?n21))
+(let (?n23 (s_count ?n22))
+(let (?n24 5)
+(let (?n25 (s_count ?n24))
+(let (?n26 (* ?n3 ?n25))
+(let (?n27 (+ ?n23 ?n26))
+(flet ($n28 (= ?n15 ?n27))
+(flet ($n29 (not $n28))
+(let (?n30 (~ ?n11))
+(flet ($n31 (<= ?n5 ?n30))
+(flet ($n32 false)
+(let (?n33 (+ arg1 ?n21))
+(flet ($n34 (<= ?n33 ?n2))
+(let (?n35 (+ ?n4 arg1))
+(flet ($n36 (<= ?n35 ?n15))
+(flet ($n37 (or $n32 $n32 $n34 $n36))
+(let (?n38 (x_count ?n2))
+(flet ($n39 (>= ?n38 ?n15))
+(let (?n40 (format ?n11))
+(flet ($n41 (<= ?n40 ?n15))
+(let (?n42 (x_count ?n22))
+(let (?n43 (+ ?n13 ?n42))
+(flet ($n44 (= ?n15 ?n43))
+(let (?n45 (s_count ?n9))
+(let (?n46 (* ?n3 ?n45))
+(let (?n47 (+ ?n23 ?n46))
+(flet ($n48 (= ?n15 ?n47))
+(flet ($n49 (or $n32 $n32 $n32 $n32 $n32 $n39 $n44 $n48))
+(let (?n50 (+ ?n2 fmt1))
+(let (?n51 (format ?n50))
+(flet ($n52 (>= ?n51 ?n15))
+(let (?n53 4)
+(let (?n54 (format ?n53))
+(flet ($n55 (>= ?n54 ?n15))
+(let (?n56 9)
+(let (?n57 (format ?n56))
+(flet ($n58 (<= ?n57 ?n15))
+(let (?n59 (format fmt1))
+(flet ($n60 (>= ?n59 ?n15))
+(let (?n61 12)
+(let (?n62 (format ?n61))
+(flet ($n63 (>= ?n62 ?n15))
+(let (?n64 (format arg1))
+(flet ($n65 (= ?n15 ?n64))
+(flet ($n66 (and $n1 $n8 $n16 $n17 $n18 $n29 $n31 $n37 $n39 $n41 $n49 $n52 $n55 $n58 $n60 $n63 $n65))
+$n66
+)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt
new file mode 100644
index 000000000..c7fed0c15
--- /dev/null
+++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta01.smt
@@ -0,0 +1,48 @@
+(benchmark mathsat
+:logic QF_UFLIA
+:extrafuns ((s_count Int Int))
+:extrafuns ((fmt1 Int))
+:extrafuns ((fmt_length Int))
+:status unsat
+:formula
+(let (?n1 0)
+(let (?n2 6)
+(let (?n3 (s_count ?n2))
+(flet ($n4 (= ?n1 ?n3))
+(let (?n5 5)
+(let (?n6 (s_count ?n5))
+(flet ($n7 (= ?n1 ?n6))
+(let (?n8 4)
+(let (?n9 (s_count ?n8))
+(flet ($n10 (= ?n1 ?n9))
+(let (?n11 3)
+(let (?n12 (s_count ?n11))
+(flet ($n13 (= ?n1 ?n12))
+(let (?n14 1)
+(let (?n15 (s_count ?n1))
+(flet ($n16 (= ?n14 ?n15))
+(let (?n17 (s_count ?n14))
+(flet ($n18 (= ?n1 ?n17))
+(flet ($n19 (and $n16 $n18))
+(let (?n20 2)
+(let (?n21 (s_count ?n20))
+(flet ($n22 (= ?n1 ?n21))
+(flet ($n23 (and $n19 $n22))
+(flet ($n24 (and $n13 $n23))
+(flet ($n25 (and $n10 $n24))
+(flet ($n26 (and $n7 $n25))
+(flet ($n27 (and $n4 $n26))
+(let (?n28 9)
+(flet ($n29 (= ?n28 fmt_length))
+(flet ($n30 (> fmt1 ?n14))
+(flet ($n31 (< fmt1 fmt_length))
+(flet ($n32 (and $n30 $n31))
+(let (?n33 (- fmt1 ?n20))
+(let (?n34 (s_count ?n33))
+(let (?n35 (+ ?n14 ?n34))
+(flet ($n36 (= ?n1 ?n35))
+(flet ($n37 (and $n32 $n36))
+(flet ($n38 (and $n29 $n37))
+(flet ($n39 (and $n27 $n38))
+$n39
+))))))))))))))))))))))))))))))))))))))))
diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt
new file mode 100644
index 000000000..fb16651ff
--- /dev/null
+++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta02.smt
@@ -0,0 +1,40 @@
+(benchmark mathsat
+:logic QF_UFLIA
+:extrafuns ((arg1 Int))
+:extrafuns ((adr_lo Int))
+:extrafuns ((select_format Int Int))
+:extrafuns ((x Int))
+:status sat
+:formula
+(let (?n1 (select_format arg1))
+(flet ($n2 (= ?n1 adr_lo))
+(let (?n3 0)
+(flet ($n4 (= ?n3 x))
+(let (?n5 4)
+(let (?n6 (select_format ?n5))
+(flet ($n7 (= adr_lo ?n6))
+(let (?n8 3)
+(let (?n9 (select_format ?n8))
+(flet ($n10 (= adr_lo ?n9))
+(let (?n11 2)
+(let (?n12 (select_format ?n11))
+(flet ($n13 (= adr_lo ?n12))
+(let (?n14 1)
+(let (?n15 (select_format ?n3))
+(flet ($n16 (= ?n14 ?n15))
+(let (?n17 (select_format ?n14))
+(flet ($n18 (= ?n3 ?n17))
+(flet ($n19 (or $n16 $n18))
+(flet ($n20 (or $n13 $n19))
+(flet ($n21 (or $n10 $n20))
+(flet ($n22 (or $n7 $n21))
+(flet ($n23 (or $n4 $n22))
+(flet ($n24 (= adr_lo ?n8))
+(flet ($n25 (< arg1 ?n5))
+(flet ($n26 (>= arg1 ?n3))
+(flet ($n27 (and $n25 $n26))
+(flet ($n28 (and $n24 $n27))
+(flet ($n29 (and $n23 $n28))
+(flet ($n30 (and $n2 $n29))
+$n30
+)))))))))))))))))))))))))))))))
diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt
new file mode 100644
index 000000000..6f65e83ec
--- /dev/null
+++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta03.smt
@@ -0,0 +1,45 @@
+(benchmark mathsat
+:logic QF_UFLIA
+:extrafuns ((fmt_length Int))
+:extrafuns ((fmt1 Int))
+:extrafuns ((arg1 Int))
+:extrafuns ((select_format Int Int))
+:status sat
+:formula
+(let (?n1 1)
+(let (?n2 (+ ?n1 fmt1))
+(let (?n3 (select_format ?n2))
+(flet ($n4 (= ?n1 ?n3))
+(let (?n5 (select_format arg1))
+(let (?n6 0)
+(flet ($n7 (= ?n5 ?n6))
+(flet ($n8 (and $n4 $n7))
+(let (?n9 7)
+(let (?n10 (select_format ?n9))
+(flet ($n11 (= ?n1 ?n10))
+(let (?n12 (select_format ?n6))
+(flet ($n13 (= ?n1 ?n12))
+(let (?n14 (select_format ?n1))
+(flet ($n15 (= ?n1 ?n14))
+(flet ($n16 (or $n13 $n15))
+(let (?n17 5)
+(let (?n18 (select_format ?n17))
+(flet ($n19 (= ?n6 ?n18))
+(flet ($n20 (or $n16 $n19))
+(let (?n21 6)
+(let (?n22 (select_format ?n21))
+(flet ($n23 (= ?n6 ?n22))
+(flet ($n24 (or $n20 $n23))
+(flet ($n25 (or $n11 $n24))
+(let (?n26 9)
+(flet ($n27 (= ?n26 fmt_length))
+(let (?n28 2)
+(let (?n29 (- fmt1 ?n28))
+(flet ($n30 (= arg1 ?n29))
+(flet ($n31 (< fmt1 fmt_length))
+(flet ($n32 (and $n30 $n31))
+(flet ($n33 (and $n27 $n32))
+(flet ($n34 (and $n25 $n33))
+(flet ($n35 (and $n8 $n34))
+$n35
+))))))))))))))))))))))))))))))))))))
diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt
new file mode 100644
index 000000000..f1212a876
--- /dev/null
+++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta04.smt
@@ -0,0 +1,67 @@
+(benchmark mathsat
+:logic QF_UFLIA
+:extrafuns ((fmt_length Int))
+:extrafuns ((fmt1 Int))
+:extrafuns ((x_count Int Int))
+:extrafuns ((select_format Int Int))
+:extrafuns ((percent Int))
+:extrafuns ((s_count Int Int))
+:status sat
+:formula
+(let (?n1 1)
+(let (?n2 5)
+(let (?n3 (x_count ?n2))
+(flet ($n4 (= ?n1 ?n3))
+(let (?n5 4)
+(let (?n6 (x_count ?n5))
+(flet ($n7 (= ?n1 ?n6))
+(let (?n8 3)
+(let (?n9 (x_count ?n8))
+(let (?n10 2)
+(let (?n11 (x_count ?n10))
+(flet ($n12 (= ?n9 ?n11))
+(let (?n13 0)
+(let (?n14 (select_format ?n8))
+(flet ($n15 (= ?n13 ?n14))
+(let (?n16 (x_count ?n13))
+(flet ($n17 (= ?n1 ?n16))
+(flet ($n18 (= ?n1 percent))
+(flet ($n19 true)
+(let (?n20 (s_count ?n13))
+(flet ($n21 (= ?n13 ?n20))
+(flet ($n22 (if_then_else $n18 $n19 $n21))
+(let (?n23 (select_format ?n10))
+(flet ($n24 (= percent ?n23))
+(flet ($n25 (= ?n1 ?n14))
+(flet ($n26 (and $n24 $n25))
+(flet ($n27 false)
+(flet ($n28 (if_then_else $n26 $n27 $n19))
+(flet ($n29 (and $n22 $n28))
+(flet ($n30 (and $n17 $n29))
+(flet ($n31 (= ?n13 percent))
+(flet ($n32 (= ?n13 ?n23))
+(flet ($n33 (and $n31 $n32))
+(let (?n34 (x_count ?n1))
+(flet ($n35 (= ?n13 ?n34))
+(flet ($n36 (= ?n16 ?n34))
+(flet ($n37 (if_then_else $n33 $n35 $n36))
+(flet ($n38 (and $n30 $n37))
+(flet ($n39 (and $n15 $n38))
+(flet ($n40 (and $n12 $n39))
+(flet ($n41 (and $n7 $n40))
+(flet ($n42 (and $n4 $n41))
+(let (?n43 9)
+(flet ($n44 (= ?n43 fmt_length))
+(let (?n45 (- fmt1 ?n10))
+(let (?n46 (x_count ?n45))
+(let (?n47 (+ ?n1 ?n46))
+(flet ($n48 (= ?n13 ?n47))
+(flet ($n49 (> fmt1 ?n1))
+(let (?n50 (- fmt_length ?n1))
+(flet ($n51 (< fmt1 ?n50))
+(flet ($n52 (and $n49 $n51))
+(flet ($n53 (and $n48 $n52))
+(flet ($n54 (and $n44 $n53))
+(flet ($n55 (and $n42 $n54))
+$n55
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))
diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp
index c64c1463e..f1dc77988 100644
--- a/test/system/boilerplate.cpp
+++ b/test/system/boilerplate.cpp
@@ -31,7 +31,8 @@ int main() {
   ExprManager em;
   Options opts;
   SmtEngine smt(&em);
-  Result r = smt.query(em.mkConst(true));
+  BoolExpr F = em.mkConst(true);
+  Result r = smt.query(F);
 
   return r == Result::VALID ? 0 : 1;
 }
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 1de3854b9..34536445f 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -57,9 +57,10 @@ public:
     push(CONFLICT, n);
   }
 
-  void propagate(TNode n)
+  bool propagate(TNode n)
     throw(AssertionException) {
     push(PROPAGATE, n);
+    return true;
   }
 
   void propagateAsDecision(TNode n)
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index ff6cba936..2d6730949 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -51,7 +51,7 @@ class FakeOutputChannel : public OutputChannel {
   void conflict(TNode n) throw(AssertionException) {
     Unimplemented();
   }
-  void propagate(TNode n) throw(AssertionException) {
+  bool propagate(TNode n) throw(AssertionException) {
     Unimplemented();
   }
   void propagateAsDecision(TNode n) throw(AssertionException) {