diff options
Diffstat (limited to 'src/expr/node_manager.cpp')
| -rw-r--r-- | src/expr/node_manager.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 17524a3c0..c9e6866d4 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -393,8 +393,8 @@ TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor, sorts.push_back(sort); } Debug("datatypes") << "ctor range: " << range << endl; - CheckArgument(!range.isFunctionLike(), range, - "cannot create higher-order function types"); + PrettyCheckArgument(!range.isFunctionLike(), range, + "cannot create higher-order function types"); sorts.push_back(range); return mkTypeNode(kind::CONSTRUCTOR_TYPE, sorts); } |