2 files changed, 6 insertions, 0 deletions
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 52522d591..460274515 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -139,6 +139,9 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
           res.asSatisfiabilityResult() == Result::UNSAT ) ) {
       g = new GetInstantiationsCommand();
     }
+    if( d_options[options::dumpSynth] && res.asSatisfiabilityResult() == Result::UNSAT ){
+      g = new GetSynthSolutionCommand();
+    }
     if( d_options[options::dumpUnsatCores] && res.asSatisfiabilityResult() == Result::UNSAT ) {
       g = new GetUnsatCoreCommand();
     }
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 610902270..e4effd239 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -378,6 +378,9 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
                  d_result.asSatisfiabilityResult() == Result::UNSAT ) ) {
         Command* gi = new GetInstantiationsCommand();
         status = doCommandSingleton(gi);
+      } else if( d_options[options::dumpSynth] && d_result.asSatisfiabilityResult() == Result::UNSAT ){
+        Command* gi = new GetSynthSolutionCommand();
+        status = doCommandSingleton(gi);
       } else if( d_options[options::dumpUnsatCores] &&
                  d_result.asSatisfiabilityResult() == Result::UNSAT ) {
         Command* guc = new GetUnsatCoreCommand();