From 054ed31cd3ff5a24322c465189879374dee0b1ca Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 4 Sep 2019 12:51:02 -0500
Subject: [PATCH]  Fixes related to destructing null (#3231)

---
 src/base/exception.cpp       |  4 +--
 src/theory/arith/cut_log.cpp | 52 +++++++++++++++++-------------------
 src/theory/arith/cut_log.h   |  6 ++---
 src/theory/type_set.cpp      | 10 ++-----
 4 files changed, 30 insertions(+), 42 deletions(-)

diff --git a/src/base/exception.cpp b/src/base/exception.cpp
index c1c174d1d..44d9b10bc 100644
--- a/src/base/exception.cpp
+++ b/src/base/exception.cpp
@@ -65,9 +65,7 @@ std::string IllegalArgumentException::formatVariadic(const char* format, ...) {
 
   for (int i = 0; i < 2; ++i){
     Assert(n > 0);
-    if(buf != NULL){
-      delete [] buf;
-    }
+    delete[] buf;
     buf = new char[n];
 
     va_list args_copy;
diff --git a/src/theory/arith/cut_log.cpp b/src/theory/arith/cut_log.cpp
index e9df7559d..43ef97123 100644
--- a/src/theory/arith/cut_log.cpp
+++ b/src/theory/arith/cut_log.cpp
@@ -98,21 +98,19 @@ std::ostream& operator<<(std::ostream& os, const PrimitiveVec& pv){
 }
 
 CutInfo::CutInfo(CutInfoKlass kl, int eid, int o)
-  : d_klass(kl)
-  , d_execOrd(eid)
-  , d_poolOrd(o)
-  , d_cutType(kind::UNDEFINED_KIND)
-  , d_cutRhs()
-  , d_cutVec()
-  , d_mAtCreation(-1)
-  , d_rowId(-1)
-  , d_exactPrecision(NULL)
-  , d_explanation(NULL)
+    : d_klass(kl),
+      d_execOrd(eid),
+      d_poolOrd(o),
+      d_cutType(kind::UNDEFINED_KIND),
+      d_cutRhs(),
+      d_cutVec(),
+      d_mAtCreation(-1),
+      d_rowId(-1),
+      d_exactPrecision(nullptr),
+      d_explanation(nullptr)
 {}
 
 CutInfo::~CutInfo(){
-  if(d_exactPrecision == NULL){ delete d_exactPrecision; }
-  if(d_explanation == NULL){ delete d_explanation; }
 }
 
 int CutInfo::getId() const {
@@ -164,9 +162,7 @@ void CutInfo::setRhs(double r){
   d_cutRhs = r;
 }
 
-bool CutInfo::reconstructed() const{
-  return d_exactPrecision != NULL;
-}
+bool CutInfo::reconstructed() const { return d_exactPrecision != nullptr; }
 
 CutInfoKlass CutInfo::getKlass() const{
   return d_klass;
@@ -190,9 +186,7 @@ int CutInfo::getMAtCreation() const{
 }
 
 /* Returns true if the cut has an explanation. */
-bool CutInfo::proven() const{
-  return d_explanation != NULL;
-}
+bool CutInfo::proven() const { return d_explanation != nullptr; }
 
 bool CutInfo::operator<(const CutInfo& o) const{
   return d_execOrd < o.d_execOrd;
@@ -201,14 +195,17 @@ bool CutInfo::operator<(const CutInfo& o) const{
 
 void CutInfo::setReconstruction(const DenseVector& ep){
   Assert(!reconstructed());
-  d_exactPrecision = new DenseVector(ep);
+  d_exactPrecision.reset(new DenseVector(ep));
 }
 
 void CutInfo::setExplanation(const ConstraintCPVec& ex){
   Assert(reconstructed());
-  if(d_explanation == NULL){
-    d_explanation = new ConstraintCPVec(ex);
-  }else{
+  if (d_explanation == nullptr)
+  {
+    d_explanation.reset(new ConstraintCPVec(ex));
+  }
+  else
+  {
     *d_explanation = ex;
   }
 }
@@ -216,8 +213,9 @@ void CutInfo::setExplanation(const ConstraintCPVec& ex){
 void CutInfo::swapExplanation(ConstraintCPVec& ex){
   Assert(reconstructed());
   Assert(!proven());
-  if(d_explanation == NULL){
-    d_explanation = new ConstraintCPVec();
+  if (d_explanation == nullptr)
+  {
+    d_explanation.reset(new ConstraintCPVec());
   }
   d_explanation->swap(ex);
 }
@@ -229,13 +227,11 @@ const DenseVector& CutInfo::getReconstruction() const {
 
 void CutInfo::clearReconstruction(){
   if(proven()){
-    delete d_explanation;
-    d_explanation = NULL;
+    d_explanation = nullptr;
   }
 
   if(reconstructed()){
-    delete d_exactPrecision;
-    d_exactPrecision = NULL;
+    d_exactPrecision = nullptr;
   }
 
   Assert(!reconstructed());
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index 44553a15b..a5a729f58 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -91,11 +91,11 @@ protected:
    * the cut is stored in exact precision in d_exactPrecision.
    * If the cut has not yet been proven, this is null.
    */
-  DenseVector* d_exactPrecision;
+  std::unique_ptr<DenseVector> d_exactPrecision;
 
-  ConstraintCPVec* d_explanation;
+  std::unique_ptr<ConstraintCPVec> d_explanation;
 
-public:
+ public:
   CutInfo(CutInfoKlass kl, int cutid, int ordinal);
 
   virtual ~CutInfo();
diff --git a/src/theory/type_set.cpp b/src/theory/type_set.cpp
index 616245e2b..0e14f9102 100644
--- a/src/theory/type_set.cpp
+++ b/src/theory/type_set.cpp
@@ -24,18 +24,12 @@ TypeSet::~TypeSet()
   iterator it;
   for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it)
   {
-    if ((*it).second != NULL)
-    {
-      delete (*it).second;
-    }
+    delete (*it).second;
   }
   TypeToTypeEnumMap::iterator it2;
   for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2)
   {
-    if ((*it2).second != NULL)
-    {
-      delete (*it2).second;
-    }
+    delete (*it2).second;
   }
 }
 
-- 
2.30.2