6 files changed, 17 insertions, 15 deletions
diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h
index 6e251fc2d..f4b5a9d11 100644
--- a/src/theory/bv/bv_solver.h
+++ b/src/theory/bv/bv_solver.h
@@ -86,7 +86,7 @@ class BVSolver
   virtual std::string identify() const = 0;
 
   virtual Theory::PPAssertStatus ppAssert(
-      TNode in, SubstitutionMap& outSubstitutions) = 0;
+      TrustNode in, TrustSubstitutionMap& outSubstitutions) = 0;
 
   virtual TrustNode ppRewrite(TNode t) { return TrustNode::null(); };
 
diff --git a/src/theory/bv/bv_solver_lazy.cpp b/src/theory/bv/bv_solver_lazy.cpp
index 417cf0c15..a19af44ac 100644
--- a/src/theory/bv/bv_solver_lazy.cpp
+++ b/src/theory/bv/bv_solver_lazy.cpp
@@ -439,9 +439,10 @@ void BVSolverLazy::propagate(Theory::Effort e)
   }
 }
 
-Theory::PPAssertStatus BVSolverLazy::ppAssert(TNode in,
-                                              SubstitutionMap& outSubstitutions)
+Theory::PPAssertStatus BVSolverLazy::ppAssert(
+    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
 {
+  TNode in = tin.getNode();
   switch (in.getKind())
   {
     case kind::EQUAL:
@@ -449,13 +450,13 @@ Theory::PPAssertStatus BVSolverLazy::ppAssert(TNode in,
       if (in[0].isVar() && d_bv.isLegalElimination(in[0], in[1]))
       {
         ++(d_statistics.d_solveSubstitutions);
-        outSubstitutions.addSubstitution(in[0], in[1]);
+        outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
         return Theory::PP_ASSERT_STATUS_SOLVED;
       }
       if (in[1].isVar() && d_bv.isLegalElimination(in[1], in[0]))
       {
         ++(d_statistics.d_solveSubstitutions);
-        outSubstitutions.addSubstitution(in[1], in[0]);
+        outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
         return Theory::PP_ASSERT_STATUS_SOLVED;
       }
       Node node = Rewriter::rewrite(in);
@@ -502,7 +503,7 @@ Theory::PPAssertStatus BVSolverLazy::ppAssert(TNode in,
           Assert(utils::getSize(concat) == utils::getSize(extract[0]));
           if (d_bv.isLegalElimination(extract[0], concat))
           {
-            outSubstitutions.addSubstitution(extract[0], concat);
+            outSubstitutions.addSubstitutionSolved(extract[0], concat, tin);
             return Theory::PP_ASSERT_STATUS_SOLVED;
           }
         }
diff --git a/src/theory/bv/bv_solver_lazy.h b/src/theory/bv/bv_solver_lazy.h
index b72d53e58..6885dbba4 100644
--- a/src/theory/bv/bv_solver_lazy.h
+++ b/src/theory/bv/bv_solver_lazy.h
@@ -92,8 +92,8 @@ class BVSolverLazy : public BVSolver
 
   std::string identify() const override { return std::string("BVSolverLazy"); }
 
-  Theory::PPAssertStatus ppAssert(TNode in,
-                                  SubstitutionMap& outSubstitutions) override;
+  Theory::PPAssertStatus ppAssert(
+      TrustNode tin, TrustSubstitutionMap& outSubstitutions) override;
 
   TrustNode ppRewrite(TNode t) override;
 
diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
index b7d86cf67..59239a52c 100644
--- a/src/theory/bv/bv_solver_simple.h
+++ b/src/theory/bv/bv_solver_simple.h
@@ -53,8 +53,8 @@ class BVSolverSimple : public BVSolver
 
   std::string identify() const override { return "BVSolverSimple"; };
 
-  Theory::PPAssertStatus ppAssert(TNode in,
-                                  SubstitutionMap& outSubstitutions) override
+  Theory::PPAssertStatus ppAssert(
+      TrustNode in, TrustSubstitutionMap& outSubstitutions) override
   {
     return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED;
   }
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 79a20c9c9..d43fa3927 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -37,7 +37,7 @@ TheoryBV::TheoryBV(context::Context* c,
       d_ufRemByZero(),
       d_rewriter(),
       d_state(c, u, valuation),
-      d_inferMgr(*this, d_state, pnm)
+      d_inferMgr(*this, d_state, nullptr)
 {
   switch (options::bvSolver())
   {
@@ -194,10 +194,10 @@ bool TheoryBV::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
 
 void TheoryBV::propagate(Effort e) { return d_internal->propagate(e); }
 
-Theory::PPAssertStatus TheoryBV::ppAssert(TNode in,
-                                          SubstitutionMap& outSubstitutions)
+Theory::PPAssertStatus TheoryBV::ppAssert(
+    TrustNode tin, TrustSubstitutionMap& outSubstitutions)
 {
-  return d_internal->ppAssert(in, outSubstitutions);
+  return d_internal->ppAssert(tin, outSubstitutions);
 }
 
 TrustNode TheoryBV::ppRewrite(TNode t) { return d_internal->ppRewrite(t); }
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index a01c74382..fa228131c 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -87,7 +87,8 @@ class TheoryBV : public Theory
 
   std::string identify() const override { return std::string("TheoryBV"); }
 
-  PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
+  PPAssertStatus ppAssert(TrustNode in,
+                          TrustSubstitutionMap& outSubstitutions) override;
 
   TrustNode ppRewrite(TNode t) override;