Merge branch 'master' into fixRefCountZerofixRefCountZero

41 files changed, 1096 insertions, 306 deletions

diff --git a/src/base/exception.h b/src/base/exception.h
index 704ca928e..0d1abd9e0 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -128,7 +128,7 @@ template <class T> inline void CheckArgument(bool cond, const T& arg,
 template <class T> inline void CheckArgument(bool cond, const T& arg CVC4_UNUSED,
                                              const char* tail CVC4_UNUSED) {
   if(__builtin_expect( ( !cond ), false )) { \
-    throw ::CVC4::IllegalArgumentException("", "", ""); \
+    throw ::CVC4::IllegalArgumentException("", "", tail); \
   } \
 }
 template <class T> inline void CheckArgument(bool cond, const T& arg)
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 8daaa04e6..f47795c15 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1095,8 +1095,10 @@ NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
   Assert(sorts.size() >= 2);
   std::vector<TypeNode> sortNodes;
   for (unsigned i = 0; i < sorts.size(); ++ i) {
-    CheckArgument(sorts[i].isFirstClass(), sorts,
-                  "cannot create function types for argument types that are not first-class");
+    CheckArgument(sorts[i].isFirstClass(),
+                  sorts,
+                  "cannot create function types for argument types that are "
+                  "not first-class. Try option --uf-ho.");
     sortNodes.push_back(sorts[i]);
   }
   CheckArgument(!sorts[sorts.size()-1].isFunction(), sorts[sorts.size()-1],
@@ -1109,8 +1111,10 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
   Assert(sorts.size() >= 1);
   std::vector<TypeNode> sortNodes;
   for (unsigned i = 0; i < sorts.size(); ++ i) {
-    CheckArgument(sorts[i].isFirstClass(), sorts,
-                  "cannot create predicate types for argument types that are not first-class");
+    CheckArgument(sorts[i].isFirstClass(),
+                  sorts,
+                  "cannot create predicate types for argument types that are "
+                  "not first-class. Try option --uf-ho.");
     sortNodes.push_back(sorts[i]);
   }
   sortNodes.push_back(booleanType());
@@ -1143,10 +1147,14 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                 "unexpected NULL index type");
   CheckArgument(!constituentType.isNull(), constituentType,
                 "unexpected NULL constituent type");
-  CheckArgument(indexType.isFirstClass(), indexType,
-                "cannot index arrays by types that are not first-class");
-  CheckArgument(constituentType.isFirstClass(), constituentType,
-                "cannot store types that are not first-class in arrays");
+  CheckArgument(indexType.isFirstClass(),
+                indexType,
+                "cannot index arrays by types that are not first-class. Try "
+                "option --uf-ho.");
+  CheckArgument(constituentType.isFirstClass(),
+                constituentType,
+                "cannot store types that are not first-class in arrays. Try "
+                "option --uf-ho.");
   Debug("arrays") << "making array type " << indexType << " "
                   << constituentType << std::endl;
   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
@@ -1155,8 +1163,10 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
 inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
   CheckArgument(!elementType.isNull(), elementType,
                 "unexpected NULL element type");
-  CheckArgument(elementType.isFirstClass(), elementType,
-                "cannot store types that are not first-class in sets");
+  CheckArgument(elementType.isFirstClass(),
+                elementType,
+                "cannot store types that are not first-class in sets. Try "
+                "option --uf-ho.");
   Debug("sets") << "making sets type " << elementType << std::endl;
   return mkTypeNode(kind::SET_TYPE, elementType);
 }
@@ -1164,8 +1174,10 @@ inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
 inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
   CheckArgument(domain.isDatatype(), domain,
                 "cannot create non-datatype selector type");
-  CheckArgument(range.isFirstClass(), range,
-                "cannot have selector fields that are not first-class types");
+  CheckArgument(range.isFirstClass(),
+                range,
+                "cannot have selector fields that are not first-class types. "
+                "Try option --uf-ho.");
   return mkTypeNode(kind::SELECTOR_TYPE, domain, range);
 }
 
diff --git a/src/options/language.cpp b/src/options/language.cpp
index 0f2c513b6..8c6f8421f 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -68,6 +68,16 @@ bool isOutputLang_smt2_6(OutputLanguage lang, bool exact)
                   && lang <= output::LANG_SMTLIB_V2_END);
 }
 
+bool isInputLangSygus(InputLanguage lang)
+{
+  return lang == input::LANG_SYGUS || lang == input::LANG_SYGUS_V2;
+}
+
+bool isOutputLangSygus(OutputLanguage lang)
+{
+  return lang == output::LANG_SYGUS || lang == output::LANG_SYGUS_V2;
+}
+
 InputLanguage toInputLanguage(OutputLanguage language) {
   switch(language) {
   case output::LANG_SMTLIB_V2_0:
diff --git a/src/options/language.h b/src/options/language.h
index b7eb16f91..3a9ebf9d5 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -220,6 +220,10 @@ bool isOutputLang_smt2_5(OutputLanguage lang, bool exact = false) CVC4_PUBLIC;
 bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC4_PUBLIC;
 bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) CVC4_PUBLIC;
 
+/** Is the language a variant of the SyGuS input language? */
+bool isInputLangSygus(InputLanguage lang) CVC4_PUBLIC;
+bool isOutputLangSygus(OutputLanguage lang) CVC4_PUBLIC;
+
 InputLanguage toInputLanguage(OutputLanguage language) CVC4_PUBLIC;
 OutputLanguage toOutputLanguage(InputLanguage language) CVC4_PUBLIC;
 InputLanguage toInputLanguage(std::string language) CVC4_PUBLIC;
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 338f5544f..019b052bc 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1218,9 +1218,17 @@ header = "options/quantifiers_options.h"
   category   = "regular"
   long       = "sygus-rec-fun"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   help       = "enable efficient support for recursive functions in sygus grammars"
 
+[[option]]
+  name       = "sygusRecFunEvalLimit"
+  category   = "regular"
+  long       = "sygus-rec-fun-eval-limit=N"
+  type       = "unsigned"
+  default    = "1000"
+  help       = "use a hard limit for how many times in a given evaluator call a recursive function can be evaluated (so infinite loops can be avoided)"
+
 # Internal uses of sygus
 
 [[option]]
@@ -1359,7 +1367,7 @@ header = "options/quantifiers_options.h"
   long       = "sygus-expr-miner-check-timeout=N"
   type       = "unsigned long"
   help       = "timeout (in milliseconds) for satisfiability checks in expression miners"
-  
+
 [[option]]
   name       = "sygusRewSynthRec"
   category   = "regular"
@@ -1420,7 +1428,7 @@ header = "options/quantifiers_options.h"
   default    = "false"
   help       = "compute backwards filtering to compute whether previous solutions are filtered based on later ones"
 
-  
+
 [[option]]
   name       = "sygusExprMinerCheckUseExport"
   category   = "expert"
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a5033278d..c1a9df887 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -305,8 +305,11 @@ command [std::unique_ptr<CVC4::Command>* cmd]
         t = PARSER_STATE->mkFlatFunctionType(sorts, t);
       }
       if(t.isFunction() && !PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
-        PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) cannot "
-                                      "be declared in logic ");
+        PARSER_STATE->parseError(
+            "Functions (of non-zero arity) cannot "
+            "be declared in logic "
+            + PARSER_STATE->getLogic().getLogicString()
+            + " unless option --uf-ho is used.");
       }
       // we allow overloading for function declarations
       if (PARSER_STATE->sygus_v1())
@@ -392,17 +395,6 @@ command [std::unique_ptr<CVC4::Command>* cmd]
         csen->setMuted(true);
         PARSER_STATE->preemptCommand(csen);
       }
-      // if sygus, check whether it has a free variable
-      // this is because, due to the sygus format, one can write assertions
-      // that have free function variables in them
-      if (PARSER_STATE->sygus())
-      {
-        if (expr.hasFreeVariable())
-        {
-          PARSER_STATE->parseError("Assertion has free variable. Perhaps you "
-                                   "meant constraint instead of assert?");
-        }
-      }
     }
   | /* check-sat */
     CHECK_SAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -1294,8 +1286,11 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
       { Type t;
         if(sorts.size() > 1) {
           if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
-            PARSER_STATE->parseErrorLogic("Functions (of non-zero arity) "
-                                          "cannot be declared in logic ");
+            PARSER_STATE->parseError(
+                "Functions (of non-zero arity) cannot "
+                "be declared in logic "
+                + PARSER_STATE->getLogic().getLogicString()
+                + " unless option --uf-ho is used");
           }
           // must flatten
           Type range = sorts.back();
@@ -1321,8 +1316,11 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
       { Type t = EXPR_MANAGER->booleanType();
         if(sorts.size() > 0) {
           if(!PARSER_STATE->isTheoryEnabled(Smt2::THEORY_UF)) {
-            PARSER_STATE->parseErrorLogic("Predicates (of non-zero arity) "
-                                          "cannot be declared in logic ");
+            PARSER_STATE->parseError(
+                "Functions (of non-zero arity) cannot "
+                "be declared in logic "
+                + PARSER_STATE->getLogic().getLogicString()
+                + " unless option --uf-ho is used");
           }
           t = EXPR_MANAGER->mkFunctionType(sorts, t);
         }
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index b693eae5b..6dc29b8fe 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1435,6 +1435,10 @@ void Smt2::addSygusConstructorTerm(Datatype& dt,
                                    std::map<Expr, Type>& ntsToUnres) const
 {
   Trace("parser-sygus2") << "Add sygus cons term " << term << std::endl;
+  // Ensure that we do type checking here to catch sygus constructors with
+  // malformed builtin operators. The argument "true" to getType here forces
+  // a recursive well-typedness check.
+  term.getType(true);
   // purify each occurrence of a non-terminal symbol in term, replace by
   // free variables. These become arguments to constructors. Notice we must do
   // a tree traversal in this function, since unique paths to the same term
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 930edf869..6708f3c3a 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -202,7 +202,7 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions,
                  == free_functions.end());
           free_functions.push_back(cur);
         }
-        else if (cur.getKind() == FORALL)
+        else if (cur.isClosure())
         {
           Trace("sygus-infer")
               << "...fail: non-top-level quantifier." << std::endl;
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index fa4c1ecb5..bbf5b0064 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -579,9 +579,13 @@ void LFSCProof::toStream(std::ostream& out) const
     CodeTimer skeletonProofTimer{
         ProofManager::currentPM()->getStats().d_skeletonProofTraceTime};
     Assert(!d_satProof->proofConstructed());
+
+    // Here we give our SAT solver a chance to flesh out the resolution proof.
+    // It proves bottom from a set of clauses.
     d_satProof->constructProof();
 
-    // collecting leaf clauses in resolution proof
+    // We ask the SAT solver which clauses are used in that proof.
+    // For a resolution proof, these are the leaves of the tree.
     d_satProof->collectClausesUsed(used_inputs, used_lemmas);
 
     IdToSatClause::iterator it2;
@@ -672,6 +676,8 @@ void LFSCProof::toStream(std::ostream& out) const
       }
     }
 
