3 files changed, 4 insertions, 22 deletions
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 5be612b20..8ded902b7 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -231,12 +231,6 @@ void PopCommand::invoke(SmtEngine* smtEngine) throw() {
   }
 }
 
-/* class CheckSatCommand */
-
-CheckSatCommand::CheckSatCommand() throw() :
-  d_expr() {
-}
-
 Command* PopCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
   return new PopCommand();
 }
@@ -247,6 +241,10 @@ Command* PopCommand::clone() const {
 
 /* class CheckSatCommand */
 
+CheckSatCommand::CheckSatCommand() throw() :
+  d_expr() {
+}
+
 CheckSatCommand::CheckSatCommand(const Expr& expr) throw() :
   d_expr(expr) {
 }
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 7cb5eb459..5159f6b5a 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -700,10 +700,6 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
       // CVC4::Datatype class, but this actually needs to be checked.
       AlwaysAssert(!SelectorType(selectorType).getRangeType().d_typeNode->isFunctionLike(),
                    "cannot put function-like things in datatypes");
-      // currently don't play well with Boolean terms
-      if(SelectorType(selectorType).getRangeType().d_typeNode->isBoolean()) {
-        WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a datatype containing a Boolean)" << std::endl;
-      }
     }
   }
 }
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 6e08a9bc2..5cf591f9d 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1055,9 +1055,6 @@ NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
   for (unsigned i = 0; i < sorts.size(); ++ i) {
     CheckArgument(!sorts[i].isFunctionLike(), sorts,
                   "cannot create higher-order function types");
-    if(i + 1 < sorts.size() && sorts[i].isBoolean()) {
-      WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a function type with a Boolean argument)" << std::endl;
-    }
     sortNodes.push_back(sorts[i]);
   }
   return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
@@ -1070,9 +1067,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
   for (unsigned i = 0; i < sorts.size(); ++ i) {
     CheckArgument(!sorts[i].isFunctionLike(), sorts,
                   "cannot create higher-order function types");
-    if(i + 1 < sorts.size() && sorts[i].isBoolean()) {
-      WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a predicate type with a Boolean argument)" << std::endl;
-    }
     sortNodes.push_back(sorts[i]);
   }
   sortNodes.push_back(booleanType());
@@ -1085,9 +1079,6 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
   for (unsigned i = 0; i < types.size(); ++ i) {
     CheckArgument(!types[i].isFunctionLike(), types,
                   "cannot put function-like types in tuples");
-    if(types[i].isBoolean()) {
-      WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a tuple type with a Boolean argument)" << std::endl;
-    }
     typeNodes.push_back(types[i]);
   }
   return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
@@ -1119,9 +1110,6 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                 "cannot index arrays by a function-like type");
   CheckArgument(!constituentType.isFunctionLike(), constituentType,
                 "cannot store function-like types in arrays");
-  if(indexType.isBoolean() || constituentType.isBoolean()) {
-    WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created an array type with a Boolean index or constituent type)" << std::endl;
-  }
   Debug("arrays") << "making array type " << indexType << " " << constituentType << std::endl;
   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
 }