diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-04 19:55:16 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-09 17:21:42 -0400 |
| commit | 42d28850d4f2f4816af24dedf8d1cbd0a0d58b6f (patch) | |
| tree | a1183f01ad74389d5e6c5d9c949e18d25f75d1cd /src/expr | |
| parent | 9d0734cf73454ecfd51556ca84daaba9025b28f8 (diff) | |
Support empty (and 1-ary) tuples and records.
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/expr_manager_template.cpp | 1 | ||||
| -rw-r--r-- | src/expr/node_manager.h | 1 |
2 files changed, 0 insertions, 2 deletions
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 424ebab11..a838d6d30 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -509,7 +509,6 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { TupleType ExprManager::mkTupleType(const std::vector<Type>& types) { NodeManagerScope nms(d_nodeManager); - Assert( types.size() >= 1 ); std::vector<TypeNode> typeNodes; for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) { typeNodes.push_back(*types[i].d_typeNode); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index f44c7e78b..7c84f3f15 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1090,7 +1090,6 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { } inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { - Assert(types.size() >= 1); std::vector<TypeNode> typeNodes; for (unsigned i = 0; i < types.size(); ++ i) { CheckArgument(!types[i].isFunctionLike(), types, |