+    // From the clauses, compute the atoms (atomic theory predicates in
+    // assertions and lemmas).
     d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
     d_cnfProof->collectAtomsForClauses(used_lemmas, atoms);
 
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 073c2ebc5..ca5558e87 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -751,7 +751,12 @@ class SmtEnginePrivate : public NodeManagerListener {
    * formula might be pushed out to the propositional layer
    * immediately, or it might be simplified and kept, or it might not
    * even be simplified.
-   * the 2nd and 3rd arguments added for bookkeeping for proofs
+   * The arguments isInput and isAssumption are used for bookkeeping for proofs.
+   * The argument maybeHasFv should be set to true if the assertion may have
+   * free variables. By construction, assertions from the smt2 parser are
+   * guaranteed not to have free variables. However, other cases such as
+   * assertions from the SyGuS parser may have free variables (say if the
+   * input contains an assert or define-fun-rec command).
    *
    * @param isAssumption If true, the formula is considered to be an assumption
    * (this is used to distinguish assertions and assumptions)
@@ -759,7 +764,8 @@ class SmtEnginePrivate : public NodeManagerListener {
   void addFormula(TNode n,
                   bool inUnsatCore,
                   bool inInput = true,
-                  bool isAssumption = false);
+                  bool isAssumption = false,
+                  bool maybeHasFv = false);
 
   /** Expand definitions in n. */
   Node expandDefinitions(TNode n,
@@ -1155,15 +1161,9 @@ void SmtEngine::setDefaults() {
     // option if we are sygus, since we assume SMT LIB 2.6 semantics for sygus.
     options::bitvectorDivByZeroConst.set(
         language::isInputLang_smt2_6(options::inputLanguage())
-        || options::inputLanguage() == language::input::LANG_SYGUS
-        || options::inputLanguage() == language::input::LANG_SYGUS_V2);
-  }
-  bool is_sygus = false;
-  if (options::inputLanguage() == language::input::LANG_SYGUS
-      || options::inputLanguage() == language::input::LANG_SYGUS_V2)
-  {
-    is_sygus = true;
+        || language::isInputLangSygus(options::inputLanguage()));
   }
+  bool is_sygus = language::isInputLangSygus(options::inputLanguage());
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER)
   {
@@ -2647,6 +2647,7 @@ void SmtEngine::defineFunctionsRec(
   }
 
   ExprManager* em = getExprManager();
+  bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
   for (unsigned i = 0, size = funcs.size(); i < size; i++)
   {
     // we assert a quantified formula
@@ -2686,7 +2687,7 @@ void SmtEngine::defineFunctionsRec(
     {
       d_assertionList->push_back(e);
     }
-    d_private->addFormula(e.getNode(), false);
+    d_private->addFormula(e.getNode(), false, true, false, maybeHasFv);
   }
 }
 
@@ -3579,10 +3580,8 @@ void SmtEnginePrivate::processAssertions() {
   getIteSkolemMap().clear();
 }
 
-void SmtEnginePrivate::addFormula(TNode n,
-                                  bool inUnsatCore,
-                                  bool inInput,
-                                  bool isAssumption)
+void SmtEnginePrivate::addFormula(
+    TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv)
 {
   if (n == d_true) {
     // nothing to do
@@ -3594,6 +3593,23 @@ void SmtEnginePrivate::addFormula(TNode n,
                << ", inInput = " << inInput
                << ", isAssumption = " << isAssumption << endl;
 
+  // Ensure that it does not contain free variables
+  if (maybeHasFv)
+  {
+    if (expr::hasFreeVar(n))
+    {
+      std::stringstream se;
+      se << "Cannot process assertion with free variable.";
+      if (language::isInputLangSygus(options::inputLanguage()))
+      {
+        // Common misuse of SyGuS is to use top-level assert instead of
+        // constraint when defining the synthesis conjecture.
+        se << " Perhaps you meant `constraint` instead of `assert`?";
+      }
+      throw ModalException(se.str().c_str());
+    }
+  }
+
   // Give it to proof manager
   PROOF(
     if( inInput ){
@@ -3901,7 +3917,8 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore)
   if(d_assertionList != NULL) {
     d_assertionList->push_back(e);
   }
-  d_private->addFormula(e.getNode(), inUnsatCore);
+  bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
+  d_private->addFormula(e.getNode(), inUnsatCore, true, false, maybeHasFv);
   return quickCheck().asValidityResult();
 }/* SmtEngine::assertFormula() */
 
@@ -4861,6 +4878,7 @@ void SmtEngine::checkSynthSolution()
   SmtEngine solChecker(d_exprManager);
   solChecker.setLogic(getLogicInfo());
   setOption("check-synth-sol", SExpr("false"));
+  setOption("sygus-rec-fun", SExpr("false"));
 
   Trace("check-synth-sol") << "Retrieving assertions\n";
   // Build conjecture from original assertions
diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp
index 62bdf310b..762e8b141 100644
--- a/src/theory/arith/nl_model.cpp
+++ b/src/theory/arith/nl_model.cpp
@@ -73,31 +73,22 @@ Node NlModel::computeModelValue(Node n, bool isConcrete)
   Trace("nl-ext-mv-debug") << "computeModelValue " << n << ", index=" << index
                            << std::endl;
   Node ret;
+  Kind nk = n.getKind();
   if (n.isConst())
   {
     ret = n;
   }
-  else if (index == 1
-           && (n.getKind() == NONLINEAR_MULT
-               || isTranscendentalKind(n.getKind())))
+  else if (!isConcrete && hasTerm(n))
   {
-    if (hasTerm(n))
-    {
-      // use model value for abstraction
-      ret = getRepresentative(n);
-    }
-    else
-    {
-      // abstraction does not exist, use model value
-      ret = getValueInternal(n);
-    }
+    // use model value for abstraction
+    ret = getRepresentative(n);
   }
   else if (n.getNumChildren() == 0)
   {
-    if (n.getKind() == PI)
+    // we are interested in the exact value of PI, which cannot be computed.
+    // hence, we return PI itself when asked for the concrete value.
+    if (nk == PI)
     {
-      // we are interested in the exact value of PI, which cannot be computed.
-      // hence, we return PI itself when asked for the concrete value.
       ret = n;
     }
     else
@@ -108,23 +99,25 @@ Node NlModel::computeModelValue(Node n, bool isConcrete)
   else
   {
     // otherwise, compute true value
-    std::vector<Node> children;
-    if (n.getMetaKind() == metakind::PARAMETERIZED)
-    {
-      children.push_back(n.getOperator());
-    }
-    for (unsigned i = 0; i < n.getNumChildren(); i++)
+    TheoryId ctid = theory::kindToTheoryId(nk);
+    if (ctid != THEORY_ARITH && ctid != THEORY_BOOL && ctid != THEORY_BUILTIN)
     {
-      Node mc = computeModelValue(n[i], isConcrete);
-      children.push_back(mc);
-    }
-    ret = NodeManager::currentNM()->mkNode(n.getKind(), children);
-    if (n.getKind() == APPLY_UF)
-    {
-      ret = getValueInternal(ret);
+      // we directly look up terms not belonging to arithmetic
+      ret = getValueInternal(n);
     }
     else
     {
+      std::vector<Node> children;
+      if (n.getMetaKind() == metakind::PARAMETERIZED)
+      {
+        children.push_back(n.getOperator());
+      }
+      for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+      {
+        Node mc = computeModelValue(n[i], isConcrete);
+        children.push_back(mc);
+      }
+      ret = NodeManager::currentNM()->mkNode(nk, children);
       ret = Rewriter::rewrite(ret);
     }
   }
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index a6a47c73c..bc4d7db02 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4973,7 +4973,7 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
       if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
       {
         Node divByZeroNum =
-            getArithSkolemApp(logicRequest, num, arith_skolem_div_by_zero);
+            getArithSkolemApp(logicRequest, num, ArithSkolemId::DIV_BY_ZERO);
         Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
         ret = nm->mkNode(kind::ITE, denEq0, divByZeroNum, ret);
       }
@@ -4988,8 +4988,8 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
       Node ret = nm->mkNode(kind::INTS_DIVISION_TOTAL, num, den);
       if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
       {
-        Node intDivByZeroNum =
-            getArithSkolemApp(logicRequest, num, arith_skolem_int_div_by_zero);
+        Node intDivByZeroNum = getArithSkolemApp(
+            logicRequest, num, ArithSkolemId::INT_DIV_BY_ZERO);
         Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
         ret = nm->mkNode(kind::ITE, denEq0, intDivByZeroNum, ret);
       }
@@ -5005,7 +5005,7 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
       if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
       {
         Node modZeroNum =
-            getArithSkolemApp(logicRequest, num, arith_skolem_mod_by_zero);
+            getArithSkolemApp(logicRequest, num, ArithSkolemId::MOD_BY_ZERO);
         Node denEq0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0)));
         ret = nm->mkNode(kind::ITE, denEq0, modZeroNum, ret);
       }
@@ -5037,7 +5037,25 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node)
         Node lem;
         if (k == kind::SQRT)
         {
-          lem = nm->mkNode(kind::MULT, var, var).eqNode(node[0]);
+          Node skolemApp =
+              getArithSkolemApp(logicRequest, node[0], ArithSkolemId::SQRT);
+          Node uf = skolemApp.eqNode(var);
+          Node nonNeg = nm->mkNode(
+              kind::AND, nm->mkNode(kind::MULT, var, var).eqNode(node[0]), uf);
+
+          // sqrt(x) reduces to:
+          // choice y. ite(x >= 0.0, y * y = x ^ Uf(x), Uf(x))
+          //
+          // Uf(x) makes sure that the reduction still behaves like a function,
+          // otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be
+          // satisfiable. On the original formula, this would require that we
+          // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid
+          // model.
+          lem = nm->mkNode(
+              kind::ITE,
+              nm->mkNode(kind::GEQ, node[0], nm->mkConst(Rational(0))),
+              nonNeg,
+              uf);
         }
         else
         {
@@ -5102,23 +5120,29 @@ Node TheoryArithPrivate::getArithSkolem(LogicRequest& logicRequest,
     TypeNode tn;
     std::string name;
     std::string desc;
-    if (asi == arith_skolem_div_by_zero)
+    switch (asi)
     {
-      tn = nm->realType();
-      name = std::string("divByZero");
-      desc = std::string("partial real division");
-    }
-    else if (asi == arith_skolem_int_div_by_zero)
-    {
-      tn = nm->integerType();
-      name = std::string("intDivByZero");
-      desc = std::string("partial int division");
-    }
-    else if (asi == arith_skolem_mod_by_zero)
-    {
-      tn = nm->integerType();
-      name = std::string("modZero");
-      desc = std::string("partial modulus");
+      case ArithSkolemId::DIV_BY_ZERO:
+        tn = nm->realType();
+        name = std::string("divByZero");
+        desc = std::string("partial real division");
+        break;
+      case ArithSkolemId::INT_DIV_BY_ZERO:
+        tn = nm->integerType();
+        name = std::string("intDivByZero");
+        desc = std::string("partial int division");
+        break;
+      case ArithSkolemId::MOD_BY_ZERO:
+        tn = nm->integerType();
+        name = std::string("modZero");
+        desc = std::string("partial modulus");
+        break;
+      case ArithSkolemId::SQRT:
+        tn = nm->realType();
+        name = std::string("sqrtUf");
+        desc = std::string("partial sqrt");
+        break;
+      default: Unhandled();
     }
 
     Node skolem;
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 03cb81785..3f46ddd59 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -828,11 +828,16 @@ private:
 
   Statistics d_statistics;
 
-  enum ArithSkolemId
+  enum class ArithSkolemId
   {
-    arith_skolem_div_by_zero,
-    arith_skolem_int_div_by_zero,
-    arith_skolem_mod_by_zero,
+    /* an uninterpreted function f s.t. f(x) = x / 0.0 (real division) */
+    DIV_BY_ZERO,
+    /* an uninterpreted function f s.t. f(x) = x / 0 (integer division) */
+    INT_DIV_BY_ZERO,
+    /* an uninterpreted function f s.t. f(x) = x mod 0 */
+    MOD_BY_ZERO,
+    /* an uninterpreted function f s.t. f(x) = sqrt(x) */
+    SQRT,
   };
 
   /**
diff --git a/src/theory/quantifiers/fun_def_evaluator.cpp b/src/theory/quantifiers/fun_def_evaluator.cpp
index 376d0eb47..8eb0ef686 100644
--- a/src/theory/quantifiers/fun_def_evaluator.cpp
+++ b/src/theory/quantifiers/fun_def_evaluator.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/fun_def_evaluator.h"
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/rewriter.h"
 
@@ -53,6 +54,8 @@ Node FunDefEvaluator::evaluate(Node n) const
   Assert(Rewriter::rewrite(n) == n);
   Trace("fd-eval") << "FunDefEvaluator: evaluate " << n << std::endl;
   NodeManager* nm = NodeManager::currentNM();
+  std::unordered_map<TNode, unsigned, TNodeHashFunction> funDefCount;
+  std::unordered_map<TNode, unsigned, TNodeHashFunction>::iterator itCount;
   std::unordered_map<TNode, Node, TNodeHashFunction> visited;
   std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
   std::map<Node, FunDefInfo>::const_iterator itf;
@@ -75,6 +78,13 @@ Node FunDefEvaluator::evaluate(Node n) const
         Trace("fd-eval-debug") << "constant " << cur << std::endl;
         visited[cur] = cur;
       }
+      else if (cur.getKind() == ITE)
+      {
+        Trace("fd-eval-debug") << "ITE " << cur << std::endl;
+        visited[cur] = Node::null();
+        visit.push_back(cur);
+        visit.push_back(cur[0]);
+      }
       else
       {
         Trace("fd-eval-debug") << "recurse " << cur << std::endl;
@@ -102,6 +112,34 @@ Node FunDefEvaluator::evaluate(Node n) const
         {
           children.push_back(cur.getOperator());
         }
+        else if (ck == ITE)
+        {
+          // get evaluation of condition
+          it = visited.find(cur[0]);
+          Assert(it != visited.end());
+          Assert(!it->second.isNull());
+          if (!it->second.isConst())
+          {
+            Trace("fd-eval") << "FunDefEvaluator: couldn't reduce condition of "
+                                "ITE to const, FAIL\n";
+            return Node::null();
+          }
+          // pick child to evaluate depending on condition eval
+          unsigned childIdxToEval = it->second.getConst<bool>() ? 1 : 2;
+          Trace("fd-eval-debug2")
+              << "FunDefEvaluator: result of ITE condition : "
+              << it->second.getConst<bool>() << "\n";
+          // the result will be the result of evaluation the child
+          visited[cur] = cur[childIdxToEval];
+          // push back self and child. The child will be evaluated first and
+          // result will be the result of evaluation child
+          visit.push_back(cur);
+          visit.push_back(cur[childIdxToEval]);
+          Trace("fd-eval-debug2") << "FunDefEvaluator: result will be from : "
+                                  << cur[childIdxToEval] << "\n";
+          continue;
+        }
+        unsigned child CVC4_UNUSED = 0;
         for (const Node& cn : cur)
         {
           it = visited.find(cn);
@@ -109,20 +147,37 @@ Node FunDefEvaluator::evaluate(Node n) const
           Assert(!it->second.isNull());
           childChanged = childChanged || cn != it->second;
           children.push_back(it->second);
+          Trace("fd-eval-debug2") << "argument " << child++
+                                  << " eval : " << it->second << std::endl;
         }
         if (cur.getKind() == APPLY_UF)
         {
           // need to evaluate it
           f = cur.getOperator();
+          Trace("fd-eval-debug2")
+              << "FunDefEvaluator: need to eval " << f << "\n";
           itf = d_funDefMap.find(f);
-          if (itf == d_funDefMap.end())
+          itCount = funDefCount.find(f);
+          if (itCount == funDefCount.end())
           {
-            Trace("fd-eval") << "FunDefEvaluator: no definition for " << f
-                             << ", FAIL" << std::endl;
+            funDefCount[f] = 0;
+            itCount = funDefCount.find(f);
+          }
+          if (itf == d_funDefMap.end()
+              || itCount->second > options::sygusRecFunEvalLimit())
+          {
+            Trace("fd-eval")
+                << "FunDefEvaluator: "
+                << (itf == d_funDefMap.end() ? "no definition for "
+                                             : "too many evals for ")
+                << f << ", FAIL" << std::endl;
             return Node::null();
           }
+          ++funDefCount[f];
           // get the function definition
           Node sbody = itf->second.d_body;
+          Trace("fd-eval-debug2")
+              << "FunDefEvaluator: definition: " << sbody << "\n";
           const std::vector<Node>& args = itf->second.d_args;
           if (!args.empty())
           {
@@ -131,6 +186,17 @@ Node FunDefEvaluator::evaluate(Node n) const
                 args.begin(), args.end(), children.begin(), children.end());
             // rewrite it
             sbody = Rewriter::rewrite(sbody);
+            if (Trace.isOn("fd-eval-debug2"))
+            {
+              Trace("fd-eval-debug2")
+                  << "FunDefEvaluator: evaluation with args:\n";
+              for (const Node& child : children)
+              {
+                Trace("fd-eval-debug2") << "..." << child << "\n";
+              }
+              Trace("fd-eval-debug2")
+                  << "FunDefEvaluator: results in " << sbody << "\n";
+            }
           }
           // our result is the result of the body
           visited[cur] = sbody;
@@ -139,6 +205,8 @@ Node FunDefEvaluator::evaluate(Node n) const
           // evaluating the body.
           if (!sbody.isConst())
           {
+            Trace("fd-eval-debug2") << "FunDefEvaluator: will map " << cur
+                                    << " from body " << sbody << "\n";
             visit.push_back(cur);
             visit.push_back(sbody);
           }
@@ -150,25 +218,35 @@ Node FunDefEvaluator::evaluate(Node n) const
             ret = nm->mkNode(cur.getKind(), children);
             ret = Rewriter::rewrite(ret);
           }
+          Trace("fd-eval-debug2") << "built from arguments " << ret << "\n";
           visited[cur] = ret;
         }
       }
       else if (cur != curEval && !curEval.isConst())
       {
         Trace("fd-eval-debug") << "from body " << cur << std::endl;
+        Trace("fd-eval-debug") << "and eval  " << curEval << std::endl;
         // we had to evaluate our body, which should have a definition now
         it = visited.find(curEval);
-        Assert(it != visited.end());
-        // our definition is the result of the body
-        visited[cur] = it->second;
+        if (it == visited.end())
+        {
+          Trace("fd-eval-debug2") << "eval without definition\n";
+          // this is the case where curEval was not a constant but it was
+          // irreducible, for example (DT_SYGUS_EVAL e args)
+          visited[cur] = curEval;
+        }
+        else
+        {
+          Trace("fd-eval-debug2")
+              << "eval with definition " << it->second << "\n";
+          visited[cur] = it->second;
       }
     }
+    }
   } while (!visit.empty());
+  Trace("fd-eval") << "FunDefEvaluator: return " << visited[n] << ", SUCCESS\n";
   Assert(visited.find(n) != visited.end());
   Assert(!visited.find(n)->second.isNull());
-  Assert(visited.find(n)->second.isConst());
-  Trace("fd-eval") << "FunDefEvaluator: return SUCCESS " << visited[n]
-                   << std::endl;
   return visited[n];
 }
 
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index aa0af6f1d..c806bb1e7 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -31,12 +31,9 @@ namespace theory {
 namespace quantifiers {
 
 Cegis::Cegis(QuantifiersEngine* qe, SynthConjecture* p)
-    : SygusModule(qe, p), d_eval_unfold(nullptr), d_using_gr_repair(false)
+    : SygusModule(qe, p), d_eval_unfold(nullptr), d_usingSymCons(false)
 {
-  if (options::sygusEvalUnfold())
-  {
-    d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold();
-  }
+  d_eval_unfold = qe->getTermDatabaseSygus()->getEvalUnfold();
 }
 
 bool Cegis::initialize(Node conj,
@@ -80,7 +77,7 @@ bool Cegis::processInitialize(Node conj,
   for (unsigned i = 0; i < csize; i++)
   {
     Trace("cegis") << "...register enumerator " << candidates[i];
-    bool do_repair_const = false;
+    bool useSymCons = false;
     if (options::sygusRepairConst())
     {
       TypeNode ctn = candidates[i].getType();
@@ -88,15 +85,15 @@ bool Cegis::processInitialize(Node conj,
       SygusTypeInfo& cti = d_tds->getTypeInfo(ctn);
       if (cti.hasSubtermSymbolicCons())
       {
-        do_repair_const = true;
-        // remember that we are doing grammar-based repair
-        d_using_gr_repair = true;
-        Trace("cegis") << " (using repair)";
+        useSymCons = true;
+        // remember that we are using symbolic constructors
+        d_usingSymCons = true;
+        Trace("cegis") << " (using symbolic constructors)";
       }
     }
     Trace("cegis") << std::endl;
     d_tds->registerEnumerator(
-        candidates[i], candidates[i], d_parent, erole, do_repair_const);
+        candidates[i], candidates[i], d_parent, erole, useSymCons);
   }
   return true;
 }
@@ -135,7 +132,10 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
   }
   NodeManager* nm = NodeManager::currentNM();
   bool addedEvalLemmas = false;
-  if (options::sygusRefEval())
+  // Refinement evaluation should not be done for grammars with symbolic
+  // constructors.
+  bool doRefEval = options::sygusRefEval() && !d_usingSymCons;
+  if (doRefEval)
   {
     Trace("cegqi-engine") << "  *** Do refinement lemma evaluation"
                           << (doGen ? " with conjecture-specific refinement"
@@ -169,7 +169,8 @@ bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
     }
   }
   // we only do evaluation unfolding for passive enumerators
-  if (doGen && d_eval_unfold != nullptr)
+  bool doEvalUnfold = (doGen && options::sygusEvalUnfold()) || d_usingSymCons;
+  if (doEvalUnfold)
   {
     Trace("cegqi-engine") << "  *** Do evaluation unfolding..." << std::endl;
     std::vector<Node> eager_terms, eager_vals, eager_exps;
@@ -239,7 +240,7 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
     }
   }
   // if we are using grammar-based repair
-  if (d_using_gr_repair)
+  if (d_usingSymCons && options::sygusRepairConst())
   {
     SygusRepairConst* src = d_parent->getRepairConst();
     Assert(src != nullptr);
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index 08cf98c99..adaecc7f6 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -204,15 +204,15 @@ class Cegis : public SygusModule
    */
   std::unordered_set<unsigned> d_cegis_sample_refine;
 
-  //---------------------------------for sygus repair
-  /** are we using grammar-based repair?
+  //---------------------------------for symbolic constructors
+  /** are we using symbolic constants?
    *
    * This flag is set ot true if at least one of the enumerators allocated
    * by this class has been configured to allow model values with symbolic
    * constructors, such as the "any constant" constructor.
    */
-  bool d_using_gr_repair;
-  //---------------------------------end for sygus repair
+  bool d_usingSymCons;
+  //---------------------------------end for symbolic constructors
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 472a82e29..e4c23977e 100644
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -996,6 +996,10 @@ bool SygusEnumerator::TermEnumMasterInterp::initialize(SygusEnumerator* se,
 Node SygusEnumerator::TermEnumMasterInterp::getCurrent() { return *d_te; }
 bool SygusEnumerator::TermEnumMasterInterp::increment()
 {
+  if (d_te.isFinished())
+  {
+    return false;
+  }
   SygusEnumerator::TermCache& tc = d_se->d_tcache[d_tn];
   Node curr = getCurrent();
   tc.addTerm(curr);
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index 5286ab6f7..42ddbbb7d 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -14,7 +14,9 @@
 
 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 
+#include "expr/sygus_datatype.h"
 #include "options/quantifiers_options.h"
+#include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 using namespace std;
@@ -101,6 +103,10 @@ void SygusEvalUnfold::registerModelValue(Node a,
           antec_exp.size() == 1 ? antec_exp[0] : nm->mkNode(AND, antec_exp);
       // Node antec = n.eqNode( vn );
       TypeNode tn = n.getType();
+      // Check if the sygus type has any symbolic constructors. This will
+      // impact how the unfolding is computed below.
+      SygusTypeInfo& sti = d_tds->getTypeInfo(tn);
+      bool hasSymCons = sti.hasSubtermSymbolicCons();
       // n occurs as an evaluation head, thus it has sygus datatype type
       Assert(tn.isDatatype());
       const Datatype& dt = static_cast<DatatypeType>(tn.toType()).getDatatype();
@@ -148,7 +154,7 @@ void SygusEvalUnfold::registerModelValue(Node a,
             do_unfold = true;
           }
         }
-        if (do_unfold)
+        if (do_unfold || hasSymCons)
         {
           // note that this is replicated for different values
           std::map<Node, Node> vtm;
@@ -158,7 +164,10 @@ void SygusEvalUnfold::registerModelValue(Node a,
               eval_children.end(), it->second[i].begin(), it->second[i].end());
           Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children);
           eval_children.resize(1);
-          res = d_tds->unfold(eval_fun, vtm, exp);
+          // If we explicitly asked to unfold, we use single step, otherwise
+          // we use multi step.
+          res = unfold(eval_fun, vtm, exp, true, !do_unfold);
+          Trace("sygus-eval-unfold") << "Unfold returns " << res << std::endl;
           expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
         }
         else
@@ -170,6 +179,8 @@ void SygusEvalUnfold::registerModelValue(Node a,
           eval_children[0] = vn;
           Node eval_fun = nm->mkNode(DT_SYGUS_EVAL, eval_children);
           res = d_tds->evaluateWithUnfolding(eval_fun);
+          Trace("sygus-eval-unfold")
+              << "Evaluate with unfolding returns " << res << std::endl;
           esit.init(conj, n, res);
           eval_children.resize(1);
           eval_children[0] = n;
@@ -193,6 +204,130 @@ void SygusEvalUnfold::registerModelValue(Node a,
   }
 }
 
+Node SygusEvalUnfold::unfold(Node en,
+                             std::map<Node, Node>& vtm,
+                             std::vector<Node>& exp,
+                             bool track_exp,
+                             bool doRec)
+{
+  if (en.getKind() != DT_SYGUS_EVAL)
+  {
+    Assert(en.isConst());
+    return en;
+  }
+  Trace("sygus-eval-unfold-debug")
+      << "Unfold : " << en << ", track exp is " << track_exp << ", doRec is "
+      << doRec << std::endl;
+  Node ev = en[0];
+  if (track_exp)
+  {
+    std::map<Node, Node>::iterator itv = vtm.find(en[0]);
+    Assert(itv != vtm.end());
+    if (itv != vtm.end())
+    {
+      ev = itv->second;
+    }
+    Assert(en[0].getType() == ev.getType());
+    Assert(ev.isConst());
+  }
+  Trace("sygus-eval-unfold-debug")
+      << "Unfold model value is : " << ev << std::endl;
+  AlwaysAssert(ev.getKind() == APPLY_CONSTRUCTOR);
+  std::vector<Node> args;
+  for (unsigned i = 1, nchild = en.getNumChildren(); i < nchild; i++)
+  {
+    args.push_back(en[i]);
+  }
+
+  TypeNode headType = en[0].getType();
+  Type headTypeT = headType.toType();
+  NodeManager* nm = NodeManager::currentNM();
+  const Datatype& dt = headType.getDatatype();
+  unsigned i = datatypes::utils::indexOf(ev.getOperator());
+  if (track_exp)
+  {
+    // explanation
+    Node ee =
+        nm->mkNode(APPLY_TESTER, Node::fromExpr(dt[i].getTester()), en[0]);
+    if (std::find(exp.begin(), exp.end(), ee) == exp.end())
+    {
+      exp.push_back(ee);
+    }
+  }
+  // if we are a symbolic constructor, unfolding returns the subterm itself
+  Node sop = Node::fromExpr(dt[i].getSygusOp());
+  if (sop.getAttribute(SygusAnyConstAttribute()))
+  {
+    Trace("sygus-eval-unfold-debug")
+        << "...it is an any-constant constructor" << std::endl;
+    Assert(dt[i].getNumArgs() == 1);
+    // If the argument to evaluate is itself concrete, then we use its
+    // argument; otherwise we return its selector.
+    if (en[0].getKind() == APPLY_CONSTRUCTOR)
+    {
+      Trace("sygus-eval-unfold-debug")
+          << "...return (from constructor) " << en[0][0] << std::endl;
+      return en[0][0];
+    }
+    else
+    {
+      Node ret = nm->mkNode(
+          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headTypeT, 0), en[0]);
+      Trace("sygus-eval-unfold-debug")
+          << "...return (from constructor) " << ret << std::endl;
+      return ret;
+    }
+  }
+
+  Assert(!dt.isParametric());
+  std::map<int, Node> pre;
+  for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+  {
+    std::vector<Node> cc;
+    Node s;
+    // get the j^th subfield of en
+    if (en[0].getKind() == APPLY_CONSTRUCTOR)
+    {
+      // if it is a concrete constructor application, as an optimization,
+      // just return the argument
+      s = en[0][j];
+    }
+    else
+    {
+      s = nm->mkNode(
+          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headTypeT, j), en[0]);
+    }
+    cc.push_back(s);
+    if (track_exp)
+    {
+      // update vtm map
+      vtm[s] = ev[j];
+    }
+    cc.insert(cc.end(), args.begin(), args.end());
+    Node argj = nm->mkNode(DT_SYGUS_EVAL, cc);
+    if (doRec)
+    {
+      Trace("sygus-eval-unfold-debug") << "Recurse on " << s << std::endl;
+      // evaluate recursively
+      argj = unfold(argj, vtm, exp, track_exp, doRec);
+    }
+    pre[j] = argj;
+  }
+  Node ret = d_tds->mkGeneric(dt, i, pre);
+  // apply the appropriate substitution to ret
+  ret = datatypes::utils::applySygusArgs(dt, sop, ret, args);
+  // rewrite
+  ret = Rewriter::rewrite(ret);
+  return ret;
+}
+
+Node SygusEvalUnfold::unfold(Node en)
+{
+  std::map<Node, Node> vtm;
+  std::vector<Node> exp;
+  return unfold(en, vtm, exp, false, false);
+}
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.h b/src/theory/quantifiers/sygus/sygus_eval_unfold.h
index adc54c6a7..50b361fc4 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.h
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.h
@@ -83,6 +83,49 @@ class SygusEvalUnfold
                           std::vector<Node>& exps,
                           std::vector<Node>& terms,
                           std::vector<Node>& vals);
+  /** unfold
+   *
+   * This method is called when a sygus term d (typically a variable for a SyGuS
+   * enumerator) has a model value specified by the map vtm. The argument en
+   * is an application of kind DT_SYGUS_EVAL, i.e. eval( d, c1, ..., cm ).
+   * Typically, d is a shared selector chain, although it may also be a
+   * non-constant application of a constructor.
+   *
+   * If doRec is false, this method returns the one-step unfolding of this
+   * evaluation function application. An example of a one step unfolding is:
+   *    eval( C_+( d1, d2 ), t ) ---> +( eval( d1, t ), eval( d2, t ) )
+   *
+   * This function does this unfolding for a (possibly symbolic) evaluation
+   * head, where the argument "variable to model" vtm stores the model value of
+   * variables from this head. This allows us to track an explanation of the
+   * unfolding in the vector exp when track_exp is true.
+   *
+   * For example, if vtm[d] = C_+( C_x(), C_0() ) and track_exp is true, then
+   * this method applied to eval( d, t ) will return
+   * +( eval( d.0, t ), eval( d.1, t ) ), and is-C_+( d ) is added to exp.
+   *
+   * If the argument doRec is true, we do a multi-step unfolding instead of
+   * a single-step unfolding. For example, if vtm[d] = C_+( C_x(), C_0() ),
+   * then this method applied to eval(d,5) will return 5+0 = 0.
+   *
+   * Furthermore, notice that any-constant constructors are *never* expanded to
+   * their concrete model values. This means that the multi-step unfolding when
+   * vtm[d] = C_+( C_x(), any_constant(n) ), then this method applied to
+   * eval(d,5) will return 5 + d.2.1, where the latter term is a shared selector
+   * chain. In other words, this unfolding elaborates the connection between
+   * the builtin integer field d.2.1 of d and the builtin interpretation of
+   * this sygus term, for the given argument.
+   */
+  Node unfold(Node en,
+              std::map<Node, Node>& vtm,
+              std::vector<Node>& exp,
+              bool track_exp = true,
+              bool doRec = false);
+  /**
+   * Same as above, but without explanation tracking. This is used for concrete
+   * evaluation heads
+   */
+  Node unfold(Node en);
 
  private:
   /** sygus term database associated with this utility */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index 3f09a4346..5d4aaf7ae 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -105,7 +105,8 @@ Node SygusUnifRl::purifyLemma(Node n,
       {
         TNode cand = n[0];
         Node tmp = n.substitute(cand, it->second);
-        nv = d_tds->evaluateWithUnfolding(tmp);
+        // should be concrete, can just use the rewriter
+        nv = Rewriter::rewrite(tmp);
         Trace("sygus-unif-rl-purify")
             << "PurifyLemma : model value for " << tmp << " is " << nv << "\n";
       }
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index e74068ace..07997221f 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -15,6 +15,7 @@
 #include "theory/quantifiers/sygus/sygus_unif_strat.h"
 
 #include "theory/datatypes/theory_datatypes_utils.h"
+#include "theory/quantifiers/sygus/sygus_eval_unfold.h"
 #include "theory/quantifiers/sygus/sygus_unif.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
@@ -258,7 +259,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
     Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren);
     Trace("sygus-unif-debug2") << "  Test evaluation of " << eut << "..."
                                << std::endl;
-    eut = d_qe->getTermDatabaseSygus()->unfold(eut);
+    eut = d_qe->getTermDatabaseSygus()->getEvalUnfold()->unfold(eut);
     Trace("sygus-unif-debug2") << "  ...got " << eut;
     Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl;
 
diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 6e69715ef..da4275365 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -591,7 +591,8 @@ bool SynthConjecture::doCheck(std::vector<Node>& lems)
         Trace("cegqi-debug") << "...squery : " << squery << std::endl;
         squery = Rewriter::rewrite(squery);
         Trace("cegqi-debug") << "...rewrites to : " << squery << std::endl;
-        Assert(squery.isConst() && squery.getConst<bool>());
+        Assert(options::sygusRecFun()
+               || (squery.isConst() && squery.getConst<bool>()));
 #endif
         return false;
       }
