diff options
Diffstat (limited to 'src/expr/node_algorithm.cpp')
| -rw-r--r-- | src/expr/node_algorithm.cpp | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp index 52c5165a6..be436bf8b 100644 --- a/src/expr/node_algorithm.cpp +++ b/src/expr/node_algorithm.cpp @@ -491,7 +491,13 @@ void getOperatorsMap( // add the current operator to the result if (cur.hasOperator()) { - ops[tn].insert(NodeManager::currentNM()->operatorOf(cur.getKind())); + Node o; + if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) { + o = cur.getOperator(); + } else { + o = NodeManager::currentNM()->operatorOf(cur.getKind()); + } + ops[tn].insert(o); } // add children to visit in the future for (TNode cn : cur) |