From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 3 Nov 2017 20:36:38 +0000 (-0500)
Subject: Sygus clean main (#1297)
X-Git-Tag: cvc5-1.0.0~5514
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5cafed748989602263b8ad1a27ac6b9bd159a441;p=cvc5.git

Sygus clean main (#1297)

* Remove front end hack for sygus.

* Remove other hack, add sygus solution output mode.

* Clang format

* Minor

* Fix

* Minor

* Remove unused field.
---

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 8ffb47e40..ebfc7266b 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -187,16 +187,6 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage()));
   }
 
-  // if doing sygus, turn on CEGQI by default
-  if(opts.getInputLanguage() == language::input::LANG_SYGUS ){
-    if( !opts.wasSetByUserCeGuidedInst()) {
-      opts.setCeGuidedInst(true);
-    }
-    if( !opts.wasSetByUserDumpSynth()) {
-      opts.setDumpSynth(true);
-    }
-  }
-
   // Determine which messages to show based on smtcomp_mode and verbosity
   if(Configuration::isMuzzledBuild()) {
     DebugChannel.setStream(&CVC4::null_os);
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index ff889bcb2..54027c128 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -252,6 +252,7 @@ liboptions_la_SOURCES = \
 	set_language.h \
 	simplification_mode.cpp \
 	simplification_mode.h \
+	sygus_out_mode.h \
 	theoryof_mode.cpp \
 	theoryof_mode.h \
 	ufss_mode.h
diff --git a/src/options/options.h b/src/options/options.h
index f93663095..474ef0f96 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -242,8 +242,6 @@ public:
 
 
   // TODO: Document these.
-  void setCeGuidedInst(bool);
-  void setDumpSynth(bool);
   void setInputLanguage(InputLanguage);
   void setInteractive(bool);
   void setOut(std::ostream*);
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 351c8b608..3d74091fd 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -554,7 +554,6 @@ all \n\
 \n\
 ";
 
-
 theory::quantifiers::InstWhenMode OptionsHandler::stringToInstWhenMode(std::string option, std::string optarg) throw(OptionException) {
   if(optarg == "pre-full") {
     return theory::quantifiers::INST_WHEN_PRE_FULL;
@@ -1311,6 +1310,56 @@ SimplificationMode OptionsHandler::stringToSimplificationMode(std::string option
   }
 }
 
+const std::string OptionsHandler::s_sygusSolutionOutModeHelp =
+    "\
+Modes for finite model finding bound minimization, supported by --sygus-out:\n\
+\n\
+status \n\
++ Print only status for check-synth calls.\n\
+\n\
+status-and-def (default) \n\
++ Print status followed by definition corresponding to solution.\n\
+\n\
+status-or-def \n\
++ Print status if infeasible, or definition corresponding to\n\
+  solution if feasible.\n\
+\n\
+sygus-standard \n\
++ Print based on SyGuS standard.\n\
+\n\
+";
+
+SygusSolutionOutMode OptionsHandler::stringToSygusSolutionOutMode(
+    std::string option, std::string optarg) throw(OptionException)
+{
+  if (optarg == "status")
+  {
+    return SYGUS_SOL_OUT_STATUS;
+  }
+  else if (optarg == "status-and-def")
+  {
+    return SYGUS_SOL_OUT_STATUS_AND_DEF;
+  }
+  else if (optarg == "status-or-def")
+  {
+    return SYGUS_SOL_OUT_STATUS_OR_DEF;
+  }
+  else if (optarg == "sygus-standard")
+  {
+    return SYGUS_SOL_OUT_STANDARD;
+  }
+  else if (optarg == "help")
+  {
+    puts(s_sygusSolutionOutModeHelp.c_str());
+    exit(1);
+  }
+  else
+  {
+    throw OptionException(std::string("unknown option for --sygus-out: `")
+                          + optarg
+                          + "'.  Try --sygus-out help.");
+  }
+}
 
 void OptionsHandler::setProduceAssertions(std::string option, bool value) throw() {
   options::produceAssertions.set(value);
diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index c525c9e0e..9d5f8cc6e 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -28,14 +28,15 @@
 #include "options/arith_unate_lemma_mode.h"
 #include "options/base_handlers.h"
 #include "options/bv_bitblast_mode.h"
-#include "options/decision_mode.h"
 #include "options/datatypes_modes.h"
+#include "options/decision_mode.h"
 #include "options/language.h"
 #include "options/option_exception.h"
 #include "options/options.h"
 #include "options/printer_modes.h"
 #include "options/quantifiers_modes.h"
 #include "options/simplification_mode.h"
+#include "options/sygus_out_mode.h"
 #include "options/theoryof_mode.h"
 #include "options/ufss_mode.h"
 
@@ -143,6 +144,8 @@ public:
   void notifyBeforeSearch(const std::string& option) throw(ModalException);
   void notifyDumpMode(std::string option) throw(OptionException);
   SimplificationMode stringToSimplificationMode(std::string option, std::string optarg) throw(OptionException);
+  SygusSolutionOutMode stringToSygusSolutionOutMode(
+      std::string option, std::string optarg) throw(OptionException);
   void setProduceAssertions(std::string option, bool value) throw();
   void proofEnabledBuild(std::string option, bool value) throw(OptionException);
   void LFSCEnabledBuild(std::string option, bool value);
@@ -218,6 +221,7 @@ public:
   static const std::string s_qcfModeHelp;
   static const std::string s_qcfWhenModeHelp;
   static const std::string s_simplificationHelp;
+  static const std::string s_sygusSolutionOutModeHelp;
   static const std::string s_cbqiBvIneqModeHelp;
   static const std::string s_cegqiSingleInvHelp;
   static const std::string s_sygusInvTemplHelp;
diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index 7d71c267a..b8db9d9da 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -241,13 +241,6 @@ std::ostream* Options::currentGetOut() {
 
 
 // TODO: Document these.
-void Options::setCeGuidedInst(bool value) {
-  set(options::ceGuidedInst, value);
-}
-
-void Options::setDumpSynth(bool value) {
-  set(options::dumpSynth, value);
-}
 
 void Options::setInputLanguage(InputLanguage value) {
   set(options::inputLanguage, value);
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index ba7c8338a..c92813bf4 100644
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -246,7 +246,7 @@ option conjectureGenMaxDepth --conjecture-gen-max-depth=N int :default 3
 ### synthesis options 
 
 option ceGuidedInst --cegqi bool :default false :read-write
-  counterexample-guided quantifier instantiation
+  counterexample-guided quantifier instantiation for sygus
 option cegqiSingleInvMode --cegqi-si=MODE CVC4::theory::quantifiers::CegqiSingleInvMode :default CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToCegqiSingleInvMode :read-write
   mode for processing single invocation synthesis conjectures
 option cegqiSingleInvPartial --cegqi-si-partial bool :default false
diff --git a/src/options/smt_options b/src/options/smt_options
index 00424e103..c701d5c20 100644
--- a/src/options/smt_options
+++ b/src/options/smt_options
@@ -39,6 +39,8 @@ option dumpProofs --dump-proofs bool :default false :link --proof :link-smt prod
  output proofs after every UNSAT/VALID response
 option dumpInstantiations --dump-instantiations bool :default false
  output instantiations of quantified formulas after every UNSAT/VALID response
+option sygusOut --sygus-out=MODE SygusSolutionOutMode :default SYGUS_SOL_OUT_STATUS_AND_DEF :include "options/sygus_out_mode.h" :handler stringToSygusSolutionOutMode :read-write
+  output mode for sygus
 option dumpSynth --dump-synth bool :read-write :default false
  output solution for synthesis conjectures after every UNSAT/VALID response
 option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate proofEnabledBuild :notify :notify notifyBeforeSearch
diff --git a/src/options/sygus_out_mode.h b/src/options/sygus_out_mode.h
new file mode 100644
index 000000000..9f94be27f
--- /dev/null
+++ b/src/options/sygus_out_mode.h
@@ -0,0 +1,39 @@
+/*********************                                                        */
+/*! \file sygus_out_mode.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Options for sygus solution output.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__SMT__SYGUS_OUT_MODE_H
+#define __CVC4__SMT__SYGUS_OUT_MODE_H
+
+#include <iosfwd>
+
+namespace CVC4 {
+
+/** Mode for printing sygus solutions. */
+enum SygusSolutionOutMode
+{
+  /** print status */
+  SYGUS_SOL_OUT_STATUS,
+  /** (default) print status and solution */
+  SYGUS_SOL_OUT_STATUS_AND_DEF,
+  /** print status if infeasible, or solution if feasible */
+  SYGUS_SOL_OUT_STATUS_OR_DEF,
+  /** print output specified by sygus standard */
+  SYGUS_SOL_OUT_STANDARD,
+};
+
+} /* CVC4 namespace */
+
+#endif /* __CVC4__SMT__SYGUS_OUT_MODE_H */
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 8012c868c..fee109923 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -383,8 +383,8 @@ CheckSynthCommand::CheckSynthCommand() throw() :
   d_expr() {
 }
 
-CheckSynthCommand::CheckSynthCommand(const Expr& expr, bool inUnsatCore) throw() :
-  d_expr(expr), d_inUnsatCore(inUnsatCore) {
+CheckSynthCommand::CheckSynthCommand(const Expr& expr) throw() :
+  d_expr(expr) {
 }
 
 Expr CheckSynthCommand::getExpr() const throw() {
@@ -395,6 +395,33 @@ void CheckSynthCommand::invoke(SmtEngine* smtEngine) {
   try {
     d_result = smtEngine->checkSynth(d_expr);
     d_commandStatus = CommandSuccess::instance();
+    smt::SmtScope scope(smtEngine);
+    d_solution.clear();
+    // check whether we should print the status
+    if (d_result.asSatisfiabilityResult() != Result::UNSAT
+        || options::sygusOut() == SYGUS_SOL_OUT_STATUS_AND_DEF
+        || options::sygusOut() == SYGUS_SOL_OUT_STATUS)
+    {
+      if (options::sygusOut() == SYGUS_SOL_OUT_STANDARD)
+      {
+        d_solution << "(fail)" << endl;
+      }
+      else
+      {
+        d_solution << d_result << endl;
+      }
+    }
+    // check whether we should print the solution
+    if (d_result.asSatisfiabilityResult() == Result::UNSAT
+        && options::sygusOut() != SYGUS_SOL_OUT_STATUS)
+    {
+      // printing a synthesis solution is a non-constant
+      // method, since it invokes a sophisticated algorithm
+      // (Figure 5 of Reynolds et al. CAV 2015).
+      // Hence, we must call here print solution here,
+      // instead of during printResult.
+      smtEngine->printSynthSolution(d_solution);
+    }
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }
@@ -408,18 +435,18 @@ void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
-    out << d_result << endl;
+    out << d_solution.str();
   }
 }
 
 Command* CheckSynthCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  CheckSynthCommand* c = new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
+  CheckSynthCommand* c = new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap));
   c->d_result = d_result;
   return c;
 }
 
 Command* CheckSynthCommand::clone() const {
-  CheckSynthCommand* c = new CheckSynthCommand(d_expr, d_inUnsatCore);
+  CheckSynthCommand* c = new CheckSynthCommand(d_expr);
   c->d_result = d_result;
   return c;
 }
diff --git a/src/smt/command.h b/src/smt/command.h
index f5be9ddfe..a60c85a3c 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -529,13 +529,9 @@ public:
 };/* class QueryCommand */
 
 class CVC4_PUBLIC CheckSynthCommand : public Command {
-protected:
-  Expr d_expr;
-  Result d_result;
-  bool d_inUnsatCore;
 public:
   CheckSynthCommand() throw();
-  CheckSynthCommand(const Expr& expr, bool inUnsatCore = true) throw();
+  CheckSynthCommand(const Expr& expr) throw();
   ~CheckSynthCommand() throw() {}
   Expr getExpr() const throw();
   void invoke(SmtEngine* smtEngine);
@@ -544,6 +540,14 @@ public:
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
   Command* clone() const;
   std::string getCommandName() const throw();
+
+ protected:
+  /** the assertion of check-synth */
+  Expr d_expr;
+  /** result of the check-synth call */
+  Result d_result;
+  /** string stream that stores the output of the solution */
+  std::stringstream d_solution;
 };/* class CheckSynthCommand */
 
 // this is TRANSFORM in the CVC presentation language
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f93d8bd7f..2ff115606 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1294,6 +1294,13 @@ void SmtEngine::setDefaults() {
     options::bitvectorDivByZeroConst.set(options::inputLanguage()
                                          == language::input::LANG_SMTLIB_V2_6);
   }
+  if (options::inputLanguage() == language::input::LANG_SYGUS)
+  {
+    if (!options::ceGuidedInst.wasSetByUser())
+    {
+      options::ceGuidedInst.set(true);
+    }
+  }
 
   if(options::forceLogicString.wasSetByUser()) {
     d_logic = LogicInfo(options::forceLogicString());
diff --git a/test/regress/regress0/expect/scrub.07.sy b/test/regress/regress0/expect/scrub.07.sy
index cf0e37c9f..79b917c7a 100644
--- a/test/regress/regress0/expect/scrub.07.sy
+++ b/test/regress/regress0/expect/scrub.07.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (declare-var n Int)
 
diff --git a/test/regress/regress0/expect/scrub.08.sy b/test/regress/regress0/expect/scrub.08.sy
index 7f78dbc48..360474f84 100644
--- a/test/regress/regress0/expect/scrub.08.sy
+++ b/test/regress/regress0/expect/scrub.08.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 ; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
 ; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
 ; EXPECT: The fact in question: TERM
diff --git a/test/regress/regress0/sygus/General_plus10.sy b/test/regress/regress0/sygus/General_plus10.sy
index ee26fac79..1792749e2 100755
--- a/test/regress/regress0/sygus/General_plus10.sy
+++ b/test/regress/regress0/sygus/General_plus10.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 (synth-fun fb () Int ((Start Int ((Constant Int)))))
diff --git a/test/regress/regress0/sygus/array_search_2.sy b/test/regress/regress0/sygus/array_search_2.sy
index e6683ced9..41346e655 100644
--- a/test/regress/regress0/sygus/array_search_2.sy
+++ b/test/regress/regress0/sygus/array_search_2.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)
diff --git a/test/regress/regress0/sygus/array_sum_2_5.sy b/test/regress/regress0/sygus/array_sum_2_5.sy
index 387ce9487..84a75d086 100644
--- a/test/regress/regress0/sygus/array_sum_2_5.sy
+++ b/test/regress/regress0/sygus/array_sum_2_5.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start)    (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)
diff --git a/test/regress/regress0/sygus/cegar1.sy b/test/regress/regress0/sygus/cegar1.sy
index dd7f73e27..ee85db88a 100644
--- a/test/regress/regress0/sygus/cegar1.sy
+++ b/test/regress/regress0/sygus/cegar1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inv-templ=post --no-dump-synth
+; COMMAND-LINE: --sygus-inv-templ=post --sygus-out=status
 (set-logic LIA)
 
 (synth-inv inv-f ((x Int) (y Int)))
