4 files changed, 11 insertions, 11 deletions
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 43e4a7b76..dad437bc6 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -528,7 +528,7 @@ Expr Expr::iffExpr(const Expr& e) const {
          "Don't have an expression manager for this expression!");
   PrettyCheckArgument(d_exprManager == e.d_exprManager, e,
                       "Different expression managers!");
-  return d_exprManager->mkExpr(IFF, *this, e);
+  return d_exprManager->mkExpr(EQUAL, *this, e);
 }
 
 Expr Expr::impExpr(const Expr& e) const {
diff --git a/src/expr/node.h b/src/expr/node.h
index c9bfb75a4..6dbb5aa2b 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -893,8 +893,6 @@ public:
   NodeTemplate<true> iteNode(const NodeTemplate<ref_count2>& thenpart,
                              const NodeTemplate<ref_count3>& elsepart) const;
   template <bool ref_count2>
-  NodeTemplate<true> iffNode(const NodeTemplate<ref_count2>& right) const;
-  template <bool ref_count2>
   NodeTemplate<true> impNode(const NodeTemplate<ref_count2>& right) const;
   template <bool ref_count2>
   NodeTemplate<true> xorNode(const NodeTemplate<ref_count2>& right) const;
@@ -1203,14 +1201,6 @@ NodeTemplate<ref_count>::iteNode(const NodeTemplate<ref_count2>& thenpart,
 template <bool ref_count>
 template <bool ref_count2>
 NodeTemplate<true>
-NodeTemplate<ref_count>::iffNode(const NodeTemplate<ref_count2>& right) const {
-  assertTNodeNotExpired();
-  return NodeManager::currentNM()->mkNode(kind::IFF, *this, right);
-}
-
-template <bool ref_count>
-template <bool ref_count2>
-NodeTemplate<true>
 NodeTemplate<ref_count>::impNode(const NodeTemplate<ref_count2>& right) const {
   assertTNodeNotExpired();
   return NodeManager::currentNM()->mkNode(kind::IMPLIES, *this, right);
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index a9be51418..ebf78f541 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -780,6 +780,13 @@ Node NodeManager::mkInstConstant(const TypeNode& type) {
   return n;
 }
 
+Node NodeManager::mkBooleanTermVariable() {
+  Node n = NodeBuilder<0>(this, kind::BOOLEAN_TERM_VARIABLE);
+  n.setAttribute(TypeAttr(), booleanType());
+  n.setAttribute(TypeCheckedAttr(), true);
+  return n;
+}
+
 Node NodeManager::mkUniqueVar(const TypeNode& type, Kind k) {
   std::map< TypeNode, Node >::iterator it = d_unique_vars[k].find( type );
   if( it==d_unique_vars[k].end() ){
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index d85ff23d5..d2b45a636 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -528,6 +528,9 @@ public:
 
   /** Create a instantiation constant with the given type. */
   Node mkInstConstant(const TypeNode& type);
+  
+  /** Create a boolean term variable. */
+  Node mkBooleanTermVariable();
 
   /** Make a new abstract value with the given type. */
   Node mkAbstractValue(const TypeNode& type);