diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2018-08-23 16:09:16 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-08-23 16:09:16 -0500 |
| commit | e9e15423971126408d06c705ac715433671e72cf (patch) | |
| tree | 99e131fe292c5871b0cdf4ca9691c8d36f68664a /src/main/command_executor.h | |
| parent | 408bccf70b41b1f41c8be04ffe7f7002fb57e182 (diff) | |
Makes the filename be set in the SMT engine by default (#2366)
Diffstat (limited to 'src/main/command_executor.h')
| -rw-r--r-- | src/main/command_executor.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/main/command_executor.h b/src/main/command_executor.h index 7e7202a5a..f8c6e6e5a 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -69,6 +69,8 @@ public: return d_stats; } + SmtEngine* getSmtEngine() { return d_smtEngine; } + /** * Flushes statistics to a file descriptor. */ |