@@ -711,7 +712,7 @@ void SynthConjecture::doRefine(std::vector<Node>& lems)
   base_lem = base_lem.substitute(
       sk_vars.begin(), sk_vars.end(), sk_subs.begin(), sk_subs.end());
   Trace("cegqi-refine") << "doRefine : rewrite..." << std::endl;
-  base_lem = Rewriter::rewrite(base_lem);
+  base_lem = d_tds->rewriteNode(base_lem);
   Trace("cegqi-refine") << "doRefine : register refinement lemma " << base_lem
                         << "..." << std::endl;
   d_master->registerRefinementLemma(sk_vars, base_lem, lems);
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 9f6954416..4a708e66c 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -276,28 +276,29 @@ void SynthEngine::registerQuantifier(Node q)
 {
   Trace("cegqi-debug") << "SynthEngine: Register quantifier : " << q
                        << std::endl;
-  if (d_quantEngine->getOwner(q) == this)
+  if (d_quantEngine->getOwner(q) != this)
   {
-    Trace("cegqi") << "Register conjecture : " << q << std::endl;
-    if (options::sygusQePreproc())
-    {
-      d_waiting_conj.push_back(q);
-    }
-    else
-    {
-      // assign it now
-      assignConjecture(q);
-    }
+    return;
   }
-  if (options::sygusRecFun())
+  if (d_quantEngine->getQuantAttributes()->isFunDef(q))
   {
-    if (d_quantEngine->getQuantAttributes()->isFunDef(q))
-    {
-      // If it is a recursive function definition, add it to the function
-      // definition evaluator class.
-      FunDefEvaluator* fde = d_tds->getFunDefEvaluator();
-      fde->assertDefinition(q);
-    }
+    Assert(options::sygusRecFun());
+    // If it is a recursive function definition, add it to the function
+    // definition evaluator class.
+    Trace("cegqi") << "Registering function definition : " << q << "\n";
+    FunDefEvaluator* fde = d_tds->getFunDefEvaluator();
+    fde->assertDefinition(q);
+    return;
+  }
+  Trace("cegqi") << "Register conjecture : " << q << std::endl;
+  if (options::sygusQePreproc())
+  {
+    d_waiting_conj.push_back(q);
+  }
+  else
+  {
+    // assign it now
+    assignConjecture(q);
   }
 }
 
