diff options
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r-- | src/expr/node_manager.h | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index c0f489d7a..0860365bc 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -789,15 +789,11 @@ inline TypeNode NodeManager::mkSort(TypeNode constructor, constructor.getNumChildren() == 0, "expected a sort constructor"); Assert(children.size() > 0, "expected non-zero # of children"); - uint64_t arity; - std::string name; - bool hasArityAttribute = - getAttribute(constructor.d_nv, expr::SortArityAttr(), arity); - Assert(hasArityAttribute, "expected a sort constructor"); - bool hasNameAttribute = - getAttribute(constructor.d_nv, expr::VarNameAttr(), name); - Assert(hasNameAttribute, "expected a sort constructor"); - Assert(arity == children.size(), + Assert( hasAttribute(constructor.d_nv, expr::SortArityAttr()) && + hasAttribute(constructor.d_nv, expr::VarNameAttr()), + "expected a sort constructor" ); + std::string name = getAttribute(constructor.d_nv, expr::VarNameAttr()); + Assert(getAttribute(constructor.d_nv, expr::SortArityAttr()) == children.size(), "arity mismatch in application of sort constructor"); NodeBuilder<> nb(this, kind::SORT_TYPE); Node sortTag = Node(constructor.d_nv->d_children[0]); |