Deleting the contents of d_modelGlobalsCommands before it is cleared.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0a2f50a78ff4715bdb3464c9cab7eaafd38045ea..5e97158cae2a3e23a0ad36ec9f0f55f371a9b6c7 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -110,9 +110,18 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 
 namespace CVC4 {
-
 namespace smt {
 
+struct DeleteCommandFunction : public std::unary_function<const Command*, void>
+{
+  void operator()(const Command* command) { delete command; }
+};
+
+void DeleteAndClearCommandVector(std::vector<Command*>& commands) {
+  std::for_each(commands.begin(), commands.end(), DeleteCommandFunction());
+  commands.clear();
+}
+
 /** Useful for counting the number of recursive calls. */
 class ScopeCounter {
 private:
@@ -1194,6 +1203,8 @@ SmtEngine::~SmtEngine() throw() {
     }
     d_dumpCommands.clear();
 
+    DeleteAndClearCommandVector(d_modelGlobalCommands);
+
     if(d_modelCommands != NULL) {
       d_modelCommands->deleteSelf();
     }
@@ -5295,7 +5306,7 @@ void SmtEngine::resetAssertions() throw() {
   Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1);
   d_context->popto(0);
   d_userContext->popto(0);
-  d_modelGlobalCommands.clear();
+  DeleteAndClearCommandVector(d_modelGlobalCommands);
   d_userContext->push();
   d_context->push();
 }

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 74ff0edb3ca2454cdb15dd60ad2da48521265391..0a8f8099ff8914666c087b3f46a646ea97de0675 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -244,11 +244,11 @@ class CVC4_PUBLIC SmtEngine {
   bool d_needPostsolve;
 
   /*
-   * Whether to call theory preprocessing during simplification - on by default* but gets turned off if arithRewriteEq is on
+   * Whether to call theory preprocessing during simplification - on
+   * by default* but gets turned off if arithRewriteEq is on
    */
   bool d_earlyTheoryPP;
 
-
   /**
    * Most recent result of last checkSat/query or (set-info :status).
    */