Merge branch 'master' into fix3959fix3959

27 files changed, 443 insertions, 280 deletions

diff --git a/.travis.yml b/.travis.yml
index 1f646f0de..481a9b9a9 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -28,7 +28,6 @@ addons:
   - python3-setuptools
   - swig3.0
 before_install:
- - eval "${MATRIX_EVAL}"
  # Clang does not play nice with ccache (at least the versions offered by
  # Travis), use a workaround:
  # https://github.com/travis-ci/travis-ci/issues/5383#issuecomment-224630584
@@ -107,22 +106,37 @@ matrix:
     # Test with GCC
     - compiler: gcc
       env:
-        - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='production --language-bindings=java --lfsc' TRAVIS_PYTHON="python"
+        - TRAVIS_CVC4=yes
+        - TRAVIS_WITH_LFSC=yes
+        - TRAVIS_CVC4_CONFIG="production --language-bindings=java --lfsc"
+        - TRAVIS_PYTHON=python
     - compiler: gcc
       env:
-        - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='debug --symfpu --lfsc --no-debug-symbols' TRAVIS_PYTHON="python"
+        - TRAVIS_CVC4=yes
+        - TRAVIS_WITH_LFSC=yes
+        - TRAVIS_CVC4_CONFIG="debug --symfpu --lfsc --no-debug-symbols"
+        - TRAVIS_PYTHON=python
     # Test python bindings
     - compiler: gcc
       env:
-        - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG="production --python-bindings --python2" TRAVIS_PYTHON="python"
+        - TRAVIS_CVC4=yes
+        - TRAVIS_WITH_LFSC=yes
+        - TRAVIS_CVC4_CONFIG="production --python-bindings --python2"
+        - TRAVIS_PYTHON=python
     - compiler: gcc
       env:
-        - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG="production --python-bindings --python3" TRAVIS_PYTHON="python3"
+        - TRAVIS_CVC4=yes
+        - TRAVIS_WITH_LFSC=yes
+        - TRAVIS_CVC4_CONFIG="production --python-bindings --python3"
+        - TRAVIS_PYTHON=python3
     #
     # Test with Clang
     - compiler: clang
       env:
-        - TRAVIS_CVC4=yes TRAVIS_WITH_LFSC=yes TRAVIS_CVC4_CONFIG='debug --symfpu --cln --gpl --no-debug-symbols --no-proofs' TRAVIS_PYTHON="python"
+        - TRAVIS_CVC4=yes
+        - TRAVIS_WITH_LFSC=yes
+        - TRAVIS_CVC4_CONFIG="debug --symfpu --cln --gpl --no-debug-symbols --no-proofs"
+        - TRAVIS_PYTHON=python
 notifications:
   email:
     on_success: change
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 885577260..945f71d36 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -243,6 +243,10 @@ add_check_c_cxx_flag("-Wshadow")
 # cdlist.h warnings. Remove when fixed.
 add_check_cxx_flag("-Wno-class-memaccess")
 
+if (WIN32)
+  set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -Wl,--stack,100000000")
+endif ()
+
 #-----------------------------------------------------------------------------#
 # Use ld.gold if available
 
@@ -670,6 +674,7 @@ message("")
 message("CPPLAGS (-D...)                : ${CVC4_DEFINITIONS}")
 message("CXXFLAGS                       : ${CMAKE_CXX_FLAGS}")
 message("CFLAGS                         : ${CMAKE_C_FLAGS}")