diff --git a/test/regress/regress0/sygus/cggmp.sy b/test/regress/regress0/sygus/cggmp.sy
index 1ae1f53c0..a3247e4f4 100644
--- a/test/regress/regress0/sygus/cggmp.sy
+++ b/test/regress/regress0/sygus/cggmp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inv-templ=pre --no-dump-synth
+; COMMAND-LINE: --sygus-inv-templ=pre --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/clock-inc-tuple.sy b/test/regress/regress0/sygus/clock-inc-tuple.sy
index 2409b82d2..43fd7c1ac 100644
--- a/test/regress/regress0/sygus/clock-inc-tuple.sy
+++ b/test/regress/regress0/sygus/clock-inc-tuple.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 
 (set-logic ALL_SUPPORTED)
 (declare-var m Int)
diff --git a/test/regress/regress0/sygus/commutative.sy b/test/regress/regress0/sygus/commutative.sy
index f675bddad..24201b453 100644
--- a/test/regress/regress0/sygus/commutative.sy
+++ b/test/regress/regress0/sygus/commutative.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/const-var-test.sy b/test/regress/regress0/sygus/const-var-test.sy
index b79b7eeec..305f5783a 100644
--- a/test/regress/regress0/sygus/const-var-test.sy
+++ b/test/regress/regress0/sygus/const-var-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/constant.sy b/test/regress/regress0/sygus/constant.sy
index 5c48f5e39..1bb3e59fa 100644
--- a/test/regress/regress0/sygus/constant.sy
+++ b/test/regress/regress0/sygus/constant.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/dt-no-syntax.sy b/test/regress/regress0/sygus/dt-no-syntax.sy
index 0a9fb9112..f4de9b055 100644
--- a/test/regress/regress0/sygus/dt-no-syntax.sy
+++ b/test/regress/regress0/sygus/dt-no-syntax.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 ; EXPECT: unsat
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/dt-test-ns.sy b/test/regress/regress0/sygus/dt-test-ns.sy
index 0c28769b2..a6e8ac5c2 100644
--- a/test/regress/regress0/sygus/dt-test-ns.sy
+++ b/test/regress/regress0/sygus/dt-test-ns.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
diff --git a/test/regress/regress0/sygus/dup-op.sy b/test/regress/regress0/sygus/dup-op.sy
index bed9972fd..e2c69282e 100644
--- a/test/regress/regress0/sygus/dup-op.sy
+++ b/test/regress/regress0/sygus/dup-op.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Con Con) (+ Start Start) x))
diff --git a/test/regress/regress0/sygus/enum-test.sy b/test/regress/regress0/sygus/enum-test.sy
index 7b59f5f1a..47099eeed 100644
--- a/test/regress/regress0/sygus/enum-test.sy
+++ b/test/regress/regress0/sygus/enum-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (define-sort D (Enum (a b)))
 (define-fun f ((x D)) Int (ite (= x D::a) 3 7))
