1 files changed, 13 insertions, 18 deletions

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 4cdc5e240..e4a3ac78c 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -139,14 +139,14 @@ void TheoryUF::check(Effort level) {
     }
   }
 
-
-  if (d_thss != NULL && ! d_conflict) {
-    d_thss->check(level);
-    if( d_thss->isConflict() ){
-      d_conflict = true;
+  if(! d_conflict ){
+    if (d_thss != NULL) {
+      d_thss->check(level);
+      if( d_thss->isConflict() ){
+        d_conflict = true;
+      }
     }
   }
-
 }/* TheoryUF::check() */
 
 void TheoryUF::preRegisterTerm(TNode node) {
@@ -217,7 +217,7 @@ void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqPro
   // Do the work
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
-  if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+  if (atom.getKind() == kind::EQUAL) {
     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf);
   } else {
     d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf);
@@ -336,10 +336,10 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
     if(n.getKind() == kind::OR && n.getNumChildren() == 2 &&
        n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 &&
        n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 &&
-       (n[0][0].getKind() == kind::EQUAL || n[0][0].getKind() == kind::IFF) &&
-       (n[0][1].getKind() == kind::EQUAL || n[0][1].getKind() == kind::IFF) &&
-       (n[1][0].getKind() == kind::EQUAL || n[1][0].getKind() == kind::IFF) &&
-       (n[1][1].getKind() == kind::EQUAL || n[1][1].getKind() == kind::IFF)) {
+       (n[0][0].getKind() == kind::EQUAL) &&
+       (n[0][1].getKind() == kind::EQUAL) &&
+       (n[1][0].getKind() == kind::EQUAL) &&
+       (n[1][1].getKind() == kind::EQUAL)) {
       // now we have (a = b && c = d) || (e = f && g = h)
 
       Debug("diamonds") << "has form of a diamond!" << endl;
@@ -396,7 +396,7 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
           (a == h && d == e) ) {
         // learn: n implies a == d
         Debug("diamonds") << "+ C holds" << endl;
-        Node newEquality = a.getType().isBoolean() ? a.iffNode(d) : a.eqNode(d);
+        Node newEquality = a.eqNode(d);
         Debug("diamonds") << "  ==> " << newEquality << endl;
         learned << n.impNode(newEquality);
       } else {
@@ -533,12 +533,7 @@ void TheoryUF::computeCareGraph() {
 
 void TheoryUF::conflict(TNode a, TNode b) {
   eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL;
-
-  if (a.getKind() == kind::CONST_BOOLEAN) {
-    d_conflictNode = explain(a.iffNode(b),pf);
-  } else {
-    d_conflictNode = explain(a.eqNode(b),pf);
-  }
+  d_conflictNode = explain(a.eqNode(b),pf);
   ProofUF* puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
   d_out->conflict(d_conflictNode, puf);
   d_conflict = true;