5 files changed, 28 insertions, 21 deletions

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 8faeab491..d915d2ab4 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -755,12 +755,6 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
       warning("Logics in sygus are assumed to contain quantifiers.");
       warning("Omit QF_ from the logic to avoid this warning.");
     }
-    // get unlocked copy, modify, copy and relock
-    LogicInfo log(d_logic.getUnlockedCopy());
-    // enable everything needed for sygus
-    log.enableSygus();
-    d_logic = log;
-    d_logic.lock();
   }
 
   // Core theory belongs to every logic
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 28471de72..886be0cfa 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -84,8 +84,9 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
 void Printer::toStreamSygus(std::ostream& out, TNode n) const
 {
   // no sygus-specific printing associated with this printer,
-  // just print the original term
-  toStream(out, n, -1, false, 1);
+  // just print the original term, without letification (the fifth argument is
+  // set to 0).
+  toStream(out, n, -1, false, 0);
 }
 
 void Printer::toStream(std::ostream& out, const Model& m) const
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index e9a4d0a83..6fdbd4adb 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1522,7 +1522,8 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const
         {
           out << "(";
         }
-        out << dt[cIndex].getSygusOp();
+        // print operator without letification (the fifth argument is set to 0).
+        toStream(out, dt[cIndex].getSygusOp(), -1, false, 0);
         if (n.getNumChildren() > 0)
         {
           for (Node nc : n)
@@ -1537,15 +1538,12 @@ void Smt2Printer::toStreamSygus(std::ostream& out, TNode n) const
     }
   }
   Node p = n.getAttribute(theory::SygusPrintProxyAttribute());
-  if (!p.isNull())
+  if (p.isNull())
   {
-    out << p;
-  }
-  else
-  {
-    // cannot convert term to analog, print original
-    out << n;
+    p = n;
   }
+  // cannot convert term to analog, print original, without letification.
+  toStream(out, p, -1, false, 0);
 }
 
 static void toStream(std::ostream& out, const AssertCommand* c)
diff --git a/src/printer/sygus_print_callback.cpp b/src/printer/sygus_print_callback.cpp
index ae1d97c64..92a89a18e 100644
--- a/src/printer/sygus_print_callback.cpp
+++ b/src/printer/sygus_print_callback.cpp
@@ -78,8 +78,9 @@ void SygusExprPrintCallback::toStreamSygus(const Printer* p,
     sbody =
         sbody.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
 
+    // print to stream without letification
     std::stringstream body_out;
-    body_out << sbody;
+    p->toStream(body_out, sbody, -1, false, 0);
 
     // do string substitution
     Assert(e.getNumChildren() == d_args.size());
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 081e36953..915dc603e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1313,13 +1313,18 @@ void SmtEngine::setDefaults() {
     {
       // since we are trying to recast as sygus, we assume the input is sygus
       is_sygus = true;
-      // we change the logic to incorporate sygus immediately
-      d_logic = d_logic.getUnlockedCopy();
-      d_logic.enableSygus();
-      d_logic.lock();
     }
   }
 
+  // We now know whether the input is sygus. Update the logic to incorporate
+  // the theories we need internally for handling sygus problems.
+  if (is_sygus)
+  {
+    d_logic = d_logic.getUnlockedCopy();
+    d_logic.enableSygus();
+    d_logic.lock();
+  }
+
   // sygus core connective requires unsat cores
   if (options::sygusCoreConnective())
   {
@@ -3983,6 +3988,8 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore)
 
 void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type)
 {
+  SmtScope smts(this);
+  finalOptionsAreSet();
   d_private->d_sygusVars.push_back(Node::fromExpr(var));
   Trace("smt") << "SmtEngine::declareSygusVar: " << var << "\n";
   Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type);
@@ -3991,6 +3998,8 @@ void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type)
 
 void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type)
 {
+  SmtScope smts(this);
+  finalOptionsAreSet();
   // do nothing (the command is spurious)
   Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n";
   // don't need to set that the conjecture is stale
@@ -4000,6 +4009,8 @@ void SmtEngine::declareSygusFunctionVar(const std::string& id,
                                         Expr var,
                                         Type type)
 {
+  SmtScope smts(this);
+  finalOptionsAreSet();
   d_private->d_sygusVars.push_back(Node::fromExpr(var));
   Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n";
   Dump("raw-benchmark") << DeclareSygusVarCommand(id, var, type);
@@ -4044,6 +4055,7 @@ void SmtEngine::declareSynthFun(const std::string& id,
 void SmtEngine::assertSygusConstraint(Expr constraint)
 {
   SmtScope smts(this);
+  finalOptionsAreSet();
   d_private->d_sygusConstraints.push_back(constraint);
 
   Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n";
@@ -4058,6 +4070,7 @@ void SmtEngine::assertSygusInvConstraint(const Expr& inv,
                                          const Expr& post)
 {
   SmtScope smts(this);
+  finalOptionsAreSet();
   // build invariant constraint
 
   // get variables (regular and their respective primed versions)