Fixed proof unitialized memory and minor memory leaks.

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 4bff66b9244ebce06c6f3f5b526dde785ae15a16..0f9cfa71090297d04480e9ee883b942f1be2e081 100644 (file)
--- 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 2c86d45a4b545dd17df493149824167175306d7b..3077f08ed993b620395dc5452798383267b60a13 100644 (file)
--- 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 ef4e7a5aa8d9b1ca655381782c1c932d30a38ce1..7c195c83ddc8d7a936368d6b530fc64eb043d034 100644 (file)
--- 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 eb7792d2cb1284d1d53e7bb3462fac0a52f69e4b..3e4afc0c9fec5947c2f2e14f9c4cc52a1dcc692a 100644 (file)
--- 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;