Merge branch 'master' into issue4151

69 files changed, 2651 insertions, 1873 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4520ee421..809b00b04 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -236,6 +236,8 @@ libcvc4_add_sources(
   smt/model_core_builder.h
   smt/model_blocker.cpp
   smt/model_blocker.h
+  smt/set_defaults.cpp
+  smt/set_defaults.h
   smt/smt_engine.cpp
   smt/smt_engine.h
   smt/smt_engine_scope.cpp
@@ -959,11 +961,11 @@ install(FILES
           util/proof.h
           util/rational_cln_imp.h
           util/rational_gmp_imp.h
-          util/regexp.h
           util/resource_manager.h
           util/result.h
           util/sexpr.h
           util/statistics.h
+          util/string.h
           util/tuple.h
           util/unsafe_interrupt_exception.h
           ${CMAKE_CURRENT_BINARY_DIR}/util/floatingpoint.h
diff --git a/src/cvc4.i b/src/cvc4.i
index f9f8f5743..9dcff7f8e 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -274,10 +274,10 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "util/cardinality.i"
 %include "util/hash.i"
 %include "util/proof.i"
-%include "util/regexp.i"
 %include "util/result.i"
 %include "util/sexpr.i"
 %include "util/statistics.i"
+%include "util/string.i"
 %include "util/tuple.i"
 %include "util/unsafe_interrupt_exception.i"
 
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 5d409f748..16ffd8306 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -575,6 +575,42 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor
   }
 }
 
+TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts)
+{
+  Assert(sorts.size() >= 2);
+  CheckArgument(!sorts[sorts.size() - 1].isFunction(),
+                sorts[sorts.size() - 1],
+                "must flatten function types");
+  return mkTypeNode(kind::FUNCTION_TYPE, sorts);
+}
+
+TypeNode NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts)
+{
+  Assert(sorts.size() >= 1);
+  std::vector<TypeNode> sortNodes;
+  sortNodes.insert(sortNodes.end(), sorts.begin(), sorts.end());
+  sortNodes.push_back(booleanType());
+  return mkFunctionType(sortNodes);
+}
+
+TypeNode NodeManager::mkFunctionType(const TypeNode& domain,
+                                     const TypeNode& range)
+{
+  std::vector<TypeNode> sorts;
+  sorts.push_back(domain);
+  sorts.push_back(range);
+  return mkFunctionType(sorts);
+}
+
+TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes,
+                                     const TypeNode& range)
+{
+  Assert(argTypes.size() >= 1);
+  std::vector<TypeNode> sorts(argTypes);
+  sorts.push_back(range);
+  return mkFunctionType(sorts);
+}
+
 TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
   std::vector< TypeNode > ts;
   Debug("tuprec-debug") << "Make tuple type : ";
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index eced00c48..2e8f40fff 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -807,7 +807,7 @@ public:
    * @param range the range type
    * @returns the functional type domain -> range
    */
-  inline TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range);
+  TypeNode mkFunctionType(const TypeNode& domain, const TypeNode& range);
 
   /**
    * Make a function type with input types from
@@ -817,8 +817,8 @@ public:
    * @param range the range type
    * @returns the functional type (argTypes[0], ..., argTypes[n]) -> range
    */
-  inline TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes,
-                                 const TypeNode& range);
+  TypeNode mkFunctionType(const std::vector<TypeNode>& argTypes,
+                          const TypeNode& range);
 
   /**
    * Make a function type with input types from
@@ -826,7 +826,7 @@ public:
    * <code>sorts[sorts.size()-1]</code>. <code>sorts</code> must have
    * at least 2 elements.
    */
-  inline TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
+  TypeNode mkFunctionType(const std::vector<TypeNode>& sorts);
 
   /**
    * Make a predicate type with input types from
@@ -834,7 +834,7 @@ public:
    * <code>BOOLEAN</code>. <code>sorts</code> must have at least one
    * element.
    */
-  inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
+  TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
 
   /**
    * Make a tuple type with types from
@@ -1086,52 +1086,6 @@ inline TypeNode NodeManager::builtinOperatorType() {
   return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE));
 }
 
-/** Make a function type from domain to range. */
-inline TypeNode NodeManager::mkFunctionType(const TypeNode& domain, const TypeNode& range) {
-  std::vector<TypeNode> sorts;
-  sorts.push_back(domain);
-  sorts.push_back(range);
-  return mkFunctionType(sorts);
-}
-
-inline TypeNode NodeManager::mkFunctionType(const std::vector<TypeNode>& argTypes, const TypeNode& range) {
-  Assert(argTypes.size() >= 1);
-  std::vector<TypeNode> sorts(argTypes);
-  sorts.push_back(range);
-  return mkFunctionType(sorts);
-}
-
-inline TypeNode
-NodeManager::mkFunctionType(const std::vector<TypeNode>& sorts) {
-  Assert(sorts.size() >= 2);
-  std::vector<TypeNode> sortNodes;
-  for (unsigned i = 0; i < sorts.size(); ++ i) {
-    CheckArgument(sorts[i].isFirstClass(),
-                  sorts,
-                  "cannot create function types for argument types that are "
-                  "not first-class. Try option --uf-ho.");
-    sortNodes.push_back(sorts[i]);
-  }
-  CheckArgument(!sorts[sorts.size()-1].isFunction(), sorts[sorts.size()-1],
-                "must flatten function types");
-  return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
-}
-
-inline TypeNode
-NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) {
-  Assert(sorts.size() >= 1);
-  std::vector<TypeNode> sortNodes;
-  for (unsigned i = 0; i < sorts.size(); ++ i) {
-    CheckArgument(sorts[i].isFirstClass(),
-                  sorts,
-                  "cannot create predicate types for argument types that are "
-                  "not first-class. Try option --uf-ho.");
-    sortNodes.push_back(sorts[i]);
-  }
-  sortNodes.push_back(booleanType());
-  return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
-}
-
 inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0; i < types.size(); ++ i) {
diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index ab8164130..1c0351bcb 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -551,3 +551,12 @@ header = "options/arith_options.h"
   default    = "true"
   read_only  = true
   help       = "whether to increment the precision for irrational function constraints"
+
+[[option]]
+  name       = "brabTest"
+  category   = "regular"
+  long       = "arith-brab"
+  type       = "bool"
+  default    = "true"
+  read_only  = true
+  help       = "whether to use simple rounding, similar to a unit-cube test, for integers"
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 82c0581ce..033389610 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2083,7 +2083,7 @@ stringTerm[CVC4::api::Term& f]
 
     /* string literal */
   | str[s]
-    { f = SOLVER->mkString(s, true); }
+    { f = PARSER_STATE->mkStringConstant(s); }
 
   | setsTerm[f]
   ;
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index b36f36a93..5dca92370 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -757,5 +757,153 @@ void Parser::attributeNotSupported(const std::string& attr) {
   }
 }
 
+std::vector<unsigned> Parser::processAdHocStringEsc(const std::string& s)
+{
+  std::vector<unsigned> str;
+  unsigned i = 0;
+  while (i < s.size())
+  {
+    // get the current character
+    if (s[i] != '\\')
+    {
+      // don't worry about printable here
+      str.push_back(static_cast<unsigned>(s[i]));
+      ++i;
+      continue;
+    }
+    // slash is always escaped
+    ++i;
+    if (i >= s.size())
+    {
+      // slash cannot be the last character if we are parsing escape sequences
+      std::stringstream serr;
+      serr << "Escape sequence at the end of string: \"" << s
+           << "\" should be handled by lexer";
+      parseError(serr.str());
+    }
+    switch (s[i])
+    {
+      case 'n':
+      {
+        str.push_back(static_cast<unsigned>('\n'));
+        i++;
+      }
+      break;
+      case 't':
+      {
+        str.push_back(static_cast<unsigned>('\t'));
+        i++;
+      }
+      break;
+      case 'v':
+      {
+        str.push_back(static_cast<unsigned>('\v'));
+        i++;
+      }
+      break;
+      case 'b':
+      {
+        str.push_back(static_cast<unsigned>('\b'));
+        i++;
+      }
+      break;
+      case 'r':
+      {
+        str.push_back(static_cast<unsigned>('\r'));
+        i++;
+      }
+      break;
+      case 'f':
+      {
+        str.push_back(static_cast<unsigned>('\f'));
+        i++;
+      }
+      break;
+      case 'a':
+      {
+        str.push_back(static_cast<unsigned>('\a'));
+        i++;
+      }
+      break;
+      case '\\':
+      {
+        str.push_back(static_cast<unsigned>('\\'));
+        i++;
+      }
+      break;
+      case 'x':
+      {
+        bool isValid = false;
+        if (i + 2 < s.size())
+        {
+          if (std::isxdigit(s[i + 1]) && std::isxdigit(s[i + 2]))
+          {
+            std::stringstream shex;
+            shex << s[i + 1] << s[i + 2];
+            unsigned val;
+            shex >> std::hex >> val;
+            str.push_back(val);
+            i += 3;
+            isValid = true;
+          }
+        }
+        if (!isValid)
+        {
+          std::stringstream serr;
+          serr << "Illegal String Literal: \"" << s
+               << "\", must have two digits after \\x";
+          parseError(serr.str());
+        }
+      }
+      break;
+      default:
+      {
+        if (std::isdigit(s[i]))
+        {
+          // octal escape sequences  TODO : revisit (issue #1251).
+          unsigned num = static_cast<unsigned>(s[i]) - 48;
+          bool flag = num < 4;
+          if (i + 1 < s.size() && num < 8 && std::isdigit(s[i + 1])
+              && s[i + 1] < '8')
+          {
+            num = num * 8 + static_cast<unsigned>(s[i + 1]) - 48;
+            if (flag && i + 2 < s.size() && std::isdigit(s[i + 2])
+                && s[i + 2] < '8')
+            {
+              num = num * 8 + static_cast<unsigned>(s[i + 2]) - 48;
+              str.push_back(num);
+              i += 3;
+            }
+            else
+            {
+              str.push_back(num);
+              i += 2;
+            }
+          }
+          else
+          {
+            str.push_back(num);
+            i++;
+          }
+        }
+      }
+    }
+  }
+  return str;
+}
+
+Expr Parser::mkStringConstant(const std::string& s)
+{
+  ExprManager* em = d_solver->getExprManager();
+  if (em->getOptions().getInputLanguage()
+      == language::input::LANG_SMTLIB_V2_6_1)
+  {
+    return d_solver->mkString(s, true).getExpr();
+  }
+  // otherwise, we must process ad-hoc escape sequences
+  std::vector<unsigned> str = processAdHocStringEsc(s);
+  return d_solver->mkString(str).getExpr();
+}
+
 } /* CVC4::parser namespace */
 } /* CVC4 namespace */
diff --git a/src/parser/parser.h b/src/parser/parser.h
index ecea4d3bd..d6c0e0e15 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -889,6 +889,28 @@ public:
         name, api::sortVectorToTypes(argTypes));
   }
   //------------------------ end operator overloading
+  /**
+   * Make string constant
+   *
+   * This makes the string constant based on the string s. This may involve
+   * processing ad-hoc escape sequences (if the language is not
+   * SMT-LIB 2.6.1 or higher), or otherwise calling the solver to construct
+   * the string.
+   */
+  Expr mkStringConstant(const std::string& s);
+
+ private:
+  /** ad-hoc string escaping
+   *
+   * Returns the (internal) vector of code points corresponding to processing
+   * the escape sequences in string s. This is to support string inputs that
+   * do no comply with the SMT-LIB standard.
+   *
+   * This method handles escape sequences, including \n, \t, \v, \b, \r, \f, \a,
+   * \\, \x[N] and octal escape sequences of the form \[c1]([c2]([c3])?)? where
+   * c1, c2, c3 are digits from 0 to 7.
+   */
+  std::vector<unsigned> processAdHocStringEsc(const std::string& s);
 };/* class Parser */
 
 }/* CVC4::parser namespace */
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index ec1eae7da..69f21acb7 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -2091,7 +2091,7 @@ termAtomic[CVC4::api::Term& atomTerm]
     }
 
   // String constant
-  | str[s,false] { atomTerm = SOLVER->mkString(s, true); }
+  | str[s,false] { atomTerm = PARSER_STATE->mkStringConstant(s); }
 
   // NOTE: Theory constants go here
 
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index cb78b0897..0e4bc41c0 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -401,7 +401,28 @@ Node BVToInt::bvToInt(Node n)
                   d_nm->mkNode(kind::MINUS, mult, multSig);
               d_rangeAssertions.insert(
                   mkRangeConstraint(d_bvToIntCache[current], bvsize));
