2 files changed, 24 insertions, 26 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 320be701d..f9055f56c 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -129,47 +129,43 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   }
 
   // dump the model/proof/unsat core if option is set
-  if(status) {
+  if (status) {
     Command* g = NULL;
-    if( d_options.getProduceModels() &&
-        d_options.getDumpModels() &&
-        ( res.asSatisfiabilityResult() == Result::SAT ||
-          (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
+    if (d_options.getProduceModels() && d_options.getDumpModels() &&
+        (res.asSatisfiabilityResult() == Result::SAT ||
+         (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE))) {
       g = new GetModelCommand();
     }
-    if( d_options.getProof() &&
-        d_options.getDumpProofs() &&
-        res.asSatisfiabilityResult() == Result::UNSAT ) {
+    if (d_options.getProof() && d_options.getDumpProofs() &&
+        res.asSatisfiabilityResult() == Result::UNSAT) {
       g = new GetProofCommand();
     }
 
-    if( d_options.getDumpInstantiations() &&
-        ( ( d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS &&
-            ( res.asSatisfiabilityResult() == Result::SAT ||
-              (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) ||
-          res.asSatisfiabilityResult() == Result::UNSAT ) )
-    {
+    if (d_options.getDumpInstantiations() &&
+        ((d_options.getInstFormatMode() != INST_FORMAT_MODE_SZS &&
+          (res.asSatisfiabilityResult() == Result::SAT ||
+           (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE))) ||
+         res.asSatisfiabilityResult() == Result::UNSAT)) {
       g = new GetInstantiationsCommand();
     }
 
-    if( d_options.getDumpSynth() &&
-        res.asSatisfiabilityResult() == Result::UNSAT )
-    {
+    if (d_options.getDumpSynth() &&
+        res.asSatisfiabilityResult() == Result::UNSAT) {
       g = new GetSynthSolutionCommand();
     }
 
-    if( d_options.getDumpUnsatCores() &&
-        res.asSatisfiabilityResult() == Result::UNSAT )
-    {
+    if (d_options.getDumpUnsatCores() &&
+        res.asSatisfiabilityResult() == Result::UNSAT) {
       g = new GetUnsatCoreCommand();
     }
 
-    if(g != NULL) {
+    if (g != NULL) {
       // set no time limit during dumping if applicable
-      if( d_options.getForceNoLimitCpuWhileDump() ){
+      if (d_options.getForceNoLimitCpuWhileDump()) {
         setNoLimitCPU();
       }
       status = doCommandSingleton(g);
+      delete g;
     }
   }
   return status;
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 1902e1817..bd8b6a9ed 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -277,11 +277,13 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
      * set of variables mapped.)
      */
     if(d_numThreads >= 2) {
-      for(typeof(d_vmaps[1]->d_to.begin()) i=d_vmaps[1]->d_to.begin();
-          i!=d_vmaps[1]->d_to.end(); ++i) {
-        (d_vmaps[0]->d_from)[i->first] = i->first;
+      VarMap& thread_0_from = d_vmaps[0]->d_from;
+      VarMap& thread_1_to = d_vmaps[1]->d_to;
+      for(VarMap::iterator i=thread_1_to.begin();
+          i != thread_1_to.end(); ++i) {
+        thread_0_from[i->first] = i->first;
       }
-      d_vmaps[0]->d_to = d_vmaps[0]->d_from;
+      d_vmaps[0]->d_to = thread_0_from;
     }
 
     lemmaSharingInit();