Merge branch 'master' into fix_warnsfix_warns

69 files changed, 977 insertions, 765 deletions

diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018
index 403f6c8a8..b920152b2 100644
--- a/contrib/run-script-smtcomp2018
+++ b/contrib/run-script-smtcomp2018
@@ -34,7 +34,8 @@ QF_LIA)
   finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites
   ;;
 QF_NIA)
-  trywith 300 --nl-ext --nl-ext-tplanes --decision=internal
+  trywith 300 --nl-ext-tplanes --decision=internal
+  trywith 30 --no-nl-ext-tplanes --decision=internal
   # this totals up to more than 20 minutes, although notice that smaller bit-widths may quickly fail
   trywith 300 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cryptominisat
   trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cryptominisat
@@ -43,10 +44,10 @@ QF_NIA)
   finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat
   ;;
 QF_NRA)
-  trywith 300 --nl-ext --nl-ext-tplanes --decision=internal
-  trywith 300 --nl-ext --nl-ext-tplanes --decision=justification --no-nl-ext-factor
-  trywith 30 --nl-ext --nl-ext-tplanes --decision=internal --solve-real-as-int
-  finishwith --nl-ext --nl-ext-tplanes --decision=justification
+  trywith 300 --nl-ext-tplanes --decision=internal
+  trywith 300 --nl-ext-tplanes --decision=justification --no-nl-ext-factor
+  trywith 30 --nl-ext-tplanes --decision=internal --solve-real-as-int
+  finishwith --nl-ext-tplanes --decision=justification
   ;;
 # all logics with UF + quantifiers should either fall under this or special cases below
 ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA)
diff --git a/src/Makefile.am b/src/Makefile.am
index e9fcb5913..6cb179b1d 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -92,8 +92,6 @@ libcvc4_la_SOURCES = \
 	printer/ast/ast_printer.h \
 	printer/cvc/cvc_printer.cpp \
 	printer/cvc/cvc_printer.h \
-	printer/smt1/smt1_printer.cpp \
-	printer/smt1/smt1_printer.h \
 	printer/smt2/smt2_printer.cpp \
 	printer/smt2/smt2_printer.h \
 	printer/tptp/tptp_printer.cpp \
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index 4761ba07e..e58c5319a 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -125,22 +125,25 @@ InteractiveShell::InteractiveShell(ExprManager& exprManager,
       commandsBegin = smt1_commands;
       commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands);
       break;
-    case output::LANG_SMTLIB_V2_0:
-    case output::LANG_SMTLIB_V2_5:
-    case output::LANG_SMTLIB_V2_6:
-      d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
-      commandsBegin = smt2_commands;
-      commandsEnd = smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
-      break;
     case output::LANG_TPTP:
       d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp";
       commandsBegin = tptp_commands;
       commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands);
       break;
     default:
-      std::stringstream ss;
-      ss << "internal error: unhandled language " << lang;
-      throw Exception(ss.str());
+      if (language::isOutputLang_smt2(lang))
+      {
+        d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
+        commandsBegin = smt2_commands;
+        commandsEnd =
+            smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
+      }
+      else
+      {
+        std::stringstream ss;
+        ss << "internal error: unhandled language " << lang;
+        throw Exception(ss.str());
+      }
     }
     d_usingReadline = true;
     int err = ::read_history(d_historyFilename.c_str());
