diff options
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 457e54d9b..425f78555 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -146,7 +146,7 @@ StringType ExprManager::stringType() const { RegExpType ExprManager::regExpType() const { NodeManagerScope nms(d_nodeManager); - return StringType(Type(d_nodeManager, new TypeNode(d_nodeManager->regExpType()))); + return RegExpType(Type(d_nodeManager, new TypeNode(d_nodeManager->regExpType()))); } RealType ExprManager::realType() const { @@ -831,10 +831,13 @@ SortType ExprManager::mkSort(const std::string& name, uint32_t flags) const { } SortConstructorType ExprManager::mkSortConstructor(const std::string& name, - size_t arity) const { + size_t arity, + uint32_t flags) const +{ NodeManagerScope nms(d_nodeManager); - return SortConstructorType(Type(d_nodeManager, - new TypeNode(d_nodeManager->mkSortConstructor(name, arity)))); + return SortConstructorType( + Type(d_nodeManager, + new TypeNode(d_nodeManager->mkSortConstructor(name, arity, flags)))); } /** |