summaryrefslogtreecommitdiff
path: root/src/expr/node_manager.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/node_manager.cpp')
-rw-r--r--src/expr/node_manager.cpp3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index fbfffe87d..d017ad799 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -205,6 +205,9 @@ TypeNode NodeManager::getType(TNode n, bool check)
case kind::DISTINCT:
typeNode = CVC4::theory::builtin::DistinctTypeRule::computeType(this, n, check);
break;
+ case kind::TUPLE:
+ typeNode = CVC4::theory::builtin::TupleTypeRule::computeType(this, n, check);
+ break;
case kind::CONST_BOOLEAN:
typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
break;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback