2 files changed, 28 insertions, 11 deletions
diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp
index a55adaace..ea7ba1a13 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.cpp
+++ b/src/theory/bv/bitblast/proof_bitblaster.cpp
@@ -16,7 +16,6 @@
 
 #include <unordered_set>
 
-#include "options/proof_options.h"
 #include "proof/conv_proof_generator.h"
 #include "theory/theory_model.h"
 
@@ -68,10 +67,23 @@ std::unordered_map<Kind, PfRule, kind::KindHashFunction>
         {kind::BITVECTOR_ROTATE_LEFT, PfRule::BV_BITBLAST_ROTATE_LEFT},
 };
 
-BBProof::BBProof(TheoryState* state,
-                 ProofNodeManager* pnm,
-                 TConvProofGenerator* tcpg)
-    : d_bb(new BBSimple(state)), d_pnm(pnm), d_tcpg(tcpg)
+BBProof::BBProof(TheoryState* state, ProofNodeManager* pnm, bool fineGrained)
+    : d_bb(new BBSimple(state)),
+      d_pnm(pnm),
+      d_tcpg(pnm ? new TConvProofGenerator(
+                 pnm,
+                 nullptr,
+                 /* ONCE to visit each term only once, post-order.  FIXPOINT
+                  * could lead to infinite loops due to terms being rewritten
+                  * to terms that contain themselves */
+                 TConvPolicy::ONCE,
+                 /* STATIC to get the same ProofNode for a shared subterm. */
+                 TConvCachePolicy::STATIC,
+                 "BBProof::TConvProofGenerator",
+                 nullptr,
+                 false)
+                 : nullptr),
+      d_recordFineGrainedProofs(fineGrained)
 {
 }
 
@@ -83,9 +95,7 @@ void BBProof::bbAtom(TNode node)
   visit.push_back(node);
   std::unordered_set<TNode> visited;
 
-  bool fproofs =
-      options::proofGranularityMode() != options::ProofGranularityMode::OFF;
-  bool fpenabled = isProofsEnabled() && fproofs;
+  bool fpenabled = isProofsEnabled() && d_recordFineGrainedProofs;
 
   NodeManager* nm = NodeManager::currentNM();
 
@@ -183,7 +193,8 @@ void BBProof::bbAtom(TNode node)
       visit.pop_back();
     }
   }
-  if (isProofsEnabled() && !fproofs)
+  /* Record coarse-grain bit-blast proof step. */
+  if (isProofsEnabled() && !d_recordFineGrainedProofs)
   {
     Node node_tobv = getStoredBBAtom(node);
     d_tcpg->addRewriteStep(node,
@@ -210,6 +221,8 @@ bool BBProof::collectModelValues(TheoryModel* m,
   return d_bb->collectModelValues(m, relevantTerms);
 }
 
+TConvProofGenerator* BBProof::getProofGenerator() { return d_tcpg.get(); }
+
 bool BBProof::isProofsEnabled() const { return d_pnm != nullptr; }
 
 }  // namespace bv
diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h
index ef23c05c0..86cbeae81 100644
--- a/src/theory/bv/bitblast/proof_bitblaster.h
+++ b/src/theory/bv/bitblast/proof_bitblaster.h
@@ -31,7 +31,7 @@ class BBProof
   using Bits = std::vector<Node>;
 
  public:
-  BBProof(TheoryState* state, ProofNodeManager* pnm, TConvProofGenerator* tcpg);
+  BBProof(TheoryState* state, ProofNodeManager* pnm, bool fineGrained);
   ~BBProof();
 
   /** Bit-blast atom 'node'. */
@@ -45,6 +45,8 @@ class BBProof
   /** Collect model values for all relevant terms given in 'relevantTerms'. */
   bool collectModelValues(TheoryModel* m, const std::set<Node>& relevantTerms);
 
+  TConvProofGenerator* getProofGenerator();
+
  private:
   /** Map node kinds to proof rules. */
   static std::unordered_map<Kind, PfRule, kind::KindHashFunction>
@@ -58,9 +60,11 @@ class BBProof
   /** The associated proof node manager. */
   ProofNodeManager* d_pnm;
   /** The associated term conversion proof generator. */
-  TConvProofGenerator* d_tcpg;
+  std::unique_ptr<TConvProofGenerator> d_tcpg;
   /** Map bit-vector nodes to bit-blasted nodes. */
   std::unordered_map<Node, Node> d_bbMap;
+
+  bool d_recordFineGrainedProofs;
 };
 
 }  // namespace bv