@@ -333,9 +336,8 @@ restart:
     line += "\n";
     goto restart;
   } catch(ParserException& pe) {
-    if(d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_0 ||
-       d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_5 ||
-       d_options.getOutputLanguage() == output::LANG_SMTLIB_V2_6) {
+    if (language::isOutputLang_smt2(d_options.getOutputLanguage()))
+    {
       d_out << "(error \"" << pe << "\")" << endl;
     } else {
       d_out << pe << endl;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 758d10af8..29d720b90 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -64,9 +64,8 @@ int main(int argc, char* argv[]) {
 #ifdef CVC4_COMPETITION_MODE
     *opts.getOut() << "unknown" << endl;
 #endif
-    if(opts.getOutputLanguage() == output::LANG_SMTLIB_V2_0 ||
-       opts.getOutputLanguage() == output::LANG_SMTLIB_V2_5 ||
-       opts.getOutputLanguage() == output::LANG_SMTLIB_V2_6) {
+    if (language::isOutputLang_smt2(opts.getOutputLanguage()))
+    {
       *opts.getOut() << "(error \"" << e << "\")" << endl;
     } else {
       *opts.getErr() << "CVC4 Error:" << endl << e << endl;
diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index b2b5f0c31..bb572688b 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -451,6 +451,14 @@ header = "options/arith_options.h"
   help       = "use non-terminating tangent plane strategy for non-linear"
 
 [[option]]
+  name       = "nlExtTangentPlanesInterleave"
+  category   = "regular"
+  long       = "nl-ext-tplanes-interleave"
+  type       = "bool"
+  default    = "false"
+  help       = "interleave tangent plane strategy for non-linear"
+
+[[option]]
   name       = "nlExtTfTangentPlanes"
   category   = "regular"
   long       = "nl-ext-tf-tplanes"
diff --git a/src/options/language.cpp b/src/options/language.cpp
index 86beffd6d..4c224b95d 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -19,12 +19,62 @@
 namespace CVC4 {
 namespace language {
 
+/** define the end points of smt2 languages */
+namespace input {
+Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6_1;
+}
+namespace output {
+Language LANG_SMTLIB_V2_END = LANG_SMTLIB_V2_6_1;
+}
+
+bool isInputLang_smt2(InputLanguage lang)
+{
+  return (lang >= input::LANG_SMTLIB_V2_0 && lang <= input::LANG_SMTLIB_V2_END)
+         || lang == input::LANG_Z3STR;
+}
+
+bool isOutputLang_smt2(OutputLanguage lang)
+{
+  return (lang >= output::LANG_SMTLIB_V2_0
+          && lang <= output::LANG_SMTLIB_V2_END)
+         || lang == output::LANG_Z3STR;
+}
+
+bool isInputLang_smt2_5(InputLanguage lang, bool exact)
+{
+  return exact ? lang == input::LANG_SMTLIB_V2_5
+               : (lang >= input::LANG_SMTLIB_V2_5
+                  && lang <= input::LANG_SMTLIB_V2_END);
+}
+
+bool isOutputLang_smt2_5(OutputLanguage lang, bool exact)
+{
+  return exact ? lang == output::LANG_SMTLIB_V2_5
+               : (lang >= output::LANG_SMTLIB_V2_5
+                  && lang <= output::LANG_SMTLIB_V2_END);
+}
+
+bool isInputLang_smt2_6(InputLanguage lang, bool exact)
+{
+  return exact ? lang == input::LANG_SMTLIB_V2_6
+               : (lang >= input::LANG_SMTLIB_V2_6
+                  && lang <= input::LANG_SMTLIB_V2_END);
+}
+
+bool isOutputLang_smt2_6(OutputLanguage lang, bool exact)
+{
+  return exact ? lang == output::LANG_SMTLIB_V2_6
+               : (lang >= output::LANG_SMTLIB_V2_6
+                  && lang <= output::LANG_SMTLIB_V2_END);
+}
+
 InputLanguage toInputLanguage(OutputLanguage language) {
   switch(language) {
   case output::LANG_SMTLIB_V1:
   case output::LANG_SMTLIB_V2_0:
   case output::LANG_SMTLIB_V2_5:
   case output::LANG_SMTLIB_V2_6:
+  case output::LANG_SMTLIB_V2_6_1:
   case output::LANG_TPTP:
   case output::LANG_CVC4:
   case output::LANG_Z3STR:
@@ -44,9 +94,11 @@ InputLanguage toInputLanguage(OutputLanguage language) {
 OutputLanguage toOutputLanguage(InputLanguage language) {
   switch(language) {
   case input::LANG_SMTLIB_V1:
+    return OutputLanguage(output::LANG_SMTLIB_V2_0);
   case input::LANG_SMTLIB_V2_0:
   case input::LANG_SMTLIB_V2_5:
   case input::LANG_SMTLIB_V2_6:
+  case input::LANG_SMTLIB_V2_6_1:
   case input::LANG_TPTP:
   case input::LANG_CVC4:
   case input::LANG_Z3STR:
@@ -76,9 +128,6 @@ OutputLanguage toOutputLanguage(std::string language) {
     return output::LANG_CVC4;
   } else if(language == "cvc3" || language == "LANG_CVC3") {
     return output::LANG_CVC3;
-  } else if(language == "smtlib1" || language == "smt1" ||
-            language == "LANG_SMTLIB_V1") {
-    return output::LANG_SMTLIB_V1;
   } else if(language == "smtlib" || language == "smt" ||
             language == "smtlib2" || language == "smt2" ||
             language == "smtlib2.0" || language == "smt2.0" ||
@@ -90,6 +139,11 @@ OutputLanguage toOutputLanguage(std::string language) {
   } else if(language == "smtlib2.6" || language == "smt2.6" ||
             language == "LANG_SMTLIB_V2_6") {
     return output::LANG_SMTLIB_V2_6;
+  }
+  else if (language == "smtlib2.6.1" || language == "smt2.6.1"
+           || language == "LANG_SMTLIB_V2_6_1")
+  {
+    return output::LANG_SMTLIB_V2_6_1;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return output::LANG_TPTP;
   } else if(language == "z3str" || language == "z3-str" ||
@@ -125,6 +179,11 @@ InputLanguage toInputLanguage(std::string language) {
             language == "smtlib2.6" || language == "smt2.6" ||
             language == "LANG_SMTLIB_V2_6" || language == "LANG_SMTLIB_V2") {
     return input::LANG_SMTLIB_V2_6;
+  }
+  else if (language == "smtlib2.6.1" || language == "smt2.6.1"
+           || language == "LANG_SMTLIB_V2_6_1")
+  {
+    return input::LANG_SMTLIB_V2_6_1;
   } else if(language == "tptp" || language == "LANG_TPTP") {
     return input::LANG_TPTP;
   } else if(language == "z3str" || language == "z3-str" ||
diff --git a/src/options/language.h b/src/options/language.h
index f238e765d..c573c4aef 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -30,7 +30,8 @@ namespace language {
 
 namespace input {
 
-enum CVC4_PUBLIC Language {
+enum CVC4_PUBLIC Language
+{
   // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
 
   /** Auto-detect the language */
@@ -53,6 +54,8 @@ enum CVC4_PUBLIC Language {
   LANG_SMTLIB_V2_6,
   /** Backward-compatibility for enumeration naming */
   LANG_SMTLIB_V2 = LANG_SMTLIB_V2_6,
+  /** The SMTLIB v2.6 input language, with support for the strings standard */
+  LANG_SMTLIB_V2_6_1,
   /** The TPTP input language */
   LANG_TPTP,
   /** The CVC4 input language */
@@ -67,7 +70,7 @@ enum CVC4_PUBLIC Language {
 
   /** LANG_MAX is > any valid InputLanguage id */
   LANG_MAX
-};/* enum Language */
+}; /* enum Language */
 
 inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
@@ -87,6 +90,7 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_SMTLIB_V2_6:
     out << "LANG_SMTLIB_V2_6";
     break;
+  case LANG_SMTLIB_V2_6_1: out << "LANG_SMTLIB_V2_6_1"; break;
   case LANG_TPTP:
     out << "LANG_TPTP";
     break;
@@ -109,7 +113,8 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
 
 namespace output {
 
-enum CVC4_PUBLIC Language {
+enum CVC4_PUBLIC Language
+{
   // SPECIAL "NON-LANGUAGE" LANGUAGES HAVE ENUM VALUE < 0
 
   /** Match the output language to the input language */
@@ -122,7 +127,7 @@ enum CVC4_PUBLIC Language {
   // OUTPUT LANGUAGE, IF IT IS "IN PRINCIPLE" A COMMON LANGUAGE,
   // INCLUDE IT HERE
 
-  /** The SMTLIB v1 output language */
+  /** The SMTLIB v1 output language (unsupported) */
   LANG_SMTLIB_V1 = input::LANG_SMTLIB_V1,
   /** The SMTLIB v2.0 output language */
   LANG_SMTLIB_V2_0 = input::LANG_SMTLIB_V2_0,
@@ -132,6 +137,8 @@ enum CVC4_PUBLIC Language {
   LANG_SMTLIB_V2_6 = input::LANG_SMTLIB_V2_6,
   /** Backward-compatibility for enumeration naming */
   LANG_SMTLIB_V2 = input::LANG_SMTLIB_V2,
+  /** The SMTLIB v2.6 output language */
+  LANG_SMTLIB_V2_6_1 = input::LANG_SMTLIB_V2_6_1,
   /** The TPTP output language */
   LANG_TPTP = input::LANG_TPTP,
   /** The CVC4 output language */
@@ -151,7 +158,7 @@ enum CVC4_PUBLIC Language {
 
   /** LANG_MAX is > any valid OutputLanguage id */
   LANG_MAX
-};/* enum Language */
+}; /* enum Language */
 
 inline std::ostream& operator<<(std::ostream& out, Language lang) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& out, Language lang) {
@@ -165,6 +172,8 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) {
   case LANG_SMTLIB_V2_5:
     out << "LANG_SMTLIB_V2_5";
     break;
+  case LANG_SMTLIB_V2_6: out << "LANG_SMTLIB_V2_6"; break;
+  case LANG_SMTLIB_V2_6_1: out << "LANG_SMTLIB_V2_6_1"; break;
   case LANG_TPTP:
     out << "LANG_TPTP";
     break;
@@ -198,6 +207,23 @@ typedef language::output::Language OutputLanguage;
 
 namespace language {
 
+/** Is the language a variant of the smtlib version 2 language? */
+bool isInputLang_smt2(InputLanguage lang) CVC4_PUBLIC;
+bool isOutputLang_smt2(OutputLanguage lang) CVC4_PUBLIC;
+
+/**
+  * Is the language smtlib 2.5 or above? If exact=true, then this method returns
+  * false if the input language is not exactly SMT-LIB 2.6.
+  */
+bool isInputLang_smt2_5(InputLanguage lang, bool exact = false) CVC4_PUBLIC;
+bool isOutputLang_smt2_5(OutputLanguage lang, bool exact = false) CVC4_PUBLIC;
+/**
+  * Is the language smtlib 2.6 or above? If exact=true, then this method returns
+  * false if the input language is not exactly SMT-LIB 2.6.
+  */
+bool isInputLang_smt2_6(InputLanguage lang, bool exact = false) CVC4_PUBLIC;
+bool isOutputLang_smt2_6(OutputLanguage lang, bool exact = false) 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/language.i b/src/options/language.i
index 427e6c608..177e590f5 100644
--- a/src/options/language.i
+++ b/src/options/language.i
@@ -24,6 +24,7 @@ namespace CVC4 {
 %rename(INPUT_LANG_SMTLIB_V2_0) CVC4::language::input::LANG_SMTLIB_V2_0;
 %rename(INPUT_LANG_SMTLIB_V2_5) CVC4::language::input::LANG_SMTLIB_V2_5;
 %rename(INPUT_LANG_SMTLIB_V2_6) CVC4::language::input::LANG_SMTLIB_V2_6;
+%rename(INPUT_LANG_SMTLIB_V2_6_1) CVC4::language::input::LANG_SMTLIB_V2_6_1;
 %rename(INPUT_LANG_TPTP) CVC4::language::input::LANG_TPTP;
 %rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4;
 %rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX;
@@ -36,6 +37,7 @@ namespace CVC4 {
 %rename(OUTPUT_LANG_SMTLIB_V2_0) CVC4::language::output::LANG_SMTLIB_V2_0;
 %rename(OUTPUT_LANG_SMTLIB_V2_5) CVC4::language::output::LANG_SMTLIB_V2_5;
 %rename(OUTPUT_LANG_SMTLIB_V2_6) CVC4::language::output::LANG_SMTLIB_V2_6;
+%rename(OUTPUT_LANG_SMTLIB_V2_6_1) CVC4::language::output::LANG_SMTLIB_V2_6_1;
 %rename(OUTPUT_LANG_TPTP) CVC4::language::output::LANG_TPTP;
 %rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4;
 %rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST;
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 917dae687..46f9e0741 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -423,7 +423,8 @@ static const std::string optionsFootnote = "\n\
     sense of the option.\n\
 ";
 
-static const std::string languageDescription = "\
+static const std::string languageDescription =
+    "\
 Languages currently supported as arguments to the -L / --lang option:\n\
   auto                           attempt to automatically determine language\n\
   cvc4 | presentation | pl       CVC4 presentation language\n\
@@ -432,6 +433,7 @@ Languages currently supported as arguments to the -L / --lang option:\n\
   smt2.0 | smtlib2 | smtlib2.0   SMT-LIB format 2.0\n\
   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
   smt2.6 | smtlib2.6             SMT-LIB format 2.6\n\
+  smt2.6.1 | smtlib2.6.1         SMT-LIB format 2.6 with support for the strings standard\n\
   tptp                           TPTP format (cnf and fof)\n\
   sygus                          SyGuS format\n\
 \n\
@@ -439,11 +441,11 @@ Languages currently supported as arguments to the --output-lang option:\n\
   auto                           match output language to input language\n\
   cvc4 | presentation | pl       CVC4 presentation language\n\
   cvc3                           CVC3 presentation language\n\
-  smt1 | smtlib1                 SMT-LIB format 1.2\n\
   smt | smtlib | smt2 |\n\
   smt2.0 | smtlib2.0 | smtlib2   SMT-LIB format 2.0\n\
   smt2.5 | smtlib2.5             SMT-LIB format 2.5\n\
   smt2.6 | smtlib2.6             SMT-LIB format 2.6\n\
+  smt2.6.1 | smtlib2.6.1         SMT-LIB format 2.6 with support for the strings standard\n\
   tptp                           TPTP format\n\
   z3str                          SMT-LIB 2.0 with Z3-str string constraints\n\
   ast                            internal format (simple syntax trees)\n\
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index a4bab5a8d..1e5d62ef8 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -254,12 +254,6 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     input = new Smt1Input(inputStream);
     break;
 
-  case LANG_SMTLIB_V2_0:
-  case LANG_SMTLIB_V2_5:
-  case LANG_SMTLIB_V2_6:
-    input = new Smt2Input(inputStream, lang);
-    break;
-
   case LANG_SYGUS:
     input = new SygusInput(inputStream);
     break;
@@ -269,9 +263,17 @@ AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStre
     break;
 
   default:
-    std::stringstream ss;
-    ss << "internal error: unhandled language " << lang << " in AntlrInput::newInput";
-    throw InputStreamException(ss.str());
+    if (language::isInputLang_smt2(lang))
+    {
+      input = new Smt2Input(inputStream, lang);
+    }
+    else
+    {
+      std::stringstream ss;
+      ss << "internal error: unhandled language " << lang
+         << " in AntlrInput::newInput";
+      throw InputStreamException(ss.str());
+    }
   }
 
   return input;
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index ceda2ba47..9f161b830 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -91,11 +91,6 @@ Parser* ParserBuilder::build()
   case language::input::LANG_SMTLIB_V1:
     parser = new Smt1(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
-  case language::input::LANG_SMTLIB_V2_0:
-  case language::input::LANG_SMTLIB_V2_5:
-  case language::input::LANG_SMTLIB_V2_6:
-    parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
-    break;
   case language::input::LANG_SYGUS:
     parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
@@ -103,7 +98,14 @@ Parser* ParserBuilder::build()
     parser = new Tptp(d_exprManager, input, d_strictMode, d_parseOnly);
     break;
   default:
-    parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly);
+    if (language::isInputLang_smt2(d_lang))
+    {
+      parser = new Smt2(d_exprManager, input, d_strictMode, d_parseOnly);
+    }
+    else
+    {
+      parser = new Parser(d_exprManager, input, d_strictMode, d_parseOnly);
+    }
     break;
   }
 
diff --git a/src/parser/smt1/smt1.cpp b/src/parser/smt1/smt1.cpp
index c3365eb13..047373436 100644
--- a/src/parser/smt1/smt1.cpp
+++ b/src/parser/smt1/smt1.cpp
@@ -61,6 +61,7 @@ std::unordered_map<std::string, Smt1::Logic> Smt1::newLogicMap() {
   logicMap["ALL_SUPPORTED"] = ALL_SUPPORTED;
   logicMap["QF_ALL"] = QF_ALL_SUPPORTED;
   logicMap["ALL"] = ALL_SUPPORTED;
+  logicMap["HORN"] = ALL_SUPPORTED;
   return logicMap;
 }
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index ae9d304f1..74f8e71d3 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -3103,7 +3103,7 @@ GET_PROOF_TOK : 'get-proof';
 GET_UNSAT_ASSUMPTIONS_TOK : 'get-unsat-assumptions';
 GET_UNSAT_CORE_TOK : 'get-unsat-core';
 EXIT_TOK : 'exit';
-RESET_TOK : { PARSER_STATE->v2_5(false) }? 'reset';
+RESET_TOK : { PARSER_STATE->v2_5() }? 'reset';
 RESET_ASSERTIONS_TOK : 'reset-assertions';
 ITE_TOK : 'ite';
 LET_TOK : { !PARSER_STATE->sygus() }? 'let';
@@ -3362,7 +3362,7 @@ STRING_LITERAL_2_0
  * will be part of the token text.  Use the str[] parser rule instead.
  */
 STRING_LITERAL_2_5
-  : { PARSER_STATE->v2_5(false) || PARSER_STATE->sygus() }?=>
+  : { PARSER_STATE->v2_5() || PARSER_STATE->sygus() }?=>
     '"' (~('"') | '""')* '"'
   ;
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 332c66be1..1d66ab0c1 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -129,10 +129,22 @@ void Smt2::addStringOperators() {
   addOperator(kind::STRING_STRREPL, "str.replace" );
   addOperator(kind::STRING_PREFIX, "str.prefixof" );
   addOperator(kind::STRING_SUFFIX, "str.suffixof" );
-  addOperator(kind::STRING_ITOS, "int.to.str" );
-  addOperator(kind::STRING_STOI, "str.to.int" );
-  addOperator(kind::STRING_IN_REGEXP, "str.in.re");
-  addOperator(kind::STRING_TO_REGEXP, "str.to.re");
+  // at the moment, we only use this syntax for smt2.6.1
+  if (getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_6_1)
+  {
+    addOperator(kind::STRING_ITOS, "str.from-int");
+    addOperator(kind::STRING_STOI, "str.to-int");
+    addOperator(kind::STRING_IN_REGEXP, "str.in-re");
+    addOperator(kind::STRING_TO_REGEXP, "str.to-re");
+  }
+  else
+  {
+    addOperator(kind::STRING_ITOS, "int.to.str");
+    addOperator(kind::STRING_STOI, "str.to.int");
+    addOperator(kind::STRING_IN_REGEXP, "str.in.re");
+    addOperator(kind::STRING_TO_REGEXP, "str.to.re");
+  }
+
   addOperator(kind::REGEXP_CONCAT, "re.++");
   addOperator(kind::REGEXP_UNION, "re.union");
   addOperator(kind::REGEXP_INTER, "re.inter");
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 71aa32492..e9e36e78c 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -155,14 +155,21 @@ public:
   bool v2_0() const {
     return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_0;
   }
-  // 2.6 is a superset of 2.5, use exact=false to query whether smt lib 2.5 or above
-  bool v2_5( bool exact = true ) const {
-    return exact ? getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_5 : 
-                   ( getInput()->getLanguage() >= language::input::LANG_SMTLIB_V2_5 && 
-                     getInput()->getLanguage() <= language::input::LANG_SMTLIB_V2 );
+  /**
+   * Are we using smtlib 2.5 or above? If exact=true, then this method returns
+   * false if the input language is not exactly SMT-LIB 2.5.
+   */
+  bool v2_5(bool exact = false) const
+  {
+    return language::isInputLang_smt2_5(getInput()->getLanguage(), exact);
   }
-  bool v2_6() const {
-    return getInput()->getLanguage() == language::input::LANG_SMTLIB_V2_6;
+  /**
+   * Are we using smtlib 2.6 or above? If exact=true, then this method returns
+   * false if the input language is not exactly SMT-LIB 2.6.
+   */
+  bool v2_6(bool exact = false) const
+  {
+    return language::isInputLang_smt2_6(getInput()->getLanguage(), exact);
   }
   bool sygus() const {
     return getInput()->getLanguage() == language::input::LANG_SYGUS;
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 0958e9d6c..b7ffe6991 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -66,9 +66,7 @@ Smt2Input::~Smt2Input() {
 }
 
 void Smt2Input::setLanguage(InputLanguage lang) {
-  CheckArgument(lang == language::input::LANG_SMTLIB_V2_0 ||
-                lang == language::input::LANG_SMTLIB_V2_5 ||
-                lang == language::input::LANG_SMTLIB_V2_6, lang);
+  CheckArgument(language::isInputLang_smt2(lang), lang);
   d_lang = lang;
 }
 
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index d778ccc2b..f9cd7db83 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -385,6 +385,12 @@ void CvcPrinter::toStream(
           return;
         }else{
           toStream(op, n.getOperator(), depth, types, false);
+          if (n.getNumChildren() == 0)
+          {
+            // for datatype constants d, we print "d" and not "d()"
+            out << op.str();
+            return;
+          }
         }
       }
       break;
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index e8ebadeb8..439649725 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -21,7 +21,6 @@
 #include "options/language.h"
 #include "printer/ast/ast_printer.h"
 #include "printer/cvc/cvc_printer.h"
-#include "printer/smt1/smt1_printer.h"
 #include "printer/smt2/smt2_printer.h"
 #include "printer/tptp/tptp_printer.h"
 
@@ -36,9 +35,6 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
   using namespace CVC4::language::output;
 
   switch(lang) {
-  case LANG_SMTLIB_V1: // TODO the printer
-    return unique_ptr<Printer>(new printer::smt1::Smt1Printer());
-
   case LANG_SMTLIB_V2_0:
     return unique_ptr<Printer>(
         new printer::smt2::Smt2Printer(printer::smt2::smt2_0_variant));
@@ -50,6 +46,10 @@ unique_ptr<Printer> Printer::makePrinter(OutputLanguage lang)
     return unique_ptr<Printer>(
         new printer::smt2::Smt2Printer(printer::smt2::smt2_6_variant));
 
+  case LANG_SMTLIB_V2_6_1:
+    return unique_ptr<Printer>(
+        new printer::smt2::Smt2Printer(printer::smt2::smt2_6_1_variant));
+
   case LANG_TPTP:
     return unique_ptr<Printer>(new printer::tptp::TptpPrinter());
 
diff --git a/src/printer/smt1/smt1_printer.cpp b/src/printer/smt1/smt1_printer.cpp
deleted file mode 100644
index ac3c2f970..000000000
--- a/src/printer/smt1/smt1_printer.cpp
+++ /dev/null
@@ -1,69 +0,0 @@
-/*********************                                                        */
-/*! \file smt1_printer.cpp
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Paul Meng
- ** 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 The pretty-printer interface for the SMT output language
- **
- ** The pretty-printer interface for the SMT output language.
- **/
-#include "printer/smt1/smt1_printer.h"
-
-#include <iostream>
-#include <string>
-#include <typeinfo>
-#include <vector>
-
-#include "expr/expr.h" // for ExprSetDepth etc..
-#include "expr/node_manager.h" // for VarNameAttr
-#include "options/language.h" // for LANG_AST
-#include "smt/command.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace printer {
-namespace smt1 {
-
-void Smt1Printer::toStream(
-    std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const
-{
-  n.toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
-}/* Smt1Printer::toStream() */
-
-void Smt1Printer::toStream(std::ostream& out,
-                           const Command* c,
-                           int toDepth,
-                           bool types,
-                           size_t dag) const
-{
-  c->toStream(out, toDepth, types, dag, language::output::LANG_SMTLIB_V2_5);
-}/* Smt1Printer::toStream() */
-
-void Smt1Printer::toStream(std::ostream& out, const CommandStatus* s) const
-{
-  s->toStream(out, language::output::LANG_SMTLIB_V2_5);
-}/* Smt1Printer::toStream() */
-
-void Smt1Printer::toStream(std::ostream& out, const Model& m) const
-{
-  Printer::getPrinter(language::output::LANG_SMTLIB_V2_5)->toStream(out, m);
-}
-
-void Smt1Printer::toStream(std::ostream& out,
-                           const Model& m,
-                           const Command* c) const
-{
-  // shouldn't be called; only the non-Command* version above should be
-  Unreachable();
-}
-
-}/* CVC4::printer::smt1 namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
diff --git a/src/printer/smt1/smt1_printer.h b/src/printer/smt1/smt1_printer.h
deleted file mode 100644
index 560393b81..000000000
--- a/src/printer/smt1/smt1_printer.h
+++ /dev/null
@@ -1,57 +0,0 @@
-/*********************                                                        */
-/*! \file smt1_printer.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Paul Meng
- ** 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 The pretty-printer interface for the SMT output language
- **
- ** The pretty-printer interface for the SMT output language.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__PRINTER__SMT1_PRINTER_H
-#define __CVC4__PRINTER__SMT1_PRINTER_H
-
-#include <iostream>
-
-#include "printer/printer.h"
-
-namespace CVC4 {
-namespace printer {
-namespace smt1 {
-
-class Smt1Printer : public CVC4::Printer {
- public:
-  using CVC4::Printer::toStream;
-  void toStream(std::ostream& out,
-                TNode n,
-                int toDepth,
-                bool types,
-                size_t dag) const override;
-  void toStream(std::ostream& out,
-                const Command* c,
-                int toDepth,
-                bool types,
-                size_t dag) const override;
-  void toStream(std::ostream& out, const CommandStatus* s) const override;
-  void toStream(std::ostream& out, const Model& m) const override;
-
- private:
-  void toStream(std::ostream& out,
-                const Model& m,
-                const Command* c) const override;
-  void toStream(std::ostream& out, const SExpr& sexpr) const;
-};/* class Smt1Printer */
-
-}/* CVC4::printer::smt1 namespace */
-}/* CVC4::printer namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__PRINTER__SMT1_PRINTER_H */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 8c9680a74..5d2b8972d 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -42,7 +42,13 @@ namespace smt2 {
 
 static OutputLanguage variantToLanguage(Variant v);
 
-static string smtKindString(Kind k);
+static string smtKindString(Kind k, Variant v);
+
+/** returns whether the variant is smt-lib 2.6 or greater */
+bool isVariant_2_6(Variant v)
+{
+  return v == smt2_6_variant || v == smt2_6_1_variant;
+}
 
 static void printBvParameterizedOp(std::ostream& out, TNode n);
 static void printFpParameterizedOp(std::ostream& out, TNode n);
@@ -191,10 +197,10 @@ void Smt2Printer::toStream(std::ostream& out,
       out << (n.getConst<bool>() ? "true" : "false");
       break;
     case kind::BUILTIN:
-      out << smtKindString(n.getConst<Kind>());
+      out << smtKindString(n.getConst<Kind>(), d_variant);
       break;
     case kind::CHAIN_OP:
-      out << smtKindString(n.getConst<Chain>().getOperator());
+      out << smtKindString(n.getConst<Chain>().getOperator(), d_variant);
       break;
     case kind::CONST_RATIONAL: {
       const Rational& r = n.getConst<Rational>();
@@ -323,7 +329,8 @@ void Smt2Printer::toStream(std::ostream& out,
       if (force_nt.isReal())
       {
         out << "(" << smtKindString(force_nt.isInteger() ? kind::TO_INTEGER
-                                                         : kind::TO_REAL)
+                                                         : kind::TO_REAL,
+                                    d_variant)
             << " ";
         toStream(out, n, toDepth, types, TypeNode::null());
         out << ")";
@@ -385,8 +392,8 @@ void Smt2Printer::toStream(std::ostream& out,
     // builtin theory
   case kind::APPLY: break;
   case kind::EQUAL:
-  case kind::DISTINCT: 
-    out << smtKindString(k) << " "; 
+  case kind::DISTINCT:
+    out << smtKindString(k, d_variant) << " ";
     parametricTypeChildren = true;
     break;
   case kind::CHAIN: break;
@@ -407,14 +414,16 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::IMPLIES:
   case kind::OR:
   case kind::XOR:
-  case kind::ITE: out << smtKindString(k) << " "; break;
+  case kind::ITE:
+    out << smtKindString(k, d_variant) << " ";
+    break;
 
-    // uf theory
+  // uf theory
   case kind::APPLY_UF: typeChildren = true; break;
   // higher-order
   case kind::HO_APPLY: break;
   case kind::LAMBDA:
-    out << smtKindString(k) << " ";
+    out << smtKindString(k, d_variant) << " ";
     break;
 
   // arith theory
@@ -453,7 +462,7 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::TO_REAL:
   case kind::POW: 
     parametricTypeChildren = true;
-    out << smtKindString(k) << " "; 
+    out << smtKindString(k, d_variant) << " ";
     break;
 
   case kind::DIVISIBLE:
@@ -466,9 +475,11 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::STORE: typeChildren = true;
   case kind::PARTIAL_SELECT_0:
   case kind::PARTIAL_SELECT_1:
-  case kind::ARRAY_TYPE: out << smtKindString(k) << " "; break;
+  case kind::ARRAY_TYPE:
+    out << smtKindString(k, d_variant) << " ";
+    break;
 
-    // string theory
+  // string theory
   case kind::STRING_CONCAT:
     if(d_variant == z3str_variant) {
       out << "Concat ";
@@ -499,30 +510,30 @@ void Smt2Printer::toStream(std::ostream& out,
       out << ")";
       return;
     }
-    out << "str.in.re ";
+    out << smtKindString(k, d_variant) << " ";
     break;
   }
-  case kind::STRING_LENGTH: out << (d_variant == z3str_variant ? "Length " : "str.len "); break;
-  case kind::STRING_SUBSTR: out << "str.substr "; break;
-  case kind::STRING_CHARAT: out << "str.at "; break;
-  case kind::STRING_STRCTN: out << "str.contains "; break;
-  case kind::STRING_STRIDOF: out << "str.indexof "; break;
-  case kind::STRING_STRREPL: out << "str.replace "; break;
-  case kind::STRING_PREFIX: out << "str.prefixof "; break;
-  case kind::STRING_SUFFIX: out << "str.suffixof "; break;
-  case kind::STRING_ITOS: out << "int.to.str "; break;
-  case kind::STRING_STOI: out << "str.to.int "; break;
-  case kind::STRING_TO_REGEXP: out << "str.to.re "; break;
-  case kind::REGEXP_CONCAT: out << "re.++ "; break;
-  case kind::REGEXP_UNION: out << "re.union "; break;
-  case kind::REGEXP_INTER: out << "re.inter "; break;
-  case kind::REGEXP_STAR: out << "re.* "; break;
-  case kind::REGEXP_PLUS: out << "re.+ "; break;
-  case kind::REGEXP_OPT: out << "re.opt "; break;
-  case kind::REGEXP_RANGE: out << "re.range "; break;
-  case kind::REGEXP_LOOP: out << "re.loop "; break;
-  case kind::REGEXP_EMPTY: out << "re.nostr "; break;
-  case kind::REGEXP_SIGMA: out << "re.allchar "; break;
+  case kind::STRING_LENGTH:
+  case kind::STRING_SUBSTR:
+  case kind::STRING_CHARAT:
+  case kind::STRING_STRCTN:
+  case kind::STRING_STRIDOF:
+  case kind::STRING_STRREPL:
+  case kind::STRING_PREFIX:
+  case kind::STRING_SUFFIX:
+  case kind::STRING_ITOS:
+  case kind::STRING_STOI:
+  case kind::STRING_TO_REGEXP:
+  case kind::REGEXP_CONCAT:
+  case kind::REGEXP_UNION:
+  case kind::REGEXP_INTER:
+  case kind::REGEXP_STAR:
+  case kind::REGEXP_PLUS:
+  case kind::REGEXP_OPT:
+  case kind::REGEXP_RANGE:
+  case kind::REGEXP_LOOP:
+  case kind::REGEXP_EMPTY:
+  case kind::REGEXP_SIGMA: out << smtKindString(k, d_variant) << " "; break;
 
   case kind::CARDINALITY_CONSTRAINT: out << "fmf.card "; break;
   case kind::CARDINALITY_VALUE: out << "fmf.card.val "; break;
@@ -586,12 +597,12 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::TRANSPOSE:
   case kind::TCLOSURE:
     parametricTypeChildren = true;
-    out << smtKindString(k) << " "; 
+    out << smtKindString(k, d_variant) << " ";
     break;
   case kind::MEMBER: typeChildren = true;
   case kind::SET_TYPE:
   case kind::SINGLETON:
-  case kind::COMPLEMENT:out << smtKindString(k) << " "; break;
+  case kind::COMPLEMENT: out << smtKindString(k, d_variant) << " "; break;
   case kind::UNIVERSE_SET:out << "(as univset " << n.getType() << ")";break;
 
     // fp theory
@@ -621,7 +632,8 @@ void Smt2Printer::toStream(std::ostream& out,
   case kind::FLOATINGPOINT_ISNEG:
   case kind::FLOATINGPOINT_ISPOS:
   case kind::FLOATINGPOINT_TO_REAL:
-    out << smtKindString(k) << ' '; break;
+    out << smtKindString(k, d_variant) << ' ';
+    break;
 
   case kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
   case kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT:
@@ -681,7 +693,7 @@ void Smt2Printer::toStream(std::ostream& out,
     case kind::SEP_EMP:
     case kind::SEP_PTO:
     case kind::SEP_STAR:
-    case kind::SEP_WAND: out << smtKindString(k) << " "; break;
+    case kind::SEP_WAND: out << smtKindString(k, d_variant) << " "; break;
 
     case kind::SEP_NIL:
       out << "(as sep.nil " << n.getType() << ")";
@@ -773,7 +785,8 @@ void Smt2Printer::toStream(std::ostream& out,
       }else if( n.getKind()==kind::APPLY_TESTER ){
         unsigned cindex = Datatype::indexOf(n.getOperator().toExpr());
         const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
-        if( d_variant==smt2_6_variant ){
+        if (isVariant_2_6(d_variant))
+        {
           out << "(_ is ";
           toStream(out, Node::fromExpr(dt[cindex].getConstructor()), toDepth < 0 ? toDepth : toDepth - 1, types, TypeNode::null());
           out << ")";
@@ -856,7 +869,7 @@ void Smt2Printer::toStream(std::ostream& out,
       if(forceBinary && i < n.getNumChildren() - 1) {
         // not going to work properly for parameterized kinds!
         Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED);
-        out << " (" << smtKindString(n.getKind()) << ' ';
+        out << " (" << smtKindString(n.getKind(), d_variant) << ' ';
         parens << ')';
         ++c;
       } else {
@@ -869,7 +882,7 @@ void Smt2Printer::toStream(std::ostream& out,
   }
 }/* Smt2Printer::toStream(TNode) */
 
-static string smtKindString(Kind k)
+static string smtKindString(Kind k, Variant v)
 {
   switch(k) {
     // builtin theory
@@ -1039,7 +1052,7 @@ static string smtKindString(Kind k)
 
   //string theory
   case kind::STRING_CONCAT: return "str.++";
-  case kind::STRING_LENGTH: return "str.len";
+  case kind::STRING_LENGTH: return v == z3str_variant ? "Length" : "str.len";
   case kind::STRING_SUBSTR: return "str.substr" ;
   case kind::STRING_STRCTN: return "str.contains" ;
   case kind::STRING_CHARAT: return "str.at" ;
@@ -1047,10 +1060,14 @@ static string smtKindString(Kind k)
   case kind::STRING_STRREPL: return "str.replace" ;
   case kind::STRING_PREFIX: return "str.prefixof" ;
   case kind::STRING_SUFFIX: return "str.suffixof" ;
-  case kind::STRING_ITOS: return "int.to.str" ;
-  case kind::STRING_STOI: return "str.to.int" ;
-  case kind::STRING_IN_REGEXP: return "str.in.re";
-  case kind::STRING_TO_REGEXP: return "str.to.re";
+  case kind::STRING_ITOS:
+    return v == smt2_6_1_variant ? "str.from-int" : "int.to.str";
+  case kind::STRING_STOI:
+    return v == smt2_6_1_variant ? "str.to-int" : "str.to.int";
+  case kind::STRING_IN_REGEXP:
+    return v == smt2_6_1_variant ? "str.in-re" : "str.in.re";
+  case kind::STRING_TO_REGEXP:
+    return v == smt2_6_1_variant ? "str.to-re" : "str.to.re";
   case kind::REGEXP_CONCAT: return "re.++";
   case kind::REGEXP_UNION: return "re.union";
   case kind::REGEXP_INTER: return "re.inter";
@@ -1310,7 +1327,7 @@ void DeclareTypeCommandToStream(std::ostream& out,
   const std::vector<Node>* type_refs = model.getRepSet()->getTypeRepsOrNull(tn);
   if (options::modelUninterpDtEnum() && tn.isSort() && type_refs != nullptr)
   {
-    if (variant == smt2_6_variant)
+    if (isVariant_2_6(variant))
     {
       out << "(declare-datatypes ((" << command.getSymbol() << " 0)) (";
     }
@@ -1893,7 +1910,7 @@ static void toStream(std::ostream& out,
     out << "co";
   }
   out << "datatypes";
-  if (v == smt2_6_variant)
+  if (isVariant_2_6(v))
   {
     out << " (";
     for (vector<DatatypeType>::const_iterator i = datatypes.begin(),
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 922b69a9e..1d281aed4 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -27,14 +27,16 @@ namespace CVC4 {
 namespace printer {
 namespace smt2 {
 
-enum Variant {
+enum Variant
+{
   no_variant,
-  smt2_0_variant, // old-style 2.0 syntax, when it makes a difference
-  smt2_6_variant, // new-style 2.6 syntax, when it makes a difference
-  z3str_variant, // old-style 2.0 and also z3str syntax
-  sygus_variant  // variant for sygus
-};/* enum Variant */
-
+  smt2_0_variant,    // old-style 2.0 syntax, when it makes a difference
+  smt2_6_variant,    // new-style 2.6 syntax, when it makes a difference
+  smt2_6_1_variant,  // new-style 2.6 syntax, when it makes a difference, with
+                     // support for the string standard
+  z3str_variant,     // old-style 2.0 and also z3str syntax
+  sygus_variant      // variant for sygus
+};                   /* enum Variant */
 class Smt2Printer : public CVC4::Printer {
  public:
   Smt2Printer(Variant variant = no_variant) : d_variant(variant) { }
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 97e3f0215..0cff9c8fa 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1304,8 +1304,8 @@ void SmtEngine::setDefaults() {
   // Language-based defaults
   if (!options::bitvectorDivByZeroConst.wasSetByUser())
   {
-    options::bitvectorDivByZeroConst.set(options::inputLanguage()
-                                         == language::input::LANG_SMTLIB_V2_6);
+    options::bitvectorDivByZeroConst.set(
+        language::isInputLang_smt2_6(options::inputLanguage()));
   }
   if (options::inputLanguage() == language::input::LANG_SYGUS)
   {
@@ -1726,6 +1726,14 @@ void SmtEngine::setDefaults() {
   if (options::arithRewriteEq()) {
     d_earlyTheoryPP = false;
   }
+  if (d_logic.isPure(THEORY_ARITH) && !d_logic.areRealsUsed())
+  {
+    if (!options::nlExtTangentPlanesInterleave.wasSetByUser())
+    {
+      Trace("smt") << "setting nlExtTangentPlanesInterleave to true" << endl;
+      options::nlExtTangentPlanesInterleave.set(true);
+    }
+  }
 
   // Set decision mode based on logic (if not set by user)
   if(!options::decisionMode.wasSetByUser()) {
@@ -2262,44 +2270,40 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
     d_filename = value.getValue();
     return;
   } else if(key == "smt-lib-version") {
+    language::input::Language ilang = language::input::LANG_AUTO;
     if( (value.isInteger() && value.getIntegerValue() == Integer(2)) ||
         (value.isRational() && value.getRationalValue() == Rational(2)) ||
         value.getValue() == "2" ||
         value.getValue() == "2.0" ) {
-      options::inputLanguage.set(language::input::LANG_SMTLIB_V2_0);
-
-      // supported SMT-LIB version
-      if(!options::outputLanguage.wasSetByUser() &&
-         ( options::outputLanguage() == language::output::LANG_SMTLIB_V2_5 || options::outputLanguage() == language::output::LANG_SMTLIB_V2_6 )) {
-        options::outputLanguage.set(language::output::LANG_SMTLIB_V2_0);
-        *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_0);
-      }
-      return;
+      ilang = language::input::LANG_SMTLIB_V2_0;
     } else if( (value.isRational() && value.getRationalValue() == Rational(5, 2)) ||
                value.getValue() == "2.5" ) {
-      options::inputLanguage.set(language::input::LANG_SMTLIB_V2_5);
-
-      // supported SMT-LIB version
-      if(!options::outputLanguage.wasSetByUser() &&
-         options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {
-        options::outputLanguage.set(language::output::LANG_SMTLIB_V2_5);
-        *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_5);
-      }
-      return;
+      ilang = language::input::LANG_SMTLIB_V2_5;
     } else if( (value.isRational() && value.getRationalValue() == Rational(13, 5)) ||
                value.getValue() == "2.6" ) {
-      options::inputLanguage.set(language::input::LANG_SMTLIB_V2_6);
-
-      // supported SMT-LIB version
-      if(!options::outputLanguage.wasSetByUser() &&
-         options::outputLanguage() == language::output::LANG_SMTLIB_V2_0) {
-        options::outputLanguage.set(language::output::LANG_SMTLIB_V2_6);
-        *options::out() << language::SetLanguage(language::output::LANG_SMTLIB_V2_6);
+      ilang = language::input::LANG_SMTLIB_V2_6;
+    }
+    else if (value.getValue() == "2.6.1")
+    {
+      ilang = language::input::LANG_SMTLIB_V2_6_1;
+    }
+    else
+    {
+      Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
+      throw UnrecognizedOptionException();
+    }
+    options::inputLanguage.set(ilang);
+    // also update the output language
+    if (!options::outputLanguage.wasSetByUser())
+    {
+      language::output::Language olang = language::toOutputLanguage(ilang);
+      if (options::outputLanguage() != olang)
+      {
+        options::outputLanguage.set(olang);
+        *options::out() << language::SetLanguage(olang);
       }
-      return;
     }
-    Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
-    throw UnrecognizedOptionException();
+    return;
   } else if(key == "status") {
     string s;
     if(value.isAtom()) {
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index c2ebc55b8..f790a9f1a 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -1553,6 +1553,13 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   // nt_lemmas.size() << std::endl;  prioritize lemmas that do not
   // introduce new monomials
   lemmas_proc = flushLemmas(lemmas);
+
+  if (options::nlExtTangentPlanes() && options::nlExtTangentPlanesInterleave())
+  {
+    lemmas = checkTangentPlanes();
+    lemmas_proc += flushLemmas(lemmas);
+  }
+
   if (lemmas_proc > 0) {
     Trace("nl-ext") << "  ...finished with " << lemmas_proc << " new lemmas."
                     << std::endl;
@@ -1590,7 +1597,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   }
   
   //------------------------------------tangent planes
-  if (options::nlExtTangentPlanes())
+  if (options::nlExtTangentPlanes() && !options::nlExtTangentPlanesInterleave())
   {
     lemmas = checkTangentPlanes();
     d_waiting_lemmas.insert(
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index 9fe3b713f..41d74b4a0 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -377,6 +377,14 @@ void LogicInfo::setLogicString(std::string logicString)
     enableQuantifiers();
     arithNonLinear();
     p += 3;
+  }
+  else if (!strcmp(p, "HORN"))
+  {
+    // the HORN logic
+    enableEverything();
+    enableQuantifiers();
+    arithNonLinear();
+    p += 4;
   } else {
     if(!strncmp(p, "QF_", 3)) {
       disableQuantifiers();
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 358efede7..6e59363e2 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -878,10 +878,6 @@ Node CegInstantiator::applySubstitutionToLiteral( Node lit, std::vector< Node >&
 }
   
 bool CegInstantiator::check() {
-  if( d_qe->getTheoryEngine()->needCheck() ){
-    Trace("cbqi-engine") << "  CEGQI instantiator : wait until all ground theories are finished." << std::endl;
-    return false;
-  }
   processAssertions();
   for( unsigned r=0; r<2; r++ ){
     d_effort = r == 0 ? CEG_INST_EFFORT_STANDARD : CEG_INST_EFFORT_FULL;
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index db641a82e..d5a430229 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -479,51 +479,74 @@ Node CegConjecture::getNextDecisionRequest( unsigned& priority ) {
   if( !d_qe->getValuation().hasSatValue( feasible_guard, value ) ) {
     priority = 0;
     return feasible_guard;
-  }else{
-    if( value ){  
-      // the conjecture is feasible
-      if( options::sygusStream() ){
-        Assert( !isSingleInvocation() );
-        // if we are in sygus streaming mode, then get the "next guard" 
-        // which denotes "we have not yet generated the next solution to the conjecture"
-        Node curr_stream_guard = getCurrentStreamGuard();
-        bool needs_new_stream_guard = false;
-        if( curr_stream_guard.isNull() ){
-          needs_new_stream_guard = true;
-        }else{
-          // check the polarity of the guard
-          if( !d_qe->getValuation().hasSatValue( curr_stream_guard, value ) ) {
-            priority = 0;
-            return curr_stream_guard;
-          }else{
-            if( !value ){
-              Trace("cegqi-debug") << "getNextDecision : we have a new solution since stream guard was propagated false: " << curr_stream_guard << std::endl;
-              // need to make the next stream guard
-              needs_new_stream_guard = true;
-              // the guard has propagated false, indicating that a verify
-              // lemma was unsatisfiable. Hence, the previous candidate is
-              // an actual solution. We print and continue the stream.
-              printAndContinueStream();
-            }
-          }
-        }
-        if( needs_new_stream_guard ){
-          // generate a new stream guard
-          curr_stream_guard = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G_Stream", NodeManager::currentNM()->booleanType() ) );
-          curr_stream_guard = d_qe->getValuation().ensureLiteral( curr_stream_guard );
-          AlwaysAssert( !curr_stream_guard.isNull() );
-          d_qe->getOutputChannel().requirePhase( curr_stream_guard, true );
-          d_stream_guards.push_back( curr_stream_guard );
-          Trace("cegqi-debug") << "getNextDecision : allocate new stream guard : " << curr_stream_guard << std::endl;
-          // return it as a decision
-          priority = 0;
-          return curr_stream_guard;
-        }
-      }
+  }
+  if (!value)
+  {
+    Trace("cegqi-debug") << "getNextDecision : conjecture is infeasible."
+                         << std::endl;
+    return Node::null();
+  }
+  // the conjecture is feasible
+  if (options::sygusStream())
+  {
+    Assert(!isSingleInvocation());
+    // if we are in sygus streaming mode, then get the "next guard"
+    // which denotes "we have not yet generated the next solution to the
+    // conjecture"
+    Node curr_stream_guard = getCurrentStreamGuard();
+    bool needs_new_stream_guard = false;
+    if (curr_stream_guard.isNull())
+    {
+      needs_new_stream_guard = true;
     }else{
-      Trace("cegqi-debug") << "getNextDecision : conjecture is infeasible." << std::endl;
-    } 
+      // check the polarity of the guard
+      if (!d_qe->getValuation().hasSatValue(curr_stream_guard, value))
+      {
+        priority = 0;
+        return curr_stream_guard;
+      }
+      if (!value)
+      {
+        Trace("cegqi-debug") << "getNextDecision : we have a new solution "
+                                "since stream guard was propagated false: "
+                             << curr_stream_guard << std::endl;
+        // need to make the next stream guard
+        needs_new_stream_guard = true;
+        // the guard has propagated false, indicating that a verify
+        // lemma was unsatisfiable. Hence, the previous candidate is
+        // an actual solution. We print and continue the stream.
+        printAndContinueStream();
+      }
+    }
+    if (needs_new_stream_guard)
+    {
+      // generate a new stream guard
+      curr_stream_guard = Rewriter::rewrite(NodeManager::currentNM()->mkSkolem(
+          "G_Stream", NodeManager::currentNM()->booleanType()));
+      curr_stream_guard = d_qe->getValuation().ensureLiteral(curr_stream_guard);
+      AlwaysAssert(!curr_stream_guard.isNull());
+      d_qe->getOutputChannel().requirePhase(curr_stream_guard, true);
+      d_stream_guards.push_back(curr_stream_guard);
+      Trace("cegqi-debug") << "getNextDecision : allocate new stream guard : "
+                           << curr_stream_guard << std::endl;
+      // return it as a decision
+      priority = 0;
+      return curr_stream_guard;
+    }
   }
+  // see if the master module has a decision
+  if (!isSingleInvocation())
+  {
+    Assert(d_master != nullptr);
+    Node mlit = d_master->getNextDecisionRequest(priority);
+    if (!mlit.isNull())
+    {
+      Trace("cegqi-debug") << "getNextDecision : master module returned : "
+                           << mlit << std::endl;
+      return mlit;
+    }
+  }
+
   return Node::null();
 }
 
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index 125682e8c..86f5abf61 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -39,7 +39,8 @@ CegInstantiation::~CegInstantiation(){
 }
 
 bool CegInstantiation::needsCheck( Theory::Effort e ) {
-  return e>=Theory::EFFORT_LAST_CALL;
+  return !d_quantEngine->getTheoryEngine()->needCheck()
+         && e >= Theory::EFFORT_LAST_CALL;
 }
 
 QuantifiersModule::QEffort CegInstantiation::needsModel(Theory::Effort e)
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index ab448a2b8..f48955c9f 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -65,80 +65,79 @@ void Cegis::getTermList(const std::vector<Node>& candidates,
   enums.insert(enums.end(), candidates.begin(), candidates.end());
 }
 
-/** construct candidate */
-bool Cegis::constructCandidates(const std::vector<Node>& enums,
-                                const std::vector<Node>& enum_values,
-                                const std::vector<Node>& candidates,
-                                std::vector<Node>& candidate_values,
-                                std::vector<Node>& lems)
+bool Cegis::addEvalLemmas(const std::vector<Node>& candidates,
+                          const std::vector<Node>& candidate_values)
 {
-  candidate_values.insert(
-      candidate_values.end(), enum_values.begin(), enum_values.end());
-
-  if (options::sygusDirectEval())
+  if (!options::sygusDirectEval())
   {
-    NodeManager* nm = NodeManager::currentNM();
-    bool addedEvalLemmas = false;
-    if (options::sygusCRefEval())
+    return false;
+  }
+  NodeManager* nm = NodeManager::currentNM();
+  bool addedEvalLemmas = false;
+  if (options::sygusCRefEval())
+  {
+    Trace("cegqi-engine") << "  *** Do conjecture refinement evaluation..."
+                          << std::endl;
+    // see if any refinement lemma is refuted by evaluation
+    std::vector<Node> cre_lems;
+    getRefinementEvalLemmas(candidates, candidate_values, cre_lems);
+    if (!cre_lems.empty())
     {
-      Trace("cegqi-engine") << "  *** Do conjecture refinement evaluation..."
-                            << std::endl;
-      // see if any refinement lemma is refuted by evaluation
-      std::vector<Node> cre_lems;
-      getRefinementEvalLemmas(candidates, candidate_values, cre_lems);
-      if (!cre_lems.empty())
+      for (const Node& lem : cre_lems)
       {
-        for (unsigned j = 0; j < cre_lems.size(); j++)
+        if (d_qe->addLemma(lem))
         {
-          Node lem = cre_lems[j];
-          if (d_qe->addLemma(lem))
-          {
-            Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem
-                                 << std::endl;
-            addedEvalLemmas = true;
-          }
+          Trace("cegqi-lemma") << "Cegqi::Lemma : cref evaluation : " << lem
+                               << std::endl;
+          addedEvalLemmas = true;
         }
-        // we could, but do not return here.
-        // experimentally, it is better to add the lemmas below as well,
-        // in parallel.
       }
+      /* we could, but do not return here. experimentally, it is better to
+         add the lemmas below as well, in parallel. */
     }
-    Trace("cegqi-engine") << "  *** Do direct evaluation..." << std::endl;
-    std::vector<Node> eager_terms;
-    std::vector<Node> eager_vals;
-    std::vector<Node> eager_exps;
-    TermDbSygus* tds = d_qe->getTermDatabaseSygus();
-    for (unsigned j = 0, size = candidates.size(); j < size; j++)
-    {
-      Trace("cegqi-debug") << "  register " << candidates[j] << " -> "
-                           << candidate_values[j] << std::endl;
-      tds->registerModelValue(candidates[j],
-                              candidate_values[j],
-                              eager_terms,
-                              eager_vals,
-                              eager_exps);
-    }
-    Trace("cegqi-debug") << "...produced " << eager_terms.size()
-                         << " eager evaluation lemmas." << std::endl;
-
-    for (unsigned j = 0, size = eager_terms.size(); j < size; j++)
-    {
-      Node lem = nm->mkNode(kind::OR,
-                            eager_exps[j].negate(),
-                            eager_terms[j].eqNode(eager_vals[j]));
-      if (d_qe->addLemma(lem))
-      {
-        Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem
-                             << std::endl;
-        addedEvalLemmas = true;
-      }
-    }
-    if (addedEvalLemmas)
+  }
+  Trace("cegqi-engine") << "  *** Do direct evaluation..." << std::endl;
+  std::vector<Node> eager_terms, eager_vals, eager_exps;
+  TermDbSygus* tds = d_qe->getTermDatabaseSygus();
+  for (unsigned i = 0, size = candidates.size(); i < size; ++i)
+  {
+    Trace("cegqi-debug") << "  register " << candidates[i] << " -> "
+                         << candidate_values[i] << std::endl;
+    tds->registerModelValue(candidates[i],
+                            candidate_values[i],
+                            eager_terms,
+                            eager_vals,
+                            eager_exps);
+  }
+  Trace("cegqi-debug") << "...produced " << eager_terms.size()
+                       << " eager evaluation lemmas.\n";
+  for (unsigned i = 0, size = eager_terms.size(); i < size; ++i)
+  {
+    Node lem = nm->mkNode(
+        OR, eager_exps[i].negate(), eager_terms[i].eqNode(eager_vals[i]));
+    if (d_qe->addLemma(lem))
     {
-      return false;
+      Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem
+                           << std::endl;
+      addedEvalLemmas = true;
     }
   }
+  return addedEvalLemmas;
+}
 
+/** construct candidate */
+bool Cegis::constructCandidates(const std::vector<Node>& enums,
+                                const std::vector<Node>& enum_values,
+                                const std::vector<Node>& candidates,
+                                std::vector<Node>& candidate_values,
+                                std::vector<Node>& lems)
+{
+  if (addEvalLemmas(enums, enum_values))
+  {
+    return false;
+  }
+  candidate_values.insert(
+      candidate_values.end(), enum_values.begin(), enum_values.end());
   return true;
 }
 
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index 358b50536..7500abb78 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -64,7 +64,7 @@ class Cegis : public SygusModule
                                        Node lem,
                                        std::vector<Node>& lems) override;
 
- private:
+ protected:
   /** If CegConjecture::d_base_inst is exists y. P( d, y ), then this is y. */
   std::vector<Node> d_base_vars;
   /**
@@ -94,6 +94,17 @@ class Cegis : public SygusModule
   bool sampleAddRefinementLemma(const std::vector<Node>& candidates,
                                 const std::vector<Node>& vals,
                                 std::vector<Node>& lems);
+
+  /** evaluates candidate values on current refinement lemmas
+   *
+   * Returns true if refinement lemmas are added after evaluation, false
+   * otherwise.
+   *
+   * Also eagerly unfolds evaluation functions in a heuristic manner, which is
+   * useful e.g. for boolean connectives
+   */
+  bool addEvalLemmas(const std::vector<Node>& candidates,
+                     const std::vector<Node>& candidate_values);
   //-----------------------------------end refinement lemmas
 
   /** Get refinement evaluation lemmas
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index cbd9358e0..ee8fb6f12 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/cegis_unif.h"
 
+#include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
@@ -25,7 +26,7 @@ namespace theory {
 namespace quantifiers {
 
 CegisUnif::CegisUnif(QuantifiersEngine* qe, CegConjecture* p)
-    : SygusModule(qe, p)
+    : Cegis(qe, p), d_sygus_unif(p), d_u_enum_manager(qe, p)
 {
   d_tds = d_qe->getTermDatabaseSygus();
 }
@@ -36,43 +37,51 @@ bool CegisUnif::initialize(Node n,
                            std::vector<Node>& lemmas)
 {
   Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
-  Assert(candidates.size() > 0);
-  if (candidates.size() > 1)
+  /* Init UNIF util */
+  d_sygus_unif.initialize(d_qe, candidates, d_cond_enums, lemmas);
+  Trace("cegis-unif") << "Initializing enums for pure Cegis case\n";
+  std::vector<Node> unif_candidates;
+  /* Initialize enumerators for non-unif functions-to-synhesize */
+  for (const Node& c : candidates)
   {
-    return false;
-  }
-  d_candidate = candidates[0];
-  Trace("cegis-unif") << "Initialize unif utility for " << d_candidate
-                      << "...\n";
-  d_sygus_unif.initialize(d_qe, candidates, d_enums, lemmas);
-  Assert(!d_enums.empty());
-  Trace("cegis-unif") << "Initialize " << d_enums.size() << " enumerators for "
-                      << d_candidate << "...\n";
-  /* initialize the enumerators */
-  for (const Node& e : d_enums)
-  {
-    d_tds->registerEnumerator(e, d_candidate, d_parent, true);
-    Node g = d_tds->getActiveGuardForEnumerator(e);
-    d_enum_to_active_guard[e] = g;
+    if (!d_sygus_unif.usingUnif(c))
+    {
+      Trace("cegis-unif") << "* non-unification candidate : " << c << std::endl;
+      d_tds->registerEnumerator(c, c, d_parent);
+    }
+    else
+    {
+      Trace("cegis-unif") << "* unification candidate : " << c << std::endl;
+      unif_candidates.push_back(c);
+    }
   }
+  // initialize the enumeration manager
+  d_u_enum_manager.initialize(unif_candidates);
   return true;
 }
 
 void CegisUnif::getTermList(const std::vector<Node>& candidates,
-                            std::vector<Node>& terms)
+                            std::vector<Node>& enums)
 {
-  Assert(candidates.size() == 1);
-  Valuation& valuation = d_qe->getValuation();
-  for (const Node& e : d_enums)
+  for (const Node& c : candidates)
   {
-    Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
-    Node g = d_enum_to_active_guard[e];
-    /* Get whether the active guard for this enumerator is if so, then there may
-       exist more values for it, and hence we add it to terms. */
-    Node gstatus = valuation.getSatValue(g);
-    if (!gstatus.isNull() && gstatus.getConst<bool>())
+    if (!d_sygus_unif.usingUnif(c))
     {
-      terms.push_back(e);
+      enums.push_back(c);
+      continue;
+    }
+    Valuation& valuation = d_qe->getValuation();
+    for (const Node& e : d_cond_enums)
+    {
+      Assert(d_enum_to_active_guard.find(e) != d_enum_to_active_guard.end());
+      Node g = d_enum_to_active_guard[e];
+      /* Get whether the active guard for this enumerator is set. If so, then
+         there may exist more values for it, and hence we add it to enums. */
+      Node gstatus = valuation.getSatValue(g);
+      if (!gstatus.isNull() && gstatus.getConst<bool>())
+      {
+        enums.push_back(e);
+      }
     }
   }
 }
@@ -83,16 +92,23 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
                                     std::vector<Node>& candidate_values,
                                     std::vector<Node>& lems)
 {
-  Assert(enums.size() == enum_values.size());
-  if (enums.empty())
+  if (addEvalLemmas(enums, enum_values))
   {
+    Trace("cegis-unif-lemma") << "Added eval lemmas\n";
     return false;
   }
   unsigned min_term_size = 0;
   std::vector<unsigned> enum_consider;
+  NodeManager* nm = NodeManager::currentNM();
   Trace("cegis-unif-enum") << "Register new enumerated values :\n";
   for (unsigned i = 0, size = enums.size(); i < size; ++i)
   {
+    /* Only conditional enumerators will be notified to unif utility */
+    if (std::find(d_cond_enums.begin(), d_cond_enums.end(), enums[i])
+        == d_cond_enums.end())
+    {
+      continue;
+    }
     Trace("cegis-unif-enum") << "  " << enums[i] << " -> " << enum_values[i]
                              << std::endl;
     unsigned sz = d_tds->getSygusTermSize(enum_values[i]);
@@ -110,12 +126,10 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
   /* only consider the enumerators that are at minimum size (for fairness) */
   Trace("cegis-unif-enum") << "...register " << enum_consider.size() << " / "
                            << enums.size() << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
   for (unsigned i = 0, ecsize = enum_consider.size(); i < ecsize; ++i)
   {
     unsigned j = enum_consider[i];
-    Node e = enums[j];
-    Node v = enum_values[j];
+    Node e = enums[j], v = enum_values[j];
     std::vector<Node> enum_lems;
     d_sygus_unif.notifyEnumeration(e, v, enum_lems);
     /* the lemmas must be guarded by the active guard of the enumerator */
@@ -127,123 +141,52 @@ bool CegisUnif::constructCandidates(const std::vector<Node>& enums,
     }
     lems.insert(lems.end(), enum_lems.begin(), enum_lems.end());
   }
-  /* build candidate solution */
-  Assert(candidates.size() == 1);
-  if (d_sygus_unif.constructSolution(candidate_values))
+  /* divide-and-conquer solution bulding for candidates using unif util */
+  std::vector<Node> sols;
+  if (d_sygus_unif.constructSolution(sols))
   {
-    Node vc = candidate_values[0];
-    Trace("cegis-unif-enum") << "... candidate solution :" << vc << "\n";
+    candidate_values.insert(candidate_values.end(), sols.begin(), sols.end());
     return true;
   }
   return false;
 }
 
-Node CegisUnif::purifyLemma(Node n,
-                            bool ensureConst,
-                            std::vector<Node>& model_guards,
-                            BoolNodePairMap& cache)
-{
-  Trace("cegis-unif-purify") << "PurifyLemma : " << n << "\n";
-  BoolNodePairMap::const_iterator it = cache.find(BoolNodePair(ensureConst, n));
-  if (it != cache.end())
-  {
-    Trace("cegis-unif-purify") << "... already visited " << n << "\n";
-    return it->second;
-  }
-  /* Recurse */
-  unsigned size = n.getNumChildren();
-  Kind k = n.getKind();
-  bool fapp = k == APPLY_UF && size > 0 && n[0] == d_candidate;
-  bool childChanged = false;
-  std::vector<Node> children;
-  for (unsigned i = 0; i < size; ++i)
-  {
-    if (i == 0 && fapp)
-    {
-      children.push_back(n[0]);
-      continue;
-    }
-    Node child = purifyLemma(n[i], ensureConst || fapp, model_guards, cache);
-    children.push_back(child);
-    childChanged = childChanged || child != n[i];
-  }
-  Node nb;
-  if (childChanged)
-  {
-    if (n.hasOperator())
-    {
-      children.insert(children.begin(), n.getOperator());
-    }
-    nb = NodeManager::currentNM()->mkNode(k, children);
-    Trace("cegis-unif-purify") << "PurifyLemma : transformed " << n << " into "
-                               << nb << "\n";
-  }
-  else
-  {
-    nb = n;
-  }
-  /* get model value of non-top level applications of d_candidate */
-  if (ensureConst && fapp)
-  {
-    Node nv = d_parent->getModelValue(nb);
-    Trace("cegis-unif-purify") << "PurifyLemma : model value for " << nb
-                               << " is " << nv << "\n";
-    /* test if different, then update model_guards */
-    if (nv != nb)
-    {
-      Trace("cegis-unif-purify") << "PurifyLemma : adding model eq\n";
-      model_guards.push_back(
-          NodeManager::currentNM()->mkNode(EQUAL, nv, nb).negate());
-      nb = nv;
-    }
-  }
-  nb = Rewriter::rewrite(nb);
-  /* every non-top level application of function-to-synthesize must be reduced
-     to a concrete constant */
-  Assert(!ensureConst || nb.isConst());
-  Trace("cegis-unif-purify") << "... caching [" << n << "] = " << nb << "\n";
-  cache[BoolNodePair(ensureConst, n)] = nb;
-  return nb;
-}
-
 void CegisUnif::registerRefinementLemma(const std::vector<Node>& vars,
                                         Node lem,
                                         std::vector<Node>& lems)
 {
-  Node plem;
-  std::vector<Node> model_guards;
-  BoolNodePairMap cache;
-  Trace("cegis-unif") << "Registering lemma at CegisUnif : " << lem << "\n";
-  /* Make the purified lemma which will guide the unification utility. */
-  plem = purifyLemma(lem, false, model_guards, cache);
-  if (!model_guards.empty())
-  {
-    model_guards.push_back(plem);
-    plem = NodeManager::currentNM()->mkNode(OR, model_guards);
-  }
-  plem = Rewriter::rewrite(plem);
-  Trace("cegis-unif") << "Purified lemma : " << plem << "\n";
+  /* Notify lemma to unification utility and get its purified form */
+  Node plem = d_sygus_unif.addRefLemma(lem);
   d_refinement_lemmas.push_back(plem);
-  /* Notify lemma to unification utility */
-  d_sygus_unif.addRefLemma(plem);
   /* Make the refinement lemma and add it to lems. This lemma is guarded by the
      parent's guard, which has the semantics "this conjecture has a solution",
      hence this lemma states: if the parent conjecture has a solution, it
      satisfies the specification for the given concrete point. */
-  /* Store lemma for external modules */
-  lems.push_back(
-      NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem));
+  lems.push_back(NodeManager::currentNM()->mkNode(
+      OR, d_parent->getGuard().negate(), plem));
+}
+
+Node CegisUnif::getNextDecisionRequest(unsigned& priority)
+{
+  return d_u_enum_manager.getNextDecisionRequest(priority);
 }
 
 CegisUnifEnumManager::CegisUnifEnumManager(QuantifiersEngine* qe,
                                            CegConjecture* parent)
-    : d_qe(qe), d_parent(parent), d_curr_guq_val(qe->getSatContext(), 0)
+    : d_qe(qe),
+      d_parent(parent),
+      d_ret_dec(qe->getSatContext(), false),
+      d_curr_guq_val(qe->getSatContext(), 0)
 {
   d_tds = d_qe->getTermDatabaseSygus();
 }
 
 void CegisUnifEnumManager::initialize(std::vector<Node>& cs)
 {
+  if (cs.empty())
+  {
+    return;
+  }
   for (const Node& c : cs)
   {
     // currently, we allocate the same enumerators for candidates of the same
@@ -276,10 +219,23 @@ void CegisUnifEnumManager::registerEvalPts(std::vector<Node>& eis, Node c)
 
 Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority)
 {
+  // have we returned our decision in the current SAT context?
+  if (d_ret_dec.get())
+  {
+    return Node::null();
+  }
+  // only call this after initialization
+  if (d_ce_info.empty())
+  {
+    // if no enumerators, the decision is null
+    d_ret_dec = true;
+    return Node::null();
+  }
   Node lit = getCurrentLiteral();
   bool value;
   if (!d_qe->getValuation().hasSatValue(lit, value))
   {
+    d_ret_dec = true;
     priority = 0;
     return lit;
   }
diff --git a/src/theory/quantifiers/sygus/cegis_unif.h b/src/theory/quantifiers/sygus/cegis_unif.h
index 3100d7d0d..2b1f1584a 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.h
+++ b/src/theory/quantifiers/sygus/cegis_unif.h
@@ -19,139 +19,13 @@
 #include <map>
 #include <vector>
 
-#include "theory/quantifiers/sygus/sygus_module.h"
+#include "theory/quantifiers/sygus/cegis.h"
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
 
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-using BoolNodePair = std::pair<bool, Node>;
-using BoolNodePairHashFunction =
-    PairHashFunction<bool, Node, BoolHashFunction, NodeHashFunction>;
-using BoolNodePairMap =
-    std::unordered_map<BoolNodePair, Node, BoolNodePairHashFunction>;
-
-/** Synthesizes functions in a data-driven SyGuS approach
- *
- * Data is derived from refinement lemmas generated through the regular CEGIS
- * approach. SyGuS is used to generate terms for classifying the data
- * (e.g. using decision tree learning) and thus generate a candidate for a
- * function-to-synthesize.
- *
- * This approach is inspired by the divide and conquer synthesis through
- * unification approach by Alur et al. TACAS 2017, by ICE-based invariant
- * synthesis from Garg et al. CAV 2014 and POPL 2016, and Padhi et al. PLDI 2016
- *
- * This module mantains a function-to-synthesize and a set of term
- * enumerators. When new terms are enumerated it tries to learn a new candidate
- * function, which is verified outside this module. If verification fails a
- * refinement lemma is generated, which this module sends to the utility that
- * learns candidates.
- */
-class CegisUnif : public SygusModule
-{
- public:
-  CegisUnif(QuantifiersEngine* qe, CegConjecture* p);
-  ~CegisUnif();
-  /** initialize this class
-   *
-   * The module takes ownership of a conjecture when it contains a single
-   * function-to-synthesize
-  */
-  bool initialize(Node n,
-                  const std::vector<Node>& candidates,
-                  std::vector<Node>& lemmas) override;
-  /** adds the candidate itself to enums */
-  void getTermList(const std::vector<Node>& candidates,
-                   std::vector<Node>& enums) override;
-  /** Tries to build a new candidate solution with new enumerated expresion
-   *
-   * This function relies on a data-driven unification-based approach for
-   * constructing a solutions for the function-to-synthesize. See SygusUnifRl
-   * for more details.
-   *
-   * Calls to this function are such that terms is the list of active
-   * enumerators (returned by getTermList), and term_values are their current
-   * model values. This function registers { terms -> terms_values } in
-   * the database of values that have been enumerated, which are in turn used
-   * for constructing candidate solutions when possible.
-   *
-   * This function also excludes models where (terms = terms_values) by adding
-   * blocking clauses to lems. For example, for grammar:
-   *   A -> A+A | x | 1 | 0
-   * and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds:
-   *   ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 )
-   * to lems, where G is active guard of the enumerator d (see
-   * TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause
-   * indicates that d should not be given the model value +( x, 1 ) anymore,
-   * since { d -> +( x, 1 ) } has now been added to the database of this class.
-   */
-  bool constructCandidates(const std::vector<Node>& enums,
-                           const std::vector<Node>& enum_values,
-                           const std::vector<Node>& candidates,
-                           std::vector<Node>& candidate_values,
-                           std::vector<Node>& lems) override;
-
-  /** Communicate refinement lemma to unification utility and external modules
-   *
-   * For the lemma to be sent to the external modules it adds a guard from the
-   * parent conjecture which establishes that if the conjecture has a solution
-   * then it must satisfy this refinement lemma
-   *
-   * For the lemma to be sent to the unification utility it purifies the
-   * arguments of the function-to-synthensize such that all of its applications
-   * are over concrete values. E.g.:
-   *   f(f(f(0))) > 1
-   * becomes
-   *   f(0) != c1 v f(c1) != c2 v f(c2) > 1
-   * in which c1 and c2 are concrete integer values
-   *
-   * Note that the lemma is in the deep embedding, which means that the above
-   * example would actually correspond to
-   *   eval(d, 0) != c1 v eval(d, c1) != c2 v eval(d, c2) > 1
-   * in which d is the deep embedding of the function-to-synthesize f
-  */
-  void registerRefinementLemma(const std::vector<Node>& vars,
-                               Node lem,
-                               std::vector<Node>& lems) override;
-
- private:
-  /** sygus term database of d_qe */
-  TermDbSygus* d_tds;
-  /**
-   * Sygus unif utility. This class implements the core algorithm (e.g. decision
-   * tree learning) that this module relies upon.
-   */
-  SygusUnifRl d_sygus_unif;
-  /* Function-to-synthesize (in deep embedding) */
-  Node d_candidate;
-  /**
-   * list of enumerators being used to build solutions for candidate by the
-   * above utility.
-   */
-  std::vector<Node> d_enums;
-  /** map from enumerators to active guards */
-  std::map<Node, Node> d_enum_to_active_guard;
-  /* list of learned refinement lemmas */
-  std::vector<Node> d_refinement_lemmas;
-  /**
-  * This is called on the refinement lemma and will replace the arguments of the
-  * function-to-synthesize by their model values (constants).
-  *
-  * When the traversal hits a function application of the function-to-synthesize
-  * it will proceed to ensure that the arguments of that function application
-  * are constants (the ensureConst becomes "true"). It populates a vector of
-  * guards with the (negated) equalities between the original arguments and
-  * their model values.
-  */
-  Node purifyLemma(Node n,
-                   bool ensureConst,
-                   std::vector<Node>& model_guards,
-                   BoolNodePairMap& cache);
-
-}; /* class CegisUnif */
-
 /** Cegis Unif Enumeration Manager
  *
  * This class enforces a decision heuristic that limits the number of
@@ -228,6 +102,8 @@ class CegisUnifEnumManager
   std::map<TypeNode, TypeInfo> d_ce_info;
   /** literals of the form G_uq_n for each n */
   std::map<unsigned, Node> d_guq_lit;
+  /** Have we returned a decision in the current SAT context? */
+  context::CDO<bool> d_ret_dec;
   /**
    * The minimal n such that G_uq_n is not asserted negatively in the
    * current SAT context.
@@ -252,6 +128,114 @@ class CegisUnifEnumManager
   void registerEvalPtAtSize(TypeNode ct, Node ei, Node guq_lit, unsigned n);
 };
 
+/** Synthesizes functions in a data-driven SyGuS approach
+ *
+ * Data is derived from refinement lemmas generated through the regular CEGIS
+ * approach. SyGuS is used to generate terms for classifying the data
+ * (e.g. using decision tree learning) and thus generate a candidates for
+ * functions-to-synthesize.
+ *
+ * This approach is inspired by the divide and conquer synthesis through
+ * unification approach by Alur et al. TACAS 2017, by ICE-based invariant
+ * synthesis from Garg et al. CAV 2014 and POPL 2016, and Padhi et al. PLDI 2016
+ *
+ * This module mantains a set of functions-to-synthesize and a set of term
+ * enumerators. When new terms are enumerated it tries to learn new candidate
+ * solutions, which are verified outside this module. If verification fails a
+ * refinement lemma is generated, which this module sends to the utility that
+ * learns candidates.
+ */
+class CegisUnif : public Cegis
+{
+ public:
+  CegisUnif(QuantifiersEngine* qe, CegConjecture* p);
+  ~CegisUnif();
+  /** initialize this class */
+  bool initialize(Node n,
+                  const std::vector<Node>& candidates,
+                  std::vector<Node>& lemmas) override;
+  /** Retrieves enumerators for constructing solutions
+   *
+   * Non-unification candidates have themselves as enumerators, while for
+   * unification candidates we add their conditonal enumerators to enums if
+   * their respective guards are set in the current model
+   */
+  void getTermList(const std::vector<Node>& candidates,
+                   std::vector<Node>& enums) override;
+  /** Tries to build new candidate solutions with new enumerated expressions
+   *
+   * This function relies on a data-driven unification-based approach for
+   * constructing solutions for the functions-to-synthesize. See SygusUnifRl for
+   * more details.
+   *
+   * Calls to this function are such that terms is the list of active
+   * enumerators (returned by getTermList), and term_values are their current
+   * model values. This function registers { terms -> terms_values } in
+   * the database of values that have been enumerated, which are in turn used
+   * for constructing candidate solutions when possible.
+   *
+   * This function also excludes models where (terms = terms_values) by adding
+   * blocking clauses to lems. For example, for grammar:
+   *   A -> A+A | x | 1 | 0
+   * and a call where terms = { d } and term_values = { +( x, 1 ) }, it adds:
+   *   ~G V ~is_+( d ) V ~is_x( d.1 ) V ~is_1( d.2 )
+   * to lems, where G is active guard of the enumerator d (see
+   * TermDatabaseSygus::getActiveGuardForEnumerator). This blocking clause
+   * indicates that d should not be given the model value +( x, 1 ) anymore,
+   * since { d -> +( x, 1 ) } has now been added to the database of this class.
+   */
+  bool constructCandidates(const std::vector<Node>& enums,
+                           const std::vector<Node>& enum_values,
+                           const std::vector<Node>& candidates,
+                           std::vector<Node>& candidate_values,
+                           std::vector<Node>& lems) override;
+
+  /** Communicates refinement lemma to unification utility and external modules
+   *
+   * For the lemma to be sent to the external modules it adds a guard from the
+   * parent conjecture which establishes that if the conjecture has a solution
+   * then it must satisfy this refinement lemma
+   *
+   * For the lemma to be sent to the unification utility it purifies the
+   * arguments of the function-to-synthensize such that all of its applications
+   * are over concrete values. E.g.:
+   *   f(f(f(0))) > 1
+   * becomes
+   *   f(0) != c1 v f(c1) != c2 v f(c2) > 1
+   * in which c1 and c2 are concrete integer values
+   *
+   * Note that the lemma is in the deep embedding, which means that the above
+   * example would actually correspond to
+   *   eval(d, 0) != c1 v eval(d, c1) != c2 v eval(d, c2) > 1
+   * in which d is the deep embedding of the function-to-synthesize f
+  */
+  void registerRefinementLemma(const std::vector<Node>& vars,
+                               Node lem,
+                               std::vector<Node>& lems) override;
+  /** get next decision request */
+  Node getNextDecisionRequest(unsigned& priority) override;
+
+ private:
+  /** sygus term database of d_qe */
+  TermDbSygus* d_tds;
+  /**
+   * Sygus unif utility. This class implements the core algorithm (e.g. decision
+   * tree learning) that this module relies upon.
+   */
+  SygusUnifRl d_sygus_unif;
+  /** enumerator manager utility */
+  CegisUnifEnumManager d_u_enum_manager;
+  /**
+   * list of conditonal enumerators to build solutions for candidates being
+   * synthesized with unification techniques
+   */
+  std::vector<Node> d_cond_enums;
+  /** map from enumerators to active guards */
+  std::map<Node, Node> d_enum_to_active_guard;
+  /* The null node */
+  Node d_null;
+}; /* class CegisUnif */
+
 }  // namespace quantifiers
 }  // namespace theory
 }  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/sygus_module.h b/src/theory/quantifiers/sygus/sygus_module.h
index 0a3fa9995..07f5aec9d 100644
--- a/src/theory/quantifiers/sygus/sygus_module.h
+++ b/src/theory/quantifiers/sygus/sygus_module.h
@@ -114,6 +114,14 @@ class SygusModule
                                        std::vector<Node>& lems)
   {
   }
+  /** get next decision request
+   *
+   * This has the same contract as Theory::getNextDecisionRequest.
+   */
+  virtual Node getNextDecisionRequest(unsigned& priority)
+  {
+    return Node::null();
+  }
 
  protected:
   /** reference to quantifier engine */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
index bf23cd0d1..3b7cef4b9 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/sygus_unif_rl.h"
 
+#include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 
 using namespace CVC4::kind;
@@ -22,21 +23,26 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-SygusUnifRl::SygusUnifRl() {}
-
+SygusUnifRl::SygusUnifRl(CegConjecture* p) : d_parent(p) {}
 SygusUnifRl::~SygusUnifRl() {}
 void SygusUnifRl::initialize(QuantifiersEngine* qe,
                              const std::vector<Node>& funs,
                              std::vector<Node>& enums,
                              std::vector<Node>& lemmas)
 {
-  d_true = NodeManager::currentNM()->mkConst(true);
-  d_false = NodeManager::currentNM()->mkConst(false);
-  d_prev_rlemmas = d_true;
-  d_rlemmas = d_true;
-  d_hasRLemmas = false;
   d_ecache.clear();
+  d_cand_to_cond_enum.clear();
+  d_cand_to_pt_enum.clear();
+  /* TODO populate d_unif_candidates and remove lemmas cleaning */
   SygusUnif::initialize(qe, funs, enums, lemmas);
+  lemmas.clear();
+  /* Copy candidates and check whether CegisUnif for any of them */
+  for (const Node& c : d_unif_candidates)
+  {
+    d_app_to_pt[c].clear();
+    d_cand_to_pt_enum[c].clear();
+    d_purified_count[c] = 0;
+  }
 }
 
 void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
@@ -52,95 +58,184 @@ void SygusUnifRl::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
   lemmas.push_back(exc_lemma);
 }
 
-void SygusUnifRl::addRefLemma(Node lemma)
-{
-  d_prev_rlemmas = d_rlemmas;
-  d_rlemmas = d_tds->getExtRewriter()->extendedRewrite(
-      NodeManager::currentNM()->mkNode(AND, d_rlemmas, lemma));
-  Trace("sygus-unif-rl-lemma")
-      << "SyGuSUnifRl: New collection of ref lemmas is " << d_rlemmas << "\n";
-  d_hasRLemmas = d_rlemmas != d_true;
-}
-
-void SygusUnifRl::collectPoints(Node n)
+Node SygusUnifRl::purifyLemma(Node n,
+                              bool ensureConst,
+                              std::vector<Node>& model_guards,
+                              BoolNodePairMap& cache)
 {
-  std::unordered_set<TNode, TNodeHashFunction> visited;
-  std::unordered_set<TNode, TNodeHashFunction>::iterator it;
-  std::vector<TNode> visit;
-  TNode cur;
-  visit.push_back(n);
-  do
+  Trace("sygus-unif-rl-purify") << "PurifyLemma : " << n << "\n";
+  BoolNodePairMap::const_iterator it = cache.find(BoolNodePair(ensureConst, n));
+  if (it != cache.end())
   {
-    cur = visit.back();
-    visit.pop_back();
-    if (visited.find(cur) != visited.end())
-    {
-      continue;
-    }
-    visited.insert(cur);
-    unsigned size = cur.getNumChildren();
-    if (cur.getKind() == APPLY_UF && size > 0)
+    Trace("sygus-unif-rl-purify-debug") << "... already visited " << n << "\n";
+    return it->second;
+  }
+  /* Recurse */
+  unsigned size = n.getNumChildren();
+  Kind k = n.getKind();
+  /* Whether application of a function-to-synthesize */
+  bool fapp = k == APPLY_UF && size > 0;
+  Assert(std::find(d_candidates.begin(), d_candidates.end(), n[0])
+         == d_candidates.end());
+  /* Whether application of a (non-)unification function-to-synthesize */
+  bool u_fapp = fapp && usingUnif(n[0]);
+  bool nu_fapp = fapp && !usingUnif(n[0]);
+  /* We retrive model value now because purified node may not have a value */
+  Node nv = n;
+  /* get model value of non-top level applications of functions-to-synthesize
+     occurring under a unification function-to-synthesize */
+  if (ensureConst && fapp)
+  {
+    nv = d_parent->getModelValue(n);
+    Assert(n != nv);
+    Trace("sygus-unif-rl-purify") << "PurifyLemma : model value for " << n
+                                  << " is " << nv << "\n";
+  }
+  /* Travese to purify */
+  bool childChanged = false;
+  std::vector<Node> children;
+  NodeManager* nm = NodeManager::currentNM();
+  for (unsigned i = 0; i < size; ++i)
+  {
+    if (i == 0 && fapp)
     {
-      std::vector<Node> pt;
-      for (unsigned i = 1; i < size; ++i)
-      {
-        Assert(cur[i].isConst());
-        pt.push_back(cur[i]);
-      }
-      d_app_to_pt[cur] = pt;
+      children.push_back(n[i]);
       continue;
     }
-    for (const TNode& child : cur)
+    /* Arguments of non-unif functions do not need to be constant */
+    Node child = purifyLemma(
+        n[i], !nu_fapp && (ensureConst || u_fapp), model_guards, cache);
+    children.push_back(child);
+    childChanged = childChanged || child != n[i];
+  }
+  Node nb;
+  if (childChanged)
+  {
+    if (n.hasOperator())
     {
-      visit.push_back(child);
+      children.insert(children.begin(), n.getOperator());
     }
-  } while (!visit.empty());
-}
-
-void SygusUnifRl::initializeConstructSol()
-{
-  if (d_hasRLemmas && d_rlemmas != d_prev_rlemmas)
+    nb = NodeManager::currentNM()->mkNode(k, children);
+    Trace("sygus-unif-rl-purify") << "PurifyLemma : transformed " << n
+                                  << " into " << nb << "\n";
+  }
+  else
   {
-    collectPoints(d_rlemmas);
-    if (Trace.isOn("sygus-unif-rl-sol"))
+    nb = n;
+  }
+  /* Map to point enumerator every unification function-to-synthesize  */
+  if (u_fapp)
+  {
+    Node np;
+    std::map<Node, Node>::const_iterator it = d_app_to_purified.find(nb);
+    if (it == d_app_to_purified.end())
     {
-      Trace("sygus-unif-rl-sol") << "SyGuSUnifRl: Points from " << d_rlemmas
-                                 << "\n";
-      for (const std::pair<Node, std::vector<Node>>& pair : d_app_to_pt)
+      if (!childChanged)
+      {
+        Assert(nb.hasOperator());
+        children.insert(children.begin(), n.getOperator());
+      }
+      /* Build purified head with fresh skolem and recreate node */
+      std::stringstream ss;
+      ss << nb[0] << "_" << d_purified_count[nb[0]]++;
+      Node new_f = nm->mkSkolem(ss.str(), nb[0].getType());
+      /* Adds new enumerator to map from candidate */
+      Trace("sygus-unif-rl-purify") << "...new enum " << new_f
+                                        << " for candidate " << nb[0] << "\n";
+      d_cand_to_pt_enum[nb[0]].push_back(new_f);
+      /* Maps new enumerator to its respective tuple of arguments */
+      d_app_to_pt[new_f] =
+          std::vector<Node>(children.begin() + 2, children.end());
+      if (Trace.isOn("sygus-unif-rl-purify"))
       {
-        Trace("sygus-unif-rl-sol") << "...[" << pair.first << "] --> (";
-        for (const Node& pt_i : pair.second)
+        Trace("sygus-unif-rl-purify") << "...[" << new_f << "] --> (";
+        for (const Node& pt_i : d_app_to_pt[new_f])
         {
-          Trace("sygus-unif-rl-sol") << pt_i << " ";
+          Trace("sygus-unif-rl-purify") << pt_i << " ";
         }
-        Trace("sygus-unif-rl-sol") << ")\n";
+        Trace("sygus-unif-rl-purify") << ")\n";
       }
+      /* replace first child and rebulid node */
+      children[1] = new_f;
+      np = NodeManager::currentNM()->mkNode(k, children);
+      d_app_to_purified[nb] = np;
     }
+    else
+    {
+      np = it->second;
+    }
+    Trace("sygus-unif-rl-purify")
+        << "PurifyLemma : purified head and transformed " << nb << " into "
+        << np << "\n";
+    nb = np;
   }
+  /* Add equality between purified fapp and model value */
+  if (ensureConst && fapp)
+  {
+    model_guards.push_back(
+        NodeManager::currentNM()->mkNode(EQUAL, nv, nb).negate());
+    nb = nv;
+    Trace("sygus-unif-rl-purify") << "PurifyLemma : adding model eq "
+                                  << model_guards.back() << "\n";
+  }
+  nb = Rewriter::rewrite(nb);
+  /* every non-top level application of function-to-synthesize must be reduced
+     to a concrete constant */
+  Assert(!ensureConst || nb.isConst());
+  Trace("sygus-unif-rl-purify-debug") << "... caching [" << n << "] = " << nb
+                                      << "\n";
+  cache[BoolNodePair(ensureConst, n)] = nb;
+  return nb;
 }
 
-void SygusUnifRl::initializeConstructSolFor(Node f) {}
-Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind)
+Node SygusUnifRl::addRefLemma(Node lemma)
 {
-  Node solution = canCloseBranch(e);
-  if (!solution.isNull())
+  Trace("sygus-unif-rl-purify") << "Registering lemma at SygusUnif : " << lemma
+                               << "\n";
+  std::vector<Node> model_guards;
+  BoolNodePairMap cache;
+  /* Make the purified lemma which will guide the unification utility. */
+  Node plem = purifyLemma(lemma, false, model_guards, cache);
+  if (!model_guards.empty())
   {
-    return solution;
+    model_guards.push_back(plem);
+    plem = NodeManager::currentNM()->mkNode(OR, model_guards);
   }
-  return Node::null();
+  plem = Rewriter::rewrite(plem);
+  Trace("sygus-unif-rl-purify") << "Purified lemma : " << plem << "\n";
+  return plem;
 }
 
-Node SygusUnifRl::canCloseBranch(Node e)
+void SygusUnifRl::initializeConstructSol() {}
+void SygusUnifRl::initializeConstructSolFor(Node f) {}
+bool SygusUnifRl::constructSolution(std::vector<Node>& sols)
 {
-  if (!d_hasRLemmas && !d_ecache[e].d_enum_vals.empty())
+  for (const Node& c : d_candidates)
   {
-    Trace("sygus-unif-rl-sol") << "SyGuSUnifRl: Closed branch and yielded "
-                                  << d_ecache[e].d_enum_vals[0] << "\n";
-    return d_ecache[e].d_enum_vals[0];
+    if (!usingUnif(c))
+    {
+      Node v = d_parent->getModelValue(c);
+      Trace("sygus-unif-rl-sol") << "Adding solution " << v
+                                 << " to non-unif candidate " << c << "\n";
+      sols.push_back(v);
+    }
+    else
+    {
+      return false;
+    }
   }
+  return true;
+}
+
+Node SygusUnifRl::constructSol(Node f, Node e, NodeRole nrole, int ind)
+{
   return Node::null();
 }
 
+bool SygusUnifRl::usingUnif(Node f)
+{
+  return d_unif_candidates.find(f) != d_unif_candidates.end();
+}
 
 } /* CVC4::theory::quantifiers namespace */
 } /* CVC4::theory namespace */
diff --git a/src/theory/quantifiers/sygus/sygus_unif_rl.h b/src/theory/quantifiers/sygus/sygus_unif_rl.h
index 13d0d1e56..dc1b14641 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_rl.h
+++ b/src/theory/quantifiers/sygus/sygus_unif_rl.h
@@ -20,10 +20,20 @@
 #include <map>
 #include "theory/quantifiers/sygus/sygus_unif.h"
 
+#include "theory/quantifiers_engine.h"
+
 namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
+using BoolNodePair = std::pair<bool, Node>;
+using BoolNodePairHashFunction =
+    PairHashFunction<bool, Node, BoolHashFunction, NodeHashFunction>;
+using BoolNodePairMap =
+    std::unordered_map<BoolNodePair, Node, BoolNodePairHashFunction>;
+
+class CegConjecture;
+
 /** Sygus unification Refinement Lemmas utility
  *
  * This class implement synthesis-by-unification, where the specification is a
@@ -33,7 +43,7 @@ namespace quantifiers {
 class SygusUnifRl : public SygusUnif
 {
  public:
-  SygusUnifRl();
+  SygusUnifRl(CegConjecture* p);
   ~SygusUnifRl();
 
   /** initialize */
@@ -43,25 +53,28 @@ class SygusUnifRl : public SygusUnif
                   std::vector<Node>& lemmas) override;
   /** Notify enumeration */
   void notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas) override;
+  /** Construct solution */
+  bool constructSolution(std::vector<Node>& sols) override;
+  Node constructSol(Node f, Node e, NodeRole nrole, int ind) override;
   /** add refinement lemma
    *
    * This adds a lemma to the specification for f.
    */
-  void addRefLemma(Node lemma);
+  Node addRefLemma(Node lemma);
+  /**
+   * whether f is being synthesized with unification strategies. This can be
+   * checked through wehether f has conditional or point enumerators (we use the
+   * former)
+    */
+  bool usingUnif(Node f);
 
  protected:
-  /** true and false nodes */
-  Node d_true, d_false;
-  /** current collecton of refinement lemmas */
-  Node d_rlemmas;
-  /** previous collecton of refinement lemmas */
-  Node d_prev_rlemmas;
-  /** whether there are refinement lemmas to satisfy when building solutions */
-  bool d_hasRLemmas;
-  /**
-   * maps applications of the function-to-synthesize to their tuple of arguments
-   * (which constitute a "data point") */
-  std::map<Node, std::vector<Node>> d_app_to_pt;
+  /** reference to the parent conjecture */
+  CegConjecture* d_parent;
+  /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */
+  std::unordered_set<Node, NodeHashFunction> d_unif_candidates;
+  /* Maps unif candidates to their conditonal enumerators */
+  std::map<Node, Node> d_cand_to_cond_enum;
   /**
    * This class stores information regarding an enumerator, including: a
    * database
@@ -78,9 +91,6 @@ class SygusUnifRl : public SygusUnif
   /** maps enumerators to the information above */
   std::map<Node, EnumCache> d_ecache;
 
-  /** Traverses n and populates d_app_to_pt */
-  void collectPoints(Node n);
-
   /** collects data from refinement lemmas to drive solution construction
    *
    * In particular it rebuilds d_app_to_pt whenever d_prev_rlemmas is different
@@ -89,15 +99,58 @@ class SygusUnifRl : public SygusUnif
   void initializeConstructSol() override;
   /** initialize construction solution for function-to-synthesize f */
   void initializeConstructSolFor(Node f) override;
+  /*
+    --------------------------------------------------------------
+        Purification
+    --------------------------------------------------------------
+  */
+  /* Maps unif candidates to their point enumerators */
+  std::map<Node, std::vector<Node>> d_cand_to_pt_enum;
+  /**
+   * maps applications of the function-to-synthesize to their tuple of arguments
+   * (which constitute a "data point") */
+  std::map<Node, std::vector<Node>> d_app_to_pt;
+  /** Maps applications of unif functions-to-synthesize to purified symbols*/
+  std::map<Node, Node> d_app_to_purified;
+  /** Maps unif functions-to-synthesize to counters of purified symbols */
+  std::map<Node, unsigned> d_purified_count;
   /**
-   * Returns a term covering all data points in the current branch, on null if
-   * none can be found among the currently enumerated values for the respective
-   * enumerator
+   * This is called on the refinement lemma and will rewrite applications of
+   * functions-to-synthesize to their respective purified form, i.e. such that
+   * all unification functions are applied over concrete values. Moreover
+   * unification functions are also rewritten such that every different tuple of
+   * arguments has a fresh function symbol applied to it.
+   *
+   * Non-unification functions are also equated to their model values when they
+   * occur as arguments of unification functions.
+   *
+   * A vector of guards with the (negated) equalities between the original
+   * arguments and their model values is populated accordingly.
+   *
+   * When the traversal encounters an application of a unification
+   * function-to-synthesize it will proceed to ensure that the arguments of that
+   * function application are constants (the ensureConst becomes "true"). If an
+   * applicatin of a non-unif function-to-synthesize is reached, the requirement
+   * is lifted (the ensureConst becomes "false"). This avoides introducing
+   * spurious equalities in model_guards.
+   *
+   * For example if "f" is being synthesized with a unification strategy and "g"
+   * is not then the application
+   *   f(g(f(g(0))))=1
+   * would be purified into
+   *   g(0) = c1 ^ g(f1(c1)) = c3 => f2(c3)
+   *
+   * Similarly
+   *   f(+(0,f(g(0))))
+   * would be purified into
+   *   g(0) = c1 ^ f1(c1) = c2 => f2(+(0,c2))
+   *
+   * This function also populates the maps for point enumerators
    */
-  Node canCloseBranch(Node e);
-
-  /** construct solution */
-  Node constructSol(Node f, Node e, NodeRole nrole, int ind) override;
+  Node purifyLemma(Node n,
+                   bool ensureConst,
+                   std::vector<Node>& model_guards,
+                   BoolNodePairMap& cache);
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 885c36bb5..edea22fbf 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -612,7 +612,8 @@ void TheoryEngine::check(Theory::Effort effort) {
           }
         }
       }
-      if( ! d_inConflict && ! needCheck() ){
+      if (!d_inConflict)
+      {
         if(d_logicInfo.isQuantified()) {
           // quantifiers engine must check at last call effort
           d_quantEngine->check(Theory::EFFORT_LAST_CALL);
diff --git a/src/util/result.cpp b/src/util/result.cpp
index 27d82bb6f..dfcd74ff7 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -349,24 +349,21 @@ void Result::toStreamTptp(std::ostream& out) const {
 
 void Result::toStream(std::ostream& out, OutputLanguage language) const {
   switch (language) {
-    case language::output::LANG_SMTLIB_V2_0:
-    case language::output::LANG_SMTLIB_V2_5:
-    case language::output::LANG_SMTLIB_V2_6:
     case language::output::LANG_SYGUS:
-    case language::output::LANG_Z3STR:
       toStreamSmt2(out);
       break;
     case language::output::LANG_TPTP:
       toStreamTptp(out);
       break;
-    case language::output::LANG_AST:
-    case language::output::LANG_AUTO:
-    case language::output::LANG_CVC3:
-    case language::output::LANG_CVC4:
-    case language::output::LANG_MAX:
-    case language::output::LANG_SMTLIB_V1:
     default:
-      toStreamDefault(out);
+      if (language::isOutputLang_smt2(language))
+      {
+        toStreamSmt2(out);
+      }
+      else
+      {
+        toStreamDefault(out);
+      }
       break;
   };
 }
diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index 504d58b0e..fbc8802d6 100644
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -273,18 +273,13 @@ void SExpr::toStreamRec(std::ostream& out, const SExpr& sexpr,
 bool SExpr::languageQuotesKeywords(OutputLanguage language) {
   switch (language) {
     case language::output::LANG_SMTLIB_V1:
-    case language::output::LANG_SMTLIB_V2_0:
-    case language::output::LANG_SMTLIB_V2_5:
-    case language::output::LANG_SMTLIB_V2_6:
     case language::output::LANG_SYGUS:
     case language::output::LANG_TPTP:
-    case language::output::LANG_Z3STR:
       return true;
     case language::output::LANG_AST:
     case language::output::LANG_CVC3:
     case language::output::LANG_CVC4:
-    default:
-      return false;
+    default: return language::isOutputLang_smt2(language);
   };
 }
 
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index f8a32046f..48c81a13b 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -788,6 +788,7 @@ REG0_TESTS = \
 	regress0/strings/norn-simp-rew.smt2 \
 	regress0/strings/repl-rewrites2.smt2 \
 	regress0/strings/rewrites-v2.smt2 \
+	regress0/strings/std2.6.1.smt2 \
 	regress0/strings/str003.smt2 \
 	regress0/strings/str004.smt2 \
 	regress0/strings/str005.smt2 \
@@ -1254,6 +1255,7 @@ REG1_TESTS = \
 	regress1/quantifiers/model_6_1_bv.smt2 \
 	regress1/quantifiers/mutualrec2.cvc \
 	regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 \
+	regress1/quantifiers/nra-interleave-inst.smt2 \
 	regress1/quantifiers/opisavailable-12.smt2 \
 	regress1/quantifiers/parametric-lists.smt2 \
 	regress1/quantifiers/psyco-001-bv.smt2 \
diff --git a/test/regress/regress0/strings/bug002.smt2 b/test/regress/regress0/strings/bug002.smt2
index f8a481e14..fd60089fd 100644
--- a/test/regress/regress0/strings/bug002.smt2
+++ b/test/regress/regress0/strings/bug002.smt2
@@ -1,5 +1,5 @@
-(set-logic ASLIA)
 (set-info :smt-lib-version 2.0)
+(set-logic ASLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
 
@@ -7,4 +7,4 @@
 (define-fun strinre ((?s String)) Bool (str.in.re ?s (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.union re.nostr (re.range "*" ",") (str.to.re "\t") (re.range "*" "|") ) (re.+ (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.loop re.allchar 6 ) (re.opt (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ) ) ) ) ) ) ) )  ) )
 (assert (not (strinre "6O\1\127\n?")))
 
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/strings/issue1189.smt2 b/test/regress/regress0/strings/issue1189.smt2
index fae641ea8..0b581994c 100644
--- a/test/regress/regress0/strings/issue1189.smt2
+++ b/test/regress/regress0/strings/issue1189.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress0/strings/leadingzero001.smt2 b/test/regress/regress0/strings/leadingzero001.smt2
index 2889348c1..09fd80a7b 100644
--- a/test/regress/regress0/strings/leadingzero001.smt2
+++ b/test/regress/regress0/strings/leadingzero001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status sat)
diff --git a/test/regress/regress0/strings/norn-31.smt2 b/test/regress/regress0/strings/norn-31.smt2
index 4698f966f..1830dd882 100644
--- a/test/regress/regress0/strings/norn-31.smt2
+++ b/test/regress/regress0/strings/norn-31.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status unsat)
diff --git a/test/regress/regress0/strings/norn-simp-rew.smt2 b/test/regress/regress0/strings/norn-simp-rew.smt2
index 45f7ede94..d729fe5d0 100644
--- a/test/regress/regress0/strings/norn-simp-rew.smt2
+++ b/test/regress/regress0/strings/norn-simp-rew.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status unsat)
@@ -26,4 +27,4 @@
 (assert (str.in.re var_8 (re.* (re.range "a" "u"))))
 (assert (str.in.re var_7 (re.* (re.range "a" "u"))))
 (assert (not (str.in.re (str.++ "b" var_7 ) (re.* (re.range "a" "u")))))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress0/strings/rewrites-v2.smt2 b/test/regress/regress0/strings/rewrites-v2.smt2
index 7e285b51a..ce2f140ae 100644
--- a/test/regress/regress0/strings/rewrites-v2.smt2
+++ b/test/regress/regress0/strings/rewrites-v2.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --strings-exp
 ; EXPECT: unsat
+(set-info :smt-lib-version 2.5)
 (set-logic SLIA)
 (set-info :status unsat)
 (declare-fun x () String)
diff --git a/test/regress/regress0/strings/std2.6.1.smt2 b/test/regress/regress0/strings/std2.6.1.smt2
new file mode 100644
index 000000000..3302a29e5
--- /dev/null
+++ b/test/regress/regress0/strings/std2.6.1.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --strings-exp --lang=smt2.6.1
+; EXPECT: sat
+(set-logic QF_UFSLIA)
+(set-info :status sat)
+(declare-fun x () String)
+(assert (str.in-re x (str.to-re "A")))
+(declare-fun y () Int)
+(assert (= (str.to-int (str.from-int y)) y))
+(check-sat)
diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2
index 77eabcccc..89191ac34 100644
--- a/test/regress/regress0/strings/type001.smt2
+++ b/test/regress/regress0/strings/type001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
@@ -18,4 +19,4 @@
 ;should be -1
 (assert (= j (str.to.int "-783914785582390527685649")))
 
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/nra-interleave-inst.smt2 b/test/regress/regress1/quantifiers/nra-interleave-inst.smt2
new file mode 100644
index 000000000..8e318a372
--- /dev/null
+++ b/test/regress/regress1/quantifiers/nra-interleave-inst.smt2
@@ -0,0 +1,18 @@
+(set-info :smt-lib-version 2.6)
+(set-logic NRA)
+(set-info :status unsat)
+(declare-fun xI () Real)
+(declare-fun ts35uscore2 () Real)
+(declare-fun A () Real)
+(declare-fun B () Real)
+(declare-fun t60uscore0dollarskuscore2 () Real)
+(declare-fun I1 () Real)
+(declare-fun v () Real)
+(declare-fun V () Real)
+(declare-fun xuscore2dollarskuscore50 () Real)
+(declare-fun vuscore2dollarskuscore56 () Real)
+(declare-fun ep () Real)
+(declare-fun I1uscore2dollarskuscore52 () Real)
+(declare-fun x () Real)
+(assert (not (exists ((ts35uscore2 Real)) (let ((?v_1 (- B))) (let ((?v_0 (+ (* ?v_1 ts35uscore2) vuscore2dollarskuscore56)) (?v_3 (+ (* ?v_1 t60uscore0dollarskuscore2) vuscore2dollarskuscore56)) (?v_2 (* (/ 1 2) (+ (+ (* ?v_1 (* t60uscore0dollarskuscore2 t60uscore0dollarskuscore2)) (* (* 2 t60uscore0dollarskuscore2) vuscore2dollarskuscore56)) (* 2 xuscore2dollarskuscore50))))) (=> (and (and (and (and (and (and (and (and (and (and (and (and (and (= I1uscore2dollarskuscore52 2) (=> (and (<= 0 ts35uscore2) (<= ts35uscore2 t60uscore0dollarskuscore2)) (and (and (>= ?v_0 0) (<= ?v_0 V)) (<= ts35uscore2 ep)))) (>= t60uscore0dollarskuscore2 0)) (>= vuscore2dollarskuscore56 0)) (<= vuscore2dollarskuscore56 V)) (< xI xuscore2dollarskuscore50)) (= I1 2)) (< xI x)) (> B 0)) (>= v 0)) (<= v V)) (>= A 0)) (> V 0)) (> ep 0)) (or (< xI ?v_2) (> xI (+ ?v_2 (/ (* ?v_3 ?v_3) (* 2 B)))))))))))
+(check-sat)
diff --git a/test/regress/regress1/strings/artemis-0512-nonterm.smt2 b/test/regress/regress1/strings/artemis-0512-nonterm.smt2
index 4b1cad8f6..a3cca23a2 100644
--- a/test/regress/regress1/strings/artemis-0512-nonterm.smt2
+++ b/test/regress/regress1/strings/artemis-0512-nonterm.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status unsat)
diff --git a/test/regress/regress1/strings/bug615.smt2 b/test/regress/regress1/strings/bug615.smt2
index 86cc592fb..673b0dbd0 100644
--- a/test/regress/regress1/strings/bug615.smt2
+++ b/test/regress/regress1/strings/bug615.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status sat)
diff --git a/test/regress/regress1/strings/bug686dd.smt2 b/test/regress/regress1/strings/bug686dd.smt2
index 7c923654d..0cb9fac26 100644
--- a/test/regress/regress1/strings/bug686dd.smt2
+++ b/test/regress/regress1/strings/bug686dd.smt2
@@ -1,7 +1,8 @@
+(set-info :smt-lib-version 2.5)
 (set-logic UFDTSLIA)
 (set-info :status sat)
 
-(declare-datatypes ((T 0)) ( ((TC (TCb String))) ) )
+(declare-datatypes () ((T (TC (TCb String)))))
 
 (declare-fun root5 () String)
 (declare-fun root6 () T)
diff --git a/test/regress/regress1/strings/bug799-min.smt2 b/test/regress/regress1/strings/bug799-min.smt2
index 06acffc97..0cd15af4e 100644
--- a/test/regress/regress1/strings/bug799-min.smt2
+++ b/test/regress/regress1/strings/bug799-min.smt2
@@ -1,5 +1,6 @@
 ; COMMAND-LINE: --incremental --strings-exp
 ; EXPECT: sat
+(set-info :smt-lib-version 2.5)
 (set-logic ALL)
 (set-info :status sat)
 
diff --git a/test/regress/regress1/strings/fmf001.smt2 b/test/regress/regress1/strings/fmf001.smt2
index 6081c8e06..71ae63e87 100644
--- a/test/regress/regress1/strings/fmf001.smt2
+++ b/test/regress/regress1/strings/fmf001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-option :strings-fmf true)
diff --git a/test/regress/regress1/strings/fmf002.smt2 b/test/regress/regress1/strings/fmf002.smt2
index d52dae2d2..ab3dc2ae2 100644
--- a/test/regress/regress1/strings/fmf002.smt2
+++ b/test/regress/regress1/strings/fmf002.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-option :strings-fmf true)
diff --git a/test/regress/regress1/strings/issue1105.smt2 b/test/regress/regress1/strings/issue1105.smt2
index 81e7672da..bf5cb7669 100644
--- a/test/regress/regress1/strings/issue1105.smt2
+++ b/test/regress/regress1/strings/issue1105.smt2
@@ -1,9 +1,10 @@
+(set-info :smt-lib-version 2.5)
 (set-logic ALL)
 (set-option :strings-exp true)
 (set-info :status sat)
-(declare-datatype Val (
+(declare-datatypes () ((Val
     (Str (str String))
-    (Num (num Int))))
+    (Num (num Int)))))
 
 (declare-const var0 Val)
 (assert (=> (is-Str var0) (distinct (str.to.int (str var0)) (- 1))))
diff --git a/test/regress/regress1/strings/kaluza-fl.smt2 b/test/regress/regress1/strings/kaluza-fl.smt2
index 04775d61c..20c2e6aa4 100644
--- a/test/regress/regress1/strings/kaluza-fl.smt2
+++ b/test/regress/regress1/strings/kaluza-fl.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 
diff --git a/test/regress/regress1/strings/norn-360.smt2 b/test/regress/regress1/strings/norn-360.smt2
index 573dcbe01..20ab0b338 100644
--- a/test/regress/regress1/strings/norn-360.smt2
+++ b/test/regress/regress1/strings/norn-360.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -22,4 +23,4 @@
 (assert (str.in.re var_4 (re.* (re.range "a" "u"))))
 (assert (str.in.re var_3 (re.* (re.range "a" "u"))))
 (assert (<= 0  (str.len var_4)))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/strings/norn-ab.smt2 b/test/regress/regress1/strings/norn-ab.smt2
index 48d889847..47c218179 100644
--- a/test/regress/regress1/strings/norn-ab.smt2
+++ b/test/regress/regress1/strings/norn-ab.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-info :status unsat)
 (set-option :strings-exp true)
@@ -22,4 +23,4 @@
 (assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))
 (assert (not (str.in.re (str.++ "a" var_4 "b" ) (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))))
 (assert (and (<= 0  (str.len var_4)) (not (not (exists ((v Int)) (= (* v 2 ) (+ (str.len var_4) 2 )))))))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/strings/norn-nel-bug-052116.smt2 b/test/regress/regress1/strings/norn-nel-bug-052116.smt2
index f0c2534a1..9f06152f7 100644
--- a/test/regress/regress1/strings/norn-nel-bug-052116.smt2
+++ b/test/regress/regress1/strings/norn-nel-bug-052116.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/norn-simp-rew-sat.smt2 b/test/regress/regress1/strings/norn-simp-rew-sat.smt2
index 01a102bf9..1336d3bfc 100644
--- a/test/regress/regress1/strings/norn-simp-rew-sat.smt2
+++ b/test/regress/regress1/strings/norn-simp-rew-sat.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_SLIA)
 (set-option :strings-exp true)
 (set-info :status sat)
@@ -22,4 +23,4 @@
 (assert (str.in.re var_3 (re.* (re.range "a" "u"))))
 (assert (str.in.re var_3 (re.* (str.to.re "a"))))
 (assert (<= 0  (str.len var_4)))
-(check-sat)
\ No newline at end of file
+(check-sat)
diff --git a/test/regress/regress1/strings/pierre150331.smt2 b/test/regress/regress1/strings/pierre150331.smt2
index 88d5ec10c..add60d534 100644
--- a/test/regress/regress1/strings/pierre150331.smt2
+++ b/test/regress/regress1/strings/pierre150331.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)

 (set-logic SLIA)

 (set-info :status sat)

 (set-info :smt-lib-version 2.5)

@@ -10,4 +11,4 @@
 (declare-fun s1() String)

 (declare-fun s2() String)

 (assert (and true (stringEval s0) (stringEval s1) (distinct s0 s1) (stringEval s2) (distinct s0 s2) (distinct s1 s2) ) )

-(check-sat)
\ No newline at end of file
+(check-sat)

diff --git a/test/regress/regress1/strings/regexp001.smt2 b/test/regress/regress1/strings/regexp001.smt2
index 62c142d1d..142ff679d 100644
--- a/test/regress/regress1/strings/regexp001.smt2
+++ b/test/regress/regress1/strings/regexp001.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/regexp002.smt2 b/test/regress/regress1/strings/regexp002.smt2
index a8bd2187a..f109a484e 100644
--- a/test/regress/regress1/strings/regexp002.smt2
+++ b/test/regress/regress1/strings/regexp002.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/regexp003.smt2 b/test/regress/regress1/strings/regexp003.smt2
index 7696838fe..7c05b422f 100644
--- a/test/regress/regress1/strings/regexp003.smt2
+++ b/test/regress/regress1/strings/regexp003.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/reloop.smt2 b/test/regress/regress1/strings/reloop.smt2
index 9915504ae..967e564ce 100644
--- a/test/regress/regress1/strings/reloop.smt2
+++ b/test/regress/regress1/strings/reloop.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status sat)
diff --git a/test/regress/regress1/strings/string-unsound-sem.smt2 b/test/regress/regress1/strings/string-unsound-sem.smt2
index 771d8d4b0..44591b47b 100644
--- a/test/regress/regress1/strings/string-unsound-sem.smt2
+++ b/test/regress/regress1/strings/string-unsound-sem.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic ALL)
 (set-option :strings-exp true)
 (set-info :status sat)
diff --git a/test/regress/regress1/strings/type002.smt2 b/test/regress/regress1/strings/type002.smt2
index 0df0f20b0..458ac75fe 100644
--- a/test/regress/regress1/strings/type002.smt2
+++ b/test/regress/regress1/strings/type002.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/type003.smt2 b/test/regress/regress1/strings/type003.smt2
index c2d4792cc..4185041f7 100644
--- a/test/regress/regress1/strings/type003.smt2
+++ b/test/regress/regress1/strings/type003.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-info :status sat)
 (set-option :strings-exp true)
diff --git a/test/regress/regress1/strings/username_checker_min.smt2 b/test/regress/regress1/strings/username_checker_min.smt2
index 2f1c35844..f6c152a2a 100644
--- a/test/regress/regress1/strings/username_checker_min.smt2
+++ b/test/regress/regress1/strings/username_checker_min.smt2
@@ -1,3 +1,4 @@
+(set-info :smt-lib-version 2.5)
 (set-logic QF_S)
 (set-option :strings-exp true)
 (set-info :status unsat)