5 files changed, 23 insertions, 6 deletions
diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 297ff6d9f..8e9116543 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -135,7 +135,8 @@ void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) {
       }
     }
     break;
-  case kind::IFF:
+  case kind::EQUAL:
+    Assert( parent[0].getType().isBoolean() );
     if (parentAssignment) {
       // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment [resp x = y.assignment])
       if (isAssigned(parent[0])) {
@@ -285,7 +286,8 @@ void CircuitPropagator::propagateForward(TNode child, bool childAssignment) {
         }
       }
       break;
-    case kind::IFF:
+    case kind::EQUAL:
+      Assert( parent[0].getType().isBoolean() );
       if (isAssigned(parent[0]) && isAssigned(parent[1])) {
         // IFF x y: if x or y is assigned, assign(IFF = (x.assignment <=> y.assignment))
         assignAndEnqueue(parent, getAssignment(parent[0]) == getAssignment(parent[1]));
diff --git a/src/theory/booleans/kinds b/src/theory/booleans/kinds
index ad45e3cbb..9d7b3fbd6 100644
--- a/src/theory/booleans/kinds
+++ b/src/theory/booleans/kinds
@@ -30,7 +30,6 @@ enumerator BOOLEAN_TYPE \
 
 operator NOT 1 "logical not"
 operator AND 2: "logical and (N-ary)"
-operator IFF 2 "logical equivalence (exactly two parameters)"
 operator IMPLIES 2 "logical implication (exactly two parameters)"
 operator OR 2: "logical or (N-ary)"
 operator XOR 2 "exclusive or (exactly two parameters)"
@@ -40,7 +39,6 @@ typerule CONST_BOOLEAN ::CVC4::theory::boolean::BooleanTypeRule
 
 typerule NOT ::CVC4::theory::boolean::BooleanTypeRule
 typerule AND ::CVC4::theory::boolean::BooleanTypeRule
-typerule IFF ::CVC4::theory::boolean::BooleanTypeRule
 typerule IMPLIES ::CVC4::theory::boolean::BooleanTypeRule
 typerule OR ::CVC4::theory::boolean::BooleanTypeRule
 typerule XOR ::CVC4::theory::boolean::BooleanTypeRule
diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index d483ba105..b0f2efcda 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -56,6 +56,22 @@ Theory::PPAssertStatus TheoryBool::ppAssert(TNode in, SubstitutionMap& outSubsti
   return PP_ASSERT_STATUS_SOLVED;
 }
 
+/*
+void TheoryBool::check(Effort level) {
+  if (done() && !fullEffort(level)) {
+    return;
+  }
+  while (!done())
+  {
+    // Get all the assertions
+    Assertion assertion = get();
+    TNode fact = assertion.assertion;
+    Trace("ajr-bool") << "Assert : " << fact << std::endl;
+  }
+  if( Theory::fullEffort(level) ){
+  }
+}  
+*/
 
 }/* CVC4::theory::booleans namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index eef379bf9..353143c43 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -35,6 +35,8 @@ public:
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
 
+  //void check(Effort);
+  
   std::string identify() const { return std::string("TheoryBool"); }
 };/* class TheoryBool */
 
diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index dc5f655aa..32f69e037 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -173,7 +173,6 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
     if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
     break;
   }
-  case kind::IFF:
   case kind::EQUAL: {
     // rewrite simple cases of IFF
     if(n[0] == tt) {
@@ -318,7 +317,7 @@ RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
 
     int parityTmp;
     if ((parityTmp = equalityParity(n[1], n[2])) != 0) {
-      Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].iffNode(n[1]);
+      Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].eqNode(n[1]);
       Debug("bool-ite") << "equalityParity n[1], n[2] " << parityTmp
                         << " " << n << ": " << resp << std::endl;
       return RewriteResponse(REWRITE_AGAIN, resp);