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 d4a59b4b0f9d35317f1216ff61714c4c5fa47b10..bf251660de1682d22f2e1f50784c4417e906a0e7 100644 (file)
--- 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 278c79a2fe74d40096f50dd1fbfbb71bdd5d676f..11c2293990559c92a2b04b86567604c825705008 100644 (file)
--- 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;