diff --git a/test/regress/regress0/sygus/fg_polynomial3.sy b/test/regress/regress0/sygus/fg_polynomial3.sy
index dab92bb88..d70516bf1 100644
--- a/test/regress/regress0/sygus/fg_polynomial3.sy
+++ b/test/regress/regress0/sygus/fg_polynomial3.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/hd-01-d1-prog.sy b/test/regress/regress0/sygus/hd-01-d1-prog.sy
index 2e6c6ef81..1379d4206 100644
--- a/test/regress/regress0/sygus/hd-01-d1-prog.sy
+++ b/test/regress/regress0/sygus/hd-01-d1-prog.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi --no-dump-synth
+; COMMAND-LINE: --cegqi --sygus-out=status
 
 (set-logic BV)
 
diff --git a/test/regress/regress0/sygus/icfp_14.12.sy b/test/regress/regress0/sygus/icfp_14.12.sy
index d9c19f8c1..51b86f0f5 100644
--- a/test/regress/regress0/sygus/icfp_14.12.sy
+++ b/test/regress/regress0/sygus/icfp_14.12.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic BV)
 
 (define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
diff --git a/test/regress/regress0/sygus/icfp_28_10.sy b/test/regress/regress0/sygus/icfp_28_10.sy
index 74e054159..212ae37f5 100644
--- a/test/regress/regress0/sygus/icfp_28_10.sy
+++ b/test/regress/regress0/sygus/icfp_28_10.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic BV)
 
