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.

3 files changed, 0 insertions, 18 deletions

diff --git a/src/options/options.h b/src/options/options.h
index b0dca5748..ef5bea2e3 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -153,7 +153,6 @@ public:
   bool getDumpInstantiations() const;
   bool getDumpModels() const;
   bool getDumpProofs() const;
-  bool getDumpSynth() const;
   bool getDumpUnsatCores() const;
   bool getEarlyExit() const;
   bool getFilesystemAccess() const;
@@ -190,7 +189,6 @@ public:
   void setOut(std::ostream*);
   void setOutputLanguage(OutputLanguage);
 
-  bool wasSetByUserDumpSynth() const;
   bool wasSetByUserEarlyExit() const;
   bool wasSetByUserForceLogicString() const;
   bool wasSetByUserIncrementalSolving() const;
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 4043365b9..61bb36e44 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -66,10 +66,6 @@ bool Options::getDumpProofs() const{
   return (*this)[options::dumpProofs];
 }
 
-bool Options::getDumpSynth() const{
-  return (*this)[options::dumpSynth];
-}
-
 bool Options::getDumpUnsatCores() const{
   // dump unsat cores full enables dumpUnsatCores
   return (*this)[options::dumpUnsatCores]
@@ -213,10 +209,6 @@ void Options::setOutputLanguage(OutputLanguage value) {
   set(options::outputLanguage, value);
 }
 
-bool Options::wasSetByUserDumpSynth() const {
-  return wasSetByUser(options::dumpSynth);
-}
-
 bool Options::wasSetByUserEarlyExit() const {
   return wasSetByUser(options::earlyExit);
 }
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index b01b7780f..247559c91 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -233,14 +233,6 @@ header = "options/smt_options.h"
   help       = "use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging)"
 
 [[option]]
-  name       = "dumpSynth"
-  category   = "regular"
-  long       = "dump-synth"
-  type       = "bool"
-  default    = "false"
-  help       = "output solution for synthesis conjectures after every UNSAT/VALID response"
-
-[[option]]
   name       = "unsatCores"
   category   = "regular"
   long       = "produce-unsat-cores"