1 files changed, 5 insertions, 1 deletions
diff --git a/src/expr/node.h b/src/expr/node.h
index d9e88d8af..99e1e7ee7 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1337,7 +1337,11 @@ NodeTemplate<ref_count>::substitute(TNode node, TNode replacement,
   NodeBuilder<> nb(getKind());
   if(getMetaKind() == kind::metakind::PARAMETERIZED) {
     // push the operator
-    nb << getOperator();
+    if(getOperator() == node) {
+      nb << replacement;
+    } else {
+      nb << getOperator().substitute(node, replacement, cache);
+    }
   }
   for(const_iterator i = begin(),
         iend = end();