diff options
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 4 |
1 files changed, 0 insertions, 4 deletions
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; - } } } } |