From 5d600cd2df87f81ec19034a79e7fe4eea9482b4c Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Mon, 21 Mar 2016 22:16:45 -0700
Subject: [PATCH] Deleting the contents of d_modelGlobalsCommands before it is
 cleared.

---
 src/smt/smt_engine.cpp | 15 +++++++++++++--
 src/smt/smt_engine.h   |  4 ++--
 2 files changed, 15 insertions(+), 4 deletions(-)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0a2f50a78..5e97158ca 100644
--- 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 74ff0edb3..0a8f8099f 100644
--- 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).
    */
-- 
2.30.2