-              d_rangeAssertions.insert(mkRangeConstraint(sigma, bvsize));
+              if (translated_children[0].isConst()
+                  || translated_children[1].isConst())
+              {
+                /*
+                 * based on equation (23), section 3.2.3 of:
+                 * Bozzano et al.
+                 * Encoding RTL Constructs for MathSAT: a Preliminary Report.
+                 */
+                // this is an optimization when one of the children is constant
+                Node c = translated_children[0].isConst()
+                             ? translated_children[0]
+                             : translated_children[1];
+                d_rangeAssertions.insert(
+                    d_nm->mkNode(kind::LEQ, d_zero, sigma));
+                // the value of sigma is bounded by (c - 1)
+                // where c is the constant multiplicand
+                d_rangeAssertions.insert(d_nm->mkNode(kind::LT, sigma, c));
+              }
+              else
+              {
+                d_rangeAssertions.insert(mkRangeConstraint(sigma, bvsize));
+              }
               break;
             }
             case kind::BITVECTOR_UDIV_TOTAL:
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 7b8e61359..f1e9e39c5 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -169,7 +169,7 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
       std::stringstream ssv;
       if (varCounter < 26)
       {
-        ssv << String::convertUnsignedIntToChar(varCounter + 32);
+        ssv << static_cast<char>(varCounter + 61);
       }
       else
       {
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index cad3c4640..1178c7299 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -160,6 +160,11 @@ void CvcPrinter::toStream(
       toStreamRational(out, n, false);
       break;
     }
+    case kind::CONST_STRING:
+    {
+      out << '"' << n.getConst<String>().toString() << '"';
+      break;
+    }
     case kind::TYPE_CONSTANT:
       switch(TypeConstant tc = n.getConst<TypeConstant>()) {
       case REAL_TYPE:
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 541827f89..6e4fcb63a 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -202,7 +202,7 @@ void Smt2Printer::toStream(std::ostream& out,
     }
 
     case kind::CONST_STRING: {
-      std::string s = n.getConst<String>().toString(true);
+      std::string s = n.getConst<String>().toString();
       out << '"';
       for(size_t i = 0; i < s.size(); ++i) {
         char c = s[i];
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
new file mode 100644
index 000000000..e0493b180
--- /dev/null
+++ b/src/smt/set_defaults.cpp
@@ -0,0 +1,1353 @@
+/*********************                                                        */
+/*! \file set_defaults.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Implementation of setting default options.
+ **/
+
+#include "smt/set_defaults.h"
+
+#include "base/output.h"
+#include "options/arith_options.h"
+#include "options/arrays_options.h"
+#include "options/base_options.h"
+#include "options/booleans_options.h"
+#include "options/bv_options.h"
+#include "options/datatypes_options.h"
+#include "options/decision_options.h"
+#include "options/language.h"
+#include "options/main_options.h"
+#include "options/open_ostream.h"
+#include "options/option_exception.h"
+#include "options/printer_options.h"
+#include "options/proof_options.h"
+#include "options/prop_options.h"
+#include "options/quantifiers_options.h"
+#include "options/sep_options.h"
+#include "options/set_language.h"
+#include "options/smt_options.h"
+#include "options/strings_options.h"
+#include "options/theory_options.h"
+#include "options/uf_options.h"
+#include "theory/theory.h"
+
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace smt {
+
+void setDefaults(SmtEngine& smte, LogicInfo& logic)
+{
+  // Language-based defaults
+  if (!options::bitvectorDivByZeroConst.wasSetByUser())
+  {
+    // Bitvector-divide-by-zero changed semantics in SMT LIB 2.6, thus we
+    // set this option if the input format is SMT LIB 2.6. We also set this
+    // option if we are sygus, since we assume SMT LIB 2.6 semantics for sygus.
+    options::bitvectorDivByZeroConst.set(
+        language::isInputLang_smt2_6(options::inputLanguage())
+        || language::isInputLangSygus(options::inputLanguage()));
+  }
+  bool is_sygus = language::isInputLangSygus(options::inputLanguage());
+
+  if (options::bitblastMode() == options::BitblastMode::EAGER)
+  {
+    if (options::produceModels()
+        && (logic.isTheoryEnabled(THEORY_ARRAYS)
+            || logic.isTheoryEnabled(THEORY_UF)))
+    {
+      if (options::bitblastMode.wasSetByUser()
+          || options::produceModels.wasSetByUser())
+      {
+        throw OptionException(std::string(
+            "Eager bit-blasting currently does not support model generation "
+            "for the combination of bit-vectors with arrays or uinterpreted "
+            "functions. Try --bitblast=lazy"));
+      }
+      Notice() << "SmtEngine: setting bit-blast mode to lazy to support model"
+               << "generation" << std::endl;
+      smte.setOption("bitblastMode", SExpr("lazy"));
+    }
+    else if (!options::incrementalSolving())
+    {
+      options::ackermann.set(true);
+    }
+
+    if (options::incrementalSolving() && !logic.isPure(THEORY_BV))
+    {
+      throw OptionException(
+          "Incremental eager bit-blasting is currently "
+          "only supported for QF_BV. Try --bitblast=lazy.");
+    }
+  }
+
+  if (options::solveIntAsBV() > 0)
+  {
+    logic = logic.getUnlockedCopy();
+    logic.enableTheory(THEORY_BV);
+    logic.lock();
+  }
+
+  if (options::solveBVAsInt() > 0)
+  {
+    if (logic.isTheoryEnabled(THEORY_BV))
+    {
+      logic = logic.getUnlockedCopy();
+      logic.enableTheory(THEORY_ARITH);
+      logic.arithNonLinear();
+      logic.lock();
+    }
+  }
+
+  // set options about ackermannization
+  if (options::ackermann() && options::produceModels()
+      && (logic.isTheoryEnabled(THEORY_ARRAYS)
+          || logic.isTheoryEnabled(THEORY_UF)))
+  {
+    if (options::produceModels.wasSetByUser())
+    {
+      throw OptionException(std::string(
+          "Ackermannization currently does not support model generation."));
+    }
+    Notice() << "SmtEngine: turn off ackermannization to support model"
+             << "generation" << std::endl;
+    options::ackermann.set(false);
+  }
+
+  if (options::ackermann())
+  {
+    if (options::incrementalSolving())
+    {
+      throw OptionException(
+          "Incremental Ackermannization is currently not supported.");
+    }
+
+    if (logic.isQuantified())
+    {
+      throw LogicException("Cannot use Ackermannization on quantified formula");
+    }
+
+    if (logic.isTheoryEnabled(THEORY_UF))
+    {
+      logic = logic.getUnlockedCopy();
+      logic.disableTheory(THEORY_UF);
+      logic.lock();
+    }
+    if (logic.isTheoryEnabled(THEORY_ARRAYS))
+    {
+      logic = logic.getUnlockedCopy();
+      logic.disableTheory(THEORY_ARRAYS);
+      logic.lock();
+    }
+  }
+
+  // Set default options associated with strings-exp. We also set these options
+  // if we are using eager string preprocessing, which may introduce quantified
+  // formulas at preprocess time.
+  if (options::stringExp() || !options::stringLazyPreproc())
+  {
+    // We require quantifiers since extended functions reduce using them.
+    if (!logic.isQuantified())
+    {
+      logic = logic.getUnlockedCopy();
+      logic.enableQuantifiers();
+      logic.lock();
+      Trace("smt") << "turning on quantifier logic, for strings-exp"
+                   << std::endl;
+    }
+    // We require bounded quantifier handling.
+    if (!options::fmfBound.wasSetByUser())
+    {
+      options::fmfBound.set(true);
+      Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
+    }
+    // Turn off E-matching, since some bounded quantifiers introduced by strings
+    // (e.g. for replaceall) admit matching loops.
+    if (!options::eMatching.wasSetByUser())
+    {
+      options::eMatching.set(false);
+      Trace("smt") << "turning off E-matching, for strings-exp" << std::endl;
+    }
+    // Do not eliminate extended arithmetic symbols from quantified formulas,
+    // since some strategies, e.g. --re-elim-agg, introduce them.
+    if (!options::elimExtArithQuant.wasSetByUser())
+    {
+      options::elimExtArithQuant.set(false);
+      Trace("smt") << "turning off elim-ext-arith-quant, for strings-exp"
+                   << std::endl;
+    }
+  }
+
+  // sygus inference may require datatypes
+  if (!smte.isInternalSubsolver())
+  {
+    if (options::produceAbducts() || options::sygusInference()
+        || options::sygusRewSynthInput())
+    {
+      // since we are trying to recast as sygus, we assume the input is sygus
+      is_sygus = true;
+    }
+  }
+
+  // We now know whether the input is sygus. Update the logic to incorporate
+  // the theories we need internally for handling sygus problems.
+  if (is_sygus)
+  {
+    logic = logic.getUnlockedCopy();
+    logic.enableSygus();
+    logic.lock();
+  }
+
+  // sygus core connective requires unsat cores
+  if (options::sygusCoreConnective())
+  {
+    options::unsatCores.set(true);
+  }
+
+  if ((options::checkModels() || options::checkSynthSol()
+       || options::produceAbducts()
+       || options::modelCoresMode() != options::ModelCoresMode::NONE
+       || options::blockModelsMode() != options::BlockModelsMode::NONE)
+      && !options::produceAssertions())
+  {
+    Notice() << "SmtEngine: turning on produce-assertions to support "
+             << "option requiring assertions." << std::endl;
+    smte.setOption("produce-assertions", SExpr("true"));
+  }
+
+  // Disable options incompatible with incremental solving, unsat cores, and
+  // proofs or output an error if enabled explicitly
+  if (options::incrementalSolving() || options::unsatCores()
+      || options::proof())
+  {
+    if (options::unconstrainedSimp())
+    {
+      if (options::unconstrainedSimp.wasSetByUser())
+      {
+        throw OptionException(
+            "unconstrained simplification not supported with unsat "
+            "cores/proofs/incremental solving");
+      }
+      Notice() << "SmtEngine: turning off unconstrained simplification to "
+                  "support unsat cores/proofs/incremental solving"
+               << std::endl;
+      options::unconstrainedSimp.set(false);
+    }
+  }
+  else
+  {
+    // Turn on unconstrained simplification for QF_AUFBV
+    if (!options::unconstrainedSimp.wasSetByUser())
+    {
+      bool uncSimp = !logic.isQuantified() && !options::produceModels()
+                     && !options::produceAssignments()
+                     && !options::checkModels()
+                     && (logic.isTheoryEnabled(THEORY_ARRAYS)
+                         && logic.isTheoryEnabled(THEORY_BV));
+      Trace("smt") << "setting unconstrained simplification to " << uncSimp
+                   << std::endl;
+      options::unconstrainedSimp.set(uncSimp);
+    }
+  }
+
+  if (options::incrementalSolving() || options::proof())
+  {
+    if (options::sygusInference())
+    {
+      if (options::sygusInference.wasSetByUser())
+      {
+        throw OptionException(
+            "sygus inference not supported with proofs/incremental solving");
+      }
+      Notice() << "SmtEngine: turning off sygus inference to support "
+                  "proofs/incremental solving"
+               << std::endl;
+      options::sygusInference.set(false);
+    }
+  }
+
+  // Disable options incompatible with unsat cores and proofs or output an
+  // error if enabled explicitly
+  if (options::unsatCores() || options::proof())
+  {
+    if (options::simplificationMode() != options::SimplificationMode::NONE)
+    {
+      if (options::simplificationMode.wasSetByUser())
+      {
+        throw OptionException(
+            "simplification not supported with unsat cores/proofs");
+      }
+      Notice() << "SmtEngine: turning off simplification to support unsat "
+                  "cores/proofs"
+               << std::endl;
+      options::simplificationMode.set(options::SimplificationMode::NONE);
+    }
+
+    if (options::pbRewrites())
+    {
+      if (options::pbRewrites.wasSetByUser())
+      {
+        throw OptionException(
+            "pseudoboolean rewrites not supported with unsat cores/proofs");
+      }
+      Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
+                  "unsat cores/proofs"
+               << std::endl;
+      smte.setOption("pb-rewrites", false);
+    }
+
+    if (options::sortInference())
+    {
+      if (options::sortInference.wasSetByUser())
+      {
+        throw OptionException(
+            "sort inference not supported with unsat cores/proofs");
+      }
+      Notice() << "SmtEngine: turning off sort inference to support unsat "
+                  "cores/proofs"
+               << std::endl;
+      options::sortInference.set(false);
+    }
+
+    if (options::preSkolemQuant())
+    {
+      if (options::preSkolemQuant.wasSetByUser())
+      {
+        throw OptionException(
+            "pre-skolemization not supported with unsat cores/proofs");
+      }
+      Notice() << "SmtEngine: turning off pre-skolemization to support unsat "
+                  "cores/proofs"
+               << std::endl;
+      options::preSkolemQuant.set(false);
+    }
+
+    if (options::solveBVAsInt() > 0)
+    {
+      /**
+       * Operations on 1 bits are better handled as Boolean operations
+       * than as integer operations.
+       * Therefore, we enable bv-to-bool, which runs before
+       * the translation to integers.
+       */
+      options::bitvectorToBool.set(true);
+    }
+
+    if (options::bitvectorToBool())
+    {
+      if (options::bitvectorToBool.wasSetByUser())
+      {
+        throw OptionException(
+            "bv-to-bool not supported with unsat cores/proofs");
+      }
+      Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat "
+                  "cores/proofs"
+               << std::endl;
+      options::bitvectorToBool.set(false);
+    }
+
+    if (options::boolToBitvector() != options::BoolToBVMode::OFF)
+    {
+      if (options::boolToBitvector.wasSetByUser())
+      {
+        throw OptionException(
+            "bool-to-bv != off not supported with unsat cores/proofs");
+      }
+      Notice() << "SmtEngine: turning off bool-to-bv to support unsat "
+                  "cores/proofs"
+               << std::endl;
+      smte.setOption("boolToBitvector", SExpr("off"));
+    }
+
+    if (options::bvIntroducePow2())
+    {
+      if (options::bvIntroducePow2.wasSetByUser())
+      {
+        throw OptionException(
+            "bv-intro-pow2 not supported with unsat cores/proofs");
+      }
+      Notice() << "SmtEngine: turning off bv-intro-pow2 to support "
+                  "unsat-cores/proofs"
+               << std::endl;
+      smte.setOption("bv-intro-pow2", false);
+    }
+
+    if (options::repeatSimp())
+    {
+      if (options::repeatSimp.wasSetByUser())
+      {
+        throw OptionException(
+            "repeat-simp not supported with unsat cores/proofs");
+      }
+      Notice() << "SmtEngine: turning off repeat-simp to support unsat "
+                  "cores/proofs"
+               << std::endl;
+      smte.setOption("repeat-simp", false);
+    }
+
+    if (options::globalNegate())
+    {
+      if (options::globalNegate.wasSetByUser())
+      {
+        throw OptionException(
+            "global-negate not supported with unsat cores/proofs");
+      }
+      Notice() << "SmtEngine: turning off global-negate to support unsat "
+                  "cores/proofs"
+               << std::endl;
+      smte.setOption("global-negate", false);
+    }
+
+    if (options::bitvectorAig())
+    {
+      throw OptionException(
+          "bitblast-aig not supported with unsat cores/proofs");
+    }
+  }
+  else
+  {
+    // by default, nonclausal simplification is off for QF_SAT
+    if (!options::simplificationMode.wasSetByUser())
+    {
+      bool qf_sat = logic.isPure(THEORY_BOOL) && !logic.isQuantified();
+      Trace("smt") << "setting simplification mode to <"
+                   << logic.getLogicString() << "> " << (!qf_sat) << std::endl;
+      // simplification=none works better for SMT LIB benchmarks with
+      // quantifiers, not others options::simplificationMode.set(qf_sat ||
+      // quantifiers ? options::SimplificationMode::NONE :
+      // options::SimplificationMode::BATCH);
+      options::simplificationMode.set(qf_sat
+                                          ? options::SimplificationMode::NONE
+                                          : options::SimplificationMode::BATCH);
+    }
+  }
+
+  if (options::cbqiBv() && logic.isQuantified())
+  {
+    if (options::boolToBitvector() != options::BoolToBVMode::OFF)
+    {
+      if (options::boolToBitvector.wasSetByUser())
+      {
+        throw OptionException(
+            "bool-to-bv != off not supported with CBQI BV for quantified "
+            "logics");
+      }
+      Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
+               << std::endl;
+      smte.setOption("boolToBitvector", SExpr("off"));
+    }
+  }
+
+  // cases where we need produce models
+  if (!options::produceModels()
+      && (options::produceAssignments() || options::sygusRewSynthCheck()
+          || is_sygus))
+  {
+    Notice() << "SmtEngine: turning on produce-models" << std::endl;
+    smte.setOption("produce-models", SExpr("true"));
+  }
+
+  // Set the options for the theoryOf
+  if (!options::theoryOfMode.wasSetByUser())
+  {
+    if (logic.isSharingEnabled() && !logic.isTheoryEnabled(THEORY_BV)
+        && !logic.isTheoryEnabled(THEORY_STRINGS)
+        && !logic.isTheoryEnabled(THEORY_SETS))
+    {
+      Trace("smt") << "setting theoryof-mode to term-based" << std::endl;
+      options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED);
+    }
+  }
+
+  // strings require LIA, UF; widen the logic
+  if (logic.isTheoryEnabled(THEORY_STRINGS))
+  {
+    LogicInfo log(logic.getUnlockedCopy());
+    // Strings requires arith for length constraints, and also UF
+    if (!logic.isTheoryEnabled(THEORY_UF))
+    {
+      Trace("smt") << "because strings are enabled, also enabling UF"
+                   << std::endl;
+      log.enableTheory(THEORY_UF);
+    }
+    if (!logic.isTheoryEnabled(THEORY_ARITH) || logic.isDifferenceLogic()
+        || !logic.areIntegersUsed())
+    {
+      Trace("smt") << "because strings are enabled, also enabling linear "
+                      "integer arithmetic"
+                   << std::endl;
+      log.enableTheory(THEORY_ARITH);
+      log.enableIntegers();
+      log.arithOnlyLinear();
+    }
+    logic = log;
+    logic.lock();
+  }
+  if (logic.isTheoryEnabled(THEORY_ARRAYS)
+      || logic.isTheoryEnabled(THEORY_DATATYPES)
+      || logic.isTheoryEnabled(THEORY_SETS))
+  {
+    if (!logic.isTheoryEnabled(THEORY_UF))
+    {
+      LogicInfo log(logic.getUnlockedCopy());
+      Trace("smt") << "because a theory that permits Boolean terms is enabled, "
+                      "also enabling UF"
+                   << std::endl;
+      log.enableTheory(THEORY_UF);
+      logic = log;
+      logic.lock();
+    }
+  }
+
+  // by default, symmetry breaker is on only for non-incremental QF_UF
+  if (!options::ufSymmetryBreaker.wasSetByUser())
+  {
+    bool qf_uf_noinc = logic.isPure(THEORY_UF) && !logic.isQuantified()
+                       && !options::incrementalSolving() && !options::proof()
+                       && !options::unsatCores();
+    Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc
+                 << std::endl;
+    options::ufSymmetryBreaker.set(qf_uf_noinc);
+  }
+
+  // If in arrays, set the UF handler to arrays
+  if (logic.isTheoryEnabled(THEORY_ARRAYS)
+      && (!logic.isQuantified()
+          || (logic.isQuantified() && !logic.isTheoryEnabled(THEORY_UF))))
+  {
+    Theory::setUninterpretedSortOwner(THEORY_ARRAYS);
+  }
+  else
+  {
+    Theory::setUninterpretedSortOwner(THEORY_UF);
+  }
+
+  if (!options::simplifyWithCareEnabled.wasSetByUser())
+  {
+    bool qf_aufbv =
+        !logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
+        && logic.isTheoryEnabled(THEORY_UF) && logic.isTheoryEnabled(THEORY_BV);
+
+    bool withCare = qf_aufbv;
+    Trace("smt") << "setting ite simplify with care to " << withCare
+                 << std::endl;
+    options::simplifyWithCareEnabled.set(withCare);
+  }
+  // Turn off array eager index splitting for QF_AUFLIA
+  if (!options::arraysEagerIndexSplitting.wasSetByUser())
+  {
+    if (not logic.isQuantified() && logic.isTheoryEnabled(THEORY_ARRAYS)
+        && logic.isTheoryEnabled(THEORY_UF)
+        && logic.isTheoryEnabled(THEORY_ARITH))
+    {
+      Trace("smt") << "setting array eager index splitting to false"
+                   << std::endl;
+      options::arraysEagerIndexSplitting.set(false);
+    }
+  }
+  // Turn on multiple-pass non-clausal simplification for QF_AUFBV
+  if (!options::repeatSimp.wasSetByUser())
+  {
+    bool repeatSimp = !logic.isQuantified()
+                      && (logic.isTheoryEnabled(THEORY_ARRAYS)
+                          && logic.isTheoryEnabled(THEORY_UF)
+                          && logic.isTheoryEnabled(THEORY_BV))
+                      && !options::unsatCores();
+    Trace("smt") << "setting repeat simplification to " << repeatSimp
+                 << std::endl;
+    options::repeatSimp.set(repeatSimp);
+  }
+
+  if (options::boolToBitvector() == options::BoolToBVMode::ALL
+      && !logic.isTheoryEnabled(THEORY_BV))
+  {
+    if (options::boolToBitvector.wasSetByUser())
+    {
+      throw OptionException(
+          "bool-to-bv=all not supported for non-bitvector logics.");
+    }
+    Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: "
+             << logic.getLogicString() << std::endl;
+    smte.setOption("boolToBitvector", SExpr("off"));
+  }
+
+  if (!options::bvEagerExplanations.wasSetByUser()
+      && logic.isTheoryEnabled(THEORY_ARRAYS)
+      && logic.isTheoryEnabled(THEORY_BV))
+  {
+    Trace("smt") << "enabling eager bit-vector explanations " << std::endl;
+    options::bvEagerExplanations.set(true);
+  }
+
+  // Turn on arith rewrite equalities only for pure arithmetic
+  if (!options::arithRewriteEq.wasSetByUser())
+  {
+    bool arithRewriteEq =
+        logic.isPure(THEORY_ARITH) && logic.isLinear() && !logic.isQuantified();
+    Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq
+                 << std::endl;
+    options::arithRewriteEq.set(arithRewriteEq);
+  }
+  if (!options::arithHeuristicPivots.wasSetByUser())
+  {
+    int16_t heuristicPivots = 5;
+    if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
+    {
+      if (logic.isDifferenceLogic())
+      {
+        heuristicPivots = -1;
+      }
+      else if (!logic.areIntegersUsed())
+      {
+        heuristicPivots = 0;
+      }
+    }
+    Trace("smt") << "setting arithHeuristicPivots  " << heuristicPivots
+                 << std::endl;
+    options::arithHeuristicPivots.set(heuristicPivots);
+  }
+  if (!options::arithPivotThreshold.wasSetByUser())
+  {
+    uint16_t pivotThreshold = 2;
+    if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
+    {
+      if (logic.isDifferenceLogic())
+      {
+        pivotThreshold = 16;
+      }
+    }
+    Trace("smt") << "setting arith arithPivotThreshold  " << pivotThreshold
+                 << std::endl;
+    options::arithPivotThreshold.set(pivotThreshold);
+  }
+  if (!options::arithStandardCheckVarOrderPivots.wasSetByUser())
+  {
+    int16_t varOrderPivots = -1;
+    if (logic.isPure(THEORY_ARITH) && !logic.isQuantified())
+    {
+      varOrderPivots = 200;
+    }
+    Trace("smt") << "setting arithStandardCheckVarOrderPivots  "
+                 << varOrderPivots << std::endl;
+    options::arithStandardCheckVarOrderPivots.set(varOrderPivots);
+  }
+  if (logic.isPure(THEORY_ARITH) && !logic.areRealsUsed())
+  {
+    if (!options::nlExtTangentPlanesInterleave.wasSetByUser())
+    {
+      Trace("smt") << "setting nlExtTangentPlanesInterleave to true"
+                   << std::endl;
+      options::nlExtTangentPlanesInterleave.set(true);
+    }
+  }
+
+  // Set decision mode based on logic (if not set by user)
+  if (!options::decisionMode.wasSetByUser())
+  {
+    options::DecisionMode decMode =
+        // sygus uses internal
+        is_sygus ? options::DecisionMode::INTERNAL :
+                 // ALL
+            logic.hasEverything()
+                ? options::DecisionMode::JUSTIFICATION
+                : (  // QF_BV
+                      (not logic.isQuantified() && logic.isPure(THEORY_BV)) ||
+                              // QF_AUFBV or QF_ABV or QF_UFBV
+                              (not logic.isQuantified()
+                               && (logic.isTheoryEnabled(THEORY_ARRAYS)
+                                   || logic.isTheoryEnabled(THEORY_UF))
+                               && logic.isTheoryEnabled(THEORY_BV))
+                              ||
+                              // QF_AUFLIA (and may be ends up enabling
+                              // QF_AUFLRA?)
+                              (not logic.isQuantified()
+                               && logic.isTheoryEnabled(THEORY_ARRAYS)
+                               && logic.isTheoryEnabled(THEORY_UF)
+                               && logic.isTheoryEnabled(THEORY_ARITH))
+                              ||
+                              // QF_LRA
+                              (not logic.isQuantified()
+                               && logic.isPure(THEORY_ARITH) && logic.isLinear()
+                               && !logic.isDifferenceLogic()
+                               && !logic.areIntegersUsed())
+                              ||
+                              // Quantifiers
+                              logic.isQuantified() ||
+                              // Strings
+                              logic.isTheoryEnabled(THEORY_STRINGS)
+                          ? options::DecisionMode::JUSTIFICATION
+                          : options::DecisionMode::INTERNAL);
+
+    bool stoponly =
+        // ALL
+        logic.hasEverything() || logic.isTheoryEnabled(THEORY_STRINGS)
+            ? false
+            : (  // QF_AUFLIA
+                  (not logic.isQuantified()
+                   && logic.isTheoryEnabled(THEORY_ARRAYS)
+                   && logic.isTheoryEnabled(THEORY_UF)
+                   && logic.isTheoryEnabled(THEORY_ARITH))
+                          ||
+                          // QF_LRA
+                          (not logic.isQuantified()
+                           && logic.isPure(THEORY_ARITH) && logic.isLinear()
+                           && !logic.isDifferenceLogic()
+                           && !logic.areIntegersUsed())
+                      ? true
+                      : false);
+
+    Trace("smt") << "setting decision mode to " << decMode << std::endl;
+    options::decisionMode.set(decMode);
+    options::decisionStopOnly.set(stoponly);
+  }
+  if (options::incrementalSolving())
+  {
+    // disable modes not supported by incremental
+    options::sortInference.set(false);
+    options::ufssFairnessMonotone.set(false);
+    options::quantEpr.set(false);
+    options::globalNegate.set(false);
+  }
+  if (logic.hasCardinalityConstraints())
+  {
+    // must have finite model finding on
+    options::finiteModelFind.set(true);
+  }
+
+  // if it contains a theory with non-termination, do not strictly enforce that
+  // quantifiers and theory combination must be interleaved
+  if (logic.isTheoryEnabled(THEORY_STRINGS)
+      || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
+  {
+    if (!options::instWhenStrictInterleave.wasSetByUser())
+    {
+      options::instWhenStrictInterleave.set(false);
+    }
+  }
+
+  if (options::instMaxLevel() != -1)
+  {
+    Notice() << "SmtEngine: turning off cbqi to support instMaxLevel"
+             << std::endl;
+    options::cbqi.set(false);
+  }
+  // Do we need to track instantiations?
+  // Needed for sygus due to single invocation techniques.
+  if (options::cbqiNestedQE()
+      || (options::proof() && !options::trackInstLemmas.wasSetByUser())
+      || is_sygus)
+  {
+    options::trackInstLemmas.set(true);
+  }
+
+  if ((options::fmfBoundLazy.wasSetByUser() && options::fmfBoundLazy())
+      || (options::fmfBoundInt.wasSetByUser() && options::fmfBoundInt()))
+  {
+    options::fmfBound.set(true);
+  }
+  // now have determined whether fmfBoundInt is on/off
+  // apply fmfBoundInt options
+  if (options::fmfBound())
+  {
+    if (!options::mbqiMode.wasSetByUser()
+        || (options::mbqiMode() != options::MbqiMode::NONE
+            && options::mbqiMode() != options::MbqiMode::FMC))
+    {
+      // if bounded integers are set, use no MBQI by default
+      options::mbqiMode.set(options::MbqiMode::NONE);
+    }
+    if (!options::prenexQuant.wasSetByUser())
+    {
+      options::prenexQuant.set(options::PrenexQuantMode::NONE);
+    }
+  }
+  if (options::ufHo())
+  {
+    // if higher-order, then current variants of model-based instantiation
+    // cannot be used
+    if (options::mbqiMode() != options::MbqiMode::NONE)
+    {
+      options::mbqiMode.set(options::MbqiMode::NONE);
+    }
+    if (!options::hoElimStoreAx.wasSetByUser())
+    {
+      // by default, use store axioms only if --ho-elim is set
+      options::hoElimStoreAx.set(options::hoElim());
+    }
+  }
+  if (options::fmfFunWellDefinedRelevant())
+  {
+    if (!options::fmfFunWellDefined.wasSetByUser())
+    {
+      options::fmfFunWellDefined.set(true);
+    }
+  }
+  if (options::fmfFunWellDefined())
+  {
+    if (!options::finiteModelFind.wasSetByUser())
+    {
+      options::finiteModelFind.set(true);
+    }
+  }
+  // EPR
+  if (options::quantEpr())
+  {
+    if (!options::preSkolemQuant.wasSetByUser())
+    {
+      options::preSkolemQuant.set(true);
+    }
+  }
+
+  // now, have determined whether finite model find is on/off
+  // apply finite model finding options
+  if (options::finiteModelFind())
+  {
+    // apply conservative quantifiers splitting
+    if (!options::quantDynamicSplit.wasSetByUser())
+    {
+      options::quantDynamicSplit.set(options::QuantDSplitMode::DEFAULT);
+    }
+    // do not eliminate extended arithmetic symbols from quantified formulas
+    if (!options::elimExtArithQuant.wasSetByUser())
+    {
+      options::elimExtArithQuant.set(false);
+    }
+    if (!options::eMatching.wasSetByUser())
+    {
+      options::eMatching.set(options::fmfInstEngine());
+    }
+    if (!options::instWhenMode.wasSetByUser())
+    {
+      // instantiate only on last call
+      if (options::eMatching())
+      {
+        options::instWhenMode.set(options::InstWhenMode::LAST_CALL);
+      }
+    }
+  }
+
+  // apply sygus options
+  // if we are attempting to rewrite everything to SyGuS, use sygus()
+  if (is_sygus)
+  {
+    if (!options::sygus())
+    {
+      Trace("smt") << "turning on sygus" << std::endl;
+    }
+    options::sygus.set(true);
+    // must use Ferrante/Rackoff for real arithmetic
+    if (!options::cbqiMidpoint.wasSetByUser())
+    {
+      options::cbqiMidpoint.set(true);
+    }
+    if (options::sygusRepairConst())
+    {
+      if (!options::cbqi.wasSetByUser())
+      {
+        options::cbqi.set(true);
+      }
+    }
+    if (options::sygusInference())
+    {
+      // optimization: apply preskolemization, makes it succeed more often
+      if (!options::preSkolemQuant.wasSetByUser())
+      {
+        options::preSkolemQuant.set(true);
+      }
+      if (!options::preSkolemQuantNested.wasSetByUser())
+      {
+        options::preSkolemQuantNested.set(true);
+      }
+    }
+    // counterexample-guided instantiation for sygus
+    if (!options::cegqiSingleInvMode.wasSetByUser())
+    {
+      options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::USE);
+    }
+    if (!options::quantConflictFind.wasSetByUser())
+    {
+      options::quantConflictFind.set(false);
+    }
+    if (!options::instNoEntail.wasSetByUser())
+    {
+      options::instNoEntail.set(false);
+    }
+    if (!options::cbqiFullEffort.wasSetByUser())
+    {
+      // should use full effort cbqi for single invocation and repair const
+      options::cbqiFullEffort.set(true);
+    }
+    if (options::sygusRew())
+    {
+      options::sygusRewSynth.set(true);
+      options::sygusRewVerify.set(true);
+    }
+    if (options::sygusRewSynthInput())
+    {
+      // If we are using synthesis rewrite rules from input, we use
+      // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for
+      // details on this technique.
+      options::sygusRewSynth.set(true);
+      // we should not use the extended rewriter, since we are interested
+      // in rewrites that are not in the main rewriter
+      if (!options::sygusExtRew.wasSetByUser())
+      {
+        options::sygusExtRew.set(false);
+      }
+    }
+    // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
+    // is one that is specialized for returning a single solution. Non-basic
+    // sygus algorithms currently include the PBE solver, UNIF+PI, static
+    // template inference for invariant synthesis, and single invocation
+    // techniques.
+    bool reqBasicSygus = false;
+    if (options::produceAbducts())
+    {
+      // if doing abduction, we should filter strong solutions
+      if (!options::sygusFilterSolMode.wasSetByUser())
+      {
+        options::sygusFilterSolMode.set(options::SygusFilterSolMode::STRONG);
+      }
+      // we must use basic sygus algorithms, since e.g. we require checking
+      // a sygus side condition for consistency with axioms.
+      reqBasicSygus = true;
+    }
+    if (options::sygusRewSynth() || options::sygusRewVerify()
+        || options::sygusQueryGen())
+    {
+      // rewrite rule synthesis implies that sygus stream must be true
+      options::sygusStream.set(true);
+    }
+    if (options::sygusStream() || options::incrementalSolving())
+    {
+      // Streaming and incremental mode are incompatible with techniques that
+      // focus the search towards finding a single solution.
+      reqBasicSygus = true;
+    }
+    // Now, disable options for non-basic sygus algorithms, if necessary.
+    if (reqBasicSygus)
+    {
+      if (!options::sygusUnifPbe.wasSetByUser())
+      {
+        options::sygusUnifPbe.set(false);
+      }
+      if (options::sygusUnifPi.wasSetByUser())
+      {
+        options::sygusUnifPi.set(options::SygusUnifPiMode::NONE);
+      }
+      if (!options::sygusInvTemplMode.wasSetByUser())
+      {
+        options::sygusInvTemplMode.set(options::SygusInvTemplMode::NONE);
+      }
+      if (!options::cegqiSingleInvMode.wasSetByUser())
+      {
+        options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::NONE);
+      }
+    }
+    // do not allow partial functions
+    if (!options::bitvectorDivByZeroConst())
+    {
+      if (options::bitvectorDivByZeroConst.wasSetByUser())
+      {
+        throw OptionException(
+            "--no-bv-div-zero-const is not supported with SyGuS");
+      }
+      Notice()
+          << "SmtEngine: setting bv-div-zero-const to true to support SyGuS"
+          << std::endl;
+      options::bitvectorDivByZeroConst.set(true);
+    }
+    if (!options::dtRewriteErrorSel.wasSetByUser())
+    {
+      options::dtRewriteErrorSel.set(true);
+    }
+    // do not miniscope
+    if (!options::miniscopeQuant.wasSetByUser())
+    {
+      options::miniscopeQuant.set(false);
+    }
+    if (!options::miniscopeQuantFreeVar.wasSetByUser())
+    {
+      options::miniscopeQuantFreeVar.set(false);
+    }
+    if (!options::quantSplit.wasSetByUser())
+    {
+      options::quantSplit.set(false);
+    }
+    // rewrite divk
+    if (!options::rewriteDivk.wasSetByUser())
+    {
+      options::rewriteDivk.set(true);
+    }
+    // do not do macros
+    if (!options::macrosQuant.wasSetByUser())
+    {
+      options::macrosQuant.set(false);
+    }
+    if (!options::cbqiPreRegInst.wasSetByUser())
+    {
+      options::cbqiPreRegInst.set(true);
+    }
+  }
+  // counterexample-guided instantiation for non-sygus
+  // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
+  if ((logic.isQuantified()
+       && (logic.isTheoryEnabled(THEORY_ARITH)
+           || logic.isTheoryEnabled(THEORY_DATATYPES)
+           || logic.isTheoryEnabled(THEORY_BV)
+           || logic.isTheoryEnabled(THEORY_FP)))
+      || options::cbqiAll())
+  {
+    if (!options::cbqi.wasSetByUser())
+    {
+      options::cbqi.set(true);
+    }
+    // check whether we should apply full cbqi
+    if (logic.isPure(THEORY_BV))
+    {
+      if (!options::cbqiFullEffort.wasSetByUser())
+      {
+        options::cbqiFullEffort.set(true);
+      }
+    }
+  }
+  if (options::cbqi())
+  {
+    // must rewrite divk
+    if (!options::rewriteDivk.wasSetByUser())
+    {
+      options::rewriteDivk.set(true);
+    }
+    if (options::incrementalSolving())
+    {
+      // cannot do nested quantifier elimination in incremental mode
+      options::cbqiNestedQE.set(false);
+    }
+    if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
+    {
+      if (!options::quantConflictFind.wasSetByUser())
+      {
+        options::quantConflictFind.set(false);
+      }
+      if (!options::instNoEntail.wasSetByUser())
+      {
+        options::instNoEntail.set(false);
+      }
+      if (!options::instWhenMode.wasSetByUser() && options::cbqiModel())
+      {
+        // only instantiation should happen at last call when model is avaiable
+        options::instWhenMode.set(options::InstWhenMode::LAST_CALL);
+      }
+    }
+    else
+    {
+      // only supported in pure arithmetic or pure BV
+      options::cbqiNestedQE.set(false);
+    }
+    // prenexing
+    if (options::cbqiNestedQE())
+    {
+      // only complete with prenex = disj_normal or normal
+      if (options::prenexQuant() <= options::PrenexQuantMode::DISJ_NORMAL)
+      {
+        options::prenexQuant.set(options::PrenexQuantMode::DISJ_NORMAL);
+      }
+    }
+    else if (options::globalNegate())
+    {
+      if (!options::prenexQuant.wasSetByUser())
+      {
+        options::prenexQuant.set(options::PrenexQuantMode::NONE);
+      }
+    }
+  }
+  // implied options...
+  if (options::strictTriggers())
+  {
+    if (!options::userPatternsQuant.wasSetByUser())
+    {
+      options::userPatternsQuant.set(options::UserPatMode::TRUST);
+    }
+  }
+  if (options::qcfMode.wasSetByUser() || options::qcfTConstraint())
+  {
+    options::quantConflictFind.set(true);
+  }
+  if (options::cbqiNestedQE())
+  {
+    options::prenexQuantUser.set(true);
+    if (!options::preSkolemQuant.wasSetByUser())
+    {
+      options::preSkolemQuant.set(true);
+    }
+  }
+  // for induction techniques
+  if (options::quantInduction())
+  {
+    if (!options::dtStcInduction.wasSetByUser())
+    {
+      options::dtStcInduction.set(true);
+    }
+    if (!options::intWfInduction.wasSetByUser())
+    {
+      options::intWfInduction.set(true);
+    }
+  }
+  if (options::dtStcInduction())
+  {
+    // try to remove ITEs from quantified formulas
+    if (!options::iteDtTesterSplitQuant.wasSetByUser())
+    {
+      options::iteDtTesterSplitQuant.set(true);
+    }
+    if (!options::iteLiftQuant.wasSetByUser())
+    {
+      options::iteLiftQuant.set(options::IteLiftQuantMode::ALL);
+    }
+  }
+  if (options::intWfInduction())
+  {
+    if (!options::purifyTriggers.wasSetByUser())
+    {
+      options::purifyTriggers.set(true);
+    }
+  }
+  if (options::conjectureNoFilter())
+  {
+    if (!options::conjectureFilterActiveTerms.wasSetByUser())
+    {
+      options::conjectureFilterActiveTerms.set(false);
+    }
+    if (!options::conjectureFilterCanonical.wasSetByUser())
+    {
+      options::conjectureFilterCanonical.set(false);
+    }
+    if (!options::conjectureFilterModel.wasSetByUser())
+    {
+      options::conjectureFilterModel.set(false);
+    }
+  }
+  if (options::conjectureGenPerRound.wasSetByUser())
+  {
+    if (options::conjectureGenPerRound() > 0)
+    {
+      options::conjectureGen.set(true);
+    }
+    else
+    {
+      options::conjectureGen.set(false);
+    }
+  }
+  // can't pre-skolemize nested quantifiers without UF theory
+  if (!logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant())
+  {
+    if (!options::preSkolemQuantNested.wasSetByUser())
+    {
+      options::preSkolemQuantNested.set(false);
+    }
+  }
+  if (!logic.isTheoryEnabled(THEORY_DATATYPES))
+  {
+    options::quantDynamicSplit.set(options::QuantDSplitMode::NONE);
+  }
+
+  // until bugs 371,431 are fixed
+  if (!options::minisatUseElim.wasSetByUser())
+  {
+    // cannot use minisat elimination for logics where a theory solver
+    // introduces new literals into the search. This includes quantifiers
+    // (quantifier instantiation), and the lemma schemas used in non-linear
+    // and sets. We also can't use it if models are enabled.
+    if (logic.isTheoryEnabled(THEORY_SETS) || logic.isQuantified()
+        || options::produceModels() || options::produceAssignments()
+        || options::checkModels()
+        || (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()))
+    {
+      options::minisatUseElim.set(false);
+    }
+  }
+
+  // For now, these array theory optimizations do not support model-building
+  if (options::produceModels() || options::produceAssignments()
+      || options::checkModels())
+  {
+    options::arraysOptimizeLinear.set(false);
+    options::arraysLazyRIntro1.set(false);
+  }
+
+  if (options::proof())
+  {
+    if (options::incrementalSolving())
+    {
+      if (options::incrementalSolving.wasSetByUser())
+      {
+        throw OptionException("--incremental is not supported with proofs");
+      }
+      Warning()
+          << "SmtEngine: turning off incremental solving mode (not yet "
+             "supported with --proof, try --tear-down-incremental instead)"
+          << std::endl;
+      smte.setOption("incremental", SExpr("false"));
+    }
+    if (logic > LogicInfo("QF_AUFBVLRA"))
+    {
+      throw OptionException(
+          "Proofs are only supported for sub-logics of QF_AUFBVLIA.");
+    }
+    if (options::bitvectorAlgebraicSolver())
+    {
+      if (options::bitvectorAlgebraicSolver.wasSetByUser())
+      {
+        throw OptionException(
+            "--bv-algebraic-solver is not supported with proofs");
+      }
+      Notice() << "SmtEngine: turning off bv algebraic solver to support proofs"
+               << std::endl;
+      options::bitvectorAlgebraicSolver.set(false);
+    }
+    if (options::bitvectorEqualitySolver())
+    {
+      if (options::bitvectorEqualitySolver.wasSetByUser())
+      {
+        throw OptionException("--bv-eq-solver is not supported with proofs");
+      }
+      Notice() << "SmtEngine: turning off bv eq solver to support proofs"
+               << std::endl;
+      options::bitvectorEqualitySolver.set(false);
+    }
+    if (options::bitvectorInequalitySolver())
+    {
+      if (options::bitvectorInequalitySolver.wasSetByUser())
+      {
+        throw OptionException(
+            "--bv-inequality-solver is not supported with proofs");
+      }
+      Notice() << "SmtEngine: turning off bv ineq solver to support proofs"
+               << std::endl;
+      options::bitvectorInequalitySolver.set(false);
+    }
+  }
+
+  if (!options::bitvectorEqualitySolver())
+  {
+    if (options::bvLazyRewriteExtf())
+    {
+      if (options::bvLazyRewriteExtf.wasSetByUser())
+      {
+        throw OptionException(
+            "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set");
+      }
+    }
+    Trace("smt")
+        << "disabling bvLazyRewriteExtf since equality solver is disabled"
+        << std::endl;
+    options::bvLazyRewriteExtf.set(false);
+  }
+
+  if (!options::sygusExprMinerCheckUseExport())
+  {
+    if (options::sygusExprMinerCheckTimeout.wasSetByUser())
+    {
+      throw OptionException(
+          "--sygus-expr-miner-check-timeout=N requires "
+          "--sygus-expr-miner-check-use-export");
+    }
+    if (options::sygusRewSynthInput() || options::produceAbducts())
+    {
+      std::stringstream ss;
+      ss << (options::sygusRewSynthInput() ? "--sygus-rr-synth-input"
+                                           : "--produce-abducts");
+      ss << "requires --sygus-expr-miner-check-use-export";
+      throw OptionException(ss.str());
+    }
+  }
+
+  if (options::stringFMF() && !options::stringProcessLoopMode.wasSetByUser())
+  {
+    Trace("smt") << "settting stringProcessLoopMode to 'simple' since "
+                    "--strings-fmf enabled"
+                 << std::endl;
+    options::stringProcessLoopMode.set(options::ProcessLoopMode::SIMPLE);
+  }
+
+  // !!! All options that require disabling models go here
+  bool disableModels = false;
+  std::string sOptNoModel;
+  if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp())
+  {
+    disableModels = true;
+    sOptNoModel = "unconstrained-simp";
+  }
+  else if (options::sortInference())
+  {
+    disableModels = true;
+    sOptNoModel = "sort-inference";
+  }
+  else if (options::minisatUseElim())
+  {
+    disableModels = true;
+    sOptNoModel = "minisat-elimination";
+  }
+  else if (logic.isTheoryEnabled(THEORY_ARITH) && !logic.isLinear()
+           && !options::nlExt())
+  {
+    disableModels = true;
+    sOptNoModel = "nonlinear arithmetic without nl-ext";
+  }
+  else if (options::globalNegate())
+  {
+    disableModels = true;
+    sOptNoModel = "global-negate";
+  }
+  if (disableModels)
+  {
+    if (options::produceModels())
+    {
+      if (options::produceModels.wasSetByUser())
+      {
+        std::stringstream ss;
+        ss << "Cannot use " << sOptNoModel << " with model generation.";
+        throw OptionException(ss.str());
+      }
+      Notice() << "SmtEngine: turning off produce-models to support "
+               << sOptNoModel << std::endl;
+      smte.setOption("produce-models", SExpr("false"));
+    }
+    if (options::produceAssignments())
+    {
+      if (options::produceAssignments.wasSetByUser())
+      {
+        std::stringstream ss;
+        ss << "Cannot use " << sOptNoModel
+           << " with model generation (produce-assignments).";
+        throw OptionException(ss.str());
+      }
+      Notice() << "SmtEngine: turning off produce-assignments to support "
+               << sOptNoModel << std::endl;
+      smte.setOption("produce-assignments", SExpr("false"));
+    }
+    if (options::checkModels())
+    {
+      if (options::checkModels.wasSetByUser())
+      {
+        std::stringstream ss;
+        ss << "Cannot use " << sOptNoModel
+           << " with model generation (check-models).";
+        throw OptionException(ss.str());
+      }
+      Notice() << "SmtEngine: turning off check-models to support "
+               << sOptNoModel << std::endl;
+      smte.setOption("check-models", SExpr("false"));
+    }
+  }
+}
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h
new file mode 100644
index 000000000..8871b0b38
--- /dev/null
+++ b/src/smt/set_defaults.h
@@ -0,0 +1,42 @@
+/*********************                                                        */
+/*! \file set_defaults.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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 Method for setting the default options of an SMT engine.
+ **/
+
+#ifndef CVC4__SMT__SET_DEFAULTS_H
+#define CVC4__SMT__SET_DEFAULTS_H
+
+#include "smt/smt_engine.h"
+#include "theory/logic_info.h"
+
+namespace CVC4 {
+namespace smt {
+
+/**
+ * The purpose of this method is to set the default options and update the logic
+ * info for SMT engine smte.
+ *
+ * The argument logic is a reference to the logic of SmtEngine, which can be
+ * updated by this method based on the current options and the logic itself.
+ *
+ * Note that currently, options are associated with the ExprManager. Thus, this
+ * call updates the options associated with the current ExprManager.
+ * If this designed is updated in the future so that SmtEngine has its own
+ * copy of options, this method should be updated accordingly so that it
+ * is responsible for updating this copy.
+ */
+void setDefaults(SmtEngine& smte, LogicInfo& logic);
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__SET_DEFAULTS_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 61d7fb329..30c1cd0f5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -86,6 +86,7 @@
 #include "smt/managed_ostreams.h"
 #include "smt/model_blocker.h"
 #include "smt/model_core_builder.h"
+#include "smt/set_defaults.h"
 #include "smt/smt_engine_scope.h"
 #include "smt/term_formula_removal.h"
 #include "smt/update_ostream.h"
@@ -869,7 +870,6 @@ SmtEngine::SmtEngine(ExprManager* em)
       d_fullyInited(false),
       d_queryMade(false),
       d_needPostsolve(false),
-      d_earlyTheoryPP(true),
       d_globalNegation(false),
       d_status(),
       d_expectedStatus(),
@@ -925,8 +925,11 @@ void SmtEngine::finishInit()
 
   d_private->addUseTheoryListListener(getTheoryEngine());
 
+  // set the random seed
+  Random::getRandom().setSeed(options::seed());
+
   // ensure that our heuristics are properly set up
-  setDefaults();
+  setDefaults(*this, d_logic);
 
   Trace("smt-debug") << "Making decision engine..." << std::endl;
 
@@ -1142,1216 +1145,6 @@ void SmtEngine::setLogicInternal()
   d_logic.lock();
 }
 
-void SmtEngine::setDefaults() {
-  Random::getRandom().setSeed(options::seed());
-  // Language-based defaults
-  if (!options::bitvectorDivByZeroConst.wasSetByUser())
-  {
-    // Bitvector-divide-by-zero changed semantics in SMT LIB 2.6, thus we
-    // set this option if the input format is SMT LIB 2.6. We also set this
-    // option if we are sygus, since we assume SMT LIB 2.6 semantics for sygus.
-    options::bitvectorDivByZeroConst.set(
-        language::isInputLang_smt2_6(options::inputLanguage())
-        || language::isInputLangSygus(options::inputLanguage()));
-  }
-  bool is_sygus = language::isInputLangSygus(options::inputLanguage());
-
-  if (options::bitblastMode() == options::BitblastMode::EAGER)
-  {
-    if (options::produceModels()
-        && (d_logic.isTheoryEnabled(THEORY_ARRAYS)
-            || d_logic.isTheoryEnabled(THEORY_UF)))
-    {
-      if (options::bitblastMode.wasSetByUser()
-          || options::produceModels.wasSetByUser())
-      {
-        throw OptionException(std::string(
-            "Eager bit-blasting currently does not support model generation "
-            "for the combination of bit-vectors with arrays or uinterpreted "
-            "functions. Try --bitblast=lazy"));
-      }
-      Notice() << "SmtEngine: setting bit-blast mode to lazy to support model"
-               << "generation" << endl;
-      setOption("bitblastMode", SExpr("lazy"));
-    }
-    else if (!options::incrementalSolving())
-    {
-      options::ackermann.set(true);
-    }
-
-    if (options::incrementalSolving() && !d_logic.isPure(THEORY_BV))
-    {
-      throw OptionException(
-          "Incremental eager bit-blasting is currently "
-          "only supported for QF_BV. Try --bitblast=lazy.");
-    }
-  }
-
-  if (options::solveIntAsBV() > 0)
-  {
-    d_logic = d_logic.getUnlockedCopy();
-    d_logic.enableTheory(THEORY_BV);
-    d_logic.lock();
-  }
-
-  if (options::solveBVAsInt() > 0)
-  {
-    if (d_logic.isTheoryEnabled(THEORY_BV))
-    {
-      d_logic = d_logic.getUnlockedCopy();
-      d_logic.enableTheory(THEORY_ARITH);
-      d_logic.arithNonLinear();
-      d_logic.lock();
-    }
-  }
-
-  // set options about ackermannization
-  if (options::ackermann() && options::produceModels()
-      && (d_logic.isTheoryEnabled(THEORY_ARRAYS)
-          || d_logic.isTheoryEnabled(THEORY_UF)))
-  {
-    if (options::produceModels.wasSetByUser())
-    {
-      throw OptionException(std::string(
-          "Ackermannization currently does not support model generation."));
-    }
-    Notice() << "SmtEngine: turn off ackermannization to support model"
-             << "generation" << endl;
-    options::ackermann.set(false);
-  }
-
-  if (options::ackermann())
-  {
-    if (options::incrementalSolving())
-    {
-      throw OptionException(
-          "Incremental Ackermannization is currently not supported.");
-    }
-
-    if (d_logic.isQuantified())
-    {
-      throw LogicException("Cannot use Ackermannization on quantified formula");
-    }
-
-    if (d_logic.isTheoryEnabled(THEORY_UF))
-    {
-      d_logic = d_logic.getUnlockedCopy();
-      d_logic.disableTheory(THEORY_UF);
-      d_logic.lock();
-    }
-    if (d_logic.isTheoryEnabled(THEORY_ARRAYS))
-    {
-      d_logic = d_logic.getUnlockedCopy();
-      d_logic.disableTheory(THEORY_ARRAYS);
-      d_logic.lock();
-    }
-  }
-
-  // Set default options associated with strings-exp. We also set these options
-  // if we are using eager string preprocessing, which may introduce quantified
-  // formulas at preprocess time.
-  if (options::stringExp() || !options::stringLazyPreproc())
-  {
-    // We require quantifiers since extended functions reduce using them.
-    if (!d_logic.isQuantified())
-    {
-      d_logic = d_logic.getUnlockedCopy();
-      d_logic.enableQuantifiers();
-      d_logic.lock();
-      Trace("smt") << "turning on quantifier logic, for strings-exp"
-                   << std::endl;
-    }
-    // We require bounded quantifier handling.
-    if (!options::fmfBound.wasSetByUser())
-    {
-      options::fmfBound.set( true );
-      Trace("smt") << "turning on fmf-bound-int, for strings-exp" << std::endl;
-    }
-    // Turn off E-matching, since some bounded quantifiers introduced by strings
-    // (e.g. for replaceall) admit matching loops.
-    if (!options::eMatching.wasSetByUser())
-    {
-      options::eMatching.set(false);
-      Trace("smt") << "turning off E-matching, for strings-exp" << std::endl;
-    }
-    // Do not eliminate extended arithmetic symbols from quantified formulas,
-    // since some strategies, e.g. --re-elim-agg, introduce them.
-    if (!options::elimExtArithQuant.wasSetByUser())
-    {
-      options::elimExtArithQuant.set(false);
-      Trace("smt") << "turning off elim-ext-arith-quant, for strings-exp"
-                   << std::endl;
-    }
-  }
-
-  // sygus inference may require datatypes
-  if (!d_isInternalSubsolver)
-  {
-    if (options::produceAbducts() || options::sygusInference()
-        || options::sygusRewSynthInput())
-    {
-      // since we are trying to recast as sygus, we assume the input is sygus
-      is_sygus = true;
-    }
-  }
-
-  // We now know whether the input is sygus. Update the logic to incorporate
-  // the theories we need internally for handling sygus problems.
-  if (is_sygus)
-  {
-    d_logic = d_logic.getUnlockedCopy();
-    d_logic.enableSygus();
-    d_logic.lock();
-  }
-
-  // sygus core connective requires unsat cores
-  if (options::sygusCoreConnective())
-  {
-    options::unsatCores.set(true);
-  }
-
-  if ((options::checkModels() || options::checkSynthSol()
-       || options::produceAbducts()
-       || options::modelCoresMode() != options::ModelCoresMode::NONE
-       || options::blockModelsMode() != options::BlockModelsMode::NONE)
-      && !options::produceAssertions())
-  {
-    Notice() << "SmtEngine: turning on produce-assertions to support "
-             << "option requiring assertions." << endl;
-    setOption("produce-assertions", SExpr("true"));
-  }
-
-  // Disable options incompatible with incremental solving, unsat cores, and
-  // proofs or output an error if enabled explicitly
-  if (options::incrementalSolving() || options::unsatCores()
-      || options::proof())
-  {
-    if (options::unconstrainedSimp())
-    {
-      if (options::unconstrainedSimp.wasSetByUser())
-      {
-        throw OptionException(
-            "unconstrained simplification not supported with unsat "
-            "cores/proofs/incremental solving");
-      }
-      Notice() << "SmtEngine: turning off unconstrained simplification to "
-                  "support unsat cores/proofs/incremental solving"
-               << endl;
-      options::unconstrainedSimp.set(false);
-    }
-  }
-  else
-  {
-    // Turn on unconstrained simplification for QF_AUFBV
-    if (!options::unconstrainedSimp.wasSetByUser())
-    {
-      //    bool qf_sat = d_logic.isPure(THEORY_BOOL) &&
-      //    !d_logic.isQuantified(); bool uncSimp = false && !qf_sat &&
-      //    !options::incrementalSolving();
-      bool uncSimp = !d_logic.isQuantified() && !options::produceModels()
-                     && !options::produceAssignments()
-                     && !options::checkModels()
-                     && (d_logic.isTheoryEnabled(THEORY_ARRAYS)
-                         && d_logic.isTheoryEnabled(THEORY_BV));
-      Trace("smt") << "setting unconstrained simplification to " << uncSimp
-                   << endl;
-      options::unconstrainedSimp.set(uncSimp);
-    }
-  }
-
-  if (options::incrementalSolving() || options::proof())
-  {
-    if (options::sygusInference())
-    {
-      if (options::sygusInference.wasSetByUser())
-      {
-        throw OptionException(
-            "sygus inference not supported with proofs/incremental solving");
-      }
-      Notice() << "SmtEngine: turning off sygus inference to support "
-                  "proofs/incremental solving"
-               << std::endl;
-      options::sygusInference.set(false);
-    }
-  }
-
-  // Disable options incompatible with unsat cores and proofs or output an
-  // error if enabled explicitly
-  if (options::unsatCores() || options::proof())
-  {
-    if (options::simplificationMode() != options::SimplificationMode::NONE)
-    {
-      if (options::simplificationMode.wasSetByUser())
-      {
-        throw OptionException(
-            "simplification not supported with unsat cores/proofs");
-      }
-      Notice() << "SmtEngine: turning off simplification to support unsat "
-                  "cores/proofs"
-               << endl;
-      options::simplificationMode.set(options::SimplificationMode::NONE);
-    }
-
-    if (options::pbRewrites())
-    {
-      if (options::pbRewrites.wasSetByUser())
-      {
-        throw OptionException(
-            "pseudoboolean rewrites not supported with unsat cores/proofs");
-      }
-      Notice() << "SmtEngine: turning off pseudoboolean rewrites to support "
-                  "unsat cores/proofs"
-               << endl;
-      setOption("pb-rewrites", false);
-    }
-
-    if (options::sortInference())
-    {
-      if (options::sortInference.wasSetByUser())
-      {
-        throw OptionException(
-            "sort inference not supported with unsat cores/proofs");
-      }
-      Notice() << "SmtEngine: turning off sort inference to support unsat "
-                  "cores/proofs"
-               << endl;
-      options::sortInference.set(false);
-    }
-
-    if (options::preSkolemQuant())
-    {
-      if (options::preSkolemQuant.wasSetByUser())
-      {
-        throw OptionException(
-            "pre-skolemization not supported with unsat cores/proofs");
-      }
-      Notice() << "SmtEngine: turning off pre-skolemization to support unsat "
-                  "cores/proofs"
-               << endl;
-      options::preSkolemQuant.set(false);
-    }
-
-    if (options::solveBVAsInt() > 0)
-    {
-      /**
-       * Operations on 1 bits are better handled as Boolean operations
-       * than as integer operations.
-       * Therefore, we enable bv-to-bool, which runs before
-       * the translation to integers.
-       */
-      options::bitvectorToBool.set(true);
-    }
-
-    if (options::bitvectorToBool())
-    {
-      if (options::bitvectorToBool.wasSetByUser())
-      {
-        throw OptionException(
-            "bv-to-bool not supported with unsat cores/proofs");
-      }
-      Notice() << "SmtEngine: turning off bitvector-to-bool to support unsat "
-                  "cores/proofs"
-               << endl;
-      options::bitvectorToBool.set(false);
-    }
-
-    if (options::boolToBitvector() != options::BoolToBVMode::OFF)
-    {
-      if (options::boolToBitvector.wasSetByUser())
-      {
-        throw OptionException(
-            "bool-to-bv != off not supported with unsat cores/proofs");
-      }
-      Notice() << "SmtEngine: turning off bool-to-bv to support unsat "
-                  "cores/proofs"
-               << endl;
-      setOption("boolToBitvector", SExpr("off"));
-    }
-
-    if (options::bvIntroducePow2())
-    {
-      if (options::bvIntroducePow2.wasSetByUser())
-      {
-        throw OptionException(
-            "bv-intro-pow2 not supported with unsat cores/proofs");
-      }
-      Notice() << "SmtEngine: turning off bv-intro-pow2 to support "
-                  "unsat-cores/proofs"
-               << endl;
-      setOption("bv-intro-pow2", false);
-    }
-
-    if (options::repeatSimp())
-    {
-      if (options::repeatSimp.wasSetByUser())
-      {
-        throw OptionException(
-            "repeat-simp not supported with unsat cores/proofs");
-      }
-      Notice() << "SmtEngine: turning off repeat-simp to support unsat "
-                  "cores/proofs"
-               << endl;
-      setOption("repeat-simp", false);
-    }
-
-    if (options::globalNegate())
-    {
-      if (options::globalNegate.wasSetByUser())
-      {
-        throw OptionException(
-            "global-negate not supported with unsat cores/proofs");
-      }
-      Notice() << "SmtEngine: turning off global-negate to support unsat "
-                  "cores/proofs"
-               << endl;
-      setOption("global-negate", false);
-    }
-
-    if (options::bitvectorAig())
-    {
-      throw OptionException(
-          "bitblast-aig not supported with unsat cores/proofs");
-    }
-  }
-  else
-  {
-    // by default, nonclausal simplification is off for QF_SAT
-    if (!options::simplificationMode.wasSetByUser())
-    {
-      bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified();
-      Trace("smt") << "setting simplification mode to <"
-                   << d_logic.getLogicString() << "> " << (!qf_sat) << endl;
-      // simplification=none works better for SMT LIB benchmarks with
-      // quantifiers, not others options::simplificationMode.set(qf_sat ||
-      // quantifiers ? options::SimplificationMode::NONE :
-      // options::SimplificationMode::BATCH);
-      options::simplificationMode.set(qf_sat
-                                          ? options::SimplificationMode::NONE
-                                          : options::SimplificationMode::BATCH);
-    }
-  }
-
-  if (options::cbqiBv() && d_logic.isQuantified())
-  {
-    if (options::boolToBitvector() != options::BoolToBVMode::OFF)
-    {
-      if (options::boolToBitvector.wasSetByUser())
-      {
-        throw OptionException(
-            "bool-to-bv != off not supported with CBQI BV for quantified "
-            "logics");
-      }
-      Notice() << "SmtEngine: turning off bool-to-bitvector to support CBQI BV"
-               << endl;
-      setOption("boolToBitvector", SExpr("off"));
-    }
-  }
-
-  // cases where we need produce models
-  if (!options::produceModels()
-      && (options::produceAssignments() || options::sygusRewSynthCheck()
-          || is_sygus))
-  {
-    Notice() << "SmtEngine: turning on produce-models" << endl;
-    setOption("produce-models", SExpr("true"));
-  }
-
-  // Set the options for the theoryOf
-  if(!options::theoryOfMode.wasSetByUser()) {
-    if(d_logic.isSharingEnabled() &&
-       !d_logic.isTheoryEnabled(THEORY_BV) &&
-       !d_logic.isTheoryEnabled(THEORY_STRINGS) &&
-       !d_logic.isTheoryEnabled(THEORY_SETS) ) {
-      Trace("smt") << "setting theoryof-mode to term-based" << endl;
-      options::theoryOfMode.set(options::TheoryOfMode::THEORY_OF_TERM_BASED);
-    }
-  }
-
-  // strings require LIA, UF; widen the logic
-  if(d_logic.isTheoryEnabled(THEORY_STRINGS)) {
-    LogicInfo log(d_logic.getUnlockedCopy());
-    // Strings requires arith for length constraints, and also UF
-    if(!d_logic.isTheoryEnabled(THEORY_UF)) {
-      Trace("smt") << "because strings are enabled, also enabling UF" << endl;
-      log.enableTheory(THEORY_UF);
-    }
-    if(!d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isDifferenceLogic() || !d_logic.areIntegersUsed()) {
-      Trace("smt") << "because strings are enabled, also enabling linear integer arithmetic" << endl;
-      log.enableTheory(THEORY_ARITH);
-      log.enableIntegers();
-      log.arithOnlyLinear();
-    }
-    d_logic = log;
-    d_logic.lock();
-  }
-  if(d_logic.isTheoryEnabled(THEORY_ARRAYS) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_SETS)) {
-    if(!d_logic.isTheoryEnabled(THEORY_UF)) {
-      LogicInfo log(d_logic.getUnlockedCopy());
-      Trace("smt") << "because a theory that permits Boolean terms is enabled, also enabling UF" << endl;
-      log.enableTheory(THEORY_UF);
-      d_logic = log;
-      d_logic.lock();
-    }
-  }
-
-  // by default, symmetry breaker is on only for non-incremental QF_UF
-  if(! options::ufSymmetryBreaker.wasSetByUser()) {
-    bool qf_uf_noinc = d_logic.isPure(THEORY_UF) && !d_logic.isQuantified()
-                       && !options::incrementalSolving() && !options::proof()
-                       && !options::unsatCores();
-    Trace("smt") << "setting uf symmetry breaker to " << qf_uf_noinc << endl;
-    options::ufSymmetryBreaker.set(qf_uf_noinc);
-  }
-
-  // If in arrays, set the UF handler to arrays
-  if(d_logic.isTheoryEnabled(THEORY_ARRAYS) && ( !d_logic.isQuantified() ||
-     (d_logic.isQuantified() && !d_logic.isTheoryEnabled(THEORY_UF)))) {
-    Theory::setUninterpretedSortOwner(THEORY_ARRAYS);
-  } else {
-    Theory::setUninterpretedSortOwner(THEORY_UF);
-  }
-
-  if(! options::simplifyWithCareEnabled.wasSetByUser() ){
-    bool qf_aufbv = !d_logic.isQuantified() &&
-      d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
-      d_logic.isTheoryEnabled(THEORY_UF) &&
-      d_logic.isTheoryEnabled(THEORY_BV);
-
-    bool withCare = qf_aufbv;
-    Trace("smt") << "setting ite simplify with care to " << withCare << endl;
-    options::simplifyWithCareEnabled.set(withCare);
-  }
-  // Turn off array eager index splitting for QF_AUFLIA
-  if(! options::arraysEagerIndexSplitting.wasSetByUser()) {
-    if (not d_logic.isQuantified() &&
-        d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
-        d_logic.isTheoryEnabled(THEORY_UF) &&
-        d_logic.isTheoryEnabled(THEORY_ARITH)) {
-      Trace("smt") << "setting array eager index splitting to false" << endl;
-      options::arraysEagerIndexSplitting.set(false);
-    }
-  }
-  // Turn on model-based arrays for QF_AX (unless models are enabled)
-  // if(! options::arraysModelBased.wasSetByUser()) {
-  //   if (not d_logic.isQuantified() &&
-  //       d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
-  //       d_logic.isPure(THEORY_ARRAYS) &&
-  //       !options::produceModels() &&
-  //       !options::checkModels()) {
-  //     Trace("smt") << "turning on model-based array solver" << endl;
-  //     options::arraysModelBased.set(true);
-  //   }
-  // }
-  // Turn on multiple-pass non-clausal simplification for QF_AUFBV
-  if(! options::repeatSimp.wasSetByUser()) {
-    bool repeatSimp = !d_logic.isQuantified() &&
-                      (d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
-                      d_logic.isTheoryEnabled(THEORY_UF) &&
-                      d_logic.isTheoryEnabled(THEORY_BV)) &&
-                      !options::unsatCores();
-    Trace("smt") << "setting repeat simplification to " << repeatSimp << endl;
-    options::repeatSimp.set(repeatSimp);
-  }
-
-  if (options::boolToBitvector() == options::BoolToBVMode::ALL
-      && !d_logic.isTheoryEnabled(THEORY_BV))
-  {
-    if (options::boolToBitvector.wasSetByUser())
-    {
-      throw OptionException(
-          "bool-to-bv=all not supported for non-bitvector logics.");
-    }
-    Notice() << "SmtEngine: turning off bool-to-bv for non-bv logic: "
-             << d_logic.getLogicString() << std::endl;
-    setOption("boolToBitvector", SExpr("off"));
-  }
-
-  if (! options::bvEagerExplanations.wasSetByUser() &&
-      d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
-      d_logic.isTheoryEnabled(THEORY_BV)) {
-    Trace("smt") << "enabling eager bit-vector explanations " << endl;
-    options::bvEagerExplanations.set(true);
-  }
-
-  // Turn on arith rewrite equalities only for pure arithmetic
-  if(! options::arithRewriteEq.wasSetByUser()) {
-    bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isQuantified();
-    Trace("smt") << "setting arith rewrite equalities " << arithRewriteEq << endl;
-    options::arithRewriteEq.set(arithRewriteEq);
-  }
-  if(!  options::arithHeuristicPivots.wasSetByUser()) {
-    int16_t heuristicPivots = 5;
-    if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()) {
-      if(d_logic.isDifferenceLogic()) {
-        heuristicPivots = -1;
-      } else if(!d_logic.areIntegersUsed()) {
-        heuristicPivots = 0;
-      }
-    }
-    Trace("smt") << "setting arithHeuristicPivots  " << heuristicPivots << endl;
-    options::arithHeuristicPivots.set(heuristicPivots);
-  }
-  if(! options::arithPivotThreshold.wasSetByUser()){
-    uint16_t pivotThreshold = 2;
-    if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()){
-      if(d_logic.isDifferenceLogic()){
-        pivotThreshold = 16;
-      }
-    }
-    Trace("smt") << "setting arith arithPivotThreshold  " << pivotThreshold << endl;
-    options::arithPivotThreshold.set(pivotThreshold);
-  }
-  if(! options::arithStandardCheckVarOrderPivots.wasSetByUser()){
-    int16_t varOrderPivots = -1;
-    if(d_logic.isPure(THEORY_ARITH) && !d_logic.isQuantified()){
-      varOrderPivots = 200;
-    }
-    Trace("smt") << "setting arithStandardCheckVarOrderPivots  " << varOrderPivots << endl;
-    options::arithStandardCheckVarOrderPivots.set(varOrderPivots);
-  }
-  // Turn off early theory preprocessing if arithRewriteEq is on
-  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()) {
-    options::DecisionMode decMode =
-        // sygus uses internal
-        is_sygus ? options::DecisionMode::INTERNAL :
-                 // ALL
-            d_logic.hasEverything()
-                ? options::DecisionMode::JUSTIFICATION
-                : (  // QF_BV
-                    (not d_logic.isQuantified() && d_logic.isPure(THEORY_BV)) ||
-                            // QF_AUFBV or QF_ABV or QF_UFBV
-                            (not d_logic.isQuantified()
-                             && (d_logic.isTheoryEnabled(THEORY_ARRAYS)
-                                 || d_logic.isTheoryEnabled(THEORY_UF))
-                             && d_logic.isTheoryEnabled(THEORY_BV))
-                            ||
-                            // QF_AUFLIA (and may be ends up enabling
-                            // QF_AUFLRA?)
-                            (not d_logic.isQuantified()
-                             && d_logic.isTheoryEnabled(THEORY_ARRAYS)
-                             && d_logic.isTheoryEnabled(THEORY_UF)
-                             && d_logic.isTheoryEnabled(THEORY_ARITH))
-                            ||
-                            // QF_LRA
-                            (not d_logic.isQuantified()
-                             && d_logic.isPure(THEORY_ARITH)
-                             && d_logic.isLinear()
-                             && !d_logic.isDifferenceLogic()
-                             && !d_logic.areIntegersUsed())
-                            ||
-                            // Quantifiers
-                            d_logic.isQuantified() ||
-                            // Strings
-                            d_logic.isTheoryEnabled(THEORY_STRINGS)
-                        ? options::DecisionMode::JUSTIFICATION
-                        : options::DecisionMode::INTERNAL);
-
-    bool stoponly =
-      // ALL
-      d_logic.hasEverything() || d_logic.isTheoryEnabled(THEORY_STRINGS) ? false :
-      ( // QF_AUFLIA
-        (not d_logic.isQuantified() &&
-         d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
-         d_logic.isTheoryEnabled(THEORY_UF) &&
-         d_logic.isTheoryEnabled(THEORY_ARITH)
-         ) ||
-        // QF_LRA
-        (not d_logic.isQuantified() &&
-         d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
-         )
-        ? true : false
-      );
-
-    Trace("smt") << "setting decision mode to " << decMode << endl;
-    options::decisionMode.set(decMode);
-    options::decisionStopOnly.set(stoponly);
-  }
-  if( options::incrementalSolving() ){
-    //disable modes not supported by incremental
-    options::sortInference.set( false );
-    options::ufssFairnessMonotone.set( false );
-    options::quantEpr.set( false );
-    options::globalNegate.set(false);
-  }
-  if( d_logic.hasCardinalityConstraints() ){
-    //must have finite model finding on
-    options::finiteModelFind.set( true );
-  }
-
-  //if it contains a theory with non-termination, do not strictly enforce that quantifiers and theory combination must be interleaved
-  if( d_logic.isTheoryEnabled(THEORY_STRINGS) || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) ){
-    if( !options::instWhenStrictInterleave.wasSetByUser() ){
-      options::instWhenStrictInterleave.set( false );
-    }
-  }
-
-  if( options::instMaxLevel()!=-1 ){
-    Notice() << "SmtEngine: turning off cbqi to support instMaxLevel" << endl;
-    options::cbqi.set(false);
-  }
-  // Do we need to track instantiations?
-  // Needed for sygus due to single invocation techniques.
-  if (options::cbqiNestedQE()
-      || (options::proof() && !options::trackInstLemmas.wasSetByUser())
-      || is_sygus)
-  {
-    options::trackInstLemmas.set( true );
-  }
-
-  if( ( options::fmfBoundLazy.wasSetByUser() && options::fmfBoundLazy() ) ||
-      ( options::fmfBoundInt.wasSetByUser() && options::fmfBoundInt() ) ) {
-    options::fmfBound.set( true );
-  }
-  //now have determined whether fmfBoundInt is on/off
-  //apply fmfBoundInt options
-  if( options::fmfBound() ){
-    if (!options::mbqiMode.wasSetByUser()
-        || (options::mbqiMode() != options::MbqiMode::NONE
-            && options::mbqiMode() != options::MbqiMode::FMC))
-    {
-      //if bounded integers are set, use no MBQI by default
-      options::mbqiMode.set(options::MbqiMode::NONE);
-    }
-    if( ! options::prenexQuant.wasSetByUser() ){
-      options::prenexQuant.set(options::PrenexQuantMode::NONE);
-    }
-  }
-  if( options::ufHo() ){
-    //if higher-order, then current variants of model-based instantiation cannot be used
-    if (options::mbqiMode() != options::MbqiMode::NONE)
-    {
-      options::mbqiMode.set(options::MbqiMode::NONE);
-    }
-    if (!options::hoElimStoreAx.wasSetByUser())
-    {
-      // by default, use store axioms only if --ho-elim is set
-      options::hoElimStoreAx.set(options::hoElim());
-    }
-  }
-  if( options::fmfFunWellDefinedRelevant() ){
-    if( !options::fmfFunWellDefined.wasSetByUser() ){
-      options::fmfFunWellDefined.set( true );
-    }
-  }
-  if( options::fmfFunWellDefined() ){
-    if( !options::finiteModelFind.wasSetByUser() ){
-      options::finiteModelFind.set( true );
-    }
-  }
-  //EPR
-  if( options::quantEpr() ){
-    if( !options::preSkolemQuant.wasSetByUser() ){
-      options::preSkolemQuant.set( true );
-    }
-  }
-
-  //now, have determined whether finite model find is on/off
-  //apply finite model finding options
-  if( options::finiteModelFind() ){
-    //apply conservative quantifiers splitting
-    if( !options::quantDynamicSplit.wasSetByUser() ){
-      options::quantDynamicSplit.set(options::QuantDSplitMode::DEFAULT);
-    }
-    //do not eliminate extended arithmetic symbols from quantified formulas
-    if( !options::elimExtArithQuant.wasSetByUser() ){
-      options::elimExtArithQuant.set( false );
-    }
-    if( !options::eMatching.wasSetByUser() ){
-      options::eMatching.set( options::fmfInstEngine() );
-    }
-    if( !options::instWhenMode.wasSetByUser() ){
-      //instantiate only on last call
-      if( options::eMatching() ){
-        options::instWhenMode.set(options::InstWhenMode::LAST_CALL);
-      }
-    }
-  }
-
-  // apply sygus options
-  // if we are attempting to rewrite everything to SyGuS, use sygus()
-  if (is_sygus)
-  {
-    if (!options::sygus())
-    {
-      Trace("smt") << "turning on sygus" << std::endl;
-    }
-    options::sygus.set(true);
-    // must use Ferrante/Rackoff for real arithmetic
-    if (!options::cbqiMidpoint.wasSetByUser())
-    {
-      options::cbqiMidpoint.set(true);
-    }
-    if (options::sygusRepairConst())
-    {
-      if (!options::cbqi.wasSetByUser())
-      {
-        options::cbqi.set(true);
-      }
-    }
-    if (options::sygusInference())
-    {
-      // optimization: apply preskolemization, makes it succeed more often
-      if (!options::preSkolemQuant.wasSetByUser())
-      {
-        options::preSkolemQuant.set(true);
-      }
-      if (!options::preSkolemQuantNested.wasSetByUser())
-      {
-        options::preSkolemQuantNested.set(true);
-      }
-    }
-    //counterexample-guided instantiation for sygus
-    if( !options::cegqiSingleInvMode.wasSetByUser() ){
-      options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::USE);
-    }
-    if( !options::quantConflictFind.wasSetByUser() ){
-      options::quantConflictFind.set( false );
-    }
-    if( !options::instNoEntail.wasSetByUser() ){
-      options::instNoEntail.set( false );
-    }
-    if (!options::cbqiFullEffort.wasSetByUser())
-    {
-      // should use full effort cbqi for single invocation and repair const
-      options::cbqiFullEffort.set(true);
-    }
-    if (options::sygusRew())
-    {
-      options::sygusRewSynth.set(true);
-      options::sygusRewVerify.set(true);
-    }
-    if (options::sygusRewSynthInput())
-    {
-      // If we are using synthesis rewrite rules from input, we use
-      // sygusRewSynth after preprocessing. See passes/synth_rew_rules.h for
-      // details on this technique.
-      options::sygusRewSynth.set(true);
-      // we should not use the extended rewriter, since we are interested
-      // in rewrites that are not in the main rewriter
-      if (!options::sygusExtRew.wasSetByUser())
-      {
-        options::sygusExtRew.set(false);
-      }
-    }
-    // Whether we must use "basic" sygus algorithms. A non-basic sygus algorithm
-    // is one that is specialized for returning a single solution. Non-basic
-    // sygus algorithms currently include the PBE solver, UNIF+PI, static
-    // template inference for invariant synthesis, and single invocation
-    // techniques.
-    bool reqBasicSygus = false;
-    if (options::produceAbducts())
-    {
-      // if doing abduction, we should filter strong solutions
-      if (!options::sygusFilterSolMode.wasSetByUser())
-      {
-        options::sygusFilterSolMode.set(options::SygusFilterSolMode::STRONG);
-      }
-      // we must use basic sygus algorithms, since e.g. we require checking
-      // a sygus side condition for consistency with axioms.
-      reqBasicSygus = true;
-    }
-    if (options::sygusRewSynth() || options::sygusRewVerify()
-        || options::sygusQueryGen())
-    {
-      // rewrite rule synthesis implies that sygus stream must be true
-      options::sygusStream.set(true);
-    }
-    if (options::sygusStream() || options::incrementalSolving())
-    {
-      // Streaming and incremental mode are incompatible with techniques that
-      // focus the search towards finding a single solution.
-      reqBasicSygus = true;
-    }
-    // Now, disable options for non-basic sygus algorithms, if necessary.
-    if (reqBasicSygus)
-    {
-      if (!options::sygusUnifPbe.wasSetByUser())
-      {
-        options::sygusUnifPbe.set(false);
-      }
-      if (options::sygusUnifPi.wasSetByUser())
-      {
-        options::sygusUnifPi.set(options::SygusUnifPiMode::NONE);
-      }
-      if (!options::sygusInvTemplMode.wasSetByUser())
-      {
-        options::sygusInvTemplMode.set(options::SygusInvTemplMode::NONE);
-      }
-      if (!options::cegqiSingleInvMode.wasSetByUser())
-      {
-        options::cegqiSingleInvMode.set(options::CegqiSingleInvMode::NONE);
-      }
-    }
-    //do not allow partial functions
-    if (!options::bitvectorDivByZeroConst())
-    {
-      if (options::bitvectorDivByZeroConst.wasSetByUser())
-      {
-        throw OptionException(
-            "--no-bv-div-zero-const is not supported with SyGuS");
-      }
-      Notice()
-          << "SmtEngine: setting bv-div-zero-const to true to support SyGuS"
-          << std::endl;
-      options::bitvectorDivByZeroConst.set( true );
-    }
-    if( !options::dtRewriteErrorSel.wasSetByUser() ){
-      options::dtRewriteErrorSel.set( true );
-    }
-    //do not miniscope
-    if( !options::miniscopeQuant.wasSetByUser() ){
-      options::miniscopeQuant.set( false );
-    }
-    if( !options::miniscopeQuantFreeVar.wasSetByUser() ){
-      options::miniscopeQuantFreeVar.set( false );
-    }
-    if (!options::quantSplit.wasSetByUser())
-    {
-      options::quantSplit.set(false);
-    }
-    //rewrite divk
-    if( !options::rewriteDivk.wasSetByUser()) {
-      options::rewriteDivk.set( true );
-    }
-    //do not do macros
-    if( !options::macrosQuant.wasSetByUser()) {
-      options::macrosQuant.set( false );
-    }
-    if( !options::cbqiPreRegInst.wasSetByUser()) {
-      options::cbqiPreRegInst.set( true );
-    }
-  }
-  //counterexample-guided instantiation for non-sygus
-  // enable if any possible quantifiers with arithmetic, datatypes or bitvectors
-  if ((d_logic.isQuantified()
-       && (d_logic.isTheoryEnabled(THEORY_ARITH)
-           || d_logic.isTheoryEnabled(THEORY_DATATYPES)
-           || d_logic.isTheoryEnabled(THEORY_BV)
-           || d_logic.isTheoryEnabled(THEORY_FP)))
-      || options::cbqiAll())
-  {
-    if( !options::cbqi.wasSetByUser() ){
-      options::cbqi.set( true );
-    }
-    // check whether we should apply full cbqi
-    if (d_logic.isPure(THEORY_BV))
-    {
-      if (!options::cbqiFullEffort.wasSetByUser())
-      {
-        options::cbqiFullEffort.set(true);
-      }
-    }
-  }
-  if( options::cbqi() ){
-    //must rewrite divk
-    if( !options::rewriteDivk.wasSetByUser()) {
-      options::rewriteDivk.set( true );
-    }
-    if (options::incrementalSolving())
-    {
-      // cannot do nested quantifier elimination in incremental mode
-      options::cbqiNestedQE.set(false);
-    }
-    if (d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV))
-    {
-      if( !options::quantConflictFind.wasSetByUser() ){
-        options::quantConflictFind.set( false );
-      }
-      if( !options::instNoEntail.wasSetByUser() ){
-        options::instNoEntail.set( false );
-      }
-      if( !options::instWhenMode.wasSetByUser() && options::cbqiModel() ){
-        //only instantiation should happen at last call when model is avaiable
-        options::instWhenMode.set(options::InstWhenMode::LAST_CALL);
-      }
-    }else{
-      // only supported in pure arithmetic or pure BV
-      options::cbqiNestedQE.set(false);
-    }
-    // prenexing
-    if (options::cbqiNestedQE())
-    {
-      // only complete with prenex = disj_normal or normal
-      if (options::prenexQuant() <= options::PrenexQuantMode::DISJ_NORMAL)
-      {
-        options::prenexQuant.set(options::PrenexQuantMode::DISJ_NORMAL);
-      }
-    }
-    else if (options::globalNegate())
-    {
-      if (!options::prenexQuant.wasSetByUser())
-      {
-        options::prenexQuant.set(options::PrenexQuantMode::NONE);
-      }
-    }
-  }
-  //implied options...
-  if( options::strictTriggers() ){
-    if( !options::userPatternsQuant.wasSetByUser() ){
-      options::userPatternsQuant.set(options::UserPatMode::TRUST);
-    }
-  }
-  if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
-    options::quantConflictFind.set( true );
-  }
-  if( options::cbqiNestedQE() ){
-    options::prenexQuantUser.set( true );
-    if( !options::preSkolemQuant.wasSetByUser() ){
-      options::preSkolemQuant.set( true );
-    }
-  }
-  //for induction techniques
-  if( options::quantInduction() ){
-    if( !options::dtStcInduction.wasSetByUser() ){
-      options::dtStcInduction.set( true );
-    }
-    if( !options::intWfInduction.wasSetByUser() ){
-      options::intWfInduction.set( true );
-    }
-  }
-  if( options::dtStcInduction() ){
-    //try to remove ITEs from quantified formulas
-    if( !options::iteDtTesterSplitQuant.wasSetByUser() ){
-      options::iteDtTesterSplitQuant.set( true );
-    }
-    if( !options::iteLiftQuant.wasSetByUser() ){
-      options::iteLiftQuant.set(options::IteLiftQuantMode::ALL);
-    }
-  }
-  if( options::intWfInduction() ){
-    if( !options::purifyTriggers.wasSetByUser() ){
-      options::purifyTriggers.set( true );
-    }
-  }
-  if( options::conjectureNoFilter() ){
-    if( !options::conjectureFilterActiveTerms.wasSetByUser() ){
-      options::conjectureFilterActiveTerms.set( false );
-    }
-    if( !options::conjectureFilterCanonical.wasSetByUser() ){
-      options::conjectureFilterCanonical.set( false );
-    }
-    if( !options::conjectureFilterModel.wasSetByUser() ){
-      options::conjectureFilterModel.set( false );
-    }
-  }
-  if( options::conjectureGenPerRound.wasSetByUser() ){
-    if( options::conjectureGenPerRound()>0 ){
-      options::conjectureGen.set( true );
-    }else{
-      options::conjectureGen.set( false );
-    }
-  }
-  //can't pre-skolemize nested quantifiers without UF theory
-  if( !d_logic.isTheoryEnabled(THEORY_UF) && options::preSkolemQuant() ){
-    if( !options::preSkolemQuantNested.wasSetByUser() ){
-      options::preSkolemQuantNested.set( false );
-    }
-  }
-  if( !d_logic.isTheoryEnabled(THEORY_DATATYPES) ){
-    options::quantDynamicSplit.set(options::QuantDSplitMode::NONE);
-  }
-
-  //until bugs 371,431 are fixed
-  if( ! options::minisatUseElim.wasSetByUser()){
-    // cannot use minisat elimination for logics where a theory solver
-    // introduces new literals into the search. This includes quantifiers
-    // (quantifier instantiation), and the lemma schemas used in non-linear
-    // and sets. We also can't use it if models are enabled.
-    if (d_logic.isTheoryEnabled(THEORY_SETS) || d_logic.isQuantified()
-        || options::produceModels() || options::produceAssignments()
-        || options::checkModels()
-        || (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()))
-    {
-      options::minisatUseElim.set( false );
-    }
-  }
-
-  // For now, these array theory optimizations do not support model-building
-  if (options::produceModels() || options::produceAssignments() || options::checkModels()) {
-    options::arraysOptimizeLinear.set(false);
-    options::arraysLazyRIntro1.set(false);
-  }
-
-  if (options::proof())
-  {
-    if (options::incrementalSolving())
-    {
-      if (options::incrementalSolving.wasSetByUser())
-      {
-        throw OptionException("--incremental is not supported with proofs");
-      }
-      Warning()
-          << "SmtEngine: turning off incremental solving mode (not yet "
-             "supported with --proof, try --tear-down-incremental instead)"
-          << endl;
-      setOption("incremental", SExpr("false"));
-    }
-    if (d_logic > LogicInfo("QF_AUFBVLRA"))
-    {
-      throw OptionException(
-          "Proofs are only supported for sub-logics of QF_AUFBVLIA.");
-    }
-    if (options::bitvectorAlgebraicSolver())
-    {
-      if (options::bitvectorAlgebraicSolver.wasSetByUser())
-      {
-        throw OptionException(
-            "--bv-algebraic-solver is not supported with proofs");
-      }
-      Notice() << "SmtEngine: turning off bv algebraic solver to support proofs"
-               << std::endl;
-      options::bitvectorAlgebraicSolver.set(false);
-    }
-    if (options::bitvectorEqualitySolver())
-    {
-      if (options::bitvectorEqualitySolver.wasSetByUser())
-      {
-        throw OptionException("--bv-eq-solver is not supported with proofs");
-      }
-      Notice() << "SmtEngine: turning off bv eq solver to support proofs"
-               << std::endl;
-      options::bitvectorEqualitySolver.set(false);
-    }
-    if (options::bitvectorInequalitySolver())
-    {
-      if (options::bitvectorInequalitySolver.wasSetByUser())
-      {
-        throw OptionException(
-            "--bv-inequality-solver is not supported with proofs");
-      }
-      Notice() << "SmtEngine: turning off bv ineq solver to support proofs"
-               << std::endl;
-      options::bitvectorInequalitySolver.set(false);
-    }
-  }
-
-  if (!options::bitvectorEqualitySolver())
-  {
-    if (options::bvLazyRewriteExtf())
-    {
-      if (options::bvLazyRewriteExtf.wasSetByUser())
-      {
-        throw OptionException(
-            "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set");
-      }
-    }
-    Trace("smt")
-        << "disabling bvLazyRewriteExtf since equality solver is disabled"
-        << endl;
-    options::bvLazyRewriteExtf.set(false);
-  }
-
-  if (!options::sygusExprMinerCheckUseExport())
-  {
-    if (options::sygusExprMinerCheckTimeout.wasSetByUser())
-    {
-      throw OptionException(
-          "--sygus-expr-miner-check-timeout=N requires "
-          "--sygus-expr-miner-check-use-export");
-    }
-    if (options::sygusRewSynthInput() || options::produceAbducts())
-    {
-      std::stringstream ss;
-      ss << (options::sygusRewSynthInput() ? "--sygus-rr-synth-input"
-                                           : "--produce-abducts");
-      ss << "requires --sygus-expr-miner-check-use-export";
-      throw OptionException(ss.str());
-    }
-  }
-
-  if (options::stringFMF() && !options::stringProcessLoopMode.wasSetByUser())
-  {
-    Trace("smt") << "settting stringProcessLoopMode to 'simple' since "
-                    "--strings-fmf enabled"
-                 << endl;
-    options::stringProcessLoopMode.set(options::ProcessLoopMode::SIMPLE);
-  }
-
-  // !!! All options that require disabling models go here
-  bool disableModels = false;
-  std::string sOptNoModel;
-  if (options::unconstrainedSimp.wasSetByUser() && options::unconstrainedSimp())
-  {
-    disableModels = true;
-    sOptNoModel = "unconstrained-simp";
-  }
-  else if (options::sortInference())
-  {
-    disableModels = true;
-    sOptNoModel = "sort-inference";
-  }
-  else if (options::minisatUseElim())
-  {
-    disableModels = true;
-    sOptNoModel = "minisat-elimination";
-  }
-  else if (d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()
-           && !options::nlExt())
-  {
-    disableModels = true;
-    sOptNoModel = "nonlinear arithmetic without nl-ext";
-  }
-  else if (options::globalNegate())
-  {
-    disableModels = true;
-    sOptNoModel = "global-negate";
-  }
-  if (disableModels)
-  {
-    if (options::produceModels())
-    {
-      if (options::produceModels.wasSetByUser())
-      {
-        std::stringstream ss;
-        ss << "Cannot use " << sOptNoModel << " with model generation.";
-        throw OptionException(ss.str());
-      }
-      Notice() << "SmtEngine: turning off produce-models to support "
-               << sOptNoModel << endl;
-      setOption("produce-models", SExpr("false"));
-    }
-    if (options::produceAssignments())
-    {
-      if (options::produceAssignments.wasSetByUser())
-      {
-        std::stringstream ss;
-        ss << "Cannot use " << sOptNoModel
-           << " with model generation (produce-assignments).";
-        throw OptionException(ss.str());
-      }
-      Notice() << "SmtEngine: turning off produce-assignments to support "
-               << sOptNoModel << endl;
-      setOption("produce-assignments", SExpr("false"));
-    }
-    if (options::checkModels())
-    {
-      if (options::checkModels.wasSetByUser())
-      {
-        std::stringstream ss;
-        ss << "Cannot use " << sOptNoModel
-           << " with model generation (check-models).";
-        throw OptionException(ss.str());
-      }
-      Notice() << "SmtEngine: turning off check-models to support "
-               << sOptNoModel << endl;
-      setOption("check-models", SExpr("false"));
-    }
-  }
-}
-
 void SmtEngine::setProblemExtended()
 {
   d_smtMode = SMT_MODE_ASSERT;
@@ -2963,7 +1756,8 @@ bool SmtEnginePrivate::simplifyAssertions()
     d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertions.ref());
 
     // Theory preprocessing
