diff options
Diffstat (limited to 'src/expr/node_manager.cpp')
| -rw-r--r-- | src/expr/node_manager.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 0a0781819..780fda9ab 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -724,7 +724,7 @@ TypeNode NodeManager::mkDatatypeUpdateType(TypeNode domain, TypeNode range) domain.isDatatype(), domain, "cannot create non-datatype upater type"); // It is a function type domain x range -> domain, we store only the // arguments - return mkTypeNode(kind::DT_UPDATE_TYPE, domain, range); + return mkTypeNode(kind::UPDATER_TYPE, domain, range); } TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) { |