+message("Linker flags                   : ${CMAKE_EXE_LINKER_FLAGS}")
 message("")
 message("Install prefix                 : ${CMAKE_INSTALL_PREFIX}")
 message("")
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 64eb56c74..abfd363f8 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -2331,7 +2331,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes]
       )* RBRACKET
     )?
     {
-      datatypes.push_back(Datatype(PARSER_STATE->getExprManager(),
+      datatypes.push_back(Datatype(SOLVER->getExprManager(),
                                    id,
                                    api::sortVectorToTypes(params),
                                    false));
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 87fa93dcc..e9a037d6e 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -76,11 +76,6 @@ Parser::~Parser() {
   delete d_input;
 }
 
-ExprManager* Parser::getExprManager() const
-{
-  return d_solver->getExprManager();
-}
-
 api::Solver* Parser::getSolver() const { return d_solver; }
 
 api::Term Parser::getSymbol(const std::string& name, SymbolType type)
@@ -339,7 +334,7 @@ void Parser::defineParameterizedType(const std::string& name,
 api::Sort Parser::mkSort(const std::string& name, uint32_t flags)
 {
   Debug("parser") << "newSort(" << name << ")" << std::endl;
-  api::Sort type = getExprManager()->mkSort(name, flags);
+  api::Sort type = d_solver->getExprManager()->mkSort(name, flags);
   defineType(
       name,
       type,
@@ -353,7 +348,8 @@ api::Sort Parser::mkSortConstructor(const std::string& name,
 {
   Debug("parser") << "newSortConstructor(" << name << ", " << arity << ")"
                   << std::endl;
-  api::Sort type = getExprManager()->mkSortConstructor(name, arity, flags);
+  api::Sort type =
+      d_solver->getExprManager()->mkSortConstructor(name, arity, flags);
   defineType(
       name,
       vector<api::Sort>(arity),
@@ -383,7 +379,7 @@ api::Sort Parser::mkUnresolvedTypeConstructor(
 {
   Debug("parser") << "newSortConstructor(P)(" << name << ", " << params.size()
                   << ")" << std::endl;
-  api::Sort unresolved = getExprManager()->mkSortConstructor(
+  api::Sort unresolved = d_solver->getExprManager()->mkSortConstructor(
       name, params.size(), ExprManager::SORT_FLAG_PLACEHOLDER);
   defineType(name, params, unresolved);
   api::Sort t = getSort(name, params);
@@ -404,7 +400,8 @@ std::vector<api::Sort> Parser::mkMutualDatatypeTypes(
   try {
     std::set<Type> tset = api::sortSetToTypes(d_unresolved);
     std::vector<DatatypeType> dtypes =
-        getExprManager()->mkMutualDatatypeTypes(datatypes, tset, flags);
+        d_solver->getExprManager()->mkMutualDatatypeTypes(
+            datatypes, tset, flags);
     std::vector<api::Sort> types;
     for (unsigned i = 0, dtsize = dtypes.size(); i < dtsize; i++)
     {
@@ -593,7 +590,7 @@ api::Term Parser::applyTypeAscription(api::Term t, api::Sort s)
     // parametric datatype.
     if (s.isParametricDatatype())
     {
-      ExprManager* em = getExprManager();
+      ExprManager* em = d_solver->getExprManager();
       // apply type ascription to the operator
       Expr e = t.getExpr();
       const DatatypeConstructor& dtc =
@@ -633,7 +630,8 @@ api::Term Parser::mkVar(const std::string& name,
                         const api::Sort& type,
                         uint32_t flags)
 {
-  return api::Term(getExprManager()->mkVar(name, type.getType(), flags));
+  return api::Term(
+      d_solver->getExprManager()->mkVar(name, type.getType(), flags));
 }
 //!!!!!!!!!!! temporary
 
diff --git a/src/parser/parser.h b/src/parser/parser.h
index c7efcbacb..1197c1ff6 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -265,9 +265,6 @@ public:
 
   virtual ~Parser();
 
-  /** Get the associated <code>ExprManager</code>. */
-  ExprManager* getExprManager() const;
-
   /** Get the associated solver. */
   api::Solver* getSolver() const;
 
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index aa62eab5d..d87c44a68 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -959,7 +959,7 @@ sygusGrammar[CVC4::api::Sort & ret,
       Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl;
       // make the datatype, which encodes terms generated by this non-terminal
       std::string dname = i.first;
-      datatypes.push_back(Datatype(PARSER_STATE->getExprManager(), dname));
+      datatypes.push_back(Datatype(SOLVER->getExprManager(), dname));
       // make its unresolved type, used for referencing the final version of
       // the datatype
       PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
@@ -1537,7 +1537,7 @@ datatypesDef[bool isCo,
           PARSER_STATE->parseError("Wrong number of parameters for datatype.");
         }
         Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
-        dts.push_back(Datatype(PARSER_STATE->getExprManager(), dnames[dts.size()],api::sortVectorToTypes(params),isCo));
+        dts.push_back(Datatype(SOLVER->getExprManager(), dnames[dts.size()],api::sortVectorToTypes(params),isCo));
       }
       LPAREN_TOK
       ( LPAREN_TOK constructorDef[dts.back()] RPAREN_TOK )+
@@ -1547,7 +1547,7 @@ datatypesDef[bool isCo,
           PARSER_STATE->parseError("No parameters given for datatype.");
         }
         Debug("parser-dt") << params.size() << " parameters for " << dnames[dts.size()] << std::endl;
-        dts.push_back(Datatype(PARSER_STATE->getExprManager(),
+        dts.push_back(Datatype(SOLVER->getExprManager(),
                                dnames[dts.size()],
                                api::sortVectorToTypes(params),
                                isCo));
@@ -2532,7 +2532,7 @@ datatypeDef[bool isCo, std::vector<CVC4::Datatype>& datatypes,
      * below. */
   : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); }
     {
-      datatypes.push_back(Datatype(PARSER_STATE->getExprManager(),
+      datatypes.push_back(Datatype(SOLVER->getExprManager(),
                                    id,
                                    api::sortVectorToTypes(params),
                                    isCo));
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 2df73d9e4..c0484e52b 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -1112,7 +1112,7 @@ bool Smt2::pushSygusDatatypeDef(
     std::vector<std::vector<std::string>>& unresolved_gterm_sym)
 {
   sorts.push_back(t);
-  datatypes.push_back(Datatype(getExprManager(), dname));
+  datatypes.push_back(Datatype(d_solver->getExprManager(), dname));
   ops.push_back(std::vector<ParseOp>());
   cnames.push_back(std::vector<std::string>());
   cargs.push_back(std::vector<std::vector<api::Sort>>());
@@ -1573,7 +1573,7 @@ void Smt2::addSygusConstructorVariables(Datatype& dt,
 
 InputLanguage Smt2::getLanguage() const
 {
-  return getExprManager()->getOptions().getInputLanguage();
+  return d_solver->getExprManager()->getOptions().getInputLanguage();
 }
 
 void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type)
@@ -1746,7 +1746,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     }
   }
   // Second phase: apply the arguments to the parse op
-  ExprManager* em = getExprManager();
+  const Options& opts = d_solver->getExprManager()->getOptions();
   // handle special cases
   if (p.d_kind == api::STORE_ALL && !p.d_type.isNull())
   {
@@ -1842,8 +1842,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
   else if (isBuiltinOperator)
   {
     Trace("ajr-temp") << "mkTerm builtin operator" << std::endl;
-    if (!em->getOptions().getUfHo()
-        && (kind == api::EQUAL || kind == api::DISTINCT))
+    if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT))
     {
       // need --uf-ho if these operators are applied over function args
       for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
@@ -1884,7 +1883,7 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       unsigned arity = argt.getFunctionArity();
       if (args.size() - 1 < arity)
       {
-        if (!em->getOptions().getUfHo())
+        if (!opts.getUfHo())
         {
           parseError("Cannot partially apply functions unless --uf-ho is set.");
         }
diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp
index a21cc6785..51b852eac 100644
--- a/src/parser/tptp/tptp.cpp
+++ b/src/parser/tptp/tptp.cpp
@@ -69,20 +69,19 @@ Tptp::~Tptp() {
 }
 
 void Tptp::addTheory(Theory theory) {
-  ExprManager * em = getExprManager();
   switch(theory) {
   case THEORY_CORE:
     //TPTP (CNF and FOF) is unsorted so we define this common type
     {
       std::string d_unsorted_name = "$$unsorted";
-      d_unsorted = api::Sort(em->mkSort(d_unsorted_name));
+      d_unsorted = d_solver->mkUninterpretedSort(d_unsorted_name);
       preemptCommand(
           new DeclareTypeCommand(d_unsorted_name, 0, d_unsorted.getType()));
     }
     // propositionnal
-    defineType("Bool", em->booleanType());
-    defineVar("$true", em->mkConst(true));
-    defineVar("$false", em->mkConst(false));
+    defineType("Bool", d_solver->getBooleanSort());
+    defineVar("$true", d_solver->mkTrue());
+    defineVar("$false", d_solver->mkFalse());
     addOperator(api::AND);
     addOperator(api::EQUAL);
     addOperator(api::IMPLIES);
@@ -312,12 +311,11 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
     isBuiltinKind = true;
   }
   assert(kind != api::NULL_EXPR);
-  ExprManager* em = getExprManager();
+  const Options& opts = d_solver->getExprManager()->getOptions();
   // Second phase: apply parse op to the arguments
   if (isBuiltinKind)
   {
-    if (!em->getOptions().getUfHo()
-        && (kind == api::EQUAL || kind == api::DISTINCT))
+    if (!opts.getUfHo() && (kind == api::EQUAL || kind == api::DISTINCT))
     {
       // need --uf-ho if these operators are applied over function args
       for (std::vector<api::Term>::iterator i = args.begin(); i != args.end();
@@ -352,7 +350,7 @@ api::Term Tptp::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       unsigned arity = argt.getFunctionArity();
       if (args.size() - 1 < arity)
       {
-        if (!em->getOptions().getUfHo())
+        if (!opts.getUfHo())
         {
           parseError("Cannot partially apply functions unless --uf-ho is set.");
         }
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 86dd31da2..79a8904cd 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1174,6 +1174,23 @@ void DeclareFunctionCommandToStream(std::ostream& out,
 
 }  // namespace
 
+void CvcPrinter::toStream(std::ostream& out, const Model& m) const
+{
+  // print the model comments
+  std::stringstream c;
+  m.getComments(c);
+  std::string ln;
+  while (std::getline(c, ln))
+  {
+    out << "; " << ln << std::endl;
+  }
+
+  // print the model
+  out << "MODEL BEGIN" << std::endl;
+  this->Printer::toStream(out, m);
+  out << "MODEL END;" << std::endl;
+}
+
 void CvcPrinter::toStream(std::ostream& out,
                           const Model& model,
                           const Command* command) const
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index d379af7e3..1694ea1ec 100644
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -42,6 +42,7 @@ class CvcPrinter : public CVC4::Printer {
                 bool types,
                 size_t dag) const override;
   void toStream(std::ostream& out, const CommandStatus* s) const override;
+  void toStream(std::ostream& out, const Model& m) const override;
 
  private:
   void toStream(
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 4f93ba745..222b63db5 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -753,7 +753,7 @@ RewriteResponse ArithRewriter::rewriteIntsDivModTotal(TNode t, bool pre){
     Node ret = (k == kind::INTS_DIVISION || k == kind::INTS_DIVISION_TOTAL)
                    ? nm->mkNode(kind::UMINUS, nn)
                    : nn;
-    return RewriteResponse(REWRITE_AGAIN, ret);
+    return RewriteResponse(REWRITE_AGAIN_FULL, ret);
   }
   else if (dIsConstant && n.getKind() == kind::CONST_RATIONAL)
   {
diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp
index 65aaceb80..cbb27197f 100644
--- a/src/theory/arith/arith_utilities.cpp
+++ b/src/theory/arith/arith_utilities.cpp
@@ -224,10 +224,13 @@ Node arithSubstitute(Node n, std::vector<Node>& vars, std::vector<Node>& subs)
       else
       {
         TheoryId ctid = theory::kindToTheoryId(ck);
-        if (ctid != THEORY_ARITH && ctid != THEORY_BOOL
-            && ctid != THEORY_BUILTIN)
+        if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL
+             && ctid != THEORY_BUILTIN)
+            || isTranscendentalKind(ck))
         {
-          // do not traverse beneath applications that belong to another theory
+          // Do not traverse beneath applications that belong to another theory
+          // besides (core) arithmetic. Notice that transcendental function
+          // applications are also not traversed here.
           visited[cur] = cur;
         }
         else
diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp
index d09a138fe..904300004 100644
--- a/src/theory/arith/nl_model.cpp
+++ b/src/theory/arith/nl_model.cpp
@@ -1208,31 +1208,6 @@ bool NlModel::simpleCheckModelMsum(const std::map<Node, Node>& msum, bool pol)
   return comp == d_true;
 }
 
-bool NlModel::isRefineableTfFun(Node tf)
-{
-  Assert(tf.getKind() == SINE || tf.getKind() == EXPONENTIAL);
-  if (tf.getKind() == SINE)
-  {
-    // we do not consider e.g. sin( -1*x ), since considering sin( x ) will
-    // have the same effect. We also do not consider sin(x+y) since this is
-    // handled by introducing a fresh variable (see the map d_tr_base in
-    // NonlinearExtension).
-    if (!tf[0].isVar())
-    {
-      return false;
-    }
-  }
-  // Figure 3 : c
-  Node c = computeAbstractModelValue(tf[0]);
-  Assert(c.isConst());
-  int csign = c.getConst<Rational>().sgn();
-  if (csign == 0)
-  {
-    return false;
-  }
-  return true;
-}
-
 bool NlModel::getApproximateSqrt(Node c, Node& l, Node& u, unsigned iter) const
 {
   Assert(c.isConst());
diff --git a/src/theory/arith/nl_model.h b/src/theory/arith/nl_model.h
index a8746ca2e..5129a7a32 100644
--- a/src/theory/arith/nl_model.h
+++ b/src/theory/arith/nl_model.h
@@ -256,15 +256,6 @@ class NlModel
   bool simpleCheckModelLit(Node lit);
   bool simpleCheckModelMsum(const std::map<Node, Node>& msum, bool pol);
   //---------------------------end check model
-
-  /** is refinable transcendental function
-   *
-   * A transcendental function application is not refineable if its current
-   * model value is zero, or if it is an application of SINE applied
-   * to a non-variable.
-   */
-  bool isRefineableTfFun(Node tf);
-
   /** get approximate sqrt
    *
    * This approximates the square root of positive constant c. If this method
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index cd9352b3a..af384be49 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -781,7 +781,7 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
   Trace("nl-ext-cm-debug") << "  apply pre-substitution..." << std::endl;
   std::vector<Node> pvars;
   std::vector<Node> psubs;
-  for (std::pair<const Node, Node>& tb : d_tr_base)
+  for (std::pair<const Node, Node>& tb : d_trMaster)
   {
     pvars.push_back(tb.first);
     psubs.push_back(tb.second);
@@ -804,18 +804,16 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
   }
 
   // get model bounds for all transcendental functions
-  Trace("nl-ext-cm-debug") << "  get bounds for transcendental functions..."
-                           << std::endl;
-  for (std::pair<const Kind, std::vector<Node> >& tfs : d_f_map)
+  Trace("nl-ext-cm") << "----- Get bounds for transcendental functions..."
+                     << std::endl;
+  for (std::pair<const Kind, std::vector<Node> >& tfs : d_funcMap)
   {
     Kind k = tfs.first;
     for (const Node& tf : tfs.second)
     {
+      Trace("nl-ext-cm") << "- Term: " << tf << std::endl;
       bool success = true;
       // tf is Figure 3 : tf( x )
-      Node atf = d_model.computeConcreteModelValue(tf);
-      Trace("nl-ext-cm-debug")
-          << "Value for is " << tf << " is " << atf << std::endl;
       Node bl;
       Node bu;
       if (k == PI)
@@ -823,41 +821,46 @@ bool NonlinearExtension::checkModel(const std::vector<Node>& assertions,
         bl = d_pi_bound[0];
         bu = d_pi_bound[1];
       }
-      else if (d_model.isRefineableTfFun(tf))
+      else
       {
-        d_model.setUsedApproximate();
         std::pair<Node, Node> bounds = getTfModelBounds(tf, d_taylor_degree);
         bl = bounds.first;
         bu = bounds.second;
+        if (bl != bu)
+        {
+          d_model.setUsedApproximate();
+        }
       }
       if (!bl.isNull() && !bu.isNull())
       {
-        // We have rewritten an application of a transcendental function
-        // based on the current model values.It could be that the model value
-        // rewrites sin(x) ---> sin(-c) ---> -sin(c), thus we need
-        // to negate the bounds in this case.
-        if (atf.getKind() != tf.getKind())
+        // for each function in the congruence classe
+        for (const Node& ctf : d_funcCongClass[tf])
         {
-          if (atf.getKind() == MULT && atf.getNumChildren() == 2
-              && atf[0] == d_neg_one)
+          // each term in congruence classes should be master terms
+          Assert(d_trSlaves.find(ctf) != d_trSlaves.end());
+          // we set the bounds for each slave of tf
+          for (const Node& stf : d_trSlaves[ctf])
           {
-            atf = atf[1];
-            Node btmp = bl;
-            bl = ArithMSum::negate(bu);
-            bu = ArithMSum::negate(btmp);
+            Trace("nl-ext-cm") << "...bound for " << stf << " : [" << bl << ", "
+                               << bu << "]" << std::endl;
+            success = d_model.addCheckModelBound(stf, bl, bu);
           }
         }
-        success = d_model.addCheckModelBound(atf, bl, bu);
+      }
+      else
+      {
+        Trace("nl-ext-cm") << "...no bound for " << tf << std::endl;
       }
       if (!success)
       {
-        Trace("nl-ext-cm-debug")
-            << "...failed to set bound for transcendental function."
-            << std::endl;
+        // a bound was conflicting
+        Trace("nl-ext-cm") << "...failed to set bound for " << tf << std::endl;
+        Trace("nl-ext-cm") << "-----" << std::endl;
         return false;
       }
     }
   }
+  Trace("nl-ext-cm") << "-----" << std::endl;
   bool ret = d_model.checkModel(
       passertions, false_asserts, d_taylor_degree, lemmas, gs);
   return ret;
@@ -923,7 +926,8 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   d_ci.clear();
   d_ci_exp.clear();
   d_ci_max.clear();
-  d_f_map.clear();
+  d_funcCongClass.clear();
+  d_funcMap.clear();
   d_tf_region.clear();
 
   std::vector<Node> lemmas;
@@ -932,7 +936,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   Trace("nl-ext-mv") << "Extended terms : " << std::endl;
   // register the extended function terms
   std::map< Node, Node > mvarg_to_term;
-  std::vector<Node> tr_no_base;
+  std::vector<Node> trNeedsMaster;
   bool needPi = false;
   // for computing congruence
   std::map<Kind, ArgTrie> argTrie;
@@ -943,6 +947,47 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
     d_model.computeAbstractModelValue(a);
     d_model.printModelValue("nl-ext-mv", a);
     Kind ak = a.getKind();
+    bool consider = true;
+    // if is an unpurified application of SINE, or it is a transcendental
+    // applied to a trancendental, purify.
+    if (isTranscendentalKind(ak))
+    {
+      // if we've already computed master for a
+      if (d_trMaster.find(a) != d_trMaster.end())
+      {
+        // a master has at least one slave
+        consider = (d_trSlaves.find(a) != d_trSlaves.end());
+      }
+      else
+      {
+        if (ak == SINE)
+        {
+          // always not a master
+          consider = false;
+        }
+        else
+        {
+          for (const Node& ac : a)
+          {
+            if (isTranscendentalKind(ac.getKind()))
+            {
+              consider = false;
+              break;
+            }
+          }
+        }
+        if (!consider)
+        {
+          // wait to assign a master below
+          trNeedsMaster.push_back(a);
+        }
+        else
+        {
+          d_trMaster[a] = a;
+          d_trSlaves[a].push_back(a);
+        }
+      }
+    }
     if (ak == NONLINEAR_MULT)
     {
       d_ms.push_back( a );
@@ -969,31 +1014,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
       {
         needPi = true;
       }
-      bool consider = true;
-      // if is an unpurified application of SINE, or it is a transcendental
-      // applied to a trancendental, purify.
-      if (isTranscendentalKind(ak))
-      {
-        if (ak == SINE && d_tr_is_base.find(a) == d_tr_is_base.end())
-        {
-          consider = false;
-        }
-        else
-        {
-          for (const Node& ac : a)
-          {
-            if (isTranscendentalKind(ac.getKind()))
-            {
-              consider = false;
-              break;
-            }
-          }
-        }
-        if (!consider)
-        {
-          tr_no_base.push_back(a);
-        }
-      }
+      // if we didn't indicate that it should be purified above
       if( consider ){
         std::vector<Node> repList;
         for (const Node& ac : a)
@@ -1022,14 +1043,19 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
         }
         else
         {
-          d_f_map[ak].push_back(a);
+          // new representative of congruence class
+          d_funcMap[ak].push_back(a);
         }
+        // add to congruence class
+        d_funcCongClass[aa].push_back(a);
       }
     }
     else if (ak == PI)
     {
+      Assert(consider);
       needPi = true;
-      d_f_map[ak].push_back(a);
+      d_funcMap[ak].push_back(a);
+      d_funcCongClass[a].push_back(a);
     }
     else
     {
@@ -1052,47 +1078,50 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   }
 
   // process SINE phase shifting
-  for (const Node& a : tr_no_base)
-  {
-    if (d_tr_base.find(a) == d_tr_base.end())
+  for (const Node& a : trNeedsMaster)
+  {
+    // should not have processed this already
+    Assert(d_trMaster.find(a) == d_trMaster.end());
+    Kind k = a.getKind();
+    Assert(k == SINE || k == EXPONENTIAL);
+    Node y =
+        nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg");
+    Node new_a = nm->mkNode(k, y);
+    d_trSlaves[new_a].push_back(new_a);
+    d_trSlaves[new_a].push_back(a);
+    d_trMaster[a] = new_a;
+    d_trMaster[new_a] = new_a;
+    Node lem;
+    if (k == SINE)
+    {
+      Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a
+                         << std::endl;
+      Assert(!d_pi.isNull());
+      Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts");
+      // TODO : do not introduce shift here, instead needs model-based
+      // refinement for constant shifts (cvc4-projects #1284)
+      lem = nm->mkNode(
+          AND,
+          mkValidPhase(y, d_pi),
+          nm->mkNode(
+              ITE,
+              mkValidPhase(a[0], d_pi),
+              a[0].eqNode(y),
+              a[0].eqNode(nm->mkNode(
+                  PLUS,
+                  y,
+                  nm->mkNode(MULT, nm->mkConst(Rational(2)), shift, d_pi)))),
+          new_a.eqNode(a));
+    }
+    else
     {
-      Node y =
-          nm->mkSkolem("y", nm->realType(), "phase shifted trigonometric arg");
-      Node new_a = nm->mkNode(a.getKind(), y);
-      d_tr_is_base[new_a] = true;
-      d_tr_base[a] = new_a;
-      Node lem;
-      if (a.getKind() == SINE)
-      {
-        Trace("nl-ext-tf") << "Basis sine : " << new_a << " for " << a
-                           << std::endl;
-        Assert(!d_pi.isNull());
-        Node shift = nm->mkSkolem("s", nm->integerType(), "number of shifts");
-        // FIXME : do not introduce shift here, instead needs model-based
-        // refinement for constant shifts (#1284)
-        lem = nm->mkNode(
-            AND,
-            mkValidPhase(y, d_pi),
-            nm->mkNode(
-                ITE,
-                mkValidPhase(a[0], d_pi),
-                a[0].eqNode(y),
-                a[0].eqNode(nm->mkNode(
-                    PLUS,
-                    y,
-                    nm->mkNode(MULT, nm->mkConst(Rational(2)), shift, d_pi)))),
-            new_a.eqNode(a));
-      }
-      else
-      {
-        // do both equalities to ensure that new_a becomes a preregistered term
-        lem = nm->mkNode(AND, a.eqNode(new_a), a[0].eqNode(y));
-      }
-      // must do preprocess on this one
-      Trace("nl-ext-lemma")
-          << "NonlinearExtension::Lemma : purify : " << lem << std::endl;
-      lemsPp.push_back(lem);
+      // do both equalities to ensure that new_a becomes a preregistered term
+      lem = nm->mkNode(AND, a.eqNode(new_a), a[0].eqNode(y));
     }
+    // note we must do preprocess on this lemma
+    Trace("nl-ext-lemma") << "NonlinearExtension::Lemma : purify : " << lem
+                          << std::endl;
+    lemsPp.push_back(lem);
   }
   if (!lemsPp.empty())
   {
@@ -1123,7 +1152,7 @@ int NonlinearExtension::checkLastCall(const std::vector<Node>& assertions,
   {
     Trace("nl-ext-mv") << "Arguments of trancendental functions : "
                        << std::endl;
-    for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
+    for (std::pair<const Kind, std::vector<Node> >& tfl : d_funcMap)
     {
       Kind k = tfl.first;
       if (k == SINE || k == EXPONENTIAL)
@@ -2774,7 +2803,7 @@ std::vector<Node> NonlinearExtension::checkMonomialInferResBounds() {
 std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() {
   std::vector< Node > lemmas;
   Trace("nl-ext") << "Get initial refinement lemmas for transcendental functions..." << std::endl;
-  for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
+  for (std::pair<const Kind, std::vector<Node> >& tfl : d_funcMap)
   {
     Kind k = tfl.first;
     for (const Node& t : tfl.second)
@@ -2788,9 +2817,11 @@ std::vector<Node> NonlinearExtension::checkTranscendentalInitialRefine() {
           Node symn = NodeManager::currentNM()->mkNode(
               SINE, NodeManager::currentNM()->mkNode(MULT, d_neg_one, t[0]));
           symn = Rewriter::rewrite( symn );
-          //can assume its basis since phase is split over 0
-          d_tr_is_base[symn] = true;
-          Assert(d_tr_is_base.find(t) != d_tr_is_base.end());
+          // Can assume it is its own master since phase is split over 0,
+          // hence  -pi <= t[0] <= pi implies -pi <= -t[0] <= pi.
+          d_trMaster[symn] = symn;
+          d_trSlaves[symn].push_back(symn);
+          Assert(d_trSlaves.find(t) != d_trSlaves.end());
           std::vector< Node > children;
 
           lem = NodeManager::currentNM()->mkNode(
@@ -2884,7 +2915,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
   std::map< Kind, std::vector< Node > > sorted_tf_args;
   std::map< Kind, std::map< Node, Node > > tf_arg_to_term;
 
-  for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
+  for (std::pair<const Kind, std::vector<Node> >& tfl : d_funcMap)
   {
     Kind k = tfl.first;
     if (k == EXPONENTIAL || k == SINE)
@@ -2908,7 +2939,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalMonotonic() {
   //sort by concrete values
   smv.d_isConcrete = true;
   smv.d_reverse_order = true;
-  for (std::pair<const Kind, std::vector<Node> >& tfl : d_f_map)
+  for (std::pair<const Kind, std::vector<Node> >& tfl : d_funcMap)
   {
     Kind k = tfl.first;
     if( !sorted_tf_args[k].empty() ){
@@ -3045,7 +3076,7 @@ std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes(
                   << std::endl;
   // this implements Figure 3 of "Satisfiaility Modulo Transcendental Functions
   // via Incremental Linearization" by Cimatti et al
-  for (std::pair<const Kind, std::vector<Node> >& tfs : d_f_map)
+  for (std::pair<const Kind, std::vector<Node> >& tfs : d_funcMap)
   {
     Kind k = tfs.first;
     if (k == PI)
@@ -3070,24 +3101,21 @@ std::vector<Node> NonlinearExtension::checkTranscendentalTangentPlanes(
     for (const Node& tf : tfs.second)
     {
       // tf is Figure 3 : tf( x )
-      if (d_model.isRefineableTfFun(tf))
+      Trace("nl-ext-tftp") << "Compute tangent planes " << tf << std::endl;
+      // go until max degree is reached, or we don't meet bound criteria
+      for (unsigned d = 1; d <= d_taylor_degree; d++)
       {
-        Trace("nl-ext-tftp") << "Compute tangent planes " << tf << std::endl;
-        // go until max degree is reached, or we don't meet bound criteria
-        for (unsigned d = 1; d <= d_taylor_degree; d++)
+        Trace("nl-ext-tftp") << "- run at degree " << d << "..." << std::endl;
+        unsigned prev = lemmas.size();
+        if (checkTfTangentPlanesFun(tf, d, lemmas, lemSE))
         {
-          Trace("nl-ext-tftp") << "- run at degree " << d << "..." << std::endl;
-          unsigned prev = lemmas.size();
-          if (!checkTfTangentPlanesFun(tf, d, lemmas, lemSE))
-          {
-            Trace("nl-ext-tftp")
-                << "...fail, #lemmas = " << (lemmas.size() - prev) << std::endl;
-            break;
-          }
-          else
-          {
-            Trace("nl-ext-tftp") << "...success" << std::endl;
-          }
+          Trace("nl-ext-tftp")
+              << "...fail, #lemmas = " << (lemmas.size() - prev) << std::endl;
+          break;
+        }
+        else
+        {
+          Trace("nl-ext-tftp") << "...success" << std::endl;
         }
       }
     }
@@ -3102,14 +3130,19 @@ bool NonlinearExtension::checkTfTangentPlanesFun(
     std::vector<Node>& lemmas,
     std::map<Node, NlLemmaSideEffect>& lemSE)
 {
-  Assert(d_model.isRefineableTfFun(tf));
-
   NodeManager* nm = NodeManager::currentNM();
   Kind k = tf.getKind();
+  // this should only be run on master applications
+  Assert(d_trSlaves.find(tf) != d_trSlaves.end());
 
   // Figure 3 : c
   Node c = d_model.computeAbstractModelValue(tf[0]);
   int csign = c.getConst<Rational>().sgn();
+  if (csign == 0)
+  {
+    // no secant/tangent plane is necessary
+    return true;
+  }
   Assert(csign == 1 || csign == -1);
 
   // Figure 3: P_l, P_u
@@ -3148,7 +3181,8 @@ bool NonlinearExtension::checkTfTangentPlanesFun(
   Trace("nl-ext-tftp-debug") << "  concavity is : " << concavity << std::endl;
   if (concavity == 0)
   {
-    return false;
+    // no secant/tangent plane is necessary
+    return true;
   }
   // bounds for which we are this concavity
   // Figure 3: < l, u >
@@ -3239,7 +3273,7 @@ bool NonlinearExtension::checkTfTangentPlanesFun(
   else
   {
     // we may want to continue getting better bounds
-    return true;
+    return false;
   }
 
   if (is_tangent)
@@ -3415,7 +3449,7 @@ bool NonlinearExtension::checkTfTangentPlanesFun(
     // secant point c for (tf,d).
     lemSE[lem].d_secantPoint.push_back(std::make_tuple(tf, d, c));
   }
-  return false;
+  return true;
 }
 
 int NonlinearExtension::regionToMonotonicityDir(Kind k, int region)
@@ -3819,11 +3853,21 @@ std::pair<Node, Node> NonlinearExtension::getTfModelBounds(Node tf, unsigned d)
   Node c = d_model.computeAbstractModelValue(tf[0]);
   Assert(c.isConst());
   int csign = c.getConst<Rational>().sgn();
-  Assert(csign != 0);
+  Kind k = tf.getKind();
+  if (csign == 0)
+  {
+    // at zero, its trivial
+    if (k == SINE)
+    {
+      return std::pair<Node, Node>(d_zero, d_zero);
+    }
+    Assert(k == EXPONENTIAL);
+    return std::pair<Node, Node>(d_one, d_one);
+  }
   bool isNeg = csign == -1;
 
   std::vector<Node> pbounds;
-  getPolynomialApproximationBoundForArg(tf.getKind(), c, d, pbounds);
+  getPolynomialApproximationBoundForArg(k, c, d, pbounds);
 
   std::vector<Node> bounds;
   TNode tfv = d_taylor_real_fv;
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index 64a601cc5..2fda9a895 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -511,13 +511,21 @@ class NonlinearExtension {
   
   //transcendental functions
   /**
-   * Maps arguments of SINE applications to a fresh skolem. This is used for
-   * ensuring that the argument of SINE we process are on the interval
-   * [-pi .. pi].
+   * Some transcendental functions f(t) are "purified", e.g. we add
+   * t = y ^ f(t) = f(y) where y is a fresh variable. Those that are not
+   * purified we call "master terms".
+   *
+   * The maps below maintain a master/slave relationship over
+   * transcendental functions (SINE, EXPONENTIAL, PI), where above
+   * f(y) is the master of itself and of f(t).
+   *
+   * This is used for ensuring that the argument y of SINE we process is on the
+   * interval [-pi .. pi], and that exponentials are not applied to arguments
+   * that contain transcendental functions.
    */
-  std::map<Node, Node> d_tr_base;
-  /** Stores skolems in the range of the above map */
-  std::map<Node, bool> d_tr_is_base;
+  std::map<Node, Node> d_trMaster;
+  std::map<Node, std::vector<Node> > d_trSlaves;
+  /** The transcendental functions we have done initial refinements on */
   std::map< Node, bool > d_tf_initial_refine;
 
   void mkPi();
@@ -544,8 +552,24 @@ class NonlinearExtension {
   std::map<Node, std::map<Node, std::map<Node, Node> > > d_ci_exp;
   std::map<Node, std::map<Node, std::map<Node, bool> > > d_ci_max;
 
-  /** A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI } */
-  std::map<Kind, std::vector<Node> > d_f_map;
+  /**
+   * Maps representives of a congruence class to the members of that class.
+   *
+   * In detail, a congruence class is a set of terms of the form
+   *   { f(t1), ..., f(tn) }
+   * such that t1 = ... = tn in the current context. We choose an arbitrary
+   * term among these to be the repesentative of this congruence class.
+   *
+   * Moreover, notice we compute congruence classes only over terms that
+   * are transcendental function applications that are "master terms",
+   * see d_trMaster/d_trSlave.
+   */
+  std::map<Node, std::vector<Node> > d_funcCongClass;
+  /**
+   * A list of all functions for each kind in { EXPONENTIAL, SINE, POW, PI }
+   * that are representives of their congruence class.
+   */
+  std::map<Kind, std::vector<Node> > d_funcMap;
 
   // factor skolems
   std::map< Node, Node > d_factor_skolem;
@@ -644,13 +668,6 @@ class NonlinearExtension {
    * on the model value of its argument.
    */
   std::pair<Node, Node> getTfModelBounds(Node tf, unsigned d);
-  /** is refinable transcendental function
-   *
-   * A transcendental function application is not refineable if its current
-   * model value is zero, or if it is an application of SINE applied
-   * to a non-variable.
-   */
-  bool isRefineableTfFun(Node tf);
   /** get approximate sqrt
    *
    * This approximates the square root of positive constant c. If this method
@@ -953,14 +970,20 @@ class NonlinearExtension {
       std::map<Node, NlLemmaSideEffect>& lemSE);
   /** check transcendental function refinement for tf
    *
-   * This method is called by the above method for each refineable
-   * transcendental function (see isRefineableTfFun) that occurs in an
-   * assertion in the current context.
+   * This method is called by the above method for each "master"
+   * transcendental function application that occurs in an assertion in the
+   * current context. For example, an application like sin(t) is not a master
+   * if we have introduced the constraints:
+   *   t=y+2*pi*n ^ -pi <= y <= pi ^ sin(t) = sin(y).
+   * See d_trMaster/d_trSlaves for more detail.
    *
    * This runs Figure 3 of Cimatti et al., CADE 2017 for transcendental
    * function application tf for Taylor degree d. It may add a secant or
    * tangent plane lemma to lems and its side effect (if one exists)
    * to lemSE.
+   *
+   * It returns false if the bounds are not precise enough to add a
+   * secant or tangent plane lemma.
    */
   bool checkTfTangentPlanesFun(Node tf,
                                unsigned d,
diff --git a/src/theory/strings/core_solver.cpp b/src/theory/strings/core_solver.cpp
index 5414c9b98..e2cafa4d3 100644
--- a/src/theory/strings/core_solver.cpp
+++ b/src/theory/strings/core_solver.cpp
@@ -16,10 +16,10 @@
 
 #include "theory/strings/core_solver.h"
 
-#include "theory/strings/theory_strings_utils.h"
 #include "options/strings_options.h"
 #include "theory/strings/theory_strings_rewriter.h"
-
+#include "theory/strings/theory_strings_utils.h"
+#include "theory/strings/word.h"
 
 using namespace std;
 using namespace CVC4::context;
@@ -37,7 +37,7 @@ 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 = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
+  d_emptyString = Word::mkEmptyWord(CONST_STRING);
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
 }
@@ -1071,10 +1071,10 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     Assert(!d_state.areEqual(x, y));
 
     std::vector<Node> lenExp;
-    Node xLen = d_state.getLength(x, lenExp);
-    Node yLen = d_state.getLength(y, lenExp);
+    Node xLenTerm = d_state.getLength(x, lenExp);
+    Node yLenTerm = d_state.getLength(y, lenExp);
 
-    if (d_state.areEqual(xLen, yLen))
+    if (d_state.areEqual(xLenTerm, yLenTerm))
     {
       // `x` and `y` have the same length. We infer that the two components
       // have to be the same.
@@ -1083,7 +1083,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       Trace("strings-solve-debug")
           << "Simple Case 2 : string lengths are equal" << std::endl;
       Node eq = x.eqNode(y);
-      Node leneq = xLen.eqNode(yLen);
+      Node leneq = xLenTerm.eqNode(yLenTerm);
       NormalForm::getExplanationForPrefixEq(nfi, nfj, index, index, lenExp);
       lenExp.push_back(leneq);
       d_im.sendInference(lenExp, eq, "N_Unify");
@@ -1137,13 +1137,14 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       // Constants in both normal forms.
       //
       // E.g. "abc" ++ ... = "ab" ++ ...
-      String c1 = x.getConst<String>();
-      String c2 = y.getConst<String>();
+      size_t lenX = Word::getLength(x);
+      size_t lenY = Word::getLength(y);
       Trace("strings-solve-debug")
           << "Simple Case 4 : Const Split : " << x << " vs " << y
           << " at index " << index << ", isRev = " << isRev << std::endl;
-      size_t minLen = std::min(c1.size(), c2.size());
-      bool isSameFix = isRev ? c1.rstrncmp(c2, minLen) : c1.strncmp(c2, minLen);
+      size_t minLen = std::min(lenX, lenY);
+      bool isSameFix =
+          isRev ? Word::rstrncmp(x, y, minLen) : Word::strncmp(x, y, minLen);
       if (isSameFix)
       {
         // The shorter constant is a prefix/suffix of the longer constant. We
@@ -1152,20 +1153,20 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         //
         // E.g. "abc" ++ x' ++ ... = "ab" ++ y' ++ ... --->
         //      "c" ++ x' ++ ... = y' ++ ...
-        bool c1Shorter = c1.size() < c2.size();
-        NormalForm& nfl = c1Shorter ? nfj : nfi;
-        const String& cl = c1Shorter ? c2 : c1;
-        Node ns = c1Shorter ? x : y;
+        bool xShorter = lenX < lenY;
+        NormalForm& nfl = xShorter ? nfj : nfi;
+        Node cl = xShorter ? y : x;
+        Node ns = xShorter ? x : y;
 
         Node remainderStr;
         if (isRev)
         {
-          int newlen = cl.size() - minLen;
-          remainderStr = nm->mkConst(cl.substr(0, newlen));
+          size_t newlen = std::max(lenX, lenY) - minLen;
+          remainderStr = Word::substr(cl, 0, newlen);
         }
         else
         {
-          remainderStr = nm->mkConst(cl.substr(minLen));
+          remainderStr = Word::substr(cl, minLen);
         }
         Trace("strings-solve-debug-test")
             << "Break normal form of " << cl << " into " << ns << ", "
@@ -1195,7 +1196,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     info.d_j = nfj.d_base;
     info.d_rev = isRev;
     Assert(index < nfiv.size() - rproc && index < nfjv.size() - rproc);
-    if (!d_state.areDisequal(xLen, yLen) && !d_state.areEqual(xLen, yLen)
+    if (!d_state.areDisequal(xLenTerm, yLenTerm) && !d_state.areEqual(xLenTerm, yLenTerm)
         && !x.isConst()
         && !y.isConst())  // AJR: remove the latter 2 conditions?
     {
@@ -1207,7 +1208,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
       Trace("strings-solve-debug")
           << "Non-simple Case 1 : string lengths neither equal nor disequal"
           << std::endl;
-      Node lenEq = nm->mkNode(EQUAL, xLen, yLen);
+      Node lenEq = nm->mkNode(EQUAL, xLenTerm, yLenTerm);
       lenEq = Rewriter::rewrite(lenEq);
       info.d_conc = nm->mkNode(OR, lenEq, lenEq.negate());
       info.d_pending_phase[lenEq] = true;
@@ -1395,7 +1396,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     // is a prefix/suffix of the other.
     //
     // E.g. x ++ ... = y ++ ... ---> (x = y ++ k) v (y = x ++ k)
-    Assert(d_state.areDisequal(xLen, yLen));
+    Assert(d_state.areDisequal(xLenTerm, yLenTerm));
     Assert(x.getKind() != CONST_STRING);
     Assert(y.getKind() != CONST_STRING);
 
@@ -1411,8 +1412,8 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
         // do not infer constants are larger than variables
         if (t.getKind() != CONST_STRING)
         {
-          Node lt1 = e == 0 ? xLen : yLen;
-          Node lt2 = e == 0 ? yLen : xLen;
+          Node lt1 = e == 0 ? xLenTerm : yLenTerm;
+          Node lt2 = e == 0 ? yLenTerm : xLenTerm;
           Node entLit = Rewriter::rewrite(nm->mkNode(GT, lt1, lt2));
           std::pair<bool, Node> et = d_state.entailmentCheck(
               options::TheoryOfMode::THEORY_OF_TYPE_BASED, entLit);
@@ -1465,7 +1466,7 @@ void CoreSolver::processSimpleNEq(NormalForm& nfi,
     }
     else
     {
-      Node ldeq = nm->mkNode(EQUAL, xLen, yLen).negate();
+      Node ldeq = nm->mkNode(EQUAL, xLenTerm, yLenTerm).negate();
       info.d_ant.push_back(ldeq);
       info.d_conc = nm->mkNode(OR, eq1, eq2);
       info.d_id = INFER_SSPLIT_VAR;
@@ -1625,13 +1626,12 @@ CoreSolver::ProcessLoopResult CoreSolver::processLoop(NormalForm& nfi,
   {
     Trace("strings-loop") << "Strings::Loop: Const Normal Breaking."
                           << std::endl;
-    CVC4::String s = t_yz.getConst<CVC4::String>();
-    unsigned size = s.size();
+    unsigned size = Word::getLength(t_yz);
     std::vector<Node> vconc;
     for (unsigned len = 1; len <= size; len++)
     {
-      Node y = nm->mkConst(s.substr(0, len));
-      Node z = nm->mkConst(s.substr(len, size - len));
+      Node y = Word::substr(t_yz, 0, len);
+      Node z = Word::substr(t_yz, len, size - len);
       Node restr = s_zy;
       Node cc;
       if (r != d_emptyString)
@@ -1770,8 +1770,9 @@ void CoreSolver::processDeq( Node ni, Node nj ) {
                 return;
               }else{
                 //split on first character
-                CVC4::String str = const_k.getConst<String>();
-                Node firstChar = str.size() == 1 ? const_k : NodeManager::currentNM()->mkConst( str.prefix( 1 ) );
+                Node firstChar = Word::getLength(const_k) == 1
+                                     ? const_k
+                                     : Word::prefix(const_k, 1);
                 if (d_state.areEqual(lnck, d_one))
                 {
                   if (d_state.areDisequal(firstChar, nconst_k))
@@ -1947,26 +1948,31 @@ int CoreSolver::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node >&
       if (!d_state.areEqual(i, j))
       {
         if( i.getKind()==kind::CONST_STRING && j.getKind()==kind::CONST_STRING ) {
-          unsigned int len_short = i.getConst<String>().size() < j.getConst<String>().size() ? i.getConst<String>().size() : j.getConst<String>().size();
+          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);
           if( isSameFix ) {
             //same prefix/suffix
             //k is the index of the string that is shorter
-            Node nk = i.getConst<String>().size() < j.getConst<String>().size() ? i : j;
-            Node nl = i.getConst<String>().size() < j.getConst<String>().size() ? j : i;
+            Node nk = lenI < lenJ ? i : j;
+            Node nl = lenI < lenJ ? j : i;
             Node remainderStr;
             if( isRev ){
-              int new_len = nl.getConst<String>().size() - len_short;
-              remainderStr = NodeManager::currentNM()->mkConst( nl.getConst<String>().substr(0, new_len) );
+              int new_len = Word::getLength(nl) - len_short;
+              remainderStr = Word::substr(nl, 0, new_len);
               Trace("strings-solve-debug-test") << "Rev. Break normal form of " << nl << " into " << nk << ", " << remainderStr << std::endl;
             } else {
-              remainderStr = NodeManager::currentNM()->mkConst( nl.getConst<String>().substr( len_short ) );
+              remainderStr = Word::substr(nl, len_short);
               Trace("strings-solve-debug-test") << "Break normal form of " << nl << " into " << nk << ", " << remainderStr << std::endl;
             }
-            if( i.getConst<String>().size() < j.getConst<String>().size() ) {
+            if (lenI < lenJ)
+            {
               nfj.insert( nfj.begin() + index + 1, remainderStr );
               nfj[index] = nfi[index];
-            } else {
+            }
+            else
+            {
               nfi.insert( nfi.begin() + index + 1, remainderStr );
               nfi[index] = nfj[index];
             }
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 530564a35..f91b59834 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -20,6 +20,7 @@
 #include "options/strings_options.h"
 #include "theory/strings/theory_strings_rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
+#include "theory/strings/word.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -29,11 +30,8 @@ namespace theory {
 namespace strings {
 
 RegExpOpr::RegExpOpr()
-    : d_emptyString(NodeManager::currentNM()->mkConst(::CVC4::String(""))),
-      d_true(NodeManager::currentNM()->mkConst(true)),
+    : d_true(NodeManager::currentNM()->mkConst(true)),
       d_false(NodeManager::currentNM()->mkConst(false)),
-      d_emptySingleton(NodeManager::currentNM()->mkNode(kind::STRING_TO_REGEXP,
-                                                        d_emptyString)),
       d_emptyRegexp(NodeManager::currentNM()->mkNode(kind::REGEXP_EMPTY,
                                                      std::vector<Node>{})),
       d_zero(NodeManager::currentNM()->mkConst(::CVC4::Rational(0))),
@@ -42,6 +40,10 @@ RegExpOpr::RegExpOpr()
                                                std::vector<Node>{})),
       d_sigma_star(NodeManager::currentNM()->mkNode(kind::REGEXP_STAR, d_sigma))
 {
+  d_emptyString = Word::mkEmptyWord(CONST_STRING);
+
+  d_emptySingleton =
+      NodeManager::currentNM()->mkNode(STRING_TO_REGEXP, d_emptyString);
   d_lastchar = utils::getAlphabetCardinality() - 1;
 }
 
@@ -295,6 +297,7 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) {
 
   int ret = 1;
   retNode = d_emptyRegexp;
+  NodeManager* nm = NodeManager::currentNM();
 
   PairNodeStr dv = std::make_pair( r, c );
   if( d_deriv_cache.find( dv ) != d_deriv_cache.end() ) {
@@ -332,10 +335,12 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) {
           if(tmp == d_emptyString) {
             ret = 2;
           } else {
-            if (tmp.getConst<CVC4::String>().front() == c.front())
+            if (tmp.getConst<String>().front() == c.front())
             {
-              retNode =  NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP,
-                tmp.getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkConst( tmp.getConst< CVC4::String >().substr(1) ) );
+              retNode =
+                  nm->mkNode(STRING_TO_REGEXP,
+                             Word::getLength(tmp) == 1 ? d_emptyString
+                                                       : Word::substr(tmp, 1));
             } else {
               ret = 2;
             }
@@ -346,10 +351,12 @@ int RegExpOpr::derivativeS( Node r, CVC4::String c, Node &retNode ) {
           if(tmp.getKind() == kind::STRING_CONCAT) {
             Node t2 = tmp[0];
             if(t2.isConst()) {
-              if (t2.getConst<CVC4::String>().front() == c.front())
+              if (t2.getConst<String>().front() == c.front())
               {
-                Node n =  NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP,
-                  tmp.getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkConst( tmp.getConst< CVC4::String >().substr(1) ) );
+                Node n = nm->mkNode(STRING_TO_REGEXP,
+                                    Word::getLength(tmp) == 1
+                                        ? d_emptyString
+                                        : Word::substr(tmp, 1));
                 std::vector< Node > vec_nodes;
                 vec_nodes.push_back(n);
                 for(unsigned i=1; i<tmp.getNumChildren(); i++) {
@@ -541,6 +548,7 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
   Trace("regexp-derive") << "RegExp-derive starts with /" << mkString( r ) << "/, c=" << c << std::endl;
   Node retNode = d_emptyRegexp;
   PairNodeStr dv = std::make_pair( r, c );
+  NodeManager* nm = NodeManager::currentNM();
   if( d_dv_cache.find( dv ) != d_dv_cache.end() ) {
     retNode = d_dv_cache[dv];
   } else if( c.isEmptyString() ){
@@ -576,10 +584,12 @@ Node RegExpOpr::derivativeSingle( Node r, CVC4::String c ) {
           if(r[0] == d_emptyString) {
             retNode = d_emptyRegexp;
           } else {
-            if (r[0].getConst<CVC4::String>().front() == c.front())
+            if (r[0].getConst<String>().front() == c.front())
             {
-              retNode =  NodeManager::currentNM()->mkNode( kind::STRING_TO_REGEXP,
-                r[0].getConst< CVC4::String >().size() == 1 ? d_emptyString : NodeManager::currentNM()->mkConst( r[0].getConst< CVC4::String >().substr(1) ) );
+              retNode = nm->mkNode(STRING_TO_REGEXP,
+                                   Word::getLength(r[0]) == 1
+                                       ? d_emptyString
+                                       : Word::substr(r[0], 1));
             } else {
               retNode = d_emptyRegexp;
             }
@@ -743,7 +753,7 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset)
       case kind::STRING_TO_REGEXP: {
         Node st = Rewriter::rewrite(r[0]);
         if(st.isConst()) {
-          CVC4::String s = st.getConst< CVC4::String >();
+          String s = st.getConst<String>();
           if(s.size() != 0) {
             unsigned sc = s.front();
             sc = String::convertUnsignedIntToCode(sc);
@@ -753,7 +763,7 @@ void RegExpOpr::firstChars(Node r, std::set<unsigned> &pcset, SetNodes &pvset)
         else if (st.getKind() == kind::STRING_CONCAT)
         {
           if(st[0].isConst()) {
-            CVC4::String s = st[0].getConst<CVC4::String>();
+            String s = st[0].getConst<String>();
             unsigned sc = s.front();
             sc = String::convertUnsignedIntToCode(sc);
             cset.insert(sc);
@@ -1638,7 +1648,7 @@ Node RegExpOpr::intersect(Node r1, Node r2, bool &spflag) {
 //printing
 std::string RegExpOpr::niceChar(Node r) {
   if(r.isConst()) {
-    std::string s = r.getConst<CVC4::String>().toString() ;
+    std::string s = r.getConst<String>().toString();
     return s == "." ? "\\." : s;
   } else {
     std::string ss = "$" + r.toString();
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index a5604925c..5015db3f1 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -29,6 +29,7 @@
 #include "theory/strings/theory_strings_rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
 #include "theory/strings/type_enumerator.h"
+#include "theory/strings/word.h"
 #include "theory/theory_model.h"
 #include "theory/valuation.h"
 
@@ -111,7 +112,7 @@ TheoryStrings::TheoryStrings(context::Context* 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 = NodeManager::currentNM()->mkConst( ::CVC4::String("") );
+  d_emptyString = Word::mkEmptyWord(CONST_STRING);
   d_true = NodeManager::currentNM()->mkConst( true );
   d_false = NodeManager::currentNM()->mkConst( false );
 
diff --git a/src/theory/strings/word.cpp b/src/theory/strings/word.cpp
index a0ee0d224..dd573b68c 100644
--- a/src/theory/strings/word.cpp
+++ b/src/theory/strings/word.cpp
@@ -78,6 +78,34 @@ size_t Word::getLength(TNode x)
 
 bool Word::isEmpty(TNode x) { return getLength(x) == 0; }
 
+bool Word::strncmp(TNode x, TNode y, std::size_t n)
+{
+  Kind k = x.getKind();
+  if (k == CONST_STRING)
+  {
+    Assert(y.getKind() == CONST_STRING);
+    String sx = x.getConst<String>();
+    String sy = y.getConst<String>();
+    return sx.strncmp(sy, n);
+  }
+  Unimplemented();
+  return false;
+}
+
+bool Word::rstrncmp(TNode x, TNode y, std::size_t n)
+{
+  Kind k = x.getKind();
+  if (k == CONST_STRING)
+  {
+    Assert(y.getKind() == CONST_STRING);
+    String sx = x.getConst<String>();
+    String sy = y.getConst<String>();
+    return sx.rstrncmp(sy, n);
+  }
+  Unimplemented();
+  return false;
+}
+
 std::size_t Word::find(TNode x, TNode y, std::size_t start)
 {
   Kind k = x.getKind();
diff --git a/src/theory/strings/word.h b/src/theory/strings/word.h
index 74f50ee9a..7b813a0b2 100644
--- a/src/theory/strings/word.h
+++ b/src/theory/strings/word.h
@@ -45,6 +45,22 @@ class Word
   /** Return true if x is empty */
   static bool isEmpty(TNode x);
 
+  /** string compare
+   *
+   * Returns true if x is equal to y for their first n characters.
+   * If n is larger than the length of x or y, this method returns
+   * true if and only if x is equal to y.
+   */
+  static bool strncmp(TNode x, TNode y, std::size_t n);
+
+  /** reverse string compare
+   *
+   * Returns true if x is equal to y for their last n characters.
+   * If n is larger than the length of tx or y, this method returns
+   * true if and only if x is equal to y.
+   */
+  static bool rstrncmp(TNode x, TNode y, std::size_t n);
+
   /** Return the first position y occurs in x, or std::string::npos otherwise */
   static std::size_t find(TNode x, TNode y, std::size_t start = 0);
 
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 4dfe68b51..00066edb6 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -88,8 +88,8 @@ String String::concat(const String &other) const {
   return String(ret_vec);
 }
 
-bool String::strncmp(const String &y, const std::size_t np) const {
-  std::size_t n = np;
+bool String::strncmp(const String& y, std::size_t n) const
+{
   std::size_t b = (size() >= y.size()) ? size() : y.size();
   std::size_t s = (size() <= y.size()) ? size() : y.size();
   if (n > s) {
@@ -105,8 +105,8 @@ bool String::strncmp(const String &y, const std::size_t np) const {
   return true;
 }
 
-bool String::rstrncmp(const String &y, const std::size_t np) const {
-  std::size_t n = np;
+bool String::rstrncmp(const String& y, std::size_t n) const
+{
   std::size_t b = (size() >= y.size()) ? size() : y.size();
   std::size_t s = (size() <= y.size()) ? size() : y.size();
   if (n > s) {
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 1cde53687..731736f72 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -109,8 +109,18 @@ class CVC4_PUBLIC String {
   bool operator<=(const String& y) const { return cmp(y) <= 0; }
   bool operator>=(const String& y) const { return cmp(y) >= 0; }
 
-  bool strncmp(const String& y, const std::size_t np) const;
-  bool rstrncmp(const String& y, const std::size_t np) const;
+  /**
+   * Returns true if this string is equal to y for their first n characters.
+   * If n is larger than the length of this string or y, this method returns
+   * true if and only if this string is equal to y.
+   */
+  bool strncmp(const String& y, std::size_t n) const;
+  /**
+   * Returns true if this string is equal to y for their last n characters.
+   * Similar to strncmp, if n is larger than the length of this string or y,
+   * this method returns true if and only if this string is equal to y.
+   */
+  bool rstrncmp(const String& y, std::size_t n) const;
 
   /* toString
   * Converts this string to a std::string.
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d32a16c13..d96360ad6 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -646,6 +646,7 @@ set(regress_0_tests
   regress0/preprocess/preprocess_14.cvc
   regress0/preprocess/preprocess_15.cvc
   regress0/print_lambda.cvc
+  regress0/print_model.cvc
   regress0/printer/bv_consts_bin.smt2
   regress0/printer/bv_consts_dec.smt2
   regress0/printer/empty_sort.smt2
@@ -1839,6 +1840,7 @@ set(regress_1_tests
   regress1/sygus/issue3649.sy
   regress1/sygus/issue3802-default-consts.sy
   regress1/sygus/issue3839-cond-rewrite.smt2
+  regress1/sygus/issue3944-div-rewrite.smt2
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy
diff --git a/test/regress/regress0/print_lambda.cvc b/test/regress/regress0/print_lambda.cvc
index 548623954..99e5ff174 100644
--- a/test/regress/regress0/print_lambda.cvc
+++ b/test/regress/regress0/print_lambda.cvc
@@ -1,7 +1,9 @@
 % SCRUBBER: sed -e 's/f : (INT) -> INT = (LAMBDA(.*:INT): 0);$/f : (INT) -> INT = (LAMBDA(VAR:INT): 0);/'
 % COMMAND-LINE: --produce-models
 % EXPECT: sat
+% EXPECT: MODEL BEGIN
 % EXPECT: f : (INT) -> INT = (LAMBDA(VAR:INT): 0);
+% EXPECT: MODEL END;
 
 f : INT -> INT;
 ASSERT f(1) = 0;
diff --git a/test/regress/regress0/print_model.cvc b/test/regress/regress0/print_model.cvc
new file mode 100644
index 000000000..0ad9ddf4c
--- /dev/null
+++ b/test/regress/regress0/print_model.cvc
@@ -0,0 +1,12 @@
+% COMMAND-LINE: --produce-models
+% EXPECT: sat
+% EXPECT: MODEL BEGIN
+% EXPECT: s1 : INT = 2;
+% EXPECT: s2 : INT = 1;
+% EXPECT: MODEL END;
+
+OPTION "produce-models";
+s1, s2 : INT;
+ASSERT s1 = 2;
+CHECKSAT s2 > 0 AND s2 < s1;
+COUNTERMODEL;
diff --git a/test/regress/regress1/sygus/issue3944-div-rewrite.smt2 b/test/regress/regress1/sygus/issue3944-div-rewrite.smt2
new file mode 100644
index 000000000..78035790b
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3944-div-rewrite.smt2
@@ -0,0 +1,11 @@
+; EXPECT: sat
+; COMMAND-LINE: --sygus-inference
+(set-logic ALL)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(declare-fun d () Int)
+(assert (= c d))
+(assert (> (+ a (div 0 b)) c))
+(assert (= b (- 1)))
+(check-sat)