-    if (d_smt.d_earlyTheoryPP)
+    bool doEarlyTheoryPp = !options::arithRewriteEq();
+    if (doEarlyTheoryPp)
     {
       d_passes["theory-preprocess"]->apply(&d_assertions);
     }
@@ -5681,6 +4475,9 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value)
 }
 
 void SmtEngine::setIsInternalSubsolver() { d_isInternalSubsolver = true; }
+
+bool SmtEngine::isInternalSubsolver() const { return d_isInternalSubsolver; }
+
 CVC4::SExpr SmtEngine::getOption(const std::string& key) const
 {
   NodeManagerScope nms(d_nodeManager);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index fbd92bcf2..f5abda1b0 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -203,6 +203,8 @@ class CVC4_PUBLIC SmtEngine
    * --sygus-abduct.
    */
   void setIsInternalSubsolver();
+  /** Is this an internal subsolver? */
+  bool isInternalSubsolver() const;
 
   /** set the input name */
   void setFilename(std::string filename);
@@ -939,12 +941,6 @@ class CVC4_PUBLIC SmtEngine
   void finalOptionsAreSet();
 
   /**
-   * Apply heuristics settings and other defaults.  Done once, at
-   * finishInit() time.
-   */
-  void setDefaults();
-
-  /**
    * Sets that the problem has been extended. This sets the smt mode of the
    * solver to SMT_MODE_ASSERT, and clears the list of assumptions from the
    * previous call to checkSatisfiability.
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 4e2a5bba1..bed59baf5 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -3943,15 +3943,38 @@ Node TheoryArithPrivate::branchIntegerVariable(ArithVar x) const {
   TNode var = d_partialModel.asNode(x);
   Integer floor_d = d.floor();
 
-  //Node eq = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::EQUAL, var, mkRationalNode(floor_d+1)));
-  //Node diseq = eq.notNode();
-
-  Node ub = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
-  Node lb = ub.notNode();
-
+  Node lem;
+  NodeManager* nm = NodeManager::currentNM();
+  if (options::brabTest())
+  {
+    Trace("integers") << "branch-round-and-bound enabled" << endl;
+    Integer ceil_d = d.ceiling();
+    Rational f = r - floor_d;
+    // Multiply by -1 to get abs value.
+    Rational c = (r - ceil_d) * (-1); 
+    Integer nearest = (c > f) ? floor_d : ceil_d;
+
+    // Prioritize trying a simple rounding of the real solution first,
+    // it that fails, fall back on original branch and bound strategy.
+    Node ub = Rewriter::rewrite(
+        nm->mkNode(kind::LEQ, var, mkRationalNode(nearest - 1)));
+    Node lb = Rewriter::rewrite(
+        nm->mkNode(kind::GEQ, var, mkRationalNode(nearest + 1)));
+    lem = nm->mkNode(kind::OR, ub, lb);
+    Node eq = Rewriter::rewrite(
+        nm->mkNode(kind::EQUAL, var, mkRationalNode(nearest)));
+    Node literal = d_containing.getValuation().ensureLiteral(eq);
+    d_containing.getOutputChannel().requirePhase(literal, true);
+    lem = nm->mkNode(kind::OR, literal, lem);
+  }
+  else
+  {
+    Node ub =
+        Rewriter::rewrite(nm->mkNode(kind::LEQ, var, mkRationalNode(floor_d)));
+    Node lb = ub.notNode();
+    lem = nm->mkNode(kind::OR, ub, lb);
+  }
 
-  //Node lem = NodeManager::currentNM()->mkNode(kind::OR, eq, diseq);
-  Node lem = NodeManager::currentNM()->mkNode(kind::OR, ub, lb);
   Trace("integers") << "integers: branch & bound: " << lem << endl;
   if(isSatLiteral(lem[0])) {
     Debug("integers") << "    " << lem[0] << " == " << getSatValue(lem[0]) << endl;
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index b827912d5..646f903f5 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -626,8 +626,7 @@ EvalResult Evaluator::evalInternal(
           const String& s = results[currNode[0]].d_str;
           if (s.size() == 1)
           {
-            results[currNode] = EvalResult(
-                Rational(String::convertUnsignedIntToCode(s.getVec()[0])));
+            results[currNode] = EvalResult(Rational(s.getVec()[0]));
           }
           else
           {
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index 58e179fbe..b9b15c6c6 100644
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -27,7 +27,7 @@
 #include "expr/node.h"
 #include "util/bitvector.h"
 #include "util/rational.h"
-#include "util/regexp.h"
+#include "util/string.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 231c81bbf..10c5741fe 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1009,7 +1009,7 @@ bool QuantifiersRewriter::getVarElimLit(Node lit,
     {
       slv = getVarElimLitBv(lit, args, var);
     }
-    else if (tt.isString())
+    else if (tt.isStringLike())
     {
       slv = getVarElimLitString(lit, args, var);
     }
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index d33c72ede..f15b6780c 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -27,6 +27,7 @@
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/strings/word.h"
 
 using namespace CVC4::kind;
 
@@ -405,11 +406,15 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
     ops.push_back(nm->mkConst(true));
     ops.push_back(nm->mkConst(false));
   }
-  else if (type.isString())
+  else if (type.isStringLike())
   {
-    ops.push_back(nm->mkConst(String("")));
-    // dummy character "A"
-    ops.push_back(nm->mkConst(String("A")));
+    ops.push_back(strings::Word::mkEmptyWord(type));
+    if (type.isString())
+    {
+      // Dummy character "A". This is not necessary for sequences which
+      // have the generic constructor seq.unit.
+      ops.push_back(nm->mkConst(String("A")));
+    }
   }
   else if (type.isArray() || type.isSet())
   {
@@ -449,7 +454,7 @@ void CegGrammarConstructor::collectSygusGrammarTypesFor(
       {
         collectSygusGrammarTypesFor(range.getSetElementType(), types);
       }
-      else if (range.isString() )
+      else if (range.isStringLike())
       {
         // theory of strings shares the integer type
         TypeNode intType = NodeManager::currentNM()->integerType();
diff --git a/src/theory/quantifiers/sygus_sampler.cpp b/src/theory/quantifiers/sygus_sampler.cpp
index 28cfa69df..e9c858814 100644
--- a/src/theory/quantifiers/sygus_sampler.cpp
+++ b/src/theory/quantifiers/sygus_sampler.cpp
@@ -560,8 +560,7 @@ Node SygusSampler::getRandomValue(TypeNode tn)
       for (unsigned ch : alphas)
       {
         d_rstring_alphabet.push_back(ch);
-        Trace("sygus-sample-str-alpha")
-            << " \"" << String::convertUnsignedIntToChar(ch) << "\"";
+        Trace("sygus-sample-str-alpha") << " \\u" << ch;
       }
       Trace("sygus-sample-str-alpha") << std::endl;
     }
diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp
index 7f94130f3..cc920f1d7 100644
--- a/src/theory/quantifiers/term_util.cpp
+++ b/src/theory/quantifiers/term_util.cpp
@@ -25,6 +25,7 @@
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers_engine.h"
+#include "theory/strings/word.h"
 #include "theory/theory_engine.h"
 
 using namespace std;
@@ -464,11 +465,11 @@ Node TermUtil::mkTypeValue(TypeNode tn, int val)
       n = NodeManager::currentNM()->mkConst(false);
     }
   }
-  else if (tn.isString())
+  else if (tn.isStringLike())
   {
     if (val == 0)
     {
-      n = NodeManager::currentNM()->mkConst(::CVC4::String(""));
+      n = strings::Word::mkEmptyWord(tn);
     }
   }
   return n;
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index 128893cf0..af0e7cc37 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -35,7 +35,6 @@ BaseSolver::BaseSolver(context::Context* c,
   d_emptyString = NodeManager::currentNM()->mkConst(::CVC4::String(""));
   d_false = NodeManager::currentNM()->mkConst(false);
   d_cardSize = utils::getAlphabetCardinality();
-  d_type = NodeManager::currentNM()->stringType();
 }
 
 BaseSolver::~BaseSolver() {}
@@ -254,7 +253,7 @@ void BaseSolver::checkConstantEquivalenceClasses(TermIndex* ti,
   if (!n.isNull())
   {
     // construct the constant
-    Node c = utils::mkNConcat(vecc, d_type);
+    Node c = utils::mkNConcat(vecc, n.getType());
     if (!d_state.areEqual(n, c))
     {
       if (Trace.isOn("strings-debug"))
diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h
index bf223bc0a..3681b49a4 100644
--- a/src/theory/strings/base_solver.h
+++ b/src/theory/strings/base_solver.h
@@ -191,8 +191,6 @@ class BaseSolver
   std::map<Kind, TermIndex> d_termIndex;
   /** the cardinality of the alphabet */
   uint32_t d_cardSize;
-  /** The string-like type for this base solver */
-  TypeNode d_type;
 }; /* class BaseSolver */
 
 }  // namespace strings
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 556ae28c3..3384499a2 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -37,10 +37,8 @@ d_nf_pairs(c)
   d_zero = NodeManager::currentNM()->mkConst( Rational( 0 ) );
   d_one = NodeManager::currentNM()->mkConst( Rational( 1 ) );
   d_neg_one = NodeManager::currentNM()->mkConst(Rational(-1));
