output a warning message when a function type (or datatype, or array, etc.) is created with a Boolean term inside it

1 files changed, 4 insertions, 0 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 8819684fc..cf2616011 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -685,6 +685,10 @@ 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;
+      }
     }
   }
 }