Dumping unsat cores after check-sat-assuming/QUERY (#5724)

Previously we were not printing unsat cores when passing the option to dump them if we used the check-sat-assuming command or the QUERY command. This commit fixes this.

It also kills the redundant dump-synth option, as it simplifies a bit what is going on in the command executor.

1 files changed, 11 insertions, 12 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index fe4af6361..04ed5147a 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -136,14 +136,16 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   if(cs != nullptr) {
     d_result = res = cs->getResult();
   }
+  const CheckSatAssumingCommand* csa =
+      dynamic_cast<const CheckSatAssumingCommand*>(cmd);
+  if (csa != nullptr)
+  {
+    d_result = res = csa->getResult();
+  }
   const QueryCommand* q = dynamic_cast<const QueryCommand*>(cmd);
   if(q != nullptr) {
     d_result = res = q->getResult();
   }
- const  CheckSynthCommand* csy = dynamic_cast<const CheckSynthCommand*>(cmd);
-  if(csy != nullptr) {
-    d_result = res = csy->getResult();
-  }
 
   if((cs != nullptr || q != nullptr) && d_options.getStatsEveryQuery()) {
     std::ostringstream ossCurStats;
@@ -153,6 +155,8 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     d_lastStatistics = ossCurStats.str();
   }
 
+  bool isResultUnsat = res.isUnsat() || res.isEntailed();
+
   // dump the model/proof/unsat core if option is set
   if (status) {
     std::vector<std::unique_ptr<Command> > getterCommands;
@@ -163,7 +167,7 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
     {
       getterCommands.emplace_back(new GetModelCommand());
     }
-    if (d_options.getDumpProofs() && res.isUnsat())
+    if (d_options.getDumpProofs() && isResultUnsat)
     {
       getterCommands.emplace_back(new GetProofCommand());
     }
@@ -173,17 +177,12 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
              && (res.isSat()
                  || (res.isSatUnknown()
                      && res.getResult().whyUnknown() == Result::INCOMPLETE)))
-            || res.isUnsat()))
+            || isResultUnsat))
     {
       getterCommands.emplace_back(new GetInstantiationsCommand());
     }
 
-    if (d_options.getDumpSynth() && res.isUnsat())
-    {
-      getterCommands.emplace_back(new GetSynthSolutionCommand());
-    }
-
-    if (d_options.getDumpUnsatCores() && res.isUnsat())
+    if (d_options.getDumpUnsatCores() && isResultUnsat)
     {
       getterCommands.emplace_back(new GetUnsatCoreCommand());
     }