Remove stale pointer to proof node manager from skolemize utility (#7471)

Issue was introduced when cleaning this utility to the new style (to not take explicit pnm).

diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index 830847b741f493e348f58265a4632331d9ce30f4..ccd9afe3eef68fff98b31171f919bfe83575e45e 100644 (file)
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -62,6 +62,7 @@ TrustNode Skolemize::process(Node q)
   if (isProofEnabled() && !options::dtStcInduction()
       && !options::intWfInduction())
   {
+    ProofNodeManager * pnm = d_env.getProofNodeManager();
     // if using proofs and not using induction, we use the justified
     // skolemization
     NodeManager* nm = NodeManager::currentNM();
@@ -71,12 +72,12 @@ TrustNode Skolemize::process(Node q)
     Node existsq = nm->mkNode(EXISTS, echildren);
     Node res = skm->mkSkolemize(existsq, d_skolem_constants[q], "skv");
     Node qnot = q.notNode();
-    CDProof cdp(d_pnm);
+    CDProof cdp(pnm);
     cdp.addStep(res, PfRule::SKOLEMIZE, {qnot}, {});
     std::shared_ptr<ProofNode> pf = cdp.getProofFor(res);
     std::vector<Node> assumps;
     assumps.push_back(qnot);
-    std::shared_ptr<ProofNode> pfs = d_pnm->mkScope({pf}, assumps);
+    std::shared_ptr<ProofNode> pfs = pnm->mkScope({pf}, assumps);
     lem = nm->mkNode(IMPLIES, qnot, res);
     d_epg->setProofFor(lem, pfs);
     pg = d_epg.get();

diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index 604bc60e46677405d421a193c4b91430682a00a3..f1fb78e8d692a627bd76883785948c557c85a2cf 100644 (file)
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -149,8 +149,6 @@ class Skolemize : protected EnvObj
   std::unordered_map<Node, std::vector<Node>> d_skolem_constants;
   /** map from quantified formulas to their skolemized body */
   std::unordered_map<Node, Node> d_skolem_body;
-  /** Pointer to the proof node manager */
-  ProofNodeManager* d_pnm;
   /** Eager proof generator for skolemization lemmas */
   std::unique_ptr<EagerProofGenerator> d_epg;
 };