summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
authorTim King <taking@cs.nyu.edu>2010-10-12 22:04:58 +0000
committerTim King <taking@cs.nyu.edu>2010-10-12 22:04:58 +0000
commita47b818c883eafb74afe066915bbbedf760c31e1 (patch)
tree50fd1633df1a585946723b43345214c0746dcc1f /src/expr
parent5d1fe7f3fe26e6ace5ba498054505fd28090cd90 (diff)
IDENTITY has been removed.
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/node_manager.cpp3
1 files changed, 0 insertions, 3 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 8ff83bb94..edb3a1592 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -263,9 +263,6 @@ 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