@@ -321,8 +322,6 @@ bool SynthEngine::checkConjecture(SynthConjecture* conj)
     bool addedLemma = false;
     for (const Node& lem : cclems)
     {
-      Trace("cegqi-lemma") << "Cegqi::Lemma : counterexample : " << lem
-                           << std::endl;
       if (d_quantEngine->addLemma(lem))
       {
         ++(d_statistics.d_cegqi_lemmas_ce);
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 79b4c9caa..d664a462d 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -741,9 +741,9 @@ Node TermDbSygus::rewriteNode(Node n) const
       {
         return fres;
       }
-      // It may have failed, in which case there are undefined symbols in res.
-      // In this case, we revert to the result of rewriting in the return
-      // statement below.
+      // It may have failed, in which case there are undefined symbols in res or
+      // we reached the limit of evaluations. In this case, we revert to the
+      // result of rewriting in the return statement below.
     }
   }
   return res;
@@ -953,107 +953,6 @@ unsigned TermDbSygus::getAnchorDepth( Node n ) {
   }
 }
 
-Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Node >& exp, bool track_exp ) {
-  if (en.getKind() != DT_SYGUS_EVAL)
-  {
-    Assert(en.isConst());
-    return en;
-  }
-  Trace("sygus-db-debug") << "Unfold : " << en << std::endl;
-  Node ev = en[0];
-  if (track_exp)
-  {
-    std::map<Node, Node>::iterator itv = vtm.find(en[0]);
-    Assert(itv != vtm.end());
-    if (itv != vtm.end())
-    {
-      ev = itv->second;
-    }
-    Assert(en[0].getType() == ev.getType());
-    Assert(ev.isConst());
-  }
-  Assert(ev.getKind() == kind::APPLY_CONSTRUCTOR);
-  std::vector<Node> args;
-  for (unsigned i = 1, nchild = en.getNumChildren(); i < nchild; i++)
-  {
-    args.push_back(en[i]);
-  }
-
-  Type headType = en[0].getType().toType();
-  NodeManager* nm = NodeManager::currentNM();
-  const Datatype& dt = static_cast<DatatypeType>(headType).getDatatype();
-  unsigned i = datatypes::utils::indexOf(ev.getOperator());
-  if (track_exp)
-  {
-    // explanation
-    Node ee = nm->mkNode(
-        kind::APPLY_TESTER, Node::fromExpr(dt[i].getTester()), en[0]);
-    if (std::find(exp.begin(), exp.end(), ee) == exp.end())
-    {
-      exp.push_back(ee);
-    }
-  }
-  // if we are a symbolic constructor, unfolding returns the subterm itself
-  Node sop = Node::fromExpr(dt[i].getSygusOp());
-  if (sop.getAttribute(SygusAnyConstAttribute()))
-  {
-    Trace("sygus-db-debug") << "...it is an any-constant constructor"
-                            << std::endl;
-    Assert(dt[i].getNumArgs() == 1);
-    if (en[0].getKind() == APPLY_CONSTRUCTOR)
-    {
-      return en[0][0];
-    }
-    else
-    {
-      return nm->mkNode(
-          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]);
-    }
-  }
-
-  Assert(!dt.isParametric());
-  std::map<int, Node> pre;
-  for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
-  {
-    std::vector<Node> cc;
-    Node s;
-    // get the j^th subfield of en
-    if (en[0].getKind() == kind::APPLY_CONSTRUCTOR)
-    {
-      // if it is a concrete constructor application, as an optimization,
-      // just return the argument
-      s = en[0][j];
-    }
-    else
-    {
-      s = nm->mkNode(kind::APPLY_SELECTOR_TOTAL,
-                     dt[i].getSelectorInternal(headType, j),
-                     en[0]);
-    }
-    cc.push_back(s);
-    if (track_exp)
-    {
-      // update vtm map
-      vtm[s] = ev[j];
-    }
-    cc.insert(cc.end(), args.begin(), args.end());
-    pre[j] = nm->mkNode(DT_SYGUS_EVAL, cc);
-  }
-  Node ret = mkGeneric(dt, i, pre);
-  // apply the appropriate substitution to ret
-  ret = datatypes::utils::applySygusArgs(dt, sop, ret, args);
-  // rewrite
-  ret = Rewriter::rewrite(ret);
-  return ret;
-}
-
-Node TermDbSygus::unfold(Node en)
-{
-  std::map<Node, Node> vtm;
-  std::vector<Node> exp;
-  return unfold(en, vtm, exp, false);
-}
-
 Node TermDbSygus::evaluateBuiltin(TypeNode tn,
                                   Node bn,
                                   std::vector<Node>& args,
@@ -1105,6 +1004,8 @@ Node TermDbSygus::evaluateWithUnfolding(
         Trace("dt-eval-unfold-debug")
             << "Optimize: evaluate constant head " << ret << std::endl;
         // can just do direct evaluation here
+        // notice we prefer this code to the rewriter since it may use
+        // the evaluator
         std::vector<Node> args;
         bool success = true;
         for (unsigned i = 1, nchild = ret.getNumChildren(); i < nchild; i++)
@@ -1127,7 +1028,7 @@ Node TermDbSygus::evaluateWithUnfolding(
           return rete;
         }
       }
-      ret = unfold( ret );
+      ret = d_eval_unfold->unfold(ret);
     }    
     if( ret.getNumChildren()>0 ){
       std::vector< Node > children;
@@ -1136,7 +1037,7 @@ Node TermDbSygus::evaluateWithUnfolding(
       }
       bool childChanged = false;
       for( unsigned i=0; i<ret.getNumChildren(); i++ ){
-        Node nc = evaluateWithUnfolding( ret[i], visited ); 
+        Node nc = evaluateWithUnfolding(ret[i], visited);
         childChanged = childChanged || nc!=ret[i];
         children.push_back( nc );
       }
@@ -1152,9 +1053,10 @@ Node TermDbSygus::evaluateWithUnfolding(
   }
 }
 
