Fix issue #1081, memory leak in cmd executor (#1109)
authorAndres Noetzli <andres.noetzli@gmail.com>
Wed, 20 Sep 2017 18:24:13 +0000 (11:24 -0700)
committerGitHub <noreply@github.com>
Wed, 20 Sep 2017 18:24:13 +0000 (11:24 -0700)
commit54ed57102bbd35241c68d128f88bf2b93dd236cf
tree3e98176560c7867e545aac203cae25c6f527b32a
parent480df3b40de9650387c5fceb9aee39311753e3ab
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.
src/main/command_executor.cpp