-  d_emptyString = Word::mkEmptyWord(CONST_STRING);
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
-  d_type = NodeManager::currentNM()->stringType();
 }
 
 CoreSolver::~CoreSolver() {
@@ -286,10 +284,11 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
               << "Found endpoint (in a) with non-empty b = " << b
               << ", whose flat form is " << d_flat_form[b] << std::endl;
           // endpoint
+          Node emp = Word::mkEmptyWord(a.getType());
           std::vector<Node> conc_c;
           for (unsigned j = count; j < bsize; j++)
           {
-            conc_c.push_back(b[d_flat_form_index[b][j]].eqNode(d_emptyString));
+            conc_c.push_back(b[d_flat_form_index[b][j]].eqNode(emp));
           }
           Assert(!conc_c.empty());
           conc = utils::mkAnd(conc_c);
@@ -325,10 +324,11 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
               << "Found endpoint in b = " << b << ", whose flat form is "
               << d_flat_form[b] << std::endl;
           // endpoint
+          Node emp = Word::mkEmptyWord(a.getType());
           std::vector<Node> conc_c;
           for (size_t j = count; j < asize; j++)
           {
-            conc_c.push_back(a[d_flat_form_index[a][j]].eqNode(d_emptyString));
+            conc_c.push_back(a[d_flat_form_index[a][j]].eqNode(emp));
           }
           Assert(!conc_c.empty());
           conc = utils::mkAnd(conc_c);
@@ -438,11 +438,12 @@ void CoreSolver::checkFlatForm(std::vector<Node>& eqc,
         }
         ssize_t startj = isRev ? jj + 1 : 0;
         ssize_t endj = isRev ? c.getNumChildren() : jj;
+        Node emp = Word::mkEmptyWord(a.getType());
         for (ssize_t j = startj; j < endj; j++)
         {
-          if (d_state.areEqual(c[j], d_emptyString))
+          if (d_state.areEqual(c[j], emp))
           {
-            d_im.addToExplanation(c[j], d_emptyString, exp);
+            d_im.addToExplanation(c[j], emp, exp);
           }
         }
       }
@@ -470,6 +471,7 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector<
     return eqc;
   }else if( std::find( d_strings_eqc.begin(), d_strings_eqc.end(), eqc )==d_strings_eqc.end() ){
     curr.push_back( eqc );
+    Node emp = Word::mkEmptyWord(eqc.getType());
     //look at all terms in this equivalence class
     eq::EqualityEngine* ee = d_state.getEqualityEngine();
     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, ee );
