diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-12-14 21:07:46 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-12-14 21:07:46 +0000 |
| commit | 96ce991a4b8593f7ec831c3a9b40b214d2ac3761 (patch) | |
| tree | bf804dcc18a20394a6fba8ac4bed6932ca4c7c02 /src/expr/node_manager.cpp | |
| parent | b44f183a75deea11fa379554b893b6656e1864b2 (diff) | |
congruence closure module now supports things other than APPLY_UF; ported from "arrays" branch to trunk
Diffstat (limited to 'src/expr/node_manager.cpp')
| -rw-r--r-- | src/expr/node_manager.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 280c55254..9006bf4d9 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -228,6 +228,9 @@ TypeNode NodeManager::computeType(TNode n, bool check) // Infer the type switch(n.getKind()) { + case kind::BUILTIN: + typeNode = builtinOperatorType(); + break; case kind::SORT_TYPE: typeNode = kindType(); break; |