diff --git a/test/regress/regress0/sygus/icfp_easy-ite.sy b/test/regress/regress0/sygus/icfp_easy-ite.sy
index 248264698..f0cbbdc53 100644
--- a/test/regress/regress0/sygus/icfp_easy-ite.sy
+++ b/test/regress/regress0/sygus/icfp_easy-ite.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic BV)
 
 (define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
diff --git a/test/regress/regress0/sygus/inv-example.sy b/test/regress/regress0/sygus/inv-example.sy
index b56425964..ff68bc06c 100644
--- a/test/regress/regress0/sygus/inv-example.sy
+++ b/test/regress/regress0/sygus/inv-example.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-inv inv-f ((x Int) (y Int) (b Bool)))
 (declare-primed-var x Int)
diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy
index d5d40ace4..d26edffd2 100644
--- a/test/regress/regress0/sygus/let-ringer.sy
+++ b/test/regress/regress0/sygus/let-ringer.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (define-fun g ((x Int)) Int (ite (= x 1) 15 19))
 (synth-fun f ((x Int)) Int
diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy
index d07f6a717..6f9d9fff9 100644
--- a/test/regress/regress0/sygus/let-simp.sy
+++ b/test/regress/regress0/sygus/let-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int) (y Int)) Int
     ((Start Int (x
diff --git a/test/regress/regress0/sygus/list-head-x.sy b/test/regress/regress0/sygus/list-head-x.sy
index 8d209a9a0..6c5c1a97b 100644
--- a/test/regress/regress0/sygus/list-head-x.sy
+++ b/test/regress/regress0/sygus/list-head-x.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic ALL_SUPPORTED)
 
 (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
diff --git a/test/regress/regress0/sygus/max.sy b/test/regress/regress0/sygus/max.sy
index e6e3de5fc..37ed848ef 100644
--- a/test/regress/regress0/sygus/max.sy
+++ b/test/regress/regress0/sygus/max.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 (synth-fun max ((x Int) (y Int)) Int
diff --git a/test/regress/regress0/sygus/max2-univ.sy b/test/regress/regress0/sygus/max2-univ.sy
index 927148d81..0e00cfd9b 100644
--- a/test/regress/regress0/sygus/max2-univ.sy
+++ b/test/regress/regress0/sygus/max2-univ.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 ; Synthesize the maximum of 2 integers, but property has 4 variables (requires 2 passes)
 (set-logic LIA)
 (synth-fun max2 ((x Int) (y Int)) Int)
diff --git a/test/regress/regress0/sygus/multi-fun-polynomial2.sy b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
index c238de5dd..22a2e0a4b 100644
--- a/test/regress/regress0/sygus/multi-fun-polynomial2.sy
+++ b/test/regress/regress0/sygus/multi-fun-polynomial2.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/nflat-fwd-3.sy b/test/regress/regress0/sygus/nflat-fwd-3.sy
index d3624a731..a1776cf93 100644
--- a/test/regress/regress0/sygus/nflat-fwd-3.sy
+++ b/test/regress/regress0/sygus/nflat-fwd-3.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ (+ Con Con) Con) x))
diff --git a/test/regress/regress0/sygus/nflat-fwd.sy b/test/regress/regress0/sygus/nflat-fwd.sy
index 3f15d5915..da26a6c93 100644
--- a/test/regress/regress0/sygus/nflat-fwd.sy
+++ b/test/regress/regress0/sygus/nflat-fwd.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x))
diff --git a/test/regress/regress0/sygus/nia-max-square-ns.sy b/test/regress/regress0/sygus/nia-max-square-ns.sy
index 96baab7fe..6e7f70ff0 100644
--- a/test/regress/regress0/sygus/nia-max-square-ns.sy
+++ b/test/regress/regress0/sygus/nia-max-square-ns.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth --nl-ext-tplanes
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status --nl-ext-tplanes
 (set-logic NIA)
 
 (synth-fun max ((x Int) (y Int)) Int)