-Node TermDbSygus::evaluateWithUnfolding( Node n ) {
+Node TermDbSygus::evaluateWithUnfolding(Node n)
+{
   std::unordered_map<Node, Node, NodeHashFunction> visited;
-  return evaluateWithUnfolding( n, visited );
+  return evaluateWithUnfolding(n, visited);
 }
 
 bool TermDbSygus::isEvaluationPoint(Node n) const
@@ -1180,4 +1082,3 @@ bool TermDbSygus::isEvaluationPoint(Node n) const
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
-
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 0ec883537..76b5039f6 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -453,31 +453,6 @@ class TermDbSygus {
   static Node getAnchor( Node n );
   static unsigned getAnchorDepth( Node n );
 
- public:
-  /** unfold
-   *
-   * This method returns the one-step unfolding of an evaluation function
-   * application. An example of a one step unfolding is:
-   *    eval( C_+( d1, d2 ), t ) ---> +( eval( d1, t ), eval( d2, t ) )
-   *
-   * This function does this unfolding for a (possibly symbolic) evaluation
-   * head, where the argument "variable to model" vtm stores the model value of
-   * variables from this head. This allows us to track an explanation of the
-   * unfolding in the vector exp when track_exp is true.
-   *
-   * For example, if vtm[d] = C_+( C_x(), C_0() ) and track_exp is true, then
-   * this method applied to eval( d, t ) will return
-   * +( eval( d.0, t ), eval( d.1, t ) ), and is-C_+( d ) is added to exp.
-   */
-  Node unfold(Node en,
-              std::map<Node, Node>& vtm,
-              std::vector<Node>& exp,
-              bool track_exp = true);
-  /**
-   * Same as above, but without explanation tracking. This is used for concrete
-   * evaluation heads
-   */
-  Node unfold(Node en);
 };
 
 }/* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/type_info.cpp b/src/theory/quantifiers/sygus/type_info.cpp
index 1ff0457c4..71ccd60c9 100644
--- a/src/theory/quantifiers/sygus/type_info.cpp
+++ b/src/theory/quantifiers/sygus/type_info.cpp
@@ -140,17 +140,17 @@ void SygusTypeInfo::initialize(TermDbSygus* tds, TypeNode tn)
       d_sym_cons_any_constant = i;
       d_has_subterm_sym_cons = true;
     }
-    // TODO (as part of #1170): we still do not properly catch type
-    // errors in sygus grammars for arguments of builtin operators.
-    // The challenge is that we easily ask for expected argument types of
-    // builtin operators e.g. PLUS. Hence the call to mkGeneric below
-    // will throw a type exception.
     d_ops[n] = i;
     d_arg_ops[i] = n;
     Trace("sygus-db") << std::endl;
-    // ensure that terms that this constructor encodes are
-    // of the type specified in the datatype. This will fail if
-    // e.g. bitvector-and is a constructor of an integer grammar.
+    // We must properly catch type errors in sygus grammars for arguments of
+    // builtin operators. The challenge is that we easily ask for expected
+    // argument types of builtin operators e.g. PLUS. Hence we use a call to
+    // mkGeneric below. This ensures that terms that this constructor encodes
+    // are of the type specified in the datatype. This will fail if
+    // e.g. bitvector-and is a constructor of an integer grammar. Our (version
+    // 2) SyGuS parser ensures that sygus constructors are built from well-typed
+    // terms, so the term created by mkGeneric will also be well-typed here.
     Node g = tds->mkGeneric(dt, i);
     TypeNode gtn = g.getType();
     AlwaysAssert(gtn.isSubtypeOf(btn))
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 8337ba0b0..8730e3a97 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -407,14 +407,15 @@ void QuantifiersEngine::setOwner(Node q, quantifiers::QAttributes& qa)
     // set rewrite engine as owner
     setOwner(q, d_private->d_rr_engine.get(), 2);
   }
-  if (qa.d_sygus)
+  if (qa.d_sygus || (options::sygusRecFun() && !qa.d_fundef_f.isNull()))
   {
     if (d_private->d_synth_e.get() == nullptr)
     {
       Trace("quant-warn") << "WARNING : synth engine is null, and we have : "
                           << q << std::endl;
     }
-    // set synth engine as owner
+    // set synth engine as owner since this is either a conjecture or a function
+    // definition to be used by sygus
     setOwner(q, d_private->d_synth_e.get(), 2);
   }
 }
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 9fad39b6b..7d10cbadc 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -4112,7 +4112,9 @@ void TheoryStrings::registerTerm( Node n, int effort ) {
     Node len = utils::mkNLength(n[0]);
     Node lem = nm->mkNode(AND,
                           nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))),
-                          nm->mkNode(LT, n, len));
+                          nm->mkNode(LEQ, n, len));
+    Trace("strings-lemma") << "Strings::Lemma IDOF range : " << lem
+                           << std::endl;
     d_out->lemma(lem);
   }
 }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 0312c13b7..e4b5b8057 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -537,6 +537,7 @@ set(regress_0_tests
   regress0/nl/coeff-sat.smt2
   regress0/nl/ext-rew-aggr-test.smt2
   regress0/nl/issue3407.smt2
+  regress0/nl/issue3475.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
   regress0/nl/nia-wrong-tl.smt2
@@ -552,6 +553,7 @@ set(regress_0_tests
   regress0/nl/nta/tan-rewrite.smt2
   regress0/nl/real-as-int.smt2
   regress0/nl/real-div-ufnra.smt2
+  regress0/nl/sqrt.smt2
   regress0/nl/sqrt2-value.smt2
   regress0/nl/subs0-unsat-confirm.smt2
   regress0/nl/very-easy-sat.smt2
@@ -869,6 +871,7 @@ set(regress_0_tests
   regress0/strings/indexof-sym-simp.smt2
   regress0/strings/issue1189.smt2
   regress0/strings/issue2958.smt2
+  regress0/strings/issue3497.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/leadingzero001.smt2
   regress0/strings/loop001.smt2
@@ -921,6 +924,7 @@ set(regress_0_tests
   regress0/sygus/no-syntax-test.sy
   regress0/sygus/parity-AIG-d0.sy
   regress0/sygus/parse-bv-let.sy
+  regress0/sygus/pLTL-sygus-syntax-err.sy
   regress0/sygus/real-si-all.sy
   regress0/sygus/sygus-no-wf.sy
   regress0/sygus/sygus-uf.sy
@@ -1718,6 +1722,7 @@ set(regress_1_tests
   regress1/sygus/issue3247.smt2
   regress1/sygus/issue3320-quant.sy
   regress1/sygus/issue3461.sy
+  regress1/sygus/issue3498.smt2
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy
@@ -1731,6 +1736,7 @@ set(regress_1_tests
   regress1/sygus/nia-max-square-ns.sy
   regress1/sygus/no-flat-simp.sy
   regress1/sygus/no-mention.sy
+  regress1/sygus/once_2.sy
   regress1/sygus/only-const-grammar.sy
   regress1/sygus/parity-si-rcons.sy
   regress1/sygus/pbe_multi.sy
@@ -1740,7 +1746,11 @@ set(regress_1_tests
   regress1/sygus/qe.sy
   regress1/sygus/qf_abv.smt2
   regress1/sygus/real-grammar.sy
+  regress1/sygus/rec-fun-swap.sy
   regress1/sygus/rec-fun-sygus.sy
+  regress1/sygus/rec-fun-while-1.sy
+  regress1/sygus/rec-fun-while-2.sy
+  regress1/sygus/rec-fun-while-infinite.sy
   regress1/sygus/re-concat.sy
   regress1/sygus/repair-const-rl.sy
   regress1/sygus/simple-regexp.sy
diff --git a/test/regress/regress0/nl/issue3475.smt2 b/test/regress/regress0/nl/issue3475.smt2
new file mode 100644
index 000000000..128d08a18
--- /dev/null
+++ b/test/regress/regress0/nl/issue3475.smt2
@@ -0,0 +1,6 @@
+(set-logic ALL)
+(declare-fun x () Real)
+(assert (< x 0))
+(assert (not (= (/ (sqrt x) (sqrt x)) x)))
+(set-info :status sat)
+(check-sat)
diff --git a/test/regress/regress0/nl/sqrt.smt2 b/test/regress/regress0/nl/sqrt.smt2
new file mode 100644
index 000000000..fdcec3d62
--- /dev/null
+++ b/test/regress/regress0/nl/sqrt.smt2
@@ -0,0 +1,39 @@
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: unsat
+; EXPECT: sat
+; EXPECT: unsat
+(set-option :incremental true)
+(set-logic ALL)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun z () Real)
+
+(push)
+(assert (= (sqrt 1.0) 1.0))
+(check-sat)
+(pop)
+
+(push)
+(assert (= (sqrt 1.0) (- 1.0)))
+(check-sat)
+(pop)
+
+(push)
+(assert (= x 1.0))
+(assert (not (= (sqrt 1.0) (sqrt x))))
+(check-sat)
+(pop)
+
+(push)
+(assert (< x 0))
+(assert (= (sqrt 1.0) (sqrt x)))
+(check-sat)
+(pop)
+
+(push)
+(assert (= (sqrt y) z))
+(assert (= (sqrt x) (sqrt y)))
+(assert (not (= (sqrt x) z)))
+(check-sat)
+(pop)
diff --git a/test/regress/regress0/strings/issue3497.smt2 b/test/regress/regress0/strings/issue3497.smt2
new file mode 100644
index 000000000..c804de820
--- /dev/null
+++ b/test/regress/regress0/strings/issue3497.smt2
@@ -0,0 +1,9 @@
+(set-info :smt-lib-version 2.5)
+(set-logic QF_SLIA)
+(set-info :status sat)
+(set-option :strings-exp true)
+(declare-fun x () String)
+(declare-fun y () String)
+(assert (= (str.indexof x y 1) (str.len x)))
+(assert (str.contains x y))
+(check-sat)
diff --git a/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
new file mode 100644
index 000000000..1b5690d3a
--- /dev/null
+++ b/test/regress/regress0/sygus/pLTL-sygus-syntax-err.sy
@@ -0,0 +1,93 @@
+; REQUIRES: no-competition
+; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2
+; EXPECT-ERROR: CVC4 Error:
+; EXPECT-ERROR: Parse Error: pLTL-sygus-syntax-err.sy:80.19: number of arguments does not match the constructor type
+; EXPECT-ERROR: 
+; EXPECT-ERROR: (Op2 <O2> <F>)
+; EXPECT-ERROR: ^
+; EXIT: 1
+(set-logic ALL)
+(set-option :lang sygus2)
+;(set-option :sygus-out status)
+(set-option :sygus-rec-fun true)
+(set-option :uf-ho true)
+
+(define-sort Time () Int)
+
+(declare-datatype Var ( (X0) (X1) ))
+
+; Declare Unary Operators.
+(declare-datatype UNARY_OP ( (NOT) (Y) (G) (H) ))
+
+; Declare Binary Operators.
+(declare-datatype BINARY_OP ( (AND) (OR) (IMPLIES) )) ; (S) ))
+
+; Formula Declaration.
+(declare-datatype Formula (
+  (P (Id Var))
+  (Op1 (op1 UNARY_OP) (f Formula))
+  (Op2 (op2 BINARY_OP) (f1 Formula) (f2 Formula))
+  )
+)
+
+; Trace Length.
+(declare-const tn Int)
+(assert (= tn 2))
+
+;cTrace Declaration (trace_index, variable_index)
+(define-fun val ((i Int) (x Var)) Bool
+  (or (and (= i 0) (= x X0))
+      (and (= i 0) (= x X1))
+      (and (= i 1) (= x X1))
+  )
+)
+
+;cpLTL Semantics
+(define-fun-rec holds ((f Formula) (t Time)) Bool
+  (and (<= 0 t tn)
+       (match f (
+         ((P i) (val t i))
+      
+         ((Op1 op g) 
+           (match op (
+             (NOT (not (holds g t))) 
+
+             (Y (and (< 0 t) (holds g (- t 1))))    
+
+             (G (and (holds g t) (or (= t tn) (holds f (+ t 1)))))
+
+             (H (and (holds g t) (or (= t 0) (holds f (- t 1)))))
+          )))
+
+         ((Op2 op f g)     
+           (match op (
+             (AND (and (holds f t) (holds g t)))
+
+             (OR  (or (holds f t) (holds g t)))
+
+             (IMPLIES (or (not (holds f t)) (holds g t)))
+         )))))
+    )
+)
+
+(synth-fun phi ((x0 Var) (x1 Var)) Formula
+  ((<F> Formula) (<O1> UNARY_OP) (<O2> BINARY_OP))
+  (
+   (<F> Formula (
+     (P x0)
+     (P x1)
+     (Op1 <O1> <F>)
+     (Op2 <O2> <F>)
+     )
+   )
+   (<O1> UNARY_OP (NOT Y G H))
+   (<O2> BINARY_OP (AND OR IMPLIES))
+  )
+)
+
+(constraint (holds (Op1 G (phi X0 X1)) 0))
+
+(check-synth)
+
+
+
diff --git a/test/regress/regress1/sygus/issue3498.smt2 b/test/regress/regress1/sygus/issue3498.smt2
new file mode 100644
index 000000000..9fa8fdc1e
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3498.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+; COMMAND-LINE: --sygus-inference --no-check-models
+(set-logic ALL)
+(declare-fun x () Real)
+(assert (= x 1))
+(assert (= (sqrt x) x))
+(check-sat)
diff --git a/test/regress/regress1/sygus/list_recursor.sy b/test/regress/regress1/sygus/list_recursor.sy
index 53c55397e..2e10a0c71 100644
--- a/test/regress/regress1/sygus/list_recursor.sy
+++ b/test/regress/regress1/sygus/list_recursor.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2 --uf-ho
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --uf-ho
 
 (set-logic ALL)
 
diff --git a/test/regress/regress1/sygus/once_2.sy b/test/regress/regress1/sygus/once_2.sy
new file mode 100644
index 000000000..af6d56aaf
--- /dev/null
+++ b/test/regress/regress1/sygus/once_2.sy
@@ -0,0 +1,44 @@
+; EXPECT: unsat
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+(set-logic BV)
+
+(define-sort Stream () (_ BitVec 2))
+
+(define-fun BV_ONE () Stream (_ bv1 2))
+
+(define-fun
+  O ( (X Stream) ) Stream
+  (bvneg (bvand X (bvnot (bvsub X BV_ONE))))
+)
+
+(synth-fun op ((x Stream)) Stream
+  (( y_term Stream))
+  (( y_term Stream (
+    ( Constant Stream)
+    ( Variable Stream)
+    ( bvnot y_term )
+    ( bvand y_term y_term )
+    ( bvor y_term y_term )
+    ( bvneg y_term )
+    ( bvadd y_term y_term )
+    ( bvsub y_term y_term )
+    ( bvmul y_term y_term )
+    ( bvudiv y_term y_term )
+    ( bvurem y_term y_term )
+    ( bvshl y_term y_term )
+    ( bvlshr y_term y_term )
+  ))
+))
+
+(define-fun C ((x Stream)) Bool
+  (= (op x) (O x))
+)
+
+(constraint (and
+(C (_ bv0 2))
+(C (_ bv1 2))
+(C (_ bv2 2))
+(C (_ bv3 2))
+))
+
+(check-synth)
diff --git a/test/regress/regress1/sygus/rec-fun-swap.sy b/test/regress/regress1/sygus/rec-fun-swap.sy
new file mode 100644
index 000000000..056d6a8fc
--- /dev/null
+++ b/test/regress/regress1/sygus/rec-fun-swap.sy
@@ -0,0 +1,76 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
+
+(set-logic ALL)
+
+; The environment datatypes
+(declare-datatype NVars ((x) (y)))
+
+(declare-datatype Pair ((pair (first NVars) (second Int))))
+
+(declare-datatype Env ((cons (head Pair) (tail Env)) (nil)))
+
+(define-fun-rec envStore ((var NVars) (value Int) (env Env)) Env
+  (ite (is-nil env)
+    (cons (pair var value) env)
+    (ite (= var (first (head env)))
+      (cons (pair var value) (tail env))
+      (cons (head env) (envStore var value (tail env)))
+      )
+    )
+  )
+
+(define-fun-rec envSelect ((var NVars) (env Env)) Int
+  (ite (is-nil env)
+    (- 1)
+    (ite (= var (first (head env)))
+      (second (head env))
+      (envSelect var (tail env))
+      )
+    )
+  )
+
+; Syntax for arithmetic expressions
+(declare-datatype Aexp
+  (
+    (Val (val Int))
+    )
+  )
+
+; Function to evaluate arithmetic expressions
+(define-fun-rec evalA ((env Env) (a Aexp)) Int
+    (val a)
+      )
+
+; Syntax for commands
+(declare-datatype Com
+  (
+    (Skip)
+    (Assign (lhs NVars) (rhs Aexp))
+    (CSeq (cBef Com) (aAft Com))
+    )
+  )
+
+; Function to evaluate statements
+(define-fun-rec evalC ((env Env) (c Com)) Env
+  (ite (is-Skip c)
+    env
+    (ite (is-Assign c)
+      (envStore (lhs c) (evalA env (rhs c)) env)
+      (evalC (evalC env (cBef c)) (aAft c)))
+    )
+  )
+
+(synth-fun prog () Com
+  ((C Com) (V NVars) (A Aexp) (I Int))
+  (
+    (C Com (Skip (Assign V A) (CSeq C C)))
+    (V NVars (x y))
+    (A Aexp ((Val I)))
+    (I Int (0 1))
+    )
+)
+
+(constraint (= (evalC (cons (pair y 0) (cons (pair x 1) nil)) prog) (cons (pair y 1) (cons (pair x 0) nil))))
+
+(check-synth)
diff --git a/test/regress/regress1/sygus/rec-fun-sygus.sy b/test/regress/regress1/sygus/rec-fun-sygus.sy
index 13d4782d4..769e173de 100644
--- a/test/regress/regress1/sygus/rec-fun-sygus.sy
+++ b/test/regress/regress1/sygus/rec-fun-sygus.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-rec-fun --lang=sygus2
+; COMMAND-LINE: --sygus-out=status --lang=sygus2
 
 (set-logic ALL)
 
diff --git a/test/regress/regress1/sygus/rec-fun-while-1.sy b/test/regress/regress1/sygus/rec-fun-while-1.sy
new file mode 100644
index 000000000..e805fdc20
--- /dev/null
+++ b/test/regress/regress1/sygus/rec-fun-while-1.sy
@@ -0,0 +1,92 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
+
+(set-logic ALL)
+
+; The environment datatypes
+(declare-datatype NVars ((x)))
+
+(declare-datatype Pair ((build (first NVars) (second Int))))
+
+(declare-datatype Env ((cons (head Pair) (tail Env)) (nil)))
+
+(define-fun-rec envStore ((var NVars) (value Int) (env Env)) Env
+  (ite (is-nil env)
+    (cons (build var value) env)
+    (ite (= var (first (head env)))
+      (cons (build var value) (tail env))
+      (cons (head env) (envStore var value (tail env)))
+      )
+    )
+  )
+
+(define-fun-rec envSelect ((var NVars) (env Env)) Int
+  (ite (is-nil env)
+    0
+    (ite (= var (first (head env)))
+      (second (head env))
+      (envSelect var (tail env))
+      )
+    )
+  )
+
+; Syntax for arithmetic expressions
+(declare-datatype Aexp
+  (
+    (Val (val Int))
+    (Var (name NVars))
+    (Add (addL Aexp) (addR Aexp))
+    )
+  )
+
+; Function to evaluate arithmetic expressions
+(define-fun-rec evalA ((env Env) (a Aexp)) Int
+  (ite (is-Val a)
+    (val a)
+    (envSelect (name a) env)
+    ))
+
+; Syntax for boolean expressions
+(declare-datatype Bexp
+  (
+    (LT (ltL Aexp) (ltR Aexp))
+    )
+  )
+
+; Function to evaluate boolean expressions
+(define-fun-rec evalB ((env Env) (b Bexp)) Bool
+  (< (evalA env (ltL b)) (evalA env (ltR b)))
+  )
+
+; Syntax for commands
+(declare-datatype Com
+  (
+    (Assign (lhs NVars) (rhs Aexp))
+    (While (wCond Bexp) (wCom Com))
+    )
+  )
+
+; Function to evaluate statements
+(define-fun-rec evalC ((env Env) (c Com)) Env
+  (ite (is-Assign c)
+    (envStore (lhs c) (evalA env (rhs c)) env)
+    (ite (evalB env (wCond c)) (evalC (evalC env (wCom c)) c) env)
+    )
+  )
+
+(synth-fun prog () Com
+  ((C1 Com) (C2 Com) (VX NVars) (A1 Aexp) (A2 Aexp) (B Bexp) (I Int))
+  (
+    (C1 Com ((While B C2)))
+    (C2 Com ((Assign VX A2)))
+    (VX NVars (x))
+    (A1 Aexp ((Var VX)))
+    (A2 Aexp ((Val I)))
+    (B Bexp ((LT A1 A2)))
+    (I Int (0 1 (+ I I)))
+    )
+)
+
+(constraint (= (evalC (cons (build x 0) nil) prog) (cons (build x 2) nil)))
+
+(check-synth)
diff --git a/test/regress/regress1/sygus/rec-fun-while-2.sy b/test/regress/regress1/sygus/rec-fun-while-2.sy
new file mode 100644
index 000000000..7e32384b3
--- /dev/null
+++ b/test/regress/regress1/sygus/rec-fun-while-2.sy
@@ -0,0 +1,93 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
+
+(set-logic ALL)
+
+; The environment datatypes
+(declare-datatype NVars ((x) (y)))
+
+(declare-datatype Pair ((build (first NVars) (second Int))))
+
+(declare-datatype Env ((cons (head Pair) (tail Env)) (nil)))
+
+(define-fun-rec envStore ((var NVars) (value Int) (env Env)) Env
+  (ite (is-nil env)
+    (cons (build var value) env)
+    (ite (= var (first (head env)))
+      (cons (build var value) (tail env))
+      (cons (head env) (envStore var value (tail env)))
+      )
+    )
+  )
+
+(define-fun-rec envSelect ((var NVars) (env Env)) Int
+  (ite (is-nil env)
+    0
+    (ite (= var (first (head env)))
+      (second (head env))
+      (envSelect var (tail env))
+      )
+    )
+  )
+
+; Syntax for arithmetic expressions
+(declare-datatype Aexp
+  (
+    (Val (val Int))
+    (Var (name NVars))
+    (Add (addL Aexp) (addR Aexp))
+    (Sub (subL Aexp) (subR Aexp))
+    )
+  )
+
+; Function to evaluate arithmetic expressions
+(define-fun-rec evalA ((env Env) (a Aexp)) Int
+  (ite (is-Val a)
+    (val a)
+    (envSelect (name a) env)
+    ))
+
+; Syntax for boolean expressions
+(declare-datatype Bexp
+  (
+    (GTH (geqL Aexp) (geqR Aexp))
+    )
+  )
+
+; Function to evaluate boolean expressions
+(define-fun-rec evalB ((env Env) (b Bexp)) Bool
+  (> (evalA env (geqL b)) (evalA env (geqR b)))
+  )
+
+; Syntax for commands
+(declare-datatype Com
+  (
+    (Assign (lhs NVars) (rhs Aexp))
+    (While (wCond Bexp) (wCom Com))
+    )
+  )
+
+; Function to evaluate statements
+(define-fun-rec evalC ((env Env) (c Com)) Env
+    (ite (is-Assign c)
+      (envStore (lhs c) (evalA env (rhs c)) env)
+          (ite (evalB env (wCond c)) (evalC (evalC env (wCom c)) c) env)
+        )
+      )
+
+(synth-fun prog () Com
+  ((C1 Com) (C2 Com) (VX NVars) (A1 Aexp) (A2 Aexp) (B Bexp) (I Int))
+  (
+    (C1 Com ((While B C2)))
+    (C2 Com ((Assign VX A2)))
+    (VX NVars (x))
+    (A1 Aexp ((Var VX)))
+    (A2 Aexp ((Val I)))
+    (B Bexp ((GTH A2 A1)))
+    (I Int (2))
+    )
+)
+
+(constraint (= (evalC (cons (build x 0) nil) prog) (cons (build x 2) nil)))
+
+(check-synth)
diff --git a/test/regress/regress1/sygus/rec-fun-while-infinite.sy b/test/regress/regress1/sygus/rec-fun-while-infinite.sy
new file mode 100644
index 000000000..b43b3d5e2
--- /dev/null
+++ b/test/regress/regress1/sygus/rec-fun-while-infinite.sy
@@ -0,0 +1,97 @@
+; EXPECT: unknown
+; COMMAND-LINE: --sygus-out=status --lang=sygus2 --no-check-synth-sol
+
+(set-logic ALL)
+
+; The environment datatypes
+(declare-datatype NVars ((x) (y)))
+
+(declare-datatype Pair ((build (first NVars) (second Int))))
+
+(declare-datatype Env ((cons (head Pair) (tail Env)) (nil)))
+
+(define-fun-rec envStore ((var NVars) (value Int) (env Env)) Env
+  (ite (is-nil env)
+    (cons (build var value) env)
+    (ite (= var (first (head env)))
+      (cons (build var value) (tail env))
+      (cons (head env) (envStore var value (tail env)))
+      )
+    )
+  )
+
+(define-fun-rec envSelect ((var NVars) (env Env)) Int
+  (ite (is-nil env)
+    0
+    (ite (= var (first (head env)))
+      (second (head env))
+      (envSelect var (tail env))
+      )
+    )
+  )
+
+; Syntax for arithmetic expressions
+(declare-datatype Aexp
+  (
+    (Val (val Int))
+    (Var (name NVars))
+    (Add (addL Aexp) (addR Aexp))
+    )
+  )
+
+; Function to evaluate arithmetic expressions
+(define-fun-rec evalA ((env Env) (a Aexp)) Int
+  (ite (is-Val a)
+    (val a)
+    (ite (is-Var a)
+      (envSelect (name a) env)
+      ; (is-Add a)
+      (+ (evalA env (addL a)) (evalA env (addR a)))
+      )))
+
+; Syntax for boolean expressions
+(declare-datatype Bexp
+  (
+    (TRUE)
+    ))
+
+; Function to evaluate boolean expressions
+(define-fun-rec evalB ((env Env) (b Bexp)) Bool
+  (is-TRUE b)
+)
+
+; Syntax for commands
+(declare-datatype Com
+  (
+    (Assign (lhs NVars) (rhs Aexp))
+    (While (wCond Bexp) (wCom Com))
+    )
+  )
+
+; Function to evaluate statements
+(define-fun-rec evalC ((env Env) (c Com)) Env
+  (ite (is-Assign c)
+    (envStore (lhs c) (evalA env (rhs c)) env)
+        ; (is-While c)
+          (ite (evalB env (wCond c)) (evalC (evalC env (wCom c)) c) env)
+        )
+      )
+
+
+(synth-fun prog () Com
+  ((C1 Com) (C2 Com) (V NVars) (A1 Aexp) (A2 Aexp) (A3 Aexp) (B Bexp) (I Int))
+  (
+    (C1 Com ((While B C2)))
+    (C2 Com ((Assign V A1)))
+    (V NVars (x))
+    (A1 Aexp ((Var V)))
+    (A2 Aexp ((Val I)))
+    (A3 Aexp ((Add A1 A2)))
+    (B Bexp (TRUE))
+    (I Int (1))
+    )
+)
+
+(constraint (= (evalC (cons (build x 1) nil) prog) (cons (build x 1) nil)))
+
+(check-synth)