Fix issue #1081, memory leak in cmd executor (#1109)

The variable `g` could be set multiple times depending on
the options (e.g. a combination of `--dump-unsat-cores`
and `--dump-synth`), which could lead to memory leaks and
missing output. This commit fixes the issue by replacing
`g` with a list of `getterCommands` that are all executed and
deleted.

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index a18bb1fe4c20955aa10939a1c63615f985870276..7c8ee7827d6bf944d5a9ff62299e47acfd0f41e6 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -20,7 +20,9 @@
 
 #include <cassert>
 #include <iostream>
+#include <memory>
 #include <string>
+#include <vector>
 
 #include "main/main.h"
 #include "smt/command.h"
@@ -130,15 +132,15 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
 
   // dump the model/proof/unsat core if option is set
   if (status) {
-    Command* g = NULL;
+    std::vector<std::unique_ptr<Command> > getterCommands;
     if (d_options.getProduceModels() && d_options.getDumpModels() &&
         (res.asSatisfiabilityResult() == Result::SAT ||
          (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE))) {
-      g = new GetModelCommand();
+      getterCommands.emplace_back(new GetModelCommand());
     }
     if (d_options.getProof() && d_options.getDumpProofs() &&
         res.asSatisfiabilityResult() == Result::UNSAT) {
-      g = new GetProofCommand();
+      getterCommands.emplace_back(new GetProofCommand());
     }
 
     if (d_options.getDumpInstantiations() &&
@@ -146,26 +148,30 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
           (res.asSatisfiabilityResult() == Result::SAT ||
            (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE))) ||
          res.asSatisfiabilityResult() == Result::UNSAT)) {
-      g = new GetInstantiationsCommand();
+      getterCommands.emplace_back(new GetInstantiationsCommand());
     }
 
     if (d_options.getDumpSynth() &&
         res.asSatisfiabilityResult() == Result::UNSAT) {
-      g = new GetSynthSolutionCommand();
+      getterCommands.emplace_back(new GetSynthSolutionCommand());
     }
 
     if (d_options.getDumpUnsatCores() &&
         res.asSatisfiabilityResult() == Result::UNSAT) {
-      g = new GetUnsatCoreCommand();
+      getterCommands.emplace_back(new GetUnsatCoreCommand());
     }
 
-    if (g != NULL) {
+    if (!getterCommands.empty()) {
       // set no time limit during dumping if applicable
       if (d_options.getForceNoLimitCpuWhileDump()) {
         setNoLimitCPU();
       }
-      status = doCommandSingleton(g);
-      delete g;
+      for (const auto& getterCommand : getterCommands) {
+        status = doCommandSingleton(getterCommand.get());
+        if (!status && !d_options.getContinuedExecution()) {
+          break;
+        }
+      }
     }
   }
   return status;