diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-13 19:46:27 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-13 19:46:27 +0000 |
commit | db2c74345f23b68a2421c15878311414a71cf210 (patch) | |
tree | 650340a3bc6e5f11c31942a5d4eef27a45adf2e7 /src/expr | |
parent | ecdd09877ecc4c07a22cc27cd2dd5441134476ba (diff) |
Minor cleanup. No performance difference expected.
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/node_manager.h | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 682a48bda..bad20b3b6 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -979,14 +979,11 @@ inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) { Assert(types.size() >= 2); std::vector<TypeNode> typeNodes; for (unsigned i = 0; i < types.size(); ++ i) { - /* FIXME when congruence closure no longer abuses tuples */ -#if 0 CheckArgument(!types[i].isFunctionLike(), types, "cannot put function-like types in tuples"); if(types[i].isBoolean()) { WarningOnce() << "Warning: CVC4 does not yet support Boolean terms (you have created a tuple type with a Boolean argument)" << std::endl; } -#endif /* 0 */ typeNodes.push_back(types[i]); } return mkTypeNode(kind::TUPLE_TYPE, typeNodes); |