Fixes memory leak when an exception goes through runCvc4(). (Fixes #4590) (#4750)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Thu, 16 Jul 2020 04:34:14 +0000 (06:34 +0200)
committerGitHub <noreply@github.com>
Thu, 16 Jul 2020 04:34:14 +0000 (21:34 -0700)
commit81821f40c36a6ccbee4bf6ef500cd5dccacb634c
treee3cfdc8797ed86143a351bf20883a803f76143b5
parent699af1774b7ddae0b1a8337cb4cd02532a6ad8b0
Fixes memory leak when an exception goes through runCvc4(). (Fixes #4590) (#4750)

As noted in #4590, CVC4 may leak memory if an exception is thrown that interrupts the command execution loop in runCvc4().
While not a major issue (the binary is terminated anyway in this case, this is also why we label it as feature), we should fix it nevertheless.

This commit makes sure that the current command is properly managed by using `std::unique_ptr` to handle its deletion.
src/main/command_executor.cpp
src/main/command_executor.h
src/main/driver_unified.cpp