summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-09-04 19:55:16 -0400
committerMorgan Deters <mdeters@cs.nyu.edu>2013-09-09 17:21:42 -0400
commit42d28850d4f2f4816af24dedf8d1cbd0a0d58b6f (patch)
treea1183f01ad74389d5e6c5d9c949e18d25f75d1cd /src/expr/node_manager.h
parent9d0734cf73454ecfd51556ca84daaba9025b28f8 (diff)
Support empty (and 1-ary) tuples and records.
Diffstat (limited to 'src/expr/node_manager.h')
-rw-r--r--src/expr/node_manager.h1
1 files changed, 0 insertions, 1 deletions
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,
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback