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 d017ad799..37ed4fe20 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -235,6 +235,9 @@ TypeNode NodeManager::getType(TNode n, bool check)
case kind::APPLY_UF:
typeNode = CVC4::theory::uf::UfTypeRule::computeType(this, n, check);
break;
+ case kind::IDENTITY:
+ typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
+ break;
case kind::PLUS:
typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
break;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback