From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 22 Oct 2021 22:21:02 +0000 (-0500)
Subject: Remove stale pointer to proof node manager from skolemize utility (#7471)
X-Git-Tag: cvc5-1.0.0~995
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=76c6a103fb68f75e65201da5bab572f4630cd207;p=cvc5.git

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 830847b74..ccd9afe3e 100644
--- 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 604bc60e4..f1fb78e8d 100644
--- 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;
 };