3 files changed, 5 insertions, 25 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 4a2a5f135..e1ef51d09 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -30,7 +30,7 @@ std::string PreRegisterVisitor::toString() const {
 
 bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
 
-  Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ") => ";
+  Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
 
 
   TheoryId currentTheoryId = Theory::theoryOf(current);
@@ -134,7 +134,7 @@ std::string SharedTermsVisitor::toString() const {
 
 bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
 
-  Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ") => ";
+  Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
 
   TNodeVisitedMap::const_iterator find = d_visited.find(current);
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 5a8a75aab..0ab188dc4 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -772,14 +772,8 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
     Node normalizedLiteral = Rewriter::rewrite(literal);
     if (d_propEngine->isSatLiteral(normalizedLiteral)) {
       // If there is a literal, propagate it to SAT
-      if (d_propEngine->hasValue(normalizedLiteral, value)) {
-        // if we are propagting something that already has a sat value we better be the same
-        Debug("theory") << "literal " << literal << ", normalized = " << normalizedLiteral << ", propagated by " << theory << " but already has a sat value " << (value ? "true" : "false") << std::endl;
-        Assert(value);
-      } else {
-        SharedLiteral sharedLiteral(normalizedLiteral, literal, theory::THEORY_LAST);
-        d_propagatedSharedLiterals.push_back(sharedLiteral);
-      }
+      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;
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index cddd01b07..7f173a0c4 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -112,21 +112,7 @@ void TheoryUF::propagate(Effort level) {
     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;
-      bool satValue;
-      Node normalized = Rewriter::rewrite(literal);
-      if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
-        d_out->propagate(literal);
-      } else {
-        Debug("uf") << "TheoryUF::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;
-      }
+      d_out->propagate(literal);
     }
   }
 }/* TheoryUF::propagate(Effort) */