diff --git a/test/regress/regress0/sygus/no-flat-simp.sy b/test/regress/regress0/sygus/no-flat-simp.sy
index af1284f13..c0f0e4c0f 100644
--- a/test/regress/regress0/sygus/no-flat-simp.sy
+++ b/test/regress/regress0/sygus/no-flat-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/no-mention.sy b/test/regress/regress0/sygus/no-mention.sy
index 60efc1b74..f964d6039 100644
--- a/test/regress/regress0/sygus/no-mention.sy
+++ b/test/regress/regress0/sygus/no-mention.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 
 (synth-fun p ((x Int) (y Int)) Int)
diff --git a/test/regress/regress0/sygus/no-syntax-test-bool.sy b/test/regress/regress0/sygus/no-syntax-test-bool.sy
index ee27b30eb..c6c9383bb 100644
--- a/test/regress/regress0/sygus/no-syntax-test-bool.sy
+++ b/test/regress/regress0/sygus/no-syntax-test-bool.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/no-syntax-test-no-si.sy b/test/regress/regress0/sygus/no-syntax-test-no-si.sy
index bd8da1900..8f333811c 100644
--- a/test/regress/regress0/sygus/no-syntax-test-no-si.sy
+++ b/test/regress/regress0/sygus/no-syntax-test-no-si.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/no-syntax-test.sy b/test/regress/regress0/sygus/no-syntax-test.sy
index 2b3d5f3e9..f27a07ee7 100644
--- a/test/regress/regress0/sygus/no-syntax-test.sy
+++ b/test/regress/regress0/sygus/no-syntax-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/parity-AIG-d0.sy b/test/regress/regress0/sygus/parity-AIG-d0.sy
index 3cc577bd8..50c7d39a0 100644
--- a/test/regress/regress0/sygus/parity-AIG-d0.sy
+++ b/test/regress/regress0/sygus/parity-AIG-d0.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic BV)
 
 (define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
diff --git a/test/regress/regress0/sygus/parse-bv-let.sy b/test/regress/regress0/sygus/parse-bv-let.sy
index 88ddcf139..1329918fc 100644
--- a/test/regress/regress0/sygus/parse-bv-let.sy
+++ b/test/regress/regress0/sygus/parse-bv-let.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic BV)
 
 (define-fun bit-reset ((x (BitVec 32)) (bit (BitVec 32))) (BitVec 32)
diff --git a/test/regress/regress0/sygus/qe.sy b/test/regress/regress0/sygus/qe.sy
index eaff0fd9a..5661f4469 100644
--- a/test/regress/regress0/sygus/qe.sy
+++ b/test/regress/regress0/sygus/qe.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 (synth-fun f ((x Int)) Int)
diff --git a/test/regress/regress0/sygus/strings-concat-3-args.sy b/test/regress/regress0/sygus/strings-concat-3-args.sy
index 3c93c51d3..6628ff746 100644
--- a/test/regress/regress0/sygus/strings-concat-3-args.sy
+++ b/test/regress/regress0/sygus/strings-concat-3-args.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
 (synth-fun f ((x String)) String
 ((Start String (ntString))
diff --git a/test/regress/regress0/sygus/strings-small.sy b/test/regress/regress0/sygus/strings-small.sy
index 40346bcdf..7d976ff39 100644
--- a/test/regress/regress0/sygus/strings-small.sy
+++ b/test/regress/regress0/sygus/strings-small.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
 (synth-fun f ((firstname String) (lastname String)) String
 ((Start String (ntString))
diff --git a/test/regress/regress0/sygus/strings-template-infer.sy b/test/regress/regress0/sygus/strings-template-infer.sy
index 498e713e8..13c4d7dac 100644
--- a/test/regress/regress0/sygus/strings-template-infer.sy
+++ b/test/regress/regress0/sygus/strings-template-infer.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
  
 (define-fun cA ((x String) (y String)) String (str.++ (str.++ x "A") y))
diff --git a/test/regress/regress0/sygus/strings-trivial-simp.sy b/test/regress/regress0/sygus/strings-trivial-simp.sy
index d37ac8bf4..f5e41a8f5 100644
--- a/test/regress/regress0/sygus/strings-trivial-simp.sy
+++ b/test/regress/regress0/sygus/strings-trivial-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
  
 (synth-fun f ((name String)) String
diff --git a/test/regress/regress0/sygus/strings-trivial.sy b/test/regress/regress0/sygus/strings-trivial.sy
index f4847922d..9af0a1bb1 100644
--- a/test/regress/regress0/sygus/strings-trivial.sy
+++ b/test/regress/regress0/sygus/strings-trivial.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
  
 (synth-fun f ((name String)) String
diff --git a/test/regress/regress0/sygus/strings-unconstrained.sy b/test/regress/regress0/sygus/strings-unconstrained.sy
index 38e69e337..39c392487 100644
--- a/test/regress/regress0/sygus/strings-unconstrained.sy
+++ b/test/regress/regress0/sygus/strings-unconstrained.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic SLIA)
 (synth-fun f ((firstname String) (lastname String)) String
 ((Start String (ntString))
diff --git a/test/regress/regress0/sygus/sygus-dt.sy b/test/regress/regress0/sygus/sygus-dt.sy
index 59560ed61..d496e3fdc 100644
--- a/test/regress/regress0/sygus/sygus-dt.sy
+++ b/test/regress/regress0/sygus/sygus-dt.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 
diff --git a/test/regress/regress0/sygus/tl-type-0.sy b/test/regress/regress0/sygus/tl-type-0.sy
index ef046c8e0..ceda89d78 100644
--- a/test/regress/regress0/sygus/tl-type-0.sy
+++ b/test/regress/regress0/sygus/tl-type-0.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int ((+ Term Term)))
diff --git a/test/regress/regress0/sygus/tl-type-4x.sy b/test/regress/regress0/sygus/tl-type-4x.sy
index a18d13052..bf8eee5ee 100644
--- a/test/regress/regress0/sygus/tl-type-4x.sy
+++ b/test/regress/regress0/sygus/tl-type-4x.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int (Term (+ Start Start)))
diff --git a/test/regress/regress0/sygus/tl-type.sy b/test/regress/regress0/sygus/tl-type.sy
index a6980425a..6f25a570e 100644
--- a/test/regress/regress0/sygus/tl-type.sy
+++ b/test/regress/regress0/sygus/tl-type.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
     ((Start Int (Term (+ Start Start)))
diff --git a/test/regress/regress0/sygus/triv-type-mismatch-si.sy b/test/regress/regress0/sygus/triv-type-mismatch-si.sy
index e2935af51..37c5a7f53 100644
--- a/test/regress/regress0/sygus/triv-type-mismatch-si.sy
+++ b/test/regress/regress0/sygus/triv-type-mismatch-si.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 
 (synth-fun R ((y Int)) Bool)
diff --git a/test/regress/regress0/sygus/twolets1.sy b/test/regress/regress0/sygus/twolets1.sy
index b016872b4..06d2ecb71 100644
--- a/test/regress/regress0/sygus/twolets1.sy
+++ b/test/regress/regress0/sygus/twolets1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 ;; f1 is x plus 2 ;; f2 is 2x plus 5
diff --git a/test/regress/regress0/sygus/twolets2-orig.sy b/test/regress/regress0/sygus/twolets2-orig.sy
index 70d1ffa02..50f7ad544 100644
--- a/test/regress/regress0/sygus/twolets2-orig.sy
+++ b/test/regress/regress0/sygus/twolets2-orig.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --no-dump-synth
+; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (synth-fun f1 ((x Int)) Int
      (
diff --git a/test/regress/regress0/sygus/uminus_one.sy b/test/regress/regress0/sygus/uminus_one.sy
index e98be942b..94040bf45 100644
--- a/test/regress/regress0/sygus/uminus_one.sy
+++ b/test/regress/regress0/sygus/uminus_one.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int ((Start Int ((- 1)))))
 (declare-var x Int)
diff --git a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
index 300b6b65c..d45cec38b 100644
--- a/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
+++ b/test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 
 (set-logic LIA)
 (synth-fun inv ((x Int)) Bool
diff --git a/test/regress/regress1/sygus/MPwL_d1s3.sy b/test/regress/regress1/sygus/MPwL_d1s3.sy
index b5b848848..5178cf86b 100644
--- a/test/regress/regress1/sygus/MPwL_d1s3.sy
+++ b/test/regress/regress1/sygus/MPwL_d1s3.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth 
+; COMMAND-LINE: --sygus-out=status 
 (set-logic LIA)
 
 (define-fun get-y ((currPoint Int)) Int 
diff --git a/test/regress/regress1/sygus/VC22_a.sy b/test/regress/regress1/sygus/VC22_a.sy
index 75bed6a28..32e4723aa 100644
--- a/test/regress/regress1/sygus/VC22_a.sy
+++ b/test/regress/regress1/sygus/VC22_a.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 
 (synth-fun f ((x1 Int) (x2 Int)) Int
diff --git a/test/regress/regress1/sygus/array_sum_dd.sy b/test/regress/regress1/sygus/array_sum_dd.sy
index dacd7347d..6d3354d2d 100644
--- a/test/regress/regress1/sygus/array_sum_dd.sy
+++ b/test/regress/regress1/sygus/array_sum_dd.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun findSum ( (y1 Int) (y2 Int) )Int (
 (Start Int ( 0 1 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) 
diff --git a/test/regress/regress1/sygus/hd-sdiv.sy b/test/regress/regress1/sygus/hd-sdiv.sy
index 019b48a1c..37e1daf88 100644
--- a/test/regress/regress1/sygus/hd-sdiv.sy
+++ b/test/regress/regress1/sygus/hd-sdiv.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --no-dump-synth
+; COMMAND-LINE: --cegqi-si=none --sygus-out=status
 (set-logic BV)
 
 (define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x #x00000001))
diff --git a/test/regress/regress1/sygus/icfp_easy_mt_ite.sy b/test/regress/regress1/sygus/icfp_easy_mt_ite.sy
index b7428fd51..799633fa3 100644
--- a/test/regress/regress1/sygus/icfp_easy_mt_ite.sy
+++ b/test/regress/regress1/sygus/icfp_easy_mt_ite.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic BV)
 
 (define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
diff --git a/test/regress/regress1/sygus/inv_gen_fig8.sy b/test/regress/regress1/sygus/inv_gen_fig8.sy
index 5496f3c0a..19c36e4dc 100644
--- a/test/regress/regress1/sygus/inv_gen_fig8.sy
+++ b/test/regress/regress1/sygus/inv_gen_fig8.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun inv ((l Int)) Bool
     (
diff --git a/test/regress/regress1/sygus/inv_gen_n_c11.sy b/test/regress/regress1/sygus/inv_gen_n_c11.sy
index 946f284cb..9e04682a5 100644
--- a/test/regress/regress1/sygus/inv_gen_n_c11.sy
+++ b/test/regress/regress1/sygus/inv_gen_n_c11.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun inv ((i Int) (l Int)) Bool
     (
diff --git a/test/regress/regress1/sygus/mpg_guard1-dd.sy b/test/regress/regress1/sygus/mpg_guard1-dd.sy
index e574f7eb6..31800a36f 100644
--- a/test/regress/regress1/sygus/mpg_guard1-dd.sy
+++ b/test/regress/regress1/sygus/mpg_guard1-dd.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 
 (synth-fun eq1 ( (x Int) (y Int) ) Int
diff --git a/test/regress/regress1/sygus/nia-max-square.sy b/test/regress/regress1/sygus/nia-max-square.sy
index 5858af98a..e023e837b 100644
--- a/test/regress/regress1/sygus/nia-max-square.sy
+++ b/test/regress/regress1/sygus/nia-max-square.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth --nl-ext-tplanes
+; COMMAND-LINE: --sygus-out=status --nl-ext-tplanes
 (set-logic NIA)
 
 (synth-fun max ((x Int) (y Int)) Int
diff --git a/test/regress/regress1/sygus/stopwatch-bt.sy b/test/regress/regress1/sygus/stopwatch-bt.sy
index 016280521..291ae6099 100644
--- a/test/regress/regress1/sygus/stopwatch-bt.sy
+++ b/test/regress/regress1/sygus/stopwatch-bt.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inv-templ=post --no-dump-synth
+; COMMAND-LINE: --sygus-inv-templ=post --sygus-out=status
 (set-logic LIA)
 
 (define-fun
diff --git a/test/regress/regress1/sygus/three.sy b/test/regress/regress1/sygus/three.sy
index 6e2ce3a2c..831e5beb1 100644
--- a/test/regress/regress1/sygus/three.sy
+++ b/test/regress/regress1/sygus/three.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth 
+; COMMAND-LINE: --sygus-out=status 
 
 (set-logic LIA)
 
diff --git a/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy b/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy
index f840fa519..73d410d51 100644
--- a/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy
+++ b/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --no-dump-synth
+; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
 (synth-fun inv ((i Int) (y Int) (l Int)) Bool
     (