1 files changed, 9 insertions, 10 deletions
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 11b872e72..2a57cde5e 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -18,7 +18,6 @@
 #include "expr/node_algorithm.h"
 #include "options/uf_options.h"
 #include "theory/theory_model.h"
-#include "theory/uf/theory_uf.h"
 #include "theory/uf/theory_uf_rewriter.h"
 
 using namespace std;
@@ -28,9 +27,9 @@ namespace CVC4 {
 namespace theory {
 namespace uf {
 
-HoExtension::HoExtension(TheoryUF& p, TheoryState& state)
-    : d_parent(p),
-      d_state(state),
+HoExtension::HoExtension(TheoryState& state, TheoryInferenceManager& im)
+    : d_state(state),
+      d_im(im),
       d_extensionality(state.getUserContext()),
       d_uf_std_skolem(state.getUserContext())
 {
@@ -108,7 +107,7 @@ unsigned HoExtension::applyExtensionality(TNode deq)
     Node lem = NodeManager::currentNM()->mkNode(OR, deq[0], conc);
     Trace("uf-ho-lemma") << "uf-ho-lemma : extensionality : " << lem
                          << std::endl;
-    d_parent.getOutputChannel().lemma(lem);
+    d_im.lemma(lem);
     return 1;
   }
   return 0;
@@ -168,7 +167,7 @@ Node HoExtension::getApplyUfForHoApply(Node node)
       Trace("uf-ho-lemma")
           << "uf-ho-lemma : Skolem definition for apply-conversion : " << lem
           << std::endl;
-      d_parent.getOutputChannel().lemma(lem);
+      d_im.lemma(lem);
       d_uf_std_skolem[f] = new_f;
     }
     else
@@ -257,7 +256,7 @@ unsigned HoExtension::checkExtensionality(TheoryModel* m)
               Node lem = nm->mkNode(OR, deq.negate(), eq);
               Trace("uf-ho") << "HoExtension: cmi extensionality lemma " << lem
                              << std::endl;
-              d_parent.getOutputChannel().lemma(lem);
+              d_im.lemma(lem);
               return 1;
             }
           }
@@ -282,10 +281,10 @@ unsigned HoExtension::applyAppCompletion(TNode n)
   Node ret = TheoryUfRewriter::getHoApplyForApplyUf(n);
   if (!ee->hasTerm(ret) || !ee->areEqual(ret, n))
   {
-    Node eq = ret.eqNode(n);
+    Node eq = n.eqNode(ret);
     Trace("uf-ho-lemma") << "uf-ho-lemma : infer, by apply-expand : " << eq
                          << std::endl;
-    ee->assertEquality(eq, true, d_true);
+    d_im.assertInternalFact(eq, true, PfRule::HO_APP_ENCODE, {}, {n});
     return 1;
   }
   Trace("uf-ho-debug") << "    ...already have " << ret << " == " << n << "."
@@ -442,7 +441,7 @@ bool HoExtension::collectModelInfoHoTerm(Node n, TheoryModel* m)
       Node eq = n.eqNode(hn);
       Trace("uf-ho") << "HoExtension: cmi app completion lemma " << eq
                      << std::endl;
-      d_parent.getOutputChannel().lemma(eq);
+      d_im.lemma(eq);
       return false;
     }
   }