From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 5 Sep 2018 21:31:11 +0000 (-0700)
Subject: Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432)
X-Git-Tag: cvc5-1.0.0~4677
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=90b90bdfad8c5fbf0f3208e7282fee6dd58aafc0;p=cvc5.git

Use std::uniqe_ptr for d_eq_infer to make Coverity happy. (#2432)
---

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index d4a59b4b0..bf251660d 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -28,35 +28,36 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, SetupLiteralCallBack setup, const ArithVariables& avars, RaiseEqualityEngineConflict raiseConflict)
-  : d_inConflict(c),
-    d_raiseConflict(raiseConflict),
-    d_notify(*this),
-    d_eq_infer(NULL),
-    d_eqi_counter(0,c),
-    d_keepAlive(c),
-    d_propagatations(c),
-    d_explanationMap(c),
-    d_constraintDatabase(cd),
-    d_setupLiteral(setup),
-    d_avariables(avars),
-    d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true)
+ArithCongruenceManager::ArithCongruenceManager(
+    context::Context* c,
+    ConstraintDatabase& cd,
+    SetupLiteralCallBack setup,
+    const ArithVariables& avars,
+    RaiseEqualityEngineConflict raiseConflict)
+    : d_inConflict(c),
+      d_raiseConflict(raiseConflict),
+      d_notify(*this),
+      d_eq_infer(),
+      d_eqi_counter(0, c),
+      d_keepAlive(c),
+      d_propagatations(c),
+      d_explanationMap(c),
+      d_constraintDatabase(cd),
+      d_setupLiteral(setup),
+      d_avariables(avars),
+      d_ee(d_notify, c, "theory::arith::ArithCongruenceManager", true)
 {
   d_ee.addFunctionKind(kind::NONLINEAR_MULT);
   d_ee.addFunctionKind(kind::EXPONENTIAL);
   d_ee.addFunctionKind(kind::SINE);
   //module to infer additional equalities based on normalization
   if( options::sNormInferEq() ){
-    d_eq_infer = new quantifiers::EqualityInference(c, true);
+    d_eq_infer.reset(new quantifiers::EqualityInference(c, true));
     d_true = NodeManager::currentNM()->mkConst( true );
   }
 }
 
-ArithCongruenceManager::~ArithCongruenceManager() {
-  if( d_eq_infer ){
-    delete d_eq_infer;
-  }
-}
+ArithCongruenceManager::~ArithCongruenceManager() {}
 
 ArithCongruenceManager::Statistics::Statistics():
   d_watchedVariables("theory::arith::congruence::watchedVariables", 0),
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 278c79a2f..11c229399 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -77,10 +77,11 @@ private:
     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override;
   };
   ArithCongruenceNotify d_notify;
-  
-  /** module for shostak normalization, d_eqi_counter is how many pending merges in d_eq_infer we have processed */
-  quantifiers::EqualityInference * d_eq_infer;
-  context::CDO< unsigned > d_eqi_counter;
+
+  /** module for shostak normalization, d_eqi_counter is how many pending merges
+   * in d_eq_infer we have processed */
+  std::unique_ptr<quantifiers::EqualityInference> d_eq_infer;
+  context::CDO<unsigned> d_eqi_counter;
   Node d_true;
 
   context::CDList<Node> d_keepAlive;