From 5854353603d5a3ce7e3a5914f1b6d29728d24ac2 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Tue, 26 Sep 2017 07:33:31 -0700
Subject: [PATCH] Fixing CID 1362903: Initializing d_bvp to nullptr. (#1136)

---
 src/theory/bv/bv_subtheory.h | 61 +++++++++++++++++++-----------------
 1 file changed, 32 insertions(+), 29 deletions(-)

diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 4f074a202..deb366a99 100644
--- 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 */
-- 
2.30.2