Fixing CID 1362903: Initializing d_bvp to nullptr. (#1136)

diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 4f074a202b9eb3e8d6154ced855a02384652fa3c..deb366a9952b1afdccd3f22a11743c5324f61842 100644 (file)
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -60,32 +60,20 @@ inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) {
 // forward declaration
 class TheoryBV;
 
-typedef context::CDQueue<Node> AssertionQueue;
+using AssertionQueue = context::CDQueue<Node>;
+
 /**
  * Abstract base class for bit-vector subtheory solvers
  *
  */
 class SubtheorySolver {
-
-protected:
-
-  /** The context we are using */
-  context::Context* d_context;
-
-  /** The bit-vector theory */
-  TheoryBV* d_bv;
-  /** proof log */
-  BitVectorProof * d_bvp;
-  AssertionQueue d_assertionQueue;
-  context::CDO<uint32_t>  d_assertionIndex;
-public:
-
-  SubtheorySolver(context::Context* c, TheoryBV* bv) :
-    d_context(c),
-    d_bv(bv),
-    d_assertionQueue(c),
-    d_assertionIndex(c, 0)
-  {}
+ public:
+  SubtheorySolver(context::Context* c, TheoryBV* bv)
+      : d_context(c),
+        d_bv(bv),
+        d_bvp(nullptr),
+        d_assertionQueue(c),
+        d_assertionIndex(c, 0) {}
   virtual ~SubtheorySolver() {}
   virtual bool check(Theory::Effort e) = 0;
   virtual void explain(TNode literal, std::vector<TNode>& assumptions) = 0;
@@ -98,19 +86,34 @@ public:
   virtual void addSharedTerm(TNode node) {}
   bool done() { return d_assertionQueue.size() == d_assertionIndex; }
   TNode get() {
-    Assert (!done());
+    Assert(!done());
     TNode res = d_assertionQueue[d_assertionIndex];
     d_assertionIndex = d_assertionIndex + 1;
     return res;
   }
   virtual void assertFact(TNode fact) { d_assertionQueue.push_back(fact); }
-  virtual void setProofLog( BitVectorProof * bvp ) {}
-  AssertionQueue::const_iterator assertionsBegin() { return d_assertionQueue.begin(); }
-  AssertionQueue::const_iterator assertionsEnd() { return d_assertionQueue.end(); }
-};
+  virtual void setProofLog(BitVectorProof* bvp) {}
+  AssertionQueue::const_iterator assertionsBegin() {
+    return d_assertionQueue.begin();
+  }
+  AssertionQueue::const_iterator assertionsEnd() {
+    return d_assertionQueue.end();
+  }
 
-}
-}
-}
+ protected:
+  /** The context we are using */
+  context::Context* d_context;
+
+  /** The bit-vector theory */
+  TheoryBV* d_bv;
+  /** proof log */
+  BitVectorProof* d_bvp;
+  AssertionQueue d_assertionQueue;
+  context::CDO<uint32_t> d_assertionIndex;
+}; /* class SubtheorySolver */
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4
 
 #endif /* __CVC4__THEORY__BV__BV_SUBTHEORY_H */