@@ -478,22 +480,25 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector<
       if( !d_bsolver.isCongruent(n) ){
         if( n.getKind() == kind::STRING_CONCAT ){
           Trace("strings-cycle") << eqc << " check term : " << n << " in " << eqc << std::endl;
-          if( eqc!=d_emptyString ){
+          if (eqc != emp)
+          {
             d_eqc[eqc].push_back( n );
           }
           for( unsigned i=0; i<n.getNumChildren(); i++ ){
             Node nr = d_state.getRepresentative(n[i]);
-            if( eqc==d_emptyString ){
+            if (eqc == emp)
+            {
               //for empty eqc, ensure all components are empty
-              if( nr!=d_emptyString ){
+              if (nr != emp)
+              {
                 std::vector<Node> exps;
-                exps.push_back(n.eqNode(d_emptyString));
-                d_im.sendInference(
-                    exps, n[i].eqNode(d_emptyString), "I_CYCLE_E");
+                exps.push_back(n.eqNode(emp));
+                d_im.sendInference(exps, n[i].eqNode(emp), "I_CYCLE_E");
                 return Node::null();
               }
             }else{
-              if( nr!=d_emptyString ){
+              if (nr != emp)
+              {
                 d_flat_form[n].push_back( nr );
                 d_flat_form_index[n].push_back( i );
               }
@@ -507,10 +512,9 @@ Node CoreSolver::checkCycles( Node eqc, std::vector< Node >& curr, std::vector<
                   //can infer all other components must be empty
                   for( unsigned j=0; j<n.getNumChildren(); j++ ){
                     //take first non-empty
-                    if (j != i && !d_state.areEqual(n[j], d_emptyString))
+                    if (j != i && !d_state.areEqual(n[j], emp))
                     {
-                      d_im.sendInference(
-                          exp, n[j].eqNode(d_emptyString), "I_CYCLE");
+                      d_im.sendInference(exp, n[j].eqNode(emp), "I_CYCLE");
                       return Node::null();
                     }
                   }
@@ -551,16 +555,17 @@ void CoreSolver::checkNormalFormsEq()
   std::map<Node, Node> eqc_to_exp;
   for (const Node& eqc : d_strings_eqc)
   {
+    TypeNode stype = eqc.getType();
     Trace("strings-process-debug") << "- Verify normal forms are the same for "
                                    << eqc << std::endl;
-    normalizeEquivalenceClass(eqc);
+    normalizeEquivalenceClass(eqc, stype);
     Trace("strings-debug") << "Finished normalizing eqc..." << std::endl;
     if (d_im.hasProcessed())
     {
       return;
     }
     NormalForm& nfe = getNormalForm(eqc);
-    Node nf_term = utils::mkNConcat(nfe.d_nf, d_type);
+    Node nf_term = utils::mkNConcat(nfe.d_nf, stype);
     std::map<Node, Node>::iterator itn = nf_to_eqc.find(nf_term);
     if (itn != nf_to_eqc.end())
     {
@@ -602,21 +607,23 @@ void CoreSolver::checkNormalFormsEq()
 }
 
 //compute d_normal_forms_(base,exp,exp_depend)[eqc]
-void CoreSolver::normalizeEquivalenceClass( Node eqc ) {
+void CoreSolver::normalizeEquivalenceClass(Node eqc, TypeNode stype)
+{
   Trace("strings-process-debug") << "Process equivalence class " << eqc << std::endl;
-  if (d_state.areEqual(eqc, d_emptyString))
+  Node emp = Word::mkEmptyWord(stype);
+  if (d_state.areEqual(eqc, emp))
   {
 #ifdef CVC4_ASSERTIONS
     for( unsigned j=0; j<d_eqc[eqc].size(); j++ ){
       Node n = d_eqc[eqc][j];
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        Assert(d_state.areEqual(n[i], d_emptyString));
+        Assert(d_state.areEqual(n[i], emp));
       }
     }
 #endif
     //do nothing
     Trace("strings-process-debug") << "Return process equivalence class " << eqc << " : empty." << std::endl;
-    d_normal_form[eqc].init(d_emptyString);
+    d_normal_form[eqc].init(emp);
   }
   else
   {
@@ -627,13 +634,13 @@ void CoreSolver::normalizeEquivalenceClass( Node eqc ) {
     // map each term to its index in the above vector
     std::map<Node, unsigned> term_to_nf_index;
     // get the normal forms
-    getNormalForms(eqc, normal_forms, term_to_nf_index);
+    getNormalForms(eqc, normal_forms, term_to_nf_index, stype);
     if (d_im.hasProcessed())
     {
       return;
     }
     // process the normal forms
-    processNEqc(normal_forms);
+    processNEqc(normal_forms, stype);
     if (d_im.hasProcessed())
     {
       return;
@@ -679,11 +686,12 @@ Node CoreSolver::getNormalString(Node x, std::vector<Node>& nf_exp)
   if (!x.isConst())
   {
     Node xr = d_state.getRepresentative(x);
+    TypeNode stype = xr.getType();
     std::map<Node, NormalForm>::iterator it = d_normal_form.find(xr);
     if (it != d_normal_form.end())
     {
       NormalForm& nf = it->second;
-      Node ret = utils::mkNConcat(nf.d_nf, d_type);
+      Node ret = utils::mkNConcat(nf.d_nf, stype);
       nf_exp.insert(nf_exp.end(), nf.d_exp.begin(), nf.d_exp.end());
       d_im.addToExplanation(x, nf.d_base, nf_exp);
       Trace("strings-debug")
@@ -701,16 +709,18 @@ Node CoreSolver::getNormalString(Node x, std::vector<Node>& nf_exp)
         Node nc = getNormalString(x[i], nf_exp);
         vec_nodes.push_back(nc);
       }
-      return utils::mkNConcat(vec_nodes, d_type);
+      return utils::mkNConcat(vec_nodes, stype);
     }
   }
   return x;
 }
 
 void CoreSolver::getNormalForms(Node eqc,
-                                   std::vector<NormalForm>& normal_forms,
-                                   std::map<Node, unsigned>& term_to_nf_index)
+                                std::vector<NormalForm>& normal_forms,
+                                std::map<Node, unsigned>& term_to_nf_index,
+                                TypeNode stype)
 {
+  Node emp = Word::mkEmptyWord(stype);
   //constant for equivalence class
   Node eqc_non_c = eqc;
   Trace("strings-process-debug") << "Get normal forms " << eqc << std::endl;
@@ -719,11 +729,11 @@ void CoreSolver::getNormalForms(Node eqc,
   while( !eqc_i.isFinished() ){
     Node n = (*eqc_i);
     if( !d_bsolver.isCongruent(n) ){
-      if (n.getKind() == CONST_STRING || n.getKind() == STRING_CONCAT)
+      if (n.isConst() || n.getKind() == STRING_CONCAT)
       {
         Trace("strings-process-debug") << "Get Normal Form : Process term " << n << " in eqc " << eqc << std::endl;
         NormalForm nf_curr;
-        if (n.getKind() == CONST_STRING)
+        if (n.isConst())
         {
           nf_curr.init(n);
         }
@@ -803,8 +813,7 @@ void CoreSolver::getNormalForms(Node eqc,
         }
         //if not equal to self
         std::vector<Node>& currv = nf_curr.d_nf;
-        if (currv.size() > 1
-            || (currv.size() == 1 && currv[0].getKind() == CONST_STRING))
+        if (currv.size() > 1 || (currv.size() == 1 && currv[0].isConst()))
         {
           // if in a build with assertions, check that normal form is acyclic
           if (Configuration::isAssertionBuild())
@@ -827,7 +836,7 @@ void CoreSolver::getNormalForms(Node eqc,
           normal_forms.push_back(nf_curr);
         }else{
           //this was redundant: combination of self + empty string(s)
-          Node nn = currv.size() == 0 ? d_emptyString : currv[0];
+          Node nn = currv.size() == 0 ? emp : currv[0];
           Assert(d_state.areEqual(nn, eqc));
         }
       }else{
@@ -926,7 +935,8 @@ void CoreSolver::getNormalForms(Node eqc,
   }
 }
 
-void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms)
+void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms,
+                             TypeNode stype)
 {
   //the possible inferences
   std::vector< InferInfo > pinfer;
@@ -946,7 +956,7 @@ void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms)
         unsigned rindex = 0;
         nfi.reverse();
         nfj.reverse();
-        processSimpleNEq(nfi, nfj, rindex, true, 0, pinfer);
+        processSimpleNEq(nfi, nfj, rindex, true, 0, pinfer, stype);
         nfi.reverse();
         nfj.reverse();
         if (d_im.hasProcessed())
@@ -957,7 +967,7 @@ void CoreSolver::processNEqc(std::vector<NormalForm>& normal_forms)
         //rindex = 0;
 
         unsigned index = 0;
-        processSimpleNEq(nfi, nfj, index, false, rindex, pinfer);
+        processSimpleNEq(nfi, nfj, index, false, rindex, pinfer, stype);
         if (d_im.hasProcessed())
         {
           return;
@@ -1001,10 +1011,12 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
                                   unsigned& index,
                                   bool isRev,
                                   unsigned rproc,
-                                  std::vector<InferInfo>& pinfer)
+                                  std::vector<InferInfo>& pinfer,
+                                  TypeNode stype)
 {
   NodeManager* nm = NodeManager::currentNM();
   eq::EqualityEngine* ee = d_state.getEqualityEngine();
+  Node emp = Word::mkEmptyWord(stype);
 
   const std::vector<Node>& nfiv = nfi.d_nf;
   const std::vector<Node>& nfjv = nfj.d_nf;
@@ -1029,8 +1041,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       while (!d_state.isInConflict() && index_k < (nfkv.size() - rproc))
       {
         // can infer that this string must be empty
-        Node eq = nfkv[index_k].eqNode(d_emptyString);
-        Assert(!d_state.areEqual(d_emptyString, nfkv[index_k]));
+        Node eq = nfkv[index_k].eqNode(emp);
+        Assert(!d_state.areEqual(emp, nfkv[index_k]));
         d_im.sendInference(curr_exp, eq, Inference::N_ENDPOINT_EMP);
         index_k++;
       }
@@ -1082,9 +1094,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       d_im.sendInference(lenExp, eq, Inference::N_UNIFY);
       break;
     }
-    else if ((x.getKind() != CONST_STRING && index == nfiv.size() - rproc - 1)
-             || (y.getKind() != CONST_STRING
-                 && index == nfjv.size() - rproc - 1))
+    else if ((!x.isConst() && index == nfiv.size() - rproc - 1)
+             || (!y.isConst() && index == nfjv.size() - rproc - 1))
     {
       // We have reached the last component in one of the normal forms and it
       // is not a constant. Thus, the last component must be equal to the
@@ -1110,7 +1121,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
             eqnc.push_back(nfkv[i]);
           }
         }
-        eqn[r] = utils::mkNConcat(eqnc, d_type);
+        eqn[r] = utils::mkNConcat(eqnc, stype);
       }
       if (!d_state.areEqual(eqn[0], eqn[1]))
       {
@@ -1253,15 +1264,15 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       NormalForm& nfnc = x.isConst() ? nfj : nfi;
       const std::vector<Node>& nfncv = nfnc.d_nf;
       Node nc = nfncv[index];
-      Assert(nc.getKind() != CONST_STRING) << "Other string is not constant.";
+      Assert(!nc.isConst()) << "Other string is not constant.";
       Assert(nc.getKind() != STRING_CONCAT) << "Other string is not CONCAT.";
-      if (!ee->areDisequal(nc, d_emptyString, true))
+      if (!ee->areDisequal(nc, emp, true))
       {
         // The non-constant side may be equal to the empty string. Split on
         // whether it is.
         //
         // E.g. "abc" ++ ... = nc ++ ... ---> (nc = "") v (nc != "")
-        Node eq = nc.eqNode(d_emptyString);
+        Node eq = nc.eqNode(emp);
         eq = Rewriter::rewrite(eq);
         if (eq.isConst())
         {
@@ -1269,7 +1280,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
           // purify variable for this string to communicate that
           // we have inferred whether it is empty.
           Node p = d_skCache.mkSkolemCached(nc, SkolemCache::SK_PURIFY, "lsym");
-          Node pEq = p.eqNode(d_emptyString);
+          Node pEq = p.eqNode(emp);
           // should not be constant
           Assert(!Rewriter::rewrite(pEq).isConst());
           // infer the purification equality, and the (dis)equality
@@ -1290,7 +1301,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
 
       // At this point, we know that `nc` is non-empty, so we add that to our
       // explanation.
-      Node ncnz = nc.eqNode(d_emptyString).negate();
+      Node ncnz = nc.eqNode(emp).negate();
       info.d_ant.push_back(ncnz);
 
       size_t ncIndex = index + 1;
@@ -1302,19 +1313,19 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         //
         // E.g. "abc" ++ ... = nc ++ "b" ++ ... ---> nc = "a" ++ k
         size_t cIndex = index;
-        Node constStr = nfc.collectConstantStringAt(cIndex);
-        Assert(!constStr.isNull());
-        CVC4::String stra = constStr.getConst<String>();
-        CVC4::String strb = nextConstStr.getConst<String>();
+        Node stra = nfc.collectConstantStringAt(cIndex);
+        size_t straLen = Word::getLength(stra);
+        Assert(!stra.isNull());
+        Node strb = nextConstStr;
         // Since `nc` is non-empty, we start with character 1
         size_t p;
         if (isRev)
         {
-          CVC4::String stra1 = stra.prefix(stra.size() - 1);
-          p = stra.size() - stra1.roverlap(strb);
-          Trace("strings-csp-debug") << "Compute roverlap : " << constStr << " "
-                                     << nextConstStr << std::endl;
-          size_t p2 = stra1.rfind(strb);
+          Node stra1 = Word::prefix(stra, straLen - 1);
+          p = straLen - Word::roverlap(stra1, strb);
+          Trace("strings-csp-debug")
+              << "Compute roverlap : " << stra1 << " " << strb << std::endl;
+          size_t p2 = Word::rfind(stra1, strb);
           p = p2 == std::string::npos ? p : (p > p2 + 1 ? p2 + 1 : p);
           Trace("strings-csp-debug")
               << "roverlap : " << stra1 << " " << strb << " returned " << p
@@ -1322,11 +1333,11 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         }
         else
         {
-          CVC4::String stra1 = stra.substr(1);
-          p = stra.size() - stra1.overlap(strb);
-          Trace("strings-csp-debug") << "Compute overlap : " << constStr << " "
-                                     << nextConstStr << std::endl;
-          size_t p2 = stra1.find(strb);
+          Node stra1 = Word::substr(stra, 1);
+          p = straLen - Word::overlap(stra1, strb);
+          Trace("strings-csp-debug")
+              << "Compute overlap : " << stra1 << " " << strb << std::endl;
+          size_t p2 = Word::find(stra1, strb);
           p = p2 == std::string::npos ? p : (p > p2 + 1 ? p2 + 1 : p);
           Trace("strings-csp-debug")
               << "overlap : " << stra1 << " " << strb << " returned " << p
@@ -1340,9 +1351,9 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         {
           NormalForm::getExplanationForPrefixEq(
               nfc, nfnc, cIndex, ncIndex, info.d_ant);
-          Node prea = p == stra.size() ? constStr
-                                       : nm->mkConst(isRev ? stra.suffix(p)
-                                                           : stra.prefix(p));
+          Node prea = p == straLen ? stra
+                                   : (isRev ? Word::suffix(stra, p)
+                                            : Word::prefix(stra, p));
           Node sk = d_skCache.mkSkolemCached(
               nc,
               prea,
@@ -1364,17 +1375,17 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       // to start with the first character of the constant.
       //
       // E.g. "abc" ++ ... = nc ++ ... ---> nc = "a" ++ k
-      Node constStr = nfcv[index];
-      CVC4::String stra = constStr.getConst<String>();
-      Node firstChar = stra.size() == 1 ? constStr
-                                        : nm->mkConst(isRev ? stra.suffix(1)
-                                                            : stra.prefix(1));
+      Node stra = nfcv[index];
+      size_t straLen = Word::getLength(stra);
+      Node firstChar = straLen == 1 ? stra
+                                    : (isRev ? Word::suffix(stra, 1)
+                                             : Word::prefix(stra, 1));
       Node sk = d_skCache.mkSkolemCached(
           nc,
           isRev ? SkolemCache::SK_ID_VC_SPT_REV : SkolemCache::SK_ID_VC_SPT,
           "c_spt");
       Trace("strings-csp") << "Const Split: " << firstChar
-                           << " is removed from " << constStr << " (serial) "
+                           << " is removed from " << stra << " (serial) "
                            << std::endl;
       NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, info.d_ant);
       info.d_conc = nc.eqNode(isRev ? utils::mkNConcat(sk, firstChar)
@@ -1391,8 +1402,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     //
     // E.g. x ++ ... = y ++ ... ---> (x = y ++ k) v (y = x ++ k)
     Assert(d_state.areDisequal(xLenTerm, yLenTerm));
-    Assert(x.getKind() != CONST_STRING);
-    Assert(y.getKind() != CONST_STRING);
+    Assert(!x.isConst());
+    Assert(!y.isConst());
 
     int32_t lentTestSuccess = -1;
     Node lentTestExp;
@@ -1404,7 +1415,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       {
         Node t = e == 0 ? x : y;
         // do not infer constants are larger than variables
-        if (t.getKind() != CONST_STRING)
+        if (!t.isConst())
         {
           Node lt1 = e == 0 ? xLenTerm : yLenTerm;
           Node lt2 = e == 0 ? yLenTerm : xLenTerm;
@@ -1431,8 +1442,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     for (unsigned xory = 0; xory < 2; xory++)
     {
       Node t = xory == 0 ? x : y;
-      Node tnz = x.eqNode(d_emptyString).negate();
-      if (ee->areDisequal(x, d_emptyString, true))
+      Node tnz = x.eqNode(emp).negate();
+      if (ee->areDisequal(x, emp, true))
       {
         info.d_ant.push_back(tnz);
       }
@@ -1529,23 +1540,27 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
   const std::vector<Node>& veci = nfi.d_nf;
   const std::vector<Node>& vecoi = nfj.d_nf;
 
+  TypeNode stype = veci[loop_index].getType();
+
   Trace("strings-loop") << "Detected possible loop for " << veci[loop_index]
                         << std::endl;
   Trace("strings-loop") << " ... (X)= " << vecoi[index] << std::endl;
   Trace("strings-loop") << " ... T(Y.Z)= ";
   std::vector<Node> vec_t(veci.begin() + index, veci.begin() + loop_index);
-  Node t_yz = utils::mkNConcat(vec_t, d_type);
+  Node t_yz = utils::mkNConcat(vec_t, stype);
   Trace("strings-loop") << " (" << t_yz << ")" << std::endl;
   Trace("strings-loop") << " ... S(Z.Y)= ";
   std::vector<Node> vec_s(vecoi.begin() + index + 1, vecoi.end());
-  Node s_zy = utils::mkNConcat(vec_s, d_type);
+  Node s_zy = utils::mkNConcat(vec_s, stype);
   Trace("strings-loop") << s_zy << std::endl;
   Trace("strings-loop") << " ... R= ";
   std::vector<Node> vec_r(veci.begin() + loop_index + 1, veci.end());
-  Node r = utils::mkNConcat(vec_r, d_type);
+  Node r = utils::mkNConcat(vec_r, stype);
   Trace("strings-loop") << r << std::endl;
 
-  if (s_zy.isConst() && r.isConst() && r != d_emptyString)
+  Node emp = Word::mkEmptyWord(stype);
+
+  if (s_zy.isConst() && r.isConst() && r != emp)
   {
     int c;
     bool flag = true;
@@ -1553,8 +1568,8 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
     {
       if (c >= 0)
       {
-        s_zy = nm->mkConst(s_zy.getConst<String>().substr(0, c));
-        r = d_emptyString;
+        s_zy = Word::substr(s_zy, 0, c);
+        r = emp;
         vec_r.clear();
         Trace("strings-loop") << "Strings::Loop: Refactor S(Z.Y)= " << s_zy
                               << ", c=" << c << std::endl;
@@ -1574,12 +1589,12 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
   for (unsigned i = 0; i < 2; i++)
   {
     Node t = i == 0 ? veci[loop_index] : t_yz;
-    split_eq = t.eqNode(d_emptyString);
+    split_eq = t.eqNode(emp);
     Node split_eqr = Rewriter::rewrite(split_eq);
     // the equality could rewrite to false
     if (!split_eqr.isConst())
     {
-      if (!d_state.areDisequal(t, d_emptyString))
+      if (!d_state.areDisequal(t, emp))
       {
         // try to make t equal to empty to avoid loop
         info.d_conc = nm->mkNode(kind::OR, split_eq, split_eq.negate());
@@ -1602,10 +1617,10 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
   info.d_antn.push_back(ant);
 
   Node str_in_re;
-  if (s_zy == t_yz && r == d_emptyString && s_zy.isConst()
+  if (s_zy == t_yz && r == emp && s_zy.isConst()
       && s_zy.getConst<String>().isRepeated())
   {
-    Node rep_c = nm->mkConst(s_zy.getConst<String>().substr(0, 1));
+    Node rep_c = Word::substr(s_zy, 0, 1);
     Trace("strings-loop") << "Special case (X)=" << vecoi[index] << " "
                           << std::endl;
     Trace("strings-loop") << "... (C)=" << rep_c << " " << std::endl;
@@ -1628,13 +1643,13 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
       Node z = Word::substr(t_yz, len, size - len);
       Node restr = s_zy;
       Node cc;
-      if (r != d_emptyString)
+      if (r != emp)
       {
         std::vector<Node> v2(vec_r);
         v2.insert(v2.begin(), y);
         v2.insert(v2.begin(), z);
         restr = utils::mkNConcat(z, y);
-        cc = Rewriter::rewrite(s_zy.eqNode(utils::mkNConcat(v2, d_type)));
+        cc = Rewriter::rewrite(s_zy.eqNode(utils::mkNConcat(v2, stype)));
       }
       else
       {
@@ -1677,16 +1692,16 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
     // right
     Node sk_w = d_skCache.mkSkolem("w_loop");
     Node sk_y = d_skCache.mkSkolem("y_loop");
-    d_im.registerLength(sk_y, LENGTH_GEQ_ONE);
+    d_im.registerTermAtomic(sk_y, LENGTH_GEQ_ONE);
     Node sk_z = d_skCache.mkSkolem("z_loop");
     // t1 * ... * tn = y * z
     Node conc1 = t_yz.eqNode(utils::mkNConcat(sk_y, sk_z));
     // s1 * ... * sk = z * y * r
     vec_r.insert(vec_r.begin(), sk_y);
     vec_r.insert(vec_r.begin(), sk_z);
-    Node conc2 = s_zy.eqNode(utils::mkNConcat(vec_r, d_type));
+    Node conc2 = s_zy.eqNode(utils::mkNConcat(vec_r, stype));
     Node conc3 = vecoi[index].eqNode(utils::mkNConcat(sk_y, sk_w));
-    Node restr = r == d_emptyString ? s_zy : utils::mkNConcat(sk_z, sk_y);
+    Node restr = r == emp ? s_zy : utils::mkNConcat(sk_z, sk_y);
     str_in_re =
         nm->mkNode(kind::STRING_IN_REGEXP,
                    sk_w,
@@ -1698,7 +1713,6 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
     vec_conc.push_back(conc2);
     vec_conc.push_back(conc3);
     vec_conc.push_back(str_in_re);
-    // vec_conc.push_back(sk_y.eqNode(d_emptyString).negate());//by mkskolems
     conc = nm->mkNode(kind::AND, vec_conc);
   }  // normal case
 
@@ -1745,20 +1759,22 @@ void CoreSolver::processDeq( Node ni, Node nj ) {
         Trace("strings-solve-debug")  << "...Processing(DEQ) " << i << " " << j << std::endl;
         if (!d_state.areEqual(i, j))
         {
-          Assert(i.getKind() != kind::CONST_STRING
-                 || j.getKind() != kind::CONST_STRING);
+          Assert(!i.isConst() || !j.isConst());
           std::vector< Node > lexp;
           Node li = d_state.getLength(i, lexp);
           Node lj = d_state.getLength(j, lexp);
           if (d_state.areDisequal(li, lj))
           {
-            if( i.getKind()==kind::CONST_STRING || j.getKind()==kind::CONST_STRING ){
+            if (i.isConst() || j.isConst())
+            {
               //check if empty
-              Node const_k = i.getKind() == kind::CONST_STRING ? i : j;
-              Node nconst_k = i.getKind() == kind::CONST_STRING ? j : i;
-              Node lnck = i.getKind() == kind::CONST_STRING ? lj : li;
-              if( !ee->areDisequal( nconst_k, d_emptyString, true ) ){
-                Node eq = nconst_k.eqNode( d_emptyString );
+              Node const_k = i.isConst() ? i : j;
+              Node nconst_k = i.isConst() ? j : i;
+              Node lnck = i.isConst() ? lj : li;
+              Node emp = Word::mkEmptyWord(nconst_k.getType());
+              if (!ee->areDisequal(nconst_k, emp, true))
+              {
+                Node eq = nconst_k.eqNode(emp);
                 Node conc = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
                 d_im.sendInference(d_emptyVec, conc, "D-DISL-Emp-Split");
                 return;
@@ -1787,7 +1803,7 @@ void CoreSolver::processDeq( Node ni, Node nj ) {
                 {
                   Node sk = d_skCache.mkSkolemCached(
                       nconst_k, SkolemCache::SK_ID_DC_SPT, "dc_spt");
-                  d_im.registerLength(sk, LENGTH_ONE);
+                  d_im.registerTermAtomic(sk, LENGTH_ONE);
                   Node skr =
                       d_skCache.mkSkolemCached(nconst_k,
                                                 SkolemCache::SK_ID_DC_SPT_REM,
@@ -1800,7 +1816,7 @@ void CoreSolver::processDeq( Node ni, Node nj ) {
                       antec.end(), nfni.d_exp.begin(), nfni.d_exp.end());
                   antec.insert(
                       antec.end(), nfnj.d_exp.begin(), nfnj.d_exp.end());
-                  antec.push_back( nconst_k.eqNode( d_emptyString ).negate() );
+                  antec.push_back(nconst_k.eqNode(emp).negate());
                   d_im.sendInference(
                       antec,
                       nm->mkNode(
@@ -1836,9 +1852,7 @@ void CoreSolver::processDeq( Node ni, Node nj ) {
                   i, j, SkolemCache::SK_ID_DEQ_Y, "y_dsplit");
               Node sk3 = d_skCache.mkSkolemCached(
                   i, j, SkolemCache::SK_ID_DEQ_Z, "z_dsplit");
-              d_im.registerLength(sk3, LENGTH_GEQ_ONE);
-              //Node nemp = sk3.eqNode(d_emptyString).negate();
-              //conc.push_back(nemp);
+              d_im.registerTermAtomic(sk3, LENGTH_GEQ_ONE);
               Node lsk1 = utils::mkNLength(sk1);
               conc.push_back( lsk1.eqNode( li ) );
               Node lsk2 = utils::mkNLength(sk2);
@@ -1914,6 +1928,8 @@ int CoreSolver::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >&
       }
     }
   }
+  TypeNode stype = ni.getType();
+  Node emp = Word::mkEmptyWord(stype);
   NormalForm& nfni = getNormalForm(ni);
   NormalForm& nfnj = getNormalForm(nj);
   while( index<nfi.size() || index<nfj.size() ) {
@@ -1929,7 +1945,7 @@ int CoreSolver::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >&
       std::vector< Node > cc;
       std::vector< Node >& nfk = index>=nfi.size() ? nfj : nfi;
       for( unsigned index_k=index; index_k<nfk.size(); index_k++ ){
-        cc.push_back( nfk[index_k].eqNode( d_emptyString ) );
+        cc.push_back(nfk[index_k].eqNode(emp));
       }
       Node conc = cc.size()==1 ? cc[0] : NodeManager::currentNM()->mkNode( kind::AND, cc );
       conc = Rewriter::rewrite( conc );
@@ -1941,11 +1957,13 @@ int CoreSolver::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >&
       Trace("strings-solve-debug")  << "...Processing(QED) " << i << " " << j << std::endl;
       if (!d_state.areEqual(i, j))
       {
-        if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ) {
+        if (i.isConst() && j.isConst())
+        {
           size_t lenI = Word::getLength(i);
           size_t lenJ = Word::getLength(j);
           unsigned int len_short = lenI < lenJ ? lenI : lenJ;
-          bool isSameFix = isRev ? i.getConst<String>().rstrncmp(j.getConst<String>(), len_short): i.getConst<String>().strncmp(j.getConst<String>(), len_short);
+          bool isSameFix = isRev ? Word::rstrncmp(i, j, len_short)
+                                 : Word::strncmp(i, j, len_short);
           if( isSameFix ) {
             //same prefix/suffix
             //k is the index of the string that is shorter
@@ -2125,6 +2143,7 @@ void CoreSolver::checkNormalFormsDeq()
 void CoreSolver::checkLengthsEqc() {
   for (unsigned i = 0; i < d_strings_eqc.size(); i++)
   {
+    TypeNode stype = d_strings_eqc[i].getType();
     NormalForm& nfi = getNormalForm(d_strings_eqc[i]);
     Trace("strings-process-debug")
         << "Process length constraints for " << d_strings_eqc[i] << std::endl;
@@ -2141,7 +2160,7 @@ void CoreSolver::checkLengthsEqc() {
     // now, check if length normalization has occurred
     if (ei->d_normalizedLength.get().isNull())
     {
-      Node nf = utils::mkNConcat(nfi.d_nf, d_type);
+      Node nf = utils::mkNConcat(nfi.d_nf, stype);
       if (Trace.isOn("strings-process-debug"))
       {
         Trace("strings-process-debug")
@@ -2190,7 +2209,7 @@ void CoreSolver::doInferInfo(const InferInfo& ii)
   {
     for (const Node& n : sks.second)
     {
-      d_im.registerLength(n, sks.first);
+      d_im.registerTermAtomic(n, sks.first);
     }
   }
 }
diff --git a/src/theory/strings/core_solver.h b/src/theory/strings/core_solver.h
index c549fa886..3fea5e8de 100644
--- a/src/theory/strings/core_solver.h
+++ b/src/theory/strings/core_solver.h
@@ -218,16 +218,21 @@ class CoreSolver
    * current normal form for each term in this equivalence class is identical.
    * If it is not, then we add an inference via sendInference and abort the
    * call.
+   *
+   * stype is the string-like type of the equivalence class we are processing.
    */
-  void normalizeEquivalenceClass(Node n);
+  void normalizeEquivalenceClass(Node n, TypeNode stype);
   /**
    * For each term in the equivalence class of eqc, this adds data regarding its
    * normal form to normal_forms. The map term_to_nf_index maps terms to the
    * index in normal_forms where their normal form data is located.
+   *
+   * stype is the string-like type of the equivalence class we are processing.
    */
   void getNormalForms(Node eqc,
                       std::vector<NormalForm>& normal_forms,
-                      std::map<Node, unsigned>& term_to_nf_index);
+                      std::map<Node, unsigned>& term_to_nf_index,
+                      TypeNode stype);
   /** process normalize equivalence class
    *
    * This is called when an equivalence class contains a set of terms that
@@ -240,8 +245,10 @@ class CoreSolver
    * corresponding to processing the normal form pair in the (forward, reverse)
    * directions. Once all possible inferences are recorded, it executes the
    * one with highest priority based on the enumeration type Inference.
+   *
+   * stype is the string-like type of the equivalence class we are processing.
    */
-  void processNEqc(std::vector<NormalForm>& normal_forms);
+  void processNEqc(std::vector<NormalForm>& normal_forms, TypeNode stype);
   /** process simple normal equality
    *
    * This method is called when two equal terms have normal forms nfi and nfj.
@@ -265,13 +272,16 @@ class CoreSolver
    *   fowards/backwards traversals of normal forms to ensure that duplicate
    *   inferences are not processed.
    * pinfer: the set of possible inferences we add to.
+   *
+   * stype is the string-like type of the equivalence class we are processing.
    */
   void processSimpleNEq(NormalForm& nfi,
                         NormalForm& nfj,
                         unsigned& index,
                         bool isRev,
                         unsigned rproc,
-                        std::vector<InferInfo>& pinfer);
+                        std::vector<InferInfo>& pinfer,
+                        TypeNode stype);
   //--------------------------end for checkNormalFormsEq
 
   //--------------------------for checkNormalFormsEq with loops
@@ -325,7 +335,6 @@ class CoreSolver
   /** reference to the base solver, used for certain queries */
   BaseSolver& d_bsolver;
   /** Commonly used constants */
-  Node d_emptyString;
   Node d_true;
   Node d_false;
   Node d_zero;
@@ -368,8 +377,6 @@ class CoreSolver
    * the argument number of the t1 ... tn they were generated from.
    */
   std::map<Node, std::vector<int> > d_flat_form_index;
-  /** The string-like type for this solver */
-  TypeNode d_type;
 }; /* class CoreSolver */
 
 }  // namespace strings
diff --git a/src/theory/strings/eqc_info.cpp b/src/theory/strings/eqc_info.cpp
index ab6d473bd..3c0dbc2a7 100644
--- a/src/theory/strings/eqc_info.cpp
+++ b/src/theory/strings/eqc_info.cpp
@@ -15,6 +15,7 @@
 #include "theory/strings/eqc_info.h"
 
 #include "theory/strings/theory_strings_utils.h"
+#include "theory/strings/word.h"
 
 using namespace std;
 using namespace CVC4::context;
@@ -44,13 +45,13 @@ Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
                                        << " post=" << isSuf << std::endl;
     Node prevC = utils::getConstantEndpoint(prev, isSuf);
     Assert(!prevC.isNull());
-    Assert(prevC.getKind() == CONST_STRING);
+    Assert(prevC.isConst());
     if (c.isNull())
     {
       c = utils::getConstantEndpoint(t, isSuf);
       Assert(!c.isNull());
     }
-    Assert(c.getKind() == CONST_STRING);
+    Assert(c.isConst());
     bool conflict = false;
     // if the constant prefixes are different
     if (c != prevC)
@@ -59,10 +60,8 @@ Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
       Assert(!t.isConst() || !prev.isConst());
       Trace("strings-eager-pconf-debug")
           << "Check conflict constants " << prevC << ", " << c << std::endl;
-      const String& ps = prevC.getConst<String>();
-      const String& cs = c.getConst<String>();
-      unsigned pvs = ps.size();
-      unsigned cvs = cs.size();
+      size_t pvs = Word::getLength(prevC);
+      size_t cvs = Word::getLength(c);
       if (pvs == cvs || (pvs > cvs && t.isConst())
           || (cvs > pvs && prev.isConst()))
       {
@@ -73,15 +72,15 @@ Node EqcInfo::addEndpointConst(Node t, Node c, bool isSuf)
       }
       else
       {
-        const String& larges = pvs > cvs ? ps : cs;
-        const String& smalls = pvs > cvs ? cs : ps;
+        Node larges = pvs > cvs ? prevC : c;
+        Node smalls = pvs > cvs ? c : prevC;
         if (isSuf)
         {
-          conflict = !larges.hasSuffix(smalls);
+          conflict = !Word::hasSuffix(larges, smalls);
         }
         else
         {
-          conflict = !larges.hasPrefix(smalls);
+          conflict = !Word::hasPrefix(larges, smalls);
         }
       }
       if (!conflict && (pvs > cvs || prev.isConst()))
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index c586df6dd..47f36af4c 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -34,14 +34,15 @@ ExtfSolver::ExtfSolver(context::Context* c,
                        SkolemCache& skc,
                        BaseSolver& bs,
                        CoreSolver& cs,
-                       ExtTheory* et)
+                       ExtTheory* et,
+                       SequencesStatistics& stats)
     : d_state(s),
       d_im(im),
       d_skCache(skc),
       d_bsolver(bs),
       d_csolver(cs),
       d_extt(et),
-      d_preproc(&skc, u),
+      d_preproc(&skc, u, stats),
       d_hasExtf(c, false),
       d_extfInferCache(c)
 {
@@ -645,7 +646,7 @@ Node ExtfSolver::getCurrentSubstitutionFor(int effort,
   {
     return c;
   }
-  else if (effort >= 1 && n.getType().isString())
+  else if (effort >= 1 && n.getType().isStringLike())
   {
     Assert(effort < 3);
     // normal forms
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h
index 4c848f430..040871ffa 100644
--- a/src/theory/strings/extf_solver.h
+++ b/src/theory/strings/extf_solver.h
@@ -26,6 +26,7 @@
 #include "theory/strings/base_solver.h"
 #include "theory/strings/core_solver.h"
 #include "theory/strings/inference_manager.h"
+#include "theory/strings/sequences_stats.h"
 #include "theory/strings/skolem_cache.h"
 #include "theory/strings/solver_state.h"
 #include "theory/strings/theory_strings_preprocess.h"
@@ -88,7 +89,8 @@ class ExtfSolver
              SkolemCache& skc,
              BaseSolver& bs,
              CoreSolver& cs,
-             ExtTheory* et);
+             ExtTheory* et,
+             SequencesStatistics& stats);
   ~ExtfSolver();
 
   /** check extended functions evaluation
diff --git a/src/theory/strings/infer_info.cpp b/src/theory/strings/infer_info.cpp
index aa7fe8974..cdf764aa8 100644
--- a/src/theory/strings/infer_info.cpp
+++ b/src/theory/strings/infer_info.cpp
@@ -14,30 +14,33 @@
 
 #include "theory/strings/infer_info.h"
 
-using namespace CVC4::kind;
-
 namespace CVC4 {
 namespace theory {
 namespace strings {
 
-std::ostream& operator<<(std::ostream& out, Inference i)
+const char* toString(Inference i)
 {
   switch (i)
   {
-    case Inference::N_ENDPOINT_EMP: out << "N_EndpointEmp"; break;
-    case Inference::N_UNIFY: out << "N_Unify"; break;
-    case Inference::N_ENDPOINT_EQ: out << "N_EndpointEq"; break;
-    case Inference::N_CONST: out << "N_Const"; break;
-    case Inference::INFER_EMP: out << "Infer-Emp"; break;
-    case Inference::SSPLIT_CST_PROP: out << "S-Split(CST-P)-prop"; break;
-    case Inference::SSPLIT_VAR_PROP: out << "S-Split(VAR)-prop"; break;
-    case Inference::LEN_SPLIT: out << "Len-Split(Len)"; break;
-    case Inference::LEN_SPLIT_EMP: out << "Len-Split(Emp)"; break;
-    case Inference::SSPLIT_CST: out << "S-Split(CST-P)"; break;
-    case Inference::SSPLIT_VAR: out << "S-Split(VAR)"; break;
-    case Inference::FLOOP: out << "F-Loop"; break;
-    default: out << "?"; break;
+    case Inference::N_ENDPOINT_EMP: return "N_EndpointEmp";
+    case Inference::N_UNIFY: return "N_Unify";
+    case Inference::N_ENDPOINT_EQ: return "N_EndpointEq";
+    case Inference::N_CONST: return "N_Const";
+    case Inference::INFER_EMP: return "Infer-Emp";
+    case Inference::SSPLIT_CST_PROP: return "S-Split(CST-P)-prop";
+    case Inference::SSPLIT_VAR_PROP: return "S-Split(VAR)-prop";
+    case Inference::LEN_SPLIT: return "Len-Split(Len)";
+    case Inference::LEN_SPLIT_EMP: return "Len-Split(Emp)";
+    case Inference::SSPLIT_CST: return "S-Split(CST-P)";
+    case Inference::SSPLIT_VAR: return "S-Split(VAR)";
+    case Inference::FLOOP: return "F-Loop";
+    default: return "?";
   }
+}
+
+std::ostream& operator<<(std::ostream& out, Inference i)
+{
+  out << toString(i);
   return out;
 }
 
diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h
index 9d2f71b53..cfabe5c51 100644
--- a/src/theory/strings/infer_info.h
+++ b/src/theory/strings/infer_info.h
@@ -19,7 +19,9 @@
 
 #include <map>
 #include <vector>
+
 #include "expr/node.h"
+#include "util/safe_print.h"
 
 namespace CVC4 {
 namespace theory {
@@ -94,6 +96,25 @@ enum class Inference : uint32_t
   FLOOP,
   NONE,
 };
+
+/**
+ * Converts an inference to a string. Note: This function is also used in
+ * `safe_print()`. Changing this functions name or signature will result in
+ * `safe_print()` printing "<unsupported>" instead of the proper strings for
+ * the enum values.
+ *
+ * @param i The inference
+ * @return The name of the inference
+ */
+const char* toString(Inference i);
+
+/**
+ * Writes an inference name to a stream.
+ *
+ * @param out The stream to write to
+ * @param i The inference to write to the stream
+ * @return The stream
+ */
 std::ostream& operator<<(std::ostream& out, Inference i);
 
 /**
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index eebad2274..cb0c807cc 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -20,6 +20,7 @@
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings.h"
 #include "theory/strings/theory_strings_utils.h"
+#include "theory/strings/word.h"
 
 using namespace std;
 using namespace CVC4::context;
@@ -225,6 +226,7 @@ void InferenceManager::sendLemma(Node ant, Node conc, const char* c)
                            << std::endl;
     Trace("strings-assert")
         << "(assert (not " << ant << ")) ; conflict " << c << std::endl;
+    ++(d_statistics.d_conflictsInfer);
     d_out.conflict(ant);
     d_state.setConflict();
     return;
@@ -368,29 +370,29 @@ Node InferenceManager::getSymbolicDefinition(Node n,
   return NodeManager::currentNM()->mkNode(n.getKind(), children);
 }
 
-void InferenceManager::registerLength(Node n)
+Node InferenceManager::registerTerm(Node n)
 {
+  Assert(n.getType().isStringLike());
   NodeManager* nm = NodeManager::currentNM();
   // register length information:
   //  for variables, split on empty vs positive length
   //  for concat/const/replace, introduce proxy var and state length relation
   Node lsum;
-  if (n.getKind() != STRING_CONCAT && n.getKind() != CONST_STRING)
+  if (n.getKind() != STRING_CONCAT && !n.isConst())
   {
     Node lsumb = nm->mkNode(STRING_LENGTH, n);
     lsum = Rewriter::rewrite(lsumb);
     // can register length term if it does not rewrite
     if (lsum == lsumb)
     {
-      registerLength(n, LENGTH_SPLIT);
-      return;
+      registerTermAtomic(n, LENGTH_SPLIT);
+      return Node::null();
     }
   }
   Node sk = d_skCache.mkSkolemCached(n, SkolemCache::SK_PURIFY, "lsym");
   StringsProxyVarAttribute spva;
   sk.setAttribute(spva, true);
   Node eq = Rewriter::rewrite(sk.eqNode(n));
-  Trace("strings-lemma") << "Strings::Lemma LENGTH Term : " << eq << std::endl;
   d_proxyVar[n] = sk;
   // If we are introducing a proxy for a constant or concat term, we do not
   // need to send lemmas about its length, since its length is already
@@ -398,10 +400,8 @@ void InferenceManager::registerLength(Node n)
   if (n.isConst() || n.getKind() == STRING_CONCAT)
   {
     // do not send length lemma for sk.
-    registerLength(sk, LENGTH_IGNORE);
+    registerTermAtomic(sk, LENGTH_IGNORE);
   }
-  Trace("strings-assert") << "(assert " << eq << ")" << std::endl;
-  d_out.lemma(eq);
   Node skl = nm->mkNode(STRING_LENGTH, sk);
   if (n.getKind() == STRING_CONCAT)
   {
@@ -422,21 +422,18 @@ void InferenceManager::registerLength(Node n)
     lsum = nm->mkNode(PLUS, nodeVec);
     lsum = Rewriter::rewrite(lsum);
   }
-  else if (n.getKind() == CONST_STRING)
+  else if (n.isConst())
   {
-    lsum = nm->mkConst(Rational(n.getConst<String>().size()));
+    lsum = nm->mkConst(Rational(Word::getLength(n)));
   }
   Assert(!lsum.isNull());
   d_proxyVarToLength[sk] = lsum;
   Node ceq = Rewriter::rewrite(skl.eqNode(lsum));
-  Trace("strings-lemma") << "Strings::Lemma LENGTH : " << ceq << std::endl;
-  Trace("strings-lemma-debug")
-      << "  prerewrite : " << skl.eqNode(lsum) << std::endl;
-  Trace("strings-assert") << "(assert " << ceq << ")" << std::endl;
-  d_out.lemma(ceq);
+
+  return nm->mkNode(AND, eq, ceq);
 }
 
-void InferenceManager::registerLength(Node n, LengthStatus s)
+void InferenceManager::registerTermAtomic(Node n, LengthStatus s)
 {
   if (d_lengthLemmaTermsCache.find(n) != d_lengthLemmaTermsCache.end())
   {
@@ -449,7 +446,25 @@ void InferenceManager::registerLength(Node n, LengthStatus s)
     // ignore it
     return;
   }
+  std::map<Node, bool> reqPhase;
+  Node lenLem = getRegisterTermAtomicLemma(n, s, reqPhase);
+  if (!lenLem.isNull())
+  {
+    Trace("strings-lemma") << "Strings::Lemma REGISTER-TERM-ATOMIC : " << lenLem
+                           << std::endl;
+    Trace("strings-assert") << "(assert " << lenLem << ")" << std::endl;
+    ++(d_statistics.d_lemmasRegisterTermAtomic);
+    d_out.lemma(lenLem);
+  }
+  for (const std::pair<const Node, bool>& rp : reqPhase)
+  {
+    d_out.requirePhase(rp.first, rp.second);
+  }
+}
 
+Node InferenceManager::getRegisterTermAtomicLemma(
+    Node n, LengthStatus s, std::map<Node, bool>& reqPhase)
+{
   NodeManager* nm = NodeManager::currentNM();
   Node n_len = nm->mkNode(kind::STRING_LENGTH, n);
 
@@ -461,8 +476,7 @@ void InferenceManager::registerLength(Node n, LengthStatus s)
     Trace("strings-lemma") << "Strings::Lemma SK-GEQ-ONE : " << len_geq_one
                            << std::endl;
     Trace("strings-assert") << "(assert " << len_geq_one << ")" << std::endl;
-    d_out.lemma(len_geq_one);
-    return;
+    return len_geq_one;
   }
 
   if (s == LENGTH_ONE)
@@ -471,11 +485,11 @@ void InferenceManager::registerLength(Node n, LengthStatus s)
     Trace("strings-lemma") << "Strings::Lemma SK-ONE : " << len_one
                            << std::endl;
     Trace("strings-assert") << "(assert " << len_one << ")" << std::endl;
-    d_out.lemma(len_one);
-    return;
+    return len_one;
   }
   Assert(s == LENGTH_SPLIT);
 
+  std::vector<Node> lems;
   if (options::stringSplitEmp() || !options::stringLenGeqZ())
   {
     Node n_len_eq_z = n_len.eqNode(d_zero);
@@ -486,7 +500,7 @@ void InferenceManager::registerLength(Node n, LengthStatus s)
     if (!case_empty.isConst())
     {
       Node lem = nm->mkNode(OR, case_empty, case_nempty);
-      d_out.lemma(lem);
+      lems.push_back(lem);
       Trace("strings-lemma")
           << "Strings::Lemma LENGTH >= 0 : " << lem << std::endl;
       // prefer trying the empty case first
@@ -494,10 +508,10 @@ void InferenceManager::registerLength(Node n, LengthStatus s)
       // occur in the CNF stream.
       n_len_eq_z = Rewriter::rewrite(n_len_eq_z);
       Assert(!n_len_eq_z.isConst());
-      d_out.requirePhase(n_len_eq_z, true);
+      reqPhase[n_len_eq_z] = true;
       n_len_eq_z_2 = Rewriter::rewrite(n_len_eq_z_2);
       Assert(!n_len_eq_z_2.isConst());
-      d_out.requirePhase(n_len_eq_z_2, true);
+      reqPhase[n_len_eq_z_2] = true;
     }
     else if (!case_empty.getConst<bool>())
     {
@@ -505,7 +519,7 @@ void InferenceManager::registerLength(Node n, LengthStatus s)
       Trace("strings-lemma")
           << "Strings::Lemma LENGTH > 0 (non-empty): " << case_nempty
           << std::endl;
-      d_out.lemma(case_nempty);
+      lems.push_back(case_nempty);
     }
     else
     {
@@ -521,8 +535,14 @@ void InferenceManager::registerLength(Node n, LengthStatus s)
   {
     Node n_len_geq = nm->mkNode(kind::GEQ, n_len, d_zero);
     n_len_geq = Rewriter::rewrite(n_len_geq);
-    d_out.lemma(n_len_geq);
+    lems.push_back(n_len_geq);
+  }
+
+  if (lems.empty())
+  {
+    return Node::null();
   }
+  return lems.size() == 1 ? lems[0] : nm->mkNode(AND, lems);
 }
 
 void InferenceManager::addToExplanation(Node a,
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index c9d483c73..bd2f85d29 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -210,18 +210,23 @@ class InferenceManager
    * exists, otherwise it returns null.
    */
   Node getProxyVariableFor(Node n) const;
-  /** register length
+  /** register term
+   *
+   * This method is called on non-constant string terms n. It returns a lemma
+   * that should be sent on the output channel of theory of strings upon
+   * registration of this term, or null if no lemma is necessary.
    *
-   * This method is called on non-constant string terms n. It sends a lemma
-   * on the output channel that ensures that the length n satisfies its assigned
-   * status (given by argument s).
+   * If n is an atomic term, the method registerTermAtomic is called for n
+   * and s = LENGTH_SPLIT and no lemma is returned.
    */
-  void registerLength(Node n);
+  Node registerTerm(Node n);
   /** register length
    *
-   * This method is called on non-constant string terms n. It sends a lemma
-   * on the output channel that ensures that the length n satisfies its assigned
-   * status (given by argument s).
+   * This method is called on non-constant string terms n that are "atomic"
+   * with respect to length. That is, the rewritten form of len(n) is itself.
+   *
+   * It sends a lemma on the output channel that ensures that the length n
+   * satisfies its assigned status (given by argument s).
    *
    * If the status is LENGTH_ONE, we send the lemma len( n ) = 1.
    *
@@ -238,7 +243,7 @@ class InferenceManager
    * In contrast to the above functions, it makes immediate calls to the output
    * channel instead of adding them to pending lists.
    */
-  void registerLength(Node n, LengthStatus s);
+  void registerTermAtomic(Node n, LengthStatus s);
   //---------------------------- end proxy variables and length elaboration
 
   //----------------------------constructing antecedants
@@ -337,6 +342,17 @@ class InferenceManager
    * equality engine of this class.
    */
   void sendInfer(Node eq_exp, Node eq, const char* c);
+  /**
+   * Get the lemma required for registering the length information for
+   * atomic term n given length status s. For details, see registerTermAtomic.
+   *
+   * Additionally, this method may map literals to a required polarity in the
+   * argument reqPhase, which should be processed by a call to requiredPhase by
+   * the caller of this method.
+   */
+  Node getRegisterTermAtomicLemma(Node n,
+                                  LengthStatus s,
+                                  std::map<Node, bool>& reqPhase);
 
   /** the parent theory of strings object */
   TheoryStrings& d_parent;
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index 5b988061b..3f7abdb7c 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -37,15 +37,15 @@ operator STRING_REV 1 "string reverse"
 sort STRING_TYPE \
     Cardinality::INTEGERS \
     well-founded \
-        "NodeManager::currentNM()->mkConst(::CVC4::String())" \
-        "util/regexp.h" \
+    "NodeManager::currentNM()->mkConst(::CVC4::String())" \
+    "util/string.h" \
     "String type"
 
 sort REGEXP_TYPE \
     Cardinality::INTEGERS \
     well-founded \
-        "NodeManager::currentNM()->mkNode(REGEXP_EMPTY, std::vector<Node>() )" \
-        "util/regexp.h" \
+    "NodeManager::currentNM()->mkNode(REGEXP_EMPTY, std::vector<Node>() )" \
+    "util/string.h" \
     "RegExp type"
 
 enumerator STRING_TYPE \
@@ -55,7 +55,7 @@ enumerator STRING_TYPE \
 constant CONST_STRING \
     ::CVC4::String \
     ::CVC4::strings::StringHashFunction \
-    "util/regexp.h" \
+    "util/string.h" \
     "a string of characters"
 
 # equal equal / less than / output
diff --git a/src/theory/strings/normal_form.cpp b/src/theory/strings/normal_form.cpp
index 7a2323d89..05be5f12a 100644
--- a/src/theory/strings/normal_form.cpp
+++ b/src/theory/strings/normal_form.cpp
@@ -18,6 +18,7 @@
 #include "options/strings_options.h"
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
+#include "theory/strings/word.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -28,7 +29,7 @@ namespace strings {
 
 void NormalForm::init(Node base)
 {
-  Assert(base.getType().isString());
+  Assert(base.getType().isStringLike());
   Assert(base.getKind() != STRING_CONCAT);
   d_base = base;
   d_nf.clear();
@@ -37,7 +38,7 @@ void NormalForm::init(Node base)
   d_expDep.clear();
 
   // add to normal form
-  if (!base.isConst() || !base.getConst<String>().isEmptyString())
+  if (!base.isConst() || Word::getLength(base) > 0)
   {
     d_nf.push_back(base);
   }
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index d5105a489..9a2091eac 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -739,9 +739,7 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset)
       }
       case kind::REGEXP_RANGE: {
         unsigned a = r[0].getConst<String>().front();
-        a = String::convertUnsignedIntToCode(a);
         unsigned b = r[1].getConst<String>().front();
-        b = String::convertUnsignedIntToCode(b);
         Assert(a < b);
         Assert(b < std::numeric_limits<unsigned>::max());
         for (unsigned c = a; c <= b; c++)
@@ -756,7 +754,6 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset)
           String s = st.getConst<String>();
           if(s.size() != 0) {
             unsigned sc = s.front();
-            sc = String::convertUnsignedIntToCode(sc);
             cset.insert(sc);
           }
         }
@@ -765,7 +762,6 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset)
           if(st[0].isConst()) {
             String s = st[0].getConst<String>();
             unsigned sc = s.front();
-            sc = String::convertUnsignedIntToCode(sc);
             cset.insert(sc);
           } else {
             vset.insert( st[0] );
@@ -887,13 +883,11 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes
       case kind::REGEXP_RANGE: {
         std::vector< Node > vec;
         unsigned a = r[0].getConst<String>().front();
-        a = String::convertUnsignedIntToCode(a);
         unsigned b = r[1].getConst<String>().front();
-        b = String::convertUnsignedIntToCode(b);
         for (unsigned c = a; c <= b; c++)
         {
           std::vector<unsigned> tmpVec;
-          tmpVec.push_back(String::convertCodeToUnsignedInt(c));
+          tmpVec.push_back(c);
           Node tmp = s.eqNode(nm->mkConst(String(tmpVec))).negate();
           vec.push_back( tmp );
         }
@@ -1522,7 +1516,7 @@ Node RegExpOpr::intersectInternal( Node r1, Node r2, std::map< PairNodes, Node >
              ++it)
         {
           std::vector<unsigned> cvec;
-          cvec.push_back(String::convertCodeToUnsignedInt(*it));
+          cvec.push_back(*it);
           String c(cvec);
           Trace("regexp-int-debug") << "Try character " << c << " ... " << std::endl;
           Node r1l = derivativeSingle(r1, c);
diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index b9dbedba5..7845b2e00 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -24,10 +24,9 @@
 #include <algorithm>
 #include <climits>
 #include "util/hash.h"
-#include "util/regexp.h"
+#include "util/string.h"
 #include "theory/theory.h"
 #include "theory/rewriter.h"
-//#include "context/cdhashmap.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/strings/regexp_solver.h b/src/theory/strings/regexp_solver.h
index 4880af905..d18604752 100644
--- a/src/theory/strings/regexp_solver.h
+++ b/src/theory/strings/regexp_solver.h
@@ -27,7 +27,7 @@
 #include "theory/strings/inference_manager.h"
 #include "theory/strings/regexp_operation.h"
 #include "theory/strings/solver_state.h"
-#include "util/regexp.h"
+#include "util/string.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 200d7a734..b0940b7e1 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -400,7 +400,7 @@ Node SequencesRewriter::rewriteEqualityExt(Node node)
   {
     return rewriteArithEqualityExt(node);
   }
-  if (node[0].getType().isString())
+  if (node[0].getType().isStringLike())
   {
     return rewriteStrEqualityExt(node);
   }
@@ -409,7 +409,7 @@ Node SequencesRewriter::rewriteEqualityExt(Node node)
 
 Node SequencesRewriter::rewriteStrEqualityExt(Node node)
 {
-  Assert(node.getKind() == EQUAL && node[0].getType().isString());
+  Assert(node.getKind() == EQUAL && node[0].getType().isStringLike());
   TypeNode stype = node[0].getType();
 
   NodeManager* nm = NodeManager::currentNM();
@@ -1421,11 +1421,8 @@ bool SequencesRewriter::testConstStringInRegExp(CVC4::String& s,
       if (s.size() == index_start + 1)
       {
         unsigned a = r[0].getConst<String>().front();
-        a = String::convertUnsignedIntToCode(a);
         unsigned b = r[1].getConst<String>().front();
-        b = String::convertUnsignedIntToCode(b);
         unsigned c = s.back();
-        c = String::convertUnsignedIntToCode(c);
         return (a <= c && c <= b);
       }
       else
diff --git a/src/theory/strings/sequences_stats.cpp b/src/theory/strings/sequences_stats.cpp
index 0f1e93599..fb13cdab2 100644
--- a/src/theory/strings/sequences_stats.cpp
+++ b/src/theory/strings/sequences_stats.cpp
@@ -22,14 +22,42 @@ namespace theory {
 namespace strings {
 
 SequencesStatistics::SequencesStatistics()
-    : d_inferences("theory::strings::inferences")
+    : d_inferences("theory::strings::inferences"),
+      d_reductions("theory::strings::reductions"),
+      d_conflictsEqEngine("theory::strings::conflictsEqEngine", 0),
+      d_conflictsEagerPrefix("theory::strings::conflictsEagerPrefix", 0),
+      d_conflictsInfer("theory::strings::conflictsInfer", 0),
+      d_lemmasEagerPreproc("theory::strings::lemmasEagerPreproc", 0),
+      d_lemmasCmiSplit("theory::strings::lemmasCmiSplit", 0),
+      d_lemmasRegisterTerm("theory::strings::lemmasRegisterTerm", 0),
+      d_lemmasRegisterTermAtomic("theory::strings::lemmasRegisterTermAtomic",
+                                 0),
+      d_lemmasInfer("theory::strings::lemmasInfer", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_inferences);
+  smtStatisticsRegistry()->registerStat(&d_reductions);
+  smtStatisticsRegistry()->registerStat(&d_conflictsEqEngine);
+  smtStatisticsRegistry()->registerStat(&d_conflictsEagerPrefix);
+  smtStatisticsRegistry()->registerStat(&d_conflictsInfer);
+  smtStatisticsRegistry()->registerStat(&d_lemmasEagerPreproc);
+  smtStatisticsRegistry()->registerStat(&d_lemmasCmiSplit);
+  smtStatisticsRegistry()->registerStat(&d_lemmasRegisterTerm);
+  smtStatisticsRegistry()->registerStat(&d_lemmasRegisterTermAtomic);
+  smtStatisticsRegistry()->registerStat(&d_lemmasInfer);
 }
 
 SequencesStatistics::~SequencesStatistics()
 {
   smtStatisticsRegistry()->unregisterStat(&d_inferences);
+  smtStatisticsRegistry()->unregisterStat(&d_reductions);
+  smtStatisticsRegistry()->unregisterStat(&d_conflictsEqEngine);
+  smtStatisticsRegistry()->unregisterStat(&d_conflictsEagerPrefix);
+  smtStatisticsRegistry()->unregisterStat(&d_conflictsInfer);
+  smtStatisticsRegistry()->unregisterStat(&d_lemmasEagerPreproc);
+  smtStatisticsRegistry()->unregisterStat(&d_lemmasCmiSplit);
+  smtStatisticsRegistry()->unregisterStat(&d_lemmasRegisterTerm);
+  smtStatisticsRegistry()->unregisterStat(&d_lemmasRegisterTermAtomic);
+  smtStatisticsRegistry()->unregisterStat(&d_lemmasInfer);
 }
 
 }
diff --git a/src/theory/strings/sequences_stats.h b/src/theory/strings/sequences_stats.h
index b55178f4c..83a16cb23 100644
--- a/src/theory/strings/sequences_stats.h
+++ b/src/theory/strings/sequences_stats.h
@@ -17,6 +17,7 @@
 #ifndef CVC4__THEORY__STRINGS__SEQUENCES_STATS_H
 #define CVC4__THEORY__STRINGS__SEQUENCES_STATS_H
 
+#include "expr/kind.h"
 #include "theory/strings/infer_info.h"
 #include "util/statistics_registry.h"
 
@@ -30,11 +31,32 @@ class SequencesStatistics
   SequencesStatistics();
   ~SequencesStatistics();
 
-  /** Counts the number of inferences made of each type of inference */
+  /** Counts the number of applications of each type of inference */
   HistogramStat<Inference> d_inferences;
+  /** Counts the number of applications of each type of reduction */
+  HistogramStat<Kind> d_reductions;
+  //--------------- conflicts, partition of calls to OutputChannel::conflict
+  /** Number of equality engine conflicts */
+  IntStat d_conflictsEqEngine;
+  /** Number of eager prefix conflicts */
+  IntStat d_conflictsEagerPrefix;
+  /** Number of inference conflicts */
+  IntStat d_conflictsInfer;
+  //--------------- end of conflicts
+  //--------------- lemmas, partition of calls to OutputChannel::lemma
+  /** Number of lemmas added due to eager preprocessing */
+  IntStat d_lemmasEagerPreproc;
+  /** Number of collect model info splits */
+  IntStat d_lemmasCmiSplit;
+  /** Number of lemmas added due to registering terms */
+  IntStat d_lemmasRegisterTerm;
+  /** Number of lemmas added due to registering atomic terms */
+  IntStat d_lemmasRegisterTermAtomic;
+  /** Number of lemmas added due to inferences */
+  IntStat d_lemmasInfer;
+  //--------------- end of lemmas
 };
 
-
 }
 }
 }
diff --git a/src/theory/strings/solver_state.cpp b/src/theory/strings/solver_state.cpp
index a38bf2c50..30acba9fd 100644
--- a/src/theory/strings/solver_state.cpp
+++ b/src/theory/strings/solver_state.cpp
@@ -108,7 +108,7 @@ void SolverState::eqNotifyNewClass(TNode t)
       ei->d_codeTerm = t[0];
     }
   }
-  else if (k == CONST_STRING)
+  else if (t.isConst())
   {
     EqcInfo* ei = getOrMakeEqcInfo(t);
     ei->d_prefixC = t;
diff --git a/src/theory/strings/strings_fmf.cpp b/src/theory/strings/strings_fmf.cpp
index 8ca6d2de1..02af3949e 100644
--- a/src/theory/strings/strings_fmf.cpp
+++ b/src/theory/strings/strings_fmf.cpp
@@ -40,7 +40,7 @@ StringsFmf::~StringsFmf() {}
 
 void StringsFmf::preRegisterTerm(TNode n)
 {
-  if (!n.getType().isString())
+  if (!n.getType().isStringLike())
   {
     return;
   }
diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp
index 75dfe7432..c7676d049 100644
--- a/src/theory/strings/strings_rewriter.cpp
+++ b/src/theory/strings/strings_rewriter.cpp
@@ -93,7 +93,7 @@ Node StringsRewriter::rewriteStrConvert(Node node)
     std::vector<unsigned> nvec = node[0].getConst<String>().getVec();
     for (unsigned i = 0, nvsize = nvec.size(); i < nvsize; i++)
     {
-      unsigned newChar = String::convertUnsignedIntToCode(nvec[i]);
+      unsigned newChar = nvec[i];
       // transform it
       // upper 65 ... 90
       // lower 97 ... 122
@@ -111,7 +111,6 @@ Node StringsRewriter::rewriteStrConvert(Node node)
           newChar = newChar + 32;
         }
       }
-      newChar = String::convertCodeToUnsignedInt(newChar);
       nvec[i] = newChar;
     }
     Node retNode = nm->mkConst(String(nvec));
@@ -231,7 +230,7 @@ Node StringsRewriter::rewriteStringToCode(Node n)
     {
       std::vector<unsigned> vec = s.getVec();
       Assert(vec.size() == 1);
-      ret = nm->mkConst(Rational(String::convertUnsignedIntToCode(vec[0])));
+      ret = nm->mkConst(Rational(vec[0]));
     }
     else
     {
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 1006076d5..a81c96318 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -69,7 +69,7 @@ TheoryStrings::TheoryStrings(context::Context* c,
                              const LogicInfo& logicInfo)
     : Theory(THEORY_STRINGS, c, u, out, valuation, logicInfo),
       d_notify(*this),
-      d_equalityEngine(d_notify, c, "theory::strings", true),
+      d_equalityEngine(d_notify, c, "theory::strings::ee", true),
       d_state(c, d_equalityEngine, d_valuation),
       d_im(*this, c, u, d_state, d_sk_cache, out, d_statistics),
       d_pregistered_terms_cache(u),
@@ -85,8 +85,15 @@ TheoryStrings::TheoryStrings(context::Context* c,
 {
   setupExtTheory();
   ExtTheory* extt = getExtTheory();
-  d_esolver.reset(new ExtfSolver(
-      c, u, d_state, d_im, d_sk_cache, d_bsolver, d_csolver, extt));
+  d_esolver.reset(new ExtfSolver(c,
+                                 u,
+                                 d_state,
+                                 d_im,
+                                 d_sk_cache,
+                                 d_bsolver,
+                                 d_csolver,
+                                 extt,
+                                 d_statistics));
   d_rsolver.reset(new RegExpSolver(*this, d_state, d_im, *d_esolver, c, u));
 
   // The kinds we are treating as function application in congruence
@@ -375,7 +382,7 @@ bool TheoryStrings::collectModelInfoType(
                   ctv.getConst<Rational>().getNumerator().toUnsignedInt();
               Trace("strings-model") << "(code: " << cvalue << ") ";
               std::vector<unsigned> vec;
-              vec.push_back(String::convertCodeToUnsignedInt(cvalue));
+              vec.push_back(cvalue);
               Node mv = nm->mkConst(String(vec));
               pure_eq_assign[eqc] = mv;
               m->getEqualityEngine()->addTerm(mv);
@@ -464,6 +471,7 @@ bool TheoryStrings::collectModelInfoType(
               for (const Node& sl : len_splits)
               {
                 Node spl = nm->mkNode(OR, sl, sl.negate());
+                ++(d_statistics.d_lemmasCmiSplit);
                 d_out->lemma(spl);
               }
               return false;
@@ -700,7 +708,8 @@ void TheoryStrings::check(Effort e) {
         Trace("strings-eqc") << (t==0 ? "STRINGS:" : "OTHER:") << std::endl;
         while( !eqcs2_i.isFinished() ){
           Node eqc = (*eqcs2_i);
-          bool print = (t==0 && eqc.getType().isString() ) || (t==1 && !eqc.getType().isString() );
+          bool print = (t == 0 && eqc.getType().isStringLike())
+                       || (t == 1 && !eqc.getType().isStringLike());
           if (print) {
             eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
             Trace("strings-eqc") << "Eqc( " << eqc << " ) : { ";
@@ -778,6 +787,7 @@ void TheoryStrings::conflict(TNode a, TNode b){
     Node conflictNode;
     conflictNode = explain( a.eqNode(b) );
     Trace("strings-conflict") << "CONFLICT: Eq engine conflict : " << conflictNode << std::endl;
+    ++(d_statistics.d_conflictsEqEngine);
     d_out->conflict( conflictNode );
   }
 }
@@ -872,7 +882,9 @@ void TheoryStrings::addCarePairs(TNodeTrie* t1,
 void TheoryStrings::computeCareGraph(){
   //computing the care graph here is probably still necessary, due to operators that take non-string arguments  TODO: verify
   Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Build term indices..." << std::endl;
-  std::map<Node, TNodeTrie> index;
+  // Term index for each (type, operator) pair. We require the operator here
+  // since operators are polymorphic, taking strings/sequences.
+  std::map<std::pair<TypeNode, Node>, TNodeTrie> index;
   std::map< Node, unsigned > arity;
   unsigned functionTerms = d_functionsTerms.size();
   for (unsigned i = 0; i < functionTerms; ++ i) {
@@ -888,16 +900,19 @@ void TheoryStrings::computeCareGraph(){
       }
     }
     if( has_trigger_arg ){
-      index[op].addTerm( f1, reps );
+      TypeNode ft = utils::getOwnerStringType(f1);
+      std::pair<TypeNode, Node> ikey = std::pair<TypeNode, Node>(ft, op);
+      index[ikey].addTerm(f1, reps);
       arity[op] = reps.size();
     }
   }
   //for each index
-  for (std::pair<const Node, TNodeTrie>& tt : index)
+  for (std::pair<const std::pair<TypeNode, Node>, TNodeTrie>& ti : index)
   {
     Trace("strings-cg") << "TheoryStrings::computeCareGraph(): Process index "
-                        << tt.first << "..." << std::endl;
-    addCarePairs(&tt.second, nullptr, arity[tt.first], 0);
+                        << ti.first << "..." << std::endl;
+    Node op = ti.first.second;
+    addCarePairs(&ti.second, nullptr, arity[op], 0);
   }
 }
 
@@ -907,7 +922,9 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
   if( atom.getKind()==kind::EQUAL ){
     Trace("strings-pending-debug") << "  Register term" << std::endl;
     for( unsigned j=0; j<2; j++ ) {
-      if( !d_equalityEngine.hasTerm( atom[j] ) && atom[j].getType().isString() ) {
+      if (!d_equalityEngine.hasTerm(atom[j])
+          && atom[j].getType().isStringLike())
+      {
         registerTerm( atom[j], 0 );
       }
     }
@@ -939,6 +956,7 @@ void TheoryStrings::assertPendingFact(Node atom, bool polarity, Node exp) {
       d_state.setConflict();
       Trace("strings-conflict")
           << "CONFLICT: Eager prefix : " << conflictNode << std::endl;
+      ++(d_statistics.d_conflictsEagerPrefix);
       d_out->conflict(conflictNode);
     }
   }
@@ -1047,7 +1065,7 @@ void TheoryStrings::registerTerm(Node n, int effort)
 {
   TypeNode tn = n.getType();
   bool do_register = true;
-  if (!tn.isString())
+  if (!tn.isStringLike())
   {
     if (options::stringEagerLen())
     {
@@ -1070,37 +1088,41 @@ void TheoryStrings::registerTerm(Node n, int effort)
   NodeManager* nm = NodeManager::currentNM();
   Debug("strings-register") << "TheoryStrings::registerTerm() " << n
                             << ", effort = " << effort << std::endl;
-  if (tn.isString())
+  Node regTermLem;
+  if (tn.isStringLike())
   {
     // register length information:
     //  for variables, split on empty vs positive length
     //  for concat/const/replace, introduce proxy var and state length relation
-    d_im.registerLength(n);
+    regTermLem = d_im.registerTerm(n);
   }
   else if (n.getKind() == STRING_TO_CODE)
   {
     d_has_str_code = true;
-    // ite( str.len(s)==1, 0 <= str.code(s) < num_codes, str.code(s)=-1 )
+    // ite( str.len(s)==1, 0 <= str.code(s) < |A|, str.code(s)=-1 )
     Node code_len = utils::mkNLength(n[0]).eqNode(d_one);
     Node code_eq_neg1 = n.eqNode(d_neg_one);
     Node code_range = nm->mkNode(
         AND,
         nm->mkNode(GEQ, n, d_zero),
-        nm->mkNode(LT, n, nm->mkConst(Rational(CVC4::String::num_codes()))));
-    Node lem = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
-    Trace("strings-lemma") << "Strings::Lemma CODE : " << lem << std::endl;
-    Trace("strings-assert") << "(assert " << lem << ")" << std::endl;
-    d_out->lemma(lem);
+        nm->mkNode(
+            LT, n, nm->mkConst(Rational(utils::getAlphabetCardinality()))));
+    regTermLem = nm->mkNode(ITE, code_len, code_range, code_eq_neg1);
   }
   else if (n.getKind() == STRING_STRIDOF)
   {
     Node len = utils::mkNLength(n[0]);
-    Node lem = nm->mkNode(AND,
-                          nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))),
-                          nm->mkNode(LEQ, n, len));
-    Trace("strings-lemma") << "Strings::Lemma IDOF range : " << lem
+    regTermLem = nm->mkNode(AND,
+                            nm->mkNode(GEQ, n, nm->mkConst(Rational(-1))),
+                            nm->mkNode(LEQ, n, len));
+  }
+  if (!regTermLem.isNull())
+  {
+    Trace("strings-lemma") << "Strings::Lemma REG-TERM : " << regTermLem
                            << std::endl;
-    d_out->lemma(lem);
+    Trace("strings-assert") << "(assert " << regTermLem << ")" << std::endl;
+    ++(d_statistics.d_lemmasRegisterTerm);
+    d_out->lemma(regTermLem);
   }
 }
 
@@ -1145,6 +1167,7 @@ Node TheoryStrings::ppRewrite(TNode atom) {
       Trace("strings-ppr") << "  rewrote " << atom << " -> " << ret << ", with " << new_nodes.size() << " lemmas." << std::endl; 
       for( unsigned i=0; i<new_nodes.size(); i++ ){
         Trace("strings-ppr") << "    lemma : " << new_nodes[i] << std::endl;
+        ++(d_statistics.d_lemmasEagerPreproc);
         d_out->lemma( new_nodes[i] );
       }
       return ret;
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index d4183700d..b35c4a921 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -31,8 +31,10 @@ namespace CVC4 {
 namespace theory {
 namespace strings {
 
-StringsPreprocess::StringsPreprocess(SkolemCache *sc, context::UserContext *u)
-    : d_sc(sc)
+StringsPreprocess::StringsPreprocess(SkolemCache* sc,
+                                     context::UserContext* u,
+                                     SequencesStatistics& stats)
+    : d_sc(sc), d_statistics(stats)
 {
   //Constants
   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
@@ -637,6 +639,7 @@ Node StringsPreprocess::simplify( Node t, std::vector< Node > &new_nodes ) {
         Trace("strings-preprocess") << "   " << new_nodes[i] << std::endl;
       }
     }
+    d_statistics.d_reductions << t.getKind();
   }
   else
   {
diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index b96d619ef..155b9014c 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -22,6 +22,7 @@
 #include <vector>
 #include "context/cdhashmap.h"
 #include "theory/rewriter.h"
+#include "theory/strings/sequences_stats.h"
 #include "theory/strings/skolem_cache.h"
 #include "theory/theory.h"
 #include "util/hash.h"
@@ -38,48 +39,52 @@ namespace strings {
  * reductions" inference schema of TheoryStrings.
  */
 class StringsPreprocess {
-public:
- StringsPreprocess(SkolemCache *sc, context::UserContext *u);
- ~StringsPreprocess();
- /**
-  * Returns a node t' such that
-  *   (exists k) new_nodes => t = t'
-  * is valid, where k are the free skolems introduced when constructing
-  * new_nodes.
-  */
- Node simplify(Node t, std::vector<Node> &new_nodes);
- /**
-  * Applies simplifyRec on t until a fixed point is reached, and returns
-  * the resulting term t', which is such that
-  *   (exists k) new_nodes => t = t'
-  * is valid, where k are the free skolems introduced when constructing
-  * new_nodes.
-  */
- Node processAssertion(Node t, std::vector<Node> &new_nodes);
- /**
-  * Replaces all formulas t in vec_node with an equivalent formula t' that
-  * contains no free instances of extended functions (that is, extended
-  * functions may only appear beneath quantifiers). This applies simplifyRec
-  * on each assertion in vec_node until a fixed point is reached.
-  */
- void processAssertions(std::vector<Node> &vec_node);
+ public:
+  StringsPreprocess(SkolemCache* sc,
+                    context::UserContext* u,
+                    SequencesStatistics& stats);
+  ~StringsPreprocess();
+  /**
+   * Returns a node t' such that
+   *   (exists k) new_nodes => t = t'
+   * is valid, where k are the free skolems introduced when constructing
+   * new_nodes.
+   */
+  Node simplify(Node t, std::vector<Node>& new_nodes);
+  /**
+   * Applies simplifyRec on t until a fixed point is reached, and returns
+   * the resulting term t', which is such that
+   *   (exists k) new_nodes => t = t'
+   * is valid, where k are the free skolems introduced when constructing
+   * new_nodes.
+   */
+  Node processAssertion(Node t, std::vector<Node>& new_nodes);
+  /**
+   * Replaces all formulas t in vec_node with an equivalent formula t' that
+   * contains no free instances of extended functions (that is, extended
+   * functions may only appear beneath quantifiers). This applies simplifyRec
+   * on each assertion in vec_node until a fixed point is reached.
+   */
+  void processAssertions(std::vector<Node>& vec_node);
 
-private:
- /** commonly used constants */
- Node d_zero;
- Node d_one;
- Node d_neg_one;
- Node d_empty_str;
- /** pointer to the skolem cache used by this class */
- SkolemCache *d_sc;
- /**
-  * Applies simplify to all top-level extended function subterms of t. New
-  * assertions created in this reduction are added to new_nodes. The argument
-  * visited stores a cache of previous results.
-  */
- Node simplifyRec(Node t,
-                  std::vector<Node> &new_nodes,
-                  std::map<Node, Node> &visited);
+ private:
+  /** commonly used constants */
+  Node d_zero;
+  Node d_one;
+  Node d_neg_one;
+  Node d_empty_str;
+  /** pointer to the skolem cache used by this class */
+  SkolemCache* d_sc;
+  /** Reference to the statistics for the theory of strings/sequences. */
+  SequencesStatistics& d_statistics;
+  /**
+   * Applies simplify to all top-level extended function subterms of t. New
+   * assertions created in this reduction are added to new_nodes. The argument
+   * visited stores a cache of previous results.
+   */
+  Node simplifyRec(Node t,
+                   std::vector<Node>& new_nodes,
+                   std::map<Node, Node>& visited);
 };
 
 }/* CVC4::theory::strings namespace */
diff --git a/src/theory/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 6abb57504..93a32f26e 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -291,14 +291,15 @@ public:
         if (!t.isString()) {
           throw TypeCheckingExceptionPrivate(n, "expecting a string term in regexp range");
         }
-        if( (*it).getKind() != kind::CONST_STRING ) {
+        if (!(*it).isConst())
+        {
           throw TypeCheckingExceptionPrivate(n, "expecting a constant string term in regexp range");
         }
         if( (*it).getConst<String>().size() != 1 ) {
           throw TypeCheckingExceptionPrivate(n, "expecting a single constant string term in regexp range");
         }
         unsigned ci = (*it).getConst<String>().front();
-        ch[i] = String::convertUnsignedIntToCode(ci);
+        ch[i] = ci;
         ++it;
       }
       if(ch[0] > ch[1]) {
diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 5d27b8e2b..a3f6f4255 100644
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -232,11 +232,10 @@ void getRegexpComponents(Node r, std::vector<Node>& result)
   }
   else if (r.getKind() == STRING_TO_REGEXP && r[0].isConst())
   {
-    String s = r[0].getConst<String>();
-    for (size_t i = 0, size = s.size(); i < size; i++)
+    size_t rlen = Word::getLength(r[0]);
+    for (size_t i = 0; i < rlen; i++)
     {
-      result.push_back(
-          nm->mkNode(STRING_TO_REGEXP, nm->mkConst(s.substr(i, 1))));
+      result.push_back(nm->mkNode(STRING_TO_REGEXP, Word::substr(r[0], i, 1)));
     }
   }
   else
@@ -264,6 +263,36 @@ void printConcatTrace(std::vector<Node>& n, const char* c)
   Trace(c) << ss.str();
 }
 
+bool isStringKind(Kind k)
+{
+  return k == STRING_STOI || k == STRING_ITOS || k == STRING_TOLOWER
+         || k == STRING_TOUPPER || k == STRING_LEQ || k == STRING_LT
+         || k == STRING_FROM_CODE || k == STRING_TO_CODE;
+}
+
+TypeNode getOwnerStringType(Node n)
+{
+  TypeNode tn;
+  Kind k = n.getKind();
+  if (k == STRING_STRIDOF || k == STRING_LENGTH || k == STRING_STRCTN
+      || k == STRING_PREFIX || k == STRING_SUFFIX)
+  {
+    // owning string type is the type of first argument
+    tn = n[0].getType();
+  }
+  else if (isStringKind(k))
+  {
+    tn = NodeManager::currentNM()->stringType();
+  }
+  else
+  {
+    tn = n.getType();
+  }
+  AlwaysAssert(tn.isStringLike())
+      << "Unexpected term in getOwnerStringType : " << n << ", type " << tn;
+  return tn;
+}
+
 }  // namespace utils
 }  // namespace strings
 }  // namespace theory
diff --git a/src/theory/strings/theory_strings_utils.h b/src/theory/strings/theory_strings_utils.h
index 5f18d3936..578c224df 100644
--- a/src/theory/strings/theory_strings_utils.h
+++ b/src/theory/strings/theory_strings_utils.h
@@ -140,6 +140,19 @@ void printConcat(std::ostream& out, std::vector<Node>& n);
 /** Print the vector n as a concatentation term on trace given by c */
 void printConcatTrace(std::vector<Node>& n, const char* c);
 
+/** Is k a string-specific kind? */
+bool isStringKind(Kind k);
+
+/** Get owner string type
+ *
+ * This returns a string-like type for a term n that belongs to the theory of
+ * strings. This type conceptually represents the subtheory of strings
+ * (Sequence(T) or String) that owns n. This is typically the type of n,
+ * but for instance, operators like str.indexof( s, t, n ), this is the type
+ * of s.
+ */
+TypeNode getOwnerStringType(Node n);
+
 }  // namespace utils
 }  // namespace strings
 }  // namespace theory
diff --git a/src/theory/strings/type_enumerator.cpp b/src/theory/strings/type_enumerator.cpp
index 12cf899b4..d24206860 100644
--- a/src/theory/strings/type_enumerator.cpp
+++ b/src/theory/strings/type_enumerator.cpp
@@ -15,12 +15,50 @@
 #include "theory/strings/type_enumerator.h"
 
 #include "theory/strings/theory_strings_utils.h"
-#include "util/regexp.h"
+#include "util/string.h"
 
 namespace CVC4 {
 namespace theory {
 namespace strings {
 
+Node makeStandardModelConstant(const std::vector<unsigned>& vec,
+                               uint32_t cardinality)
+{
+  std::vector<unsigned> mvec;
+  // if we contain all of the printable characters
+  if (cardinality >= 255)
+  {
+    for (unsigned i = 0, vsize = vec.size(); i < vsize; i++)
+    {
+      unsigned curr = vec[i];
+      // convert
+      Assert(vec[i] < cardinality);
+      if (vec[i] <= 61)
+      {
+        // first 62 printable characters [\u{65}-\u{126}]: 'A', 'B', 'C', ...
+        curr = vec[i] + 65;
+      }
+      else if (vec[i] <= 94)
+      {
+        // remaining 33 printable characters [\u{32}-\u{64}]: ' ', '!', '"', ...
+        curr = vec[i] - 30;
+      }
+      else
+      {
+        // the remaining characters, starting with \u{127} and wrapping around
+        // the first 32 non-printable characters.
+        curr = (vec[i] + 32) % cardinality;
+      }
+      mvec.push_back(curr);
+    }
+  }
+  else
+  {
+    mvec = vec;
+  }
+  return NodeManager::currentNM()->mkConst(String(mvec));
+}
+
 WordIter::WordIter(uint32_t startLength) : d_hasEndLength(false), d_endLength(0)
 {
   for (uint32_t i = 0; i < startLength; i++)
@@ -117,7 +155,7 @@ bool StringEnumLen::increment()
 
 void StringEnumLen::mkCurr()
 {
-  d_curr = NodeManager::currentNM()->mkConst(String(d_witer->getData()));
+  d_curr = makeStandardModelConstant(d_witer->getData(), d_cardinality);
 }
 
 StringEnumerator::StringEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
diff --git a/src/theory/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h
index 2061628a5..b379ce5c3 100644
--- a/src/theory/strings/type_enumerator.h
+++ b/src/theory/strings/type_enumerator.h
@@ -28,6 +28,26 @@ namespace theory {
 namespace strings {
 
 /**
+ * Make standard model constant
+ *
+ * In our string representation, we represent characters using vectors
+ * of unsigned integers indicating code points for the characters of that
+ * string.
+ *
+ * To make models user-friendly, we make unsigned integer 0 correspond to the
+ * 65th character ("A") in the ASCII alphabet to make models intuitive. In
+ * particular, say if we have a set of string variables that are distinct but
+ * otherwise unconstrained, then the model may assign them "A", "B", "C", ...
+ *
+ * @param vec The code points of the string in a given model,
+ * @param cardinality The cardinality of the alphabet,
+ * @return A string whose characters have the code points corresponding
+ * to vec in the standard model construction described above.
+ */
+Node makeStandardModelConstant(const std::vector<unsigned>& vec,
+                               uint32_t cardinality);
+
+/**
  * Generic iteration over vectors of indices of a given start/end length.
  */
 class WordIter
diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp
index dd573b68c..0faeffd99 100644
--- a/src/theory/strings/word.cpp
+++ b/src/theory/strings/word.cpp
@@ -14,7 +14,7 @@
 
 #include "theory/strings/word.h"
 
-#include "util/regexp.h"
+#include "util/string.h"
 
 using namespace CVC4::kind;
 
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 75597edac..6895dc01a 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -25,8 +25,6 @@ libcvc4_add_sources(
   proof.h
   random.cpp
   random.h
-  regexp.cpp
-  regexp.h
   resource_manager.cpp
   resource_manager.h
   result.cpp
@@ -43,6 +41,8 @@ libcvc4_add_sources(
   statistics.h
   statistics_registry.cpp
   statistics_registry.h
+  string.cpp
+  string.h
   tuple.h
   unsafe_interrupt_exception.h
   utility.cpp
diff --git a/src/util/safe_print.h b/src/util/safe_print.h
index 75a517b18..fa9430f2c 100644
--- a/src/util/safe_print.h
+++ b/src/util/safe_print.h
@@ -21,6 +21,11 @@
  ** in statistics_registry.h would require specialization or we would have to
  ** use function overloading).
  **
+ ** If there exists a function `toString(obj)` for a given object, it will be
+ ** used automatically. This is useful for printing enum values for example.
+ ** IMPORTANT: The `toString(obj)` function *must not* perform any allocations
+ ** or call other functions that are not async-signal-safe.
+ **
  ** This header is a "cvc4_private_library.h" header because it is private but
  ** the safe_print functions are used in the driver. See also the description
  ** of "statistics_registry.h" for more information on
@@ -41,6 +46,9 @@
 
 #include <unistd.h>
 
+#include <cstring>
+#include <type_traits>
+
 #include "lib/clock_gettime.h"
 #include "util/result.h"
 
@@ -58,10 +66,51 @@ void CVC4_PUBLIC safe_print(int fd, const char (&msg)[N]) {
   }
 }
 
-/** Prints a variable of type T. Safe to use in a signal handler. */
+/**
+ * The default method for converting an object to a string for safe printing.
+ * This method simply returns "<unsupported>". The `long` argument is used to
+ * indicate that we do not prefer this method over the version that calls
+ * `toString()`.
+ */
+template <typename T>
+const char* toStringImpl(const T& obj, long)
+{
+  return "<unsupported>";
+}
+
+/**
+ * Returns the result of calling `toString(obj)`. This method is only defined
+ * if such an overload of `toString()` exists. To detect the existence of such
+ * a method, we use SFINAE and a trailing return type. The trailing return type
+ * is necessary because it allows us to refer to `obj`. The `int` argument is
+ * used to prefer this version of the function instead of the one that prints
+ * "<unsupported>".
+ */
+template <typename T>
+auto toStringImpl(const T& obj, int) -> decltype(toString(obj))
+{
+  return toString(obj);
+}
+
+/**
+ * Prints a variable of type T. Safe to use in a signal handler. The default
+ * implementation either prints "<unsupported>" or the result of calling
+ * `toString(obj)` if such a method exists (this is useful for printing enum
+ * values for example without implementing a template specialization here).
+ *
+ * @param fd The file descriptor to print to
+ * @param obj The object to print
+ */
 template <typename T>
-void CVC4_PUBLIC safe_print(int fd, const T& msg) {
-  safe_print(fd, "<unsupported>");
+void CVC4_PUBLIC safe_print(int fd, const T& obj)
+{
+  const char* s =
+      toStringImpl(obj, /* prefer the method that uses `toString()` */ 0);
+  ssize_t slen = static_cast<ssize_t>(strlen(s));
+  if (write(fd, s, slen) != slen)
+  {
+    abort();
+  }
 }
 
 template <>
diff --git a/src/util/regexp.cpp b/src/util/string.cpp
index 00066edb6..ff522ba7b 100644
--- a/src/util/regexp.cpp
+++ b/src/util/string.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file regexp.cpp
+/*! \file string.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Tim King, Tianyi Liang, Andrew Reynolds
@@ -9,13 +9,10 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** \brief Implementation of the string data type.
  **/
 
-#include "util/regexp.h"
+#include "util/string.h"
 
 #include <algorithm>
 #include <climits>
@@ -32,38 +29,12 @@ namespace CVC4 {
 
 static_assert(UCHAR_MAX == 255, "Unsigned char is assumed to have 256 values.");
 
-unsigned String::convertCharToUnsignedInt(unsigned char c)
-{
-  return convertCodeToUnsignedInt(static_cast<unsigned>(c));
-}
-unsigned char String::convertUnsignedIntToChar(unsigned i)
-{
-  Assert(i < num_codes());
-  return static_cast<unsigned char>(convertUnsignedIntToCode(i));
-}
-bool String::isPrintable(unsigned i)
-{
-  Assert(i < num_codes());
-  unsigned char c = convertUnsignedIntToChar(i);
-  return (c >= ' ' && c <= '~');
-}
-unsigned String::convertCodeToUnsignedInt(unsigned c)
-{
-  Assert(c < num_codes());
-  return (c < start_code() ? c + num_codes() : c) - start_code();
-}
-unsigned String::convertUnsignedIntToCode(unsigned i)
-{
-  Assert(i < num_codes());
-  return (i + start_code()) % num_codes();
-}
-
 String::String(const std::vector<unsigned> &s) : d_str(s)
 {
 #ifdef CVC4_ASSERTIONS
   for (unsigned u : d_str)
   {
-    Assert(convertUnsignedIntToCode(u) < num_codes());
+    Assert(u < num_codes());
   }
 #endif
 }
@@ -74,8 +45,8 @@ int String::cmp(const String &y) const {
   }
   for (unsigned int i = 0; i < size(); ++i) {
     if (d_str[i] != y.d_str[i]) {
-      unsigned cp = convertUnsignedIntToCode(d_str[i]);
-      unsigned cpy = convertUnsignedIntToCode(y.d_str[i]);
+      unsigned cp = d_str[i];
+      unsigned cpy = y.d_str[i];
       return cp < cpy ? -1 : 1;
     }
   }
@@ -122,107 +93,143 @@ bool String::rstrncmp(const String& y, std::size_t n) const
   return true;
 }
 
-std::vector<unsigned> String::toInternal(const std::string &s,
-                                         bool useEscSequences) {
+void String::addCharToInternal(unsigned char ch, std::vector<unsigned>& str)
+{
+  // if not a printable character
+  if (ch > 127 || ch < 32)
+  {
+    std::stringstream serr;
+    serr << "Illegal string character: \"" << ch
+         << "\", must use escape sequence";
+    throw CVC4::Exception(serr.str());
+  }
+  else
+  {
+    str.push_back(static_cast<unsigned>(ch));
+  }
+}
+
+std::vector<unsigned> String::toInternal(const std::string& s,
+                                         bool useEscSequences)
+{
   std::vector<unsigned> str;
   unsigned i = 0;
-  while (i < s.size()) {
-    if (s[i] == '\\' && useEscSequences) {
-      i++;
-      if (i < s.size()) {
-        switch (s[i]) {
-          case 'n': {
-            str.push_back(convertCharToUnsignedInt('\n'));
-            i++;
-          } break;
-          case 't': {
-            str.push_back(convertCharToUnsignedInt('\t'));
-            i++;
-          } break;
-          case 'v': {
-            str.push_back(convertCharToUnsignedInt('\v'));
-            i++;
-          } break;
-          case 'b': {
-            str.push_back(convertCharToUnsignedInt('\b'));
-            i++;
-          } break;
-          case 'r': {
-            str.push_back(convertCharToUnsignedInt('\r'));
-            i++;
-          } break;
-          case 'f': {
-            str.push_back(convertCharToUnsignedInt('\f'));
-            i++;
-          } break;
-          case 'a': {
-            str.push_back(convertCharToUnsignedInt('\a'));
-            i++;
-          } break;
-          case '\\': {
-            str.push_back(convertCharToUnsignedInt('\\'));
-            i++;
-          } break;
-          case 'x': {
-            if (i + 2 < s.size()) {
-              if (isxdigit(s[i + 1]) && isxdigit(s[i + 2])) {
-                str.push_back(convertCharToUnsignedInt(hexToDec(s[i + 1]) * 16 +
-                                                       hexToDec(s[i + 2])));
-                i += 3;
-              } else {
-                throw CVC4::Exception("Illegal String Literal: \"" + s + "\"");
-              }
-            } else {
-              throw CVC4::Exception("Illegal String Literal: \"" + s +
-                                    "\", must have two digits after \\x");
-            }
-          } break;
-          default: {
-            if (isdigit(s[i])) {
-              // octal escape sequences  TODO : revisit (issue #1251).
-              int num = (int)s[i] - (int)'0';
-              bool flag = num < 4;
-              if (i + 1 < s.size() && num < 8 && isdigit(s[i + 1]) &&
-                  s[i + 1] < '8') {
-                num = num * 8 + (int)s[i + 1] - (int)'0';
-                if (flag && i + 2 < s.size() && isdigit(s[i + 2]) &&
-                    s[i + 2] < '8') {
-                  num = num * 8 + (int)s[i + 2] - (int)'0';
-                  str.push_back(convertCharToUnsignedInt((unsigned char)num));
-                  i += 3;
-                } else {
-                  str.push_back(convertCharToUnsignedInt((unsigned char)num));
-                  i += 2;
-                }
-              } else {
-                str.push_back(convertCharToUnsignedInt((unsigned char)num));
-                i++;
-              }
-            } else if ((unsigned)s[i] > 127) {
-              throw CVC4::Exception("Illegal String Literal: \"" + s +
-                                    "\", must use escaped sequence");
-            } else {
-              str.push_back(convertCharToUnsignedInt(s[i]));
-              i++;
-            }
+  while (i < s.size())
+  {
+    // get the current character
+    char si = s[i];
+    if (si != '\\' || !useEscSequences)
+    {
+      addCharToInternal(si, str);
+      ++i;
+      continue;
+    }
+    // the vector of characters, in case we fail to read an escape sequence
+    std::vector<unsigned> nonEscCache;
+    // process the '\'
+    addCharToInternal(si, nonEscCache);
+    ++i;
+    // are we an escape sequence?
+    bool isEscapeSequence = true;
+    // the string corresponding to the hexidecimal code point
+    std::stringstream hexString;
+    // is the slash followed by a 'u'? Could be last character.
+    if (i >= s.size() || s[i] != 'u')
+    {
+      isEscapeSequence = false;
+    }
+    else
+    {
+      // process the 'u'
+      addCharToInternal(s[i], nonEscCache);
+      ++i;
+      bool isStart = true;
+      bool isEnd = false;
+      bool hasBrace = false;
+      while (i < s.size())
+      {
+        // add the next character
+        si = s[i];
+        if (isStart)
+        {
+          isStart = false;
+          // possibly read '{'
+          if (si == '{')
+          {
+            hasBrace = true;
+            addCharToInternal(si, nonEscCache);
+            ++i;
+            continue;
           }
         }
-      } else {
-        throw CVC4::Exception("should be handled by lexer: \"" + s + "\"");
-        // str.push_back( convertCharToUnsignedInt('\\') );
+        else if (si == '}')
+        {
+          // can only end if we had an open brace and read at least one digit
+          isEscapeSequence = hasBrace && !hexString.str().empty();
+          isEnd = true;
+          addCharToInternal(si, nonEscCache);
+          ++i;
+          break;
+        }
+        // must be a hex digit at this point
+        if (!isHexDigit(static_cast<unsigned>(si)))
+        {
+          isEscapeSequence = false;
+          break;
+        }
+        hexString << si;
+        addCharToInternal(si, nonEscCache);
+        ++i;
+        if (!hasBrace && hexString.str().size() == 4)
+        {
+          // will be finished reading \ u d_3 d_2 d_1 d_0 with no parens
+          isEnd = true;
+          break;
+        }
+        else if (hasBrace && hexString.str().size() > 5)
+        {
+          // too many digits enclosed in brace, not an escape sequence
+          isEscapeSequence = false;
+          break;
+        }
+      }
+      if (!isEnd)
+      {
+        // if we were interupted before ending, then this is not a valid
+        // escape sequence
+        isEscapeSequence = false;
+      }
+    }
+    if (isEscapeSequence)
+    {
+      Assert(!hexString.str().empty() && hexString.str().size() <= 5);
+      // Otherwise, we add the escaped character.
+      // This is guaranteed not to overflow due to the length of hstr.
+      uint32_t val;
+      hexString >> std::hex >> val;
+      if (val > num_codes())
+      {
+        // Failed due to being out of range. This can happen for strings of
+        // the form \ u { d_4 d_3 d_2 d_1 d_0 } where d_4 is a hexidecimal not
+        // in the range [0-2].
+        isEscapeSequence = false;
+      }
+      else
+      {
+        str.push_back(val);
       }
-    } else if ((unsigned)s[i] > 127 && useEscSequences) {
-      throw CVC4::Exception("Illegal String Literal: \"" + s +
-                            "\", must use escaped sequence");
-    } else {
-      str.push_back(convertCharToUnsignedInt(s[i]));
-      i++;
+    }
+    // if we did not successfully parse an escape sequence, we add back all
+    // characters that we cached
+    if (!isEscapeSequence)
+    {
+      str.insert(str.end(), nonEscCache.begin(), nonEscCache.end());
     }
   }
 #ifdef CVC4_ASSERTIONS
   for (unsigned u : str)
   {
-    Assert(convertUnsignedIntToCode(u) < num_codes());
+    Assert(u < num_codes());
   }
 #endif
   return str;
@@ -265,62 +272,23 @@ std::size_t String::roverlap(const String &y) const {
 }
 
 std::string String::toString(bool useEscSequences) const {
-  std::string str;
+  std::stringstream str;
   for (unsigned int i = 0; i < size(); ++i) {
-    unsigned char c = convertUnsignedIntToChar(d_str[i]);
-    if (!useEscSequences) {
-      str += c;
-    } else if (isprint(c)) {
-      if (c == '\\') {
-        str += "\\\\";
-      }
-      // else if(c == '\"') {
-      //  str += "\\\"";
-      //}
-      else {
-        str += c;
-      }
-    } else {
-      std::string s;
-      switch (c) {
-        case '\a':
-          s = "\\a";
-          break;
-        case '\b':
-          s = "\\b";
-          break;
-        case '\t':
-          s = "\\t";
-          break;
-        case '\r':
-          s = "\\r";
-          break;
-        case '\v':
-          s = "\\v";
-          break;
-        case '\f':
-          s = "\\f";
-          break;
-        case '\n':
-          s = "\\n";
-          break;
-        case '\e':
-          s = "\\e";
-          break;
-        default: {
-          std::stringstream ss;
-          ss << std::setfill('0') << std::setw(2) << std::hex << ((int)c);
-          std::string t = ss.str();
-          t = t.substr(t.size() - 2, 2);
-          s = "\\x" + t;
-          // std::string s2 = static_cast<std::ostringstream*>(
-          // &(std::ostringstream() << (int)c) )->str();
-        }
-      }
-      str += s;
+    // we always print forward slash as a code point so that it cannot
+    // be interpreted as specifying part of a code point, e.g. the string
+    // '\' + 'u' + '0' of length three.
+    if (isPrintable(d_str[i]) && d_str[i] != '\\' && !useEscSequences)
+    {
+      str << static_cast<char>(d_str[i]);
+    }
+    else
+    {
+      std::stringstream ss;
+      ss << std::hex << d_str[i];
+      str << "\\u{" << ss.str() << "}";
     }
   }
-  return str;
+  return str.str();
 }
 
 bool String::isLeq(const String &y) const
@@ -331,8 +299,8 @@ bool String::isLeq(const String &y) const
     {
       return false;
     }
-    unsigned ci = convertUnsignedIntToCode(d_str[i]);
-    unsigned cyi = convertUnsignedIntToCode(y.d_str[i]);
+    unsigned ci = d_str[i];
+    unsigned cyi = y.d_str[i];
     if (ci > cyi)
     {
       return false;
@@ -484,8 +452,21 @@ bool String::isNumber() const {
 
 bool String::isDigit(unsigned character)
 {
-  unsigned char c = convertUnsignedIntToChar(character);
-  return c >= '0' && c <= '9';
+  // '0' to '9'
+  return 48 <= character && character <= 57;
+}
+
+bool String::isHexDigit(unsigned character)
+{
+  // '0' to '9' or 'A' to 'F' or 'a' to 'f'
+  return isDigit(character) || (65 <= character && character <= 70)
+         || (97 <= character && character <= 102);
+}
+
+bool String::isPrintable(unsigned character)
+{
+  // Unicode 0x00020 (' ') to 0x0007E ('~')
+  return 32 <= character && character <= 126;
 }
 
 size_t String::maxSize() { return std::numeric_limits<uint32_t>::max(); }
@@ -497,17 +478,6 @@ Rational String::toNumber() const
   return Rational(toString());
 }
 
-unsigned char String::hexToDec(unsigned char c) {
-  if (c >= '0' && c <= '9') {
-    return c - '0';
-  } else if (c >= 'a' && c <= 'f') {
-    return c - 'a' + 10;
-  } else {
-    Assert(c >= 'A' && c <= 'F');
-    return c - 'A' + 10;
-  }
-}
-
 std::ostream &operator<<(std::ostream &os, const String &s) {
   return os << "\"" << s.toString(true) << "\"";
 }
diff --git a/src/util/regexp.h b/src/util/string.h
index 731736f72..032105812 100644
--- a/src/util/regexp.h
+++ b/src/util/string.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file regexp.h
+/*! \file string.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, Tianyi Liang
@@ -9,16 +9,13 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
+ ** \brief The string data type.
  **/
 
 #include "cvc4_public.h"
 
-#ifndef CVC4__REGEXP_H
-#define CVC4__REGEXP_H
+#ifndef CVC4__UTIL__STRING_H
+#define CVC4__UTIL__STRING_H
 
 #include <cstddef>
 #include <functional>
@@ -37,60 +34,44 @@ namespace CVC4 {
 class CVC4_PUBLIC String {
  public:
   /**
-   * The start ASCII code. In our string representation below, we represent
-   * characters using a vector d_str of unsigned integers. We refer to this as
-   * the "internal representation" for the string.
-   *
-   * We make unsigned integer 0 correspond to the 65th character ("A") in the
-   * ASCII alphabet to make models intuitive. In particular, say if we have
-   * a set of string variables that are distinct but otherwise unconstrained,
-   * then the model may assign them "A", "B", "C", ...
-   */
-  static inline unsigned start_code() { return 65; }
-  /**
    * This is the cardinality of the alphabet that is representable by this
    * class. Notice that this must be greater than or equal to the cardinality
    * of the alphabet that the string theory reasons about.
    *
    * This must be strictly less than std::numeric_limits<unsigned>::max().
+   *
+   * As per the SMT-LIB standard for strings, we support the first 3 planes of
+   * Unicode characters, where 196608 = 3*16^4.
    */
-  static inline unsigned num_codes() { return 256; }
-  /**
-   * Convert unsigned char to the unsigned used in the internal representation
-   * in d_str below.
-   */
-  static unsigned convertCharToUnsignedInt(unsigned char c);
-  /** Convert the internal unsigned to a unsigned char. */
-  static unsigned char convertUnsignedIntToChar(unsigned i);
-  /** Does the internal unsigned correspond to a printable character? */
-  static bool isPrintable(unsigned i);
-  /** get the internal unsigned for ASCII code c. */
-  static unsigned convertCodeToUnsignedInt(unsigned c);
-  /** get the ASCII code number that internal unsigned i corresponds to. */
-  static unsigned convertUnsignedIntToCode(unsigned i);
-
+  static inline unsigned num_codes() { return 196608; }
   /** constructors for String
-  *
-  * Internally, a CVC4::String is represented by a vector of unsigned
-  * integers (d_str), where the correspondence between C++ characters
-  * to and from unsigned integers is determined by
-  * by convertCharToUnsignedInt and convertUnsignedIntToChar.
-  *
-  * If useEscSequences is true, then the escape sequences in the input
-  * are converted to the corresponding character. This constructor may
-  * throw an exception if the input contains unrecognized escape sequences.
-  * Currently supported escape sequences are \n, \t, \v, \b, \r, \f, \a, \\,
-  * \x[N] where N is a hexidecimal, and octal escape sequences of the
-  * form \[c1]([c2]([c3])?)? where c1, c2, c3 are digits from 0 to 7.
-  *
-  * If useEscSequences is false, then the characters of the constructed
-  * CVC4::String correspond one-to-one with the input string.
-  */
+   *
+   * Internally, a CVC4::String is represented by a vector of unsigned
+   * integers (d_str) representing the code points of the characters.
+   *
+   * To build a string from a C++ string, we may process escape sequences
+   * according to the SMT-LIB standard. In particular, if useEscSequences is
+   * true, we convert unicode escape sequences:
+   *  \u d_3 d_2 d_1 d_0
+   *  \u{d_0}
+   *  \u{d_1 d_0}
+   *  \u{d_2 d_1 d_0}
+   *  \u{d_3 d_2 d_1 d_0}
+   *  \u{d_4 d_3 d_2 d_1 d_0}
+   * where d_0 ... d_4 are hexidecimal digits, to the appropriate character.
+   *
+   * If useEscSequences is false, then the characters of the constructed
+   * CVC4::String correspond one-to-one with the input string.
+   */
   String() = default;
   explicit String(const std::string& s, bool useEscSequences = false)
-      : d_str(toInternal(s, useEscSequences)) {}
+      : d_str(toInternal(s, useEscSequences))
+  {
+  }
   explicit String(const char* s, bool useEscSequences = false)
-      : d_str(toInternal(std::string(s), useEscSequences)) {}
+      : d_str(toInternal(std::string(s), useEscSequences))
+  {
+  }
   explicit String(const std::vector<unsigned>& s);
 
   String& operator=(const String& y) {
@@ -123,20 +104,16 @@ class CVC4_PUBLIC String {
   bool rstrncmp(const String& y, std::size_t n) const;
 
   /* toString
-  * Converts this string to a std::string.
-  *
-  * If useEscSequences is true, then unprintable characters
-  * are converted to escape sequences. The escape sequences
-  * \n, \t, \v, \b, \r, \f, \a, \\ are printed in this way.
-  * For all other unprintable characters, we print \x[N] where
-  * [N] is the 2 digit hexidecimal corresponding to value of
-  * the character.
-  *
-  * If useEscSequences is false, the returned std::string's characters
-  * map one-to-one with the characters in this string.
-  * Notice that for all std::string s, we have that
-  *    CVC4::String( s ).toString() = s.
-  */
+   * Converts this string to a std::string.
+   *
+   * The unprintable characters are converted to unicode escape sequences as
+   * described above.
+   *
+   * If useEscSequences is false, the string's printable characters are
+   * printed as characters. Notice that for all std::string s having only
+   * printable characters, we have that
+   *    CVC4::String( s ).toString() = s.
+   */
   std::string toString(bool useEscSequences = false) const;
   /** is this the empty string? */
   bool empty() const { return d_str.empty(); }
@@ -221,16 +198,32 @@ class CVC4_PUBLIC String {
   bool isNumber() const;
   /** Returns the corresponding rational for the text of this string. */
   Rational toNumber() const;
-  /** get the internal unsigned representation of this string */
+  /** Get the unsigned representation (code points) of this string */
   const std::vector<unsigned>& getVec() const { return d_str; }
-  /** get the internal unsigned value of the first character in this string */
+  /**
+   * Get the unsigned (code point) value of the first character in this string
+   */
   unsigned front() const;
-  /** get the internal unsigned value of the last character in this string */
+  /**
+   * Get the unsigned (code point) value of the last character in this string
+   */
   unsigned back() const;
   /** is the unsigned a digit?
-  * The input should be the same type as the element type of d_str
-  */
+   *
+   * This is true for code points between 48 ('0') and 57 ('9').
+   */
   static bool isDigit(unsigned character);
+  /** is the unsigned a hexidecimal digit?
+   *
+   * This is true for code points between 48 ('0') and 57 ('9'), code points
+   * between 65 ('A') and 70 ('F) and code points between 97 ('a') and 102 ('f).
+   */
+  static bool isHexDigit(unsigned character);
+  /** is the unsigned a printable code point?
+   *
+   * This is true for Unicode 32 (' ') to 126 ('~').
+   */
+  static bool isPrintable(unsigned character);
 
   /**
    * Returns the maximum length of string representable by this class.
@@ -238,11 +231,19 @@ class CVC4_PUBLIC String {
    */
   static size_t maxSize();
  private:
-  // guarded
-  static unsigned char hexToDec(unsigned char c);
-
+  /**
+   * Helper for toInternal: add character ch to vector vec, storing a string in
+   * internal format. This throws an error if ch is not a printable character,
+   * since non-printable characters must be escaped in SMT-LIB.
+   */
+  static void addCharToInternal(unsigned char ch, std::vector<unsigned>& vec);
+  /**
+   * Convert the string s to the internal format (vector of code points).
+   * The argument useEscSequences is whether to process unicode escape
+   * sequences.
+   */
   static std::vector<unsigned> toInternal(const std::string& s,
-                                          bool useEscSequences = true);
+                                          bool useEscSequences);
 
   /**
    * Returns a negative number if *this < y, 0 if *this and y are equal and a
@@ -267,4 +268,4 @@ std::ostream& operator<<(std::ostream& os, const String& s) CVC4_PUBLIC;
 
 }  // namespace CVC4
 
-#endif /* CVC4__REGEXP_H */
+#endif /* CVC4__UTIL__STRING_H */
diff --git a/src/util/regexp.i b/src/util/string.i
index afc51abd7..1ded901aa 100644
--- a/src/util/regexp.i
+++ b/src/util/string.i
@@ -1,5 +1,5 @@
 %{
-#include "util/regexp.h"
+#include "util/string.h"
 %}
 
 %rename(CVC4String) String;
@@ -21,5 +21,5 @@
 %ignore CVC4::operator<<(std::ostream&, const String&);
 
 %apply int &OUTPUT { int &c };
-%include "util/regexp.h"
+%include "util/string.h"
 %clear int &c;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 65616cfd2..a5acd62fb 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -923,6 +923,7 @@ set(regress_0_tests
   regress0/strings/escchar.smt2
   regress0/strings/escchar_25.smt2
   regress0/strings/from_code.smt2
+  regress0/strings/gen-esc-seq.smt2
   regress0/strings/hconst-092618.smt2
   regress0/strings/idof-rewrites.smt2
   regress0/strings/idof-sem.smt2
@@ -940,6 +941,8 @@ set(regress_0_tests
   regress0/strings/leadingzero001.smt2
   regress0/strings/loop001.smt2
   regress0/strings/model001.smt2
+  regress0/strings/model-code-point.smt2
+  regress0/strings/model-friendly.smt2
   regress0/strings/ncontrib-rewrites.smt2
   regress0/strings/norn-31.smt2
   regress0/strings/norn-simp-rew.smt2
@@ -968,6 +971,7 @@ set(regress_0_tests
   regress0/strings/tolower-rrs.smt2
   regress0/strings/tolower-simple.smt2
   regress0/strings/type001.smt2
+  regress0/strings/unicode-esc.smt2
   regress0/strings/unsound-0908.smt2
   regress0/strings/unsound-repl-rewrite.smt2
   regress0/sygus/General_plus10.sy
@@ -1858,7 +1862,6 @@ set(regress_1_tests
   regress1/sygus/issue3498.smt2
   regress1/sygus/issue3514.smt2
   regress1/sygus/issue3507.smt2
-  regress1/sygus/issue3580.sy
   regress1/sygus/issue3633.smt2
   regress1/sygus/issue3634.smt2
   regress1/sygus/issue3635.smt2
@@ -2389,6 +2392,8 @@ set(regression_disabled_tests
   regress1/sygus/array_search_2.sy
   regress1/sygus/array_sum_2_5.sy
   regress1/sygus/crcy-si-rcons.sy
+  # currently slow at c9fd28a
+  regress1/sygus/issue3580.sy
   regress2/arith/arith-int-098.cvc
   regress2/arith/miplib-opt1217--27.smt2
   regress2/arith/miplib-pp08a-3000.smt2
diff --git a/test/regress/regress0/nl/ext-rew-aggr-test.smt2 b/test/regress/regress0/nl/ext-rew-aggr-test.smt2
index 47006622d..c540ecbe5 100644
--- a/test/regress/regress0/nl/ext-rew-aggr-test.smt2
+++ b/test/regress/regress0/nl/ext-rew-aggr-test.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg --no-new-prop
+; COMMAND-LINE: --ext-rew-prep --ext-rew-prep-agg --no-new-prop --nl-ext-tplanes
 ; EXPECT: sat
 (set-info :smt-lib-version 2.6)
 (set-logic QF_NIA)
diff --git a/test/regress/regress0/strings/gen-esc-seq.smt2 b/test/regress/regress0/strings/gen-esc-seq.smt2
new file mode 100644
index 000000000..59f66046f
--- /dev/null
+++ b/test/regress/regress0/strings/gen-esc-seq.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --produce-models --lang=smt2.6.1
+; EXPECT: sat
+; EXPECT: ((x "\u{5c}u1000"))
+(set-logic ALL)
+(set-info :status sat)
+(declare-const x String)
+(assert (= x (str.++ "\u" "1000")))
+(check-sat)
+(get-value (x))
diff --git a/test/regress/regress0/strings/model-code-point.smt2 b/test/regress/regress0/strings/model-code-point.smt2
new file mode 100644
index 000000000..1200ae704
--- /dev/null
+++ b/test/regress/regress0/strings/model-code-point.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --lang=smt2.6.1 --produce-models
+; EXPECT: sat
+; EXPECT: ((x "\u{a}"))
+; EXPECT: ((y "\u{7f}"))
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(declare-fun y () String)
+(assert (= (str.to_code x) 10))
+(assert (= (str.to_code y) 127))
+(check-sat)
+(get-value (x))
+(get-value (y))
diff --git a/test/regress/regress0/strings/model-friendly.smt2 b/test/regress/regress0/strings/model-friendly.smt2
new file mode 100644
index 000000000..985ffaa62
--- /dev/null
+++ b/test/regress/regress0/strings/model-friendly.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --lang=smt2.6.1 --produce-models
+; EXPECT: sat
+; EXPECT: ((x "AAAAA"))
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun x () String)
+(assert (= (str.len x) 5))
+(check-sat)
+(get-value (x))
diff --git a/test/regress/regress0/strings/unicode-esc.smt2 b/test/regress/regress0/strings/unicode-esc.smt2
new file mode 100644
index 000000000..01f5f30ab
--- /dev/null
+++ b/test/regress/regress0/strings/unicode-esc.smt2
@@ -0,0 +1,30 @@
+; COMMAND-LINE: --strings-exp --lang=smt2.6.1
+; EXPECT: sat
+(set-logic ALL)
+
+(assert (= "\u{14}" "\u0014"))
+(assert (= "\u{00}" "\u{0}"))
+(assert (= "\u0000" "\u{0}"))
+(assert (= (str.len "\u1234") 1))
+(assert (= (str.len "\u{1}") 1))
+(assert (= (str.len "\u{99}") 1))
+(assert (= (str.len "\u{779}") 1))
+(assert (= (str.len "\u{0779}") 1))
+(assert (= (str.len "\u{01779}") 1))
+(assert (= (str.len "\u{001779}") 10))
+(assert (= (str.len "\u{0vv79}") 9))
+(assert (= (str.len "\u{11\u1234}") 7))
+(assert (= (str.len "\u12345") 2))
+(assert (= (str.len "\uu") 3))
+(assert (= (str.len "\u{123}\u{567}") 2))
+(assert (= (str.len "\u{0017") 7))
+(assert (= (str.len "\\u00178") 3))
+(assert (= (str.len "2\u{}") 5))
+(assert (= (str.len "\uaaaa") 1))
+(assert (= (str.len "\uAAAA") 1))
+(assert (= (str.len "\u{0AbC}") 1))
+(assert (= (str.len "\u{E}") 1))
+(assert (= (str.len "\u{44444}") 9))
+(assert (= (str.len "\u") 2))
+
+(check-sat)
diff --git a/test/regress/regress1/arith/arith-brab-test.smt2 b/test/regress/regress1/arith/arith-brab-test.smt2
new file mode 100644
index 000000000..7856ae0e6
--- /dev/null
+++ b/test/regress/regress1/arith/arith-brab-test.smt2
@@ -0,0 +1,23 @@
+; COMMAND-LINE: --arith-brab
+; COMMAND-LINE: --no-arith-brab
+; EXPECT: sat
+(set-logic ALL)
+
+(declare-fun x1 () Real)
+(declare-fun y1 () Real)
+(declare-fun m1 () Real)
+(declare-fun b1 () Real)
+
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (= y1 (+ b1 (* m1 x1))))
+(assert (= x1 (/ m1 (- y1 b1))))
+(assert (= b1 1.25))
+(assert (= m1 (/ 1 3)))
+
+(assert (and (> x x1) (> y y1)))
+
+(check-sat)
+(exit)
+
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index 27f5aca12..0eefde700 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -556,9 +556,9 @@ void SolverBlack::testMkString()
   TS_ASSERT_THROWS_NOTHING(d_solver->mkString(""));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkString("asdfasdf"));
   TS_ASSERT_EQUALS(d_solver->mkString("asdf\\nasdf").toString(),
-                   "\"asdf\\\\nasdf\"");
-  TS_ASSERT_EQUALS(d_solver->mkString("asdf\\nasdf", true).toString(),
-                   "\"asdf\\nasdf\"");
+                   "\"asdf\\u{5c}nasdf\"");
+  TS_ASSERT_EQUALS(d_solver->mkString("asdf\\u{005c}nasdf", true).toString(),
+                    "\"asdf\\u{5c}nasdf\"");
 }
 
 void SolverBlack::testMkTerm()
diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h
index 34e8d88c6..e1b84492c 100644
--- a/test/unit/theory/theory_strings_skolem_cache_black.h
+++ b/test/unit/theory/theory_strings_skolem_cache_black.h
@@ -20,7 +20,7 @@
 #include "expr/node_manager.h"
 #include "theory/strings/skolem_cache.h"
 #include "util/rational.h"
-#include "util/regexp.h"
+#include "util/string.h"
 
 using namespace CVC4;
 using namespace CVC4::theory::strings;