From f591f7c1671b8345b56c8d3e3adef9627c5fa8c1 Mon Sep 17 00:00:00 2001
From: Liana Hadarean <lianahady@gmail.com>
Date: Mon, 16 Mar 2015 14:31:21 +0100
Subject: [PATCH] Fixed proof unitialized memory and minor memory leaks.

---
 src/proof/proof_manager.cpp |  7 +++++++
 src/proof/sat_proof.cpp     | 21 +++++++++++++--------
 src/proof/sat_proof.h       |  2 +-
 src/smt/smt_engine.cpp      |  3 +++
 4 files changed, 24 insertions(+), 9 deletions(-)

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 4bff66b92..0f9cfa710 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -45,6 +45,13 @@ ProofManager::ProofManager(ProofFormat format):
   d_satProof(NULL),
   d_cnfProof(NULL),
   d_theoryProof(NULL),
+  d_inputClauses(),
+  d_theoryLemmas(),
+  d_theoryPropagations(),
+  d_inputFormulas(),
+  d_inputCoreFormulas(),
+  d_outputCoreFormulas(),
+  d_nextId(0),
   d_fullProof(NULL),
   d_format(format),
   d_deps(),
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index 2c86d45a4..3077f08ed 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -167,6 +167,7 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) :
     d_idClause(),
     d_clauseId(),
     d_idUnit(),
+    d_unitId(),
     d_deleted(),
     d_inputClauses(),
     d_lemmaClauses(),
@@ -185,6 +186,9 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) :
   {
     d_proxy = new ProofProxy(this);
   }
+SatProof::~SatProof() {
+  delete d_proxy;
+}
 
 /**
  * Returns true if the resolution chain corresponding to id
@@ -365,15 +369,15 @@ ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind, uint6
   ClauseIdMap::iterator it = d_clauseId.find(clause);
   if (it == d_clauseId.end()) {
     ClauseId newId = ProofManager::currentPM()->nextId();
-    d_clauseId[clause] = newId;
-    d_idClause[newId] = clause;
+    d_clauseId.insert(ClauseIdMap::value_type(clause, newId)); 
+    d_idClause.insert(IdCRefMap::value_type(newId, clause));
     if (kind == INPUT) {
       Assert(d_inputClauses.find(newId) == d_inputClauses.end());
-      d_inputClauses[newId] = proof_id;
+      d_inputClauses.insert(IdProofRuleMap::value_type(newId, proof_id));
     }
     if (kind == THEORY_LEMMA) {
       Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
-      d_lemmaClauses[newId] = proof_id;
+      d_lemmaClauses.insert(IdProofRuleMap::value_type(newId, proof_id));
     }
   }
   Debug("proof:sat:detailed") << "registerClause CRef:" << clause << " id:" << d_clauseId[clause] << " " << kind << " " << int32_t((proof_id >> 32) & 0xffffffff) << "\n";
@@ -386,15 +390,16 @@ ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind, uint6
   UnitIdMap::iterator it = d_unitId.find(toInt(lit));
   if (it == d_unitId.end()) {
     ClauseId newId = ProofManager::currentPM()->nextId();
-    d_unitId[toInt(lit)] = newId;
-    d_idUnit[newId] = lit;
+    d_unitId.insert(UnitIdMap::value_type(toInt(lit), newId));
+    d_idUnit.insert(IdUnitMap::value_type(newId, lit));
+
     if (kind == INPUT) {
       Assert(d_inputClauses.find(newId) == d_inputClauses.end());
-      d_inputClauses[newId] = proof_id;
+      d_inputClauses.insert(IdProofRuleMap::value_type(newId, proof_id));
     }
     if (kind == THEORY_LEMMA) {
       Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
-      d_lemmaClauses[newId] = proof_id;
+      d_lemmaClauses.insert(IdProofRuleMap::value_type(newId, proof_id));
     }
   }
   Debug("proof:sat:detailed") << "registerUnitClause " << d_unitId[toInt(lit)] << " " << kind << "\n";
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index ef4e7a5aa..7c195c83d 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -139,7 +139,7 @@ protected:
   bool d_storedUnitConflict;
 public:
   SatProof(::Minisat::Solver* solver, bool checkRes = false);
-  virtual ~SatProof() {}
+  virtual ~SatProof();
 protected:
   void print(ClauseId id);
   void printRes(ClauseId id);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index eb7792d2c..3e4afc0c9 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -864,6 +864,9 @@ SmtEngine::~SmtEngine() throw() {
     delete d_decisionEngine;
     d_decisionEngine = NULL;
 
+    PROOF(delete d_proofManager;);
+    PROOF(d_proofManager = NULL;);
+    
     delete d_stats;
     d_stats = NULL;
     delete d_statisticsRegistry;
-- 
2.30.2