diff --git a/Kernel/LPOComparator.cpp b/Kernel/LPOComparator.cpp
index 51e513d2c..ec8ec443c 100644
--- a/Kernel/LPOComparator.cpp
+++ b/Kernel/LPOComparator.cpp
@@ -149,7 +149,7 @@ void LPOComparator::expand(Branch& branch, const LPO& lpo)
   {
     // take temporary ownership of node
     Branch nodeHolder = branch;
-    auto node = nodeHolder.n.get();
+    auto node = nodeHolder.n.ptr();
 
     // Use compare here to filter out as many
     // precomputable comparisons as possible.
diff --git a/Kernel/LPOComparator.hpp b/Kernel/LPOComparator.hpp
index cf184c678..15cb18283 100644
--- a/Kernel/LPOComparator.hpp
+++ b/Kernel/LPOComparator.hpp
@@ -43,7 +43,7 @@ class LPOComparator
 
   struct Branch {
     BranchTag tag;
-    std::shared_ptr<Node> n;
+    SmartPtr<Node> n;
 
     explicit Branch(BranchTag t) : tag(t), n(nullptr) { ASS(t==BranchTag::T_GREATER || t==BranchTag::T_NOT_GREATER); }
     explicit Branch(TermList lhs, TermList rhs) : tag(BranchTag::T_UNKNOWN), n(new Node(lhs, rhs)) {}