Merge branch 'master' into fixClangWarningsfixClangWarnings

95 files changed, 1698 insertions, 864 deletions

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index acc13c2ee..5da6b4208 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -61,10 +61,12 @@ jobs:
       run: |
         sudo apt-get update
         sudo apt-get install -y \
+          build-essential \
           ccache \
           cxxtest \
           libcln-dev \
           libgmp-dev \
+          libgtest-dev \
           libedit-dev \
           flex \
           libfl-dev \
@@ -72,6 +74,10 @@ jobs:
         python3 -m pip install toml
         python3 -m pip install setuptools
         python3 -m pip install pexpect
+        cd /usr/src/googletest
+        sudo cmake .
+        sudo cmake --build . --target install
+        cd -
         echo "/usr/lib/ccache" >> $GITHUB_PATH
 
     # Note: macOS comes with a libedit; it does not need to brew-installed
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 8eab22e4a..6c3ed4bbc 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -8,7 +8,7 @@
 ## All rights reserved.  See the file COPYING in the top-level source
 ## directory for licensing information.
 ##
-cmake_minimum_required(VERSION 3.4)
+cmake_minimum_required(VERSION 3.9)
 
 #-----------------------------------------------------------------------------#
 # Project configuration
diff --git a/INSTALL.md b/INSTALL.md
index b3308726b..5693dbc1c 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -46,7 +46,7 @@ compatible.
 
 - [GNU C and C++ (gcc and g++)](https://gcc.gnu.org)
   or [Clang](https://clang.llvm.org) (reasonably recent versions)
-- [CMake >= 3.1](https://cmake.org)
+- [CMake >= 3.9](https://cmake.org)
 - [GNU Bash](https://www.gnu.org/software/bash/)
 - [Python >= 2.7](https://www.python.org)
   + module [toml](https://pypi.org/project/toml/)
@@ -195,6 +195,12 @@ provided with CVC4.
 See [Testing CVC4](#Testing-CVC4) below for more details.
 
 
+### Google Test Unit Testing Framework (Unit Tests)
+
+[Google Test](https://github.com/google/googletest) is required to optionally
+run CVC4's unit tests (included with the distribution). 
+See [Testing CVC4](#Testing-CVC4) below for more details.
+
 ## Language bindings
 
 CVC4 provides a complete and flexible C++ API (see `examples/api` for
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 869699ac5..e56379f0c 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1137,7 +1137,6 @@ install(FILES
         DESTINATION
           ${CMAKE_INSTALL_INCLUDEDIR}/cvc4)
 install(FILES
-          expr/array.h
           expr/array_store_all.h
           expr/ascription_type.h
           expr/emptyset.h
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 5eabcfe62..748a1ce06 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -354,6 +354,7 @@ const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
         {CVC4::Kind::DISTINCT, DISTINCT},
         {CVC4::Kind::VARIABLE, CONSTANT},
         {CVC4::Kind::BOUND_VARIABLE, VARIABLE},
+        {CVC4::Kind::SEXPR, SEXPR},
         {CVC4::Kind::LAMBDA, LAMBDA},
         {CVC4::Kind::WITNESS, WITNESS},
         /* Boolean --------------------------------------------------------- */
@@ -822,6 +823,14 @@ class CVC4ApiRecoverableExceptionStream
                 << "Invalid argument '" << arg << "' for '" << #arg \
                 << "', expected "
 
+#define CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED(cond, arg)          \
+  CVC4_PREDICT_TRUE(cond)                                           \
+  ? (void)0                                                         \
+  : OstreamVoider()                                                 \
+          & CVC4ApiRecoverableExceptionStream().ostream()           \
+                << "Invalid argument '" << arg << "' for '" << #arg \
+                << "', expected "
+
 #define CVC4_API_ARG_SIZE_CHECK_EXPECTED(cond, arg) \
   CVC4_PREDICT_TRUE(cond)                           \
   ? (void)0                                         \
@@ -842,6 +851,10 @@ class CVC4ApiRecoverableExceptionStream
   {
 #define CVC4_API_SOLVER_TRY_CATCH_END                                          \
   }                                                                            \
+  catch (const UnrecognizedOptionException& e)                                 \
+  {                                                                            \
+    throw CVC4ApiRecoverableException(e.getMessage());                         \
+  }                                                                            \
   catch (const CVC4::RecoverableModalException& e)                             \
   {                                                                            \
     throw CVC4ApiRecoverableException(e.getMessage());                         \
@@ -5083,7 +5096,7 @@ std::vector<Term> Solver::getAssertions(void) const
 std::string Solver::getInfo(const std::string& flag) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_CHECK(d_smtEngine->isValidGetInfoFlag(flag))
+  CVC4_API_RECOVERABLE_CHECK(d_smtEngine->isValidGetInfoFlag(flag))
       << "Unrecognized flag for getInfo.";
 
   return d_smtEngine->getInfo(flag).toString();
@@ -5415,7 +5428,7 @@ void Solver::resetAssertions(void) const
 void Solver::setInfo(const std::string& keyword, const std::string& value) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  CVC4_API_ARG_CHECK_EXPECTED(
+  CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED(
       keyword == "source" || keyword == "category" || keyword == "difficulty"
           || keyword == "filename" || keyword == "license" || keyword == "name"
           || keyword == "notes" || keyword == "smt-lib-version"
@@ -5423,10 +5436,10 @@ void Solver::setInfo(const std::string& keyword, const std::string& value) const
       keyword)
       << "'source', 'category', 'difficulty', 'filename', 'license', 'name', "
          "'notes', 'smt-lib-version' or 'status'";
-  CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2"
-                                  || value == "2.0" || value == "2.5"
-                                  || value == "2.6",
-                              value)
+  CVC4_API_RECOVERABLE_ARG_CHECK_EXPECTED(
+      keyword != "smt-lib-version" || value == "2" || value == "2.0"
+          || value == "2.5" || value == "2.6",
+      value)
       << "'2.0', '2.5', '2.6'";
   CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat"
                                   || value == "unsat" || value == "unknown",
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 18de83e90..391db4bd4 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -9,7 +9,6 @@
 ## directory for licensing information.
 ##
 libcvc4_add_sources(
-  array.h
   array_store_all.cpp
   array_store_all.h
   ascription_type.cpp
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 19efe6285..58dfd973c 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -959,11 +959,13 @@ enum class PfRule : uint32_t
   // fixed length of component i of the regular expression concatenation R.
   RE_UNFOLD_NEG_CONCAT_FIXED,
   // ======== Regular expression elimination
-  // Children: (P:F)
-  // Arguments: none
+  // Children: none
+  // Arguments: (F, b)
   // ---------------------
-  // Conclusion: R
-  // where R = strings::RegExpElimination::eliminate(F).
+  // Conclusion: (= F strings::RegExpElimination::eliminate(F, b))
+  // where b is a Boolean indicating whether we are using aggressive
+  // eliminations. Notice this rule concludes (= F F) if no eliminations
+  // are performed for F.
   RE_ELIM,
   //======================== Code points
   // Children: none
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index 35bed1dbf..d6a632ac5 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -24,7 +24,6 @@
 #include <vector>
 
 #include "base/exception.h"
-#include "expr/expr.h"
 #include "expr/type.h"
 
 namespace CVC4 {
diff --git a/src/expr/type.h b/src/expr/type.h
index 0b923f027..0c70b1667 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -35,9 +35,6 @@ struct CVC4_PUBLIC ExprManagerMapCollection;
 
 class SmtEngine;
 
-class CVC4_PUBLIC Datatype;
-class Record;
-
 template <bool ref_count>
 class NodeTemplate;
 
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index 264d065d6..723f805b7 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -22,8 +22,8 @@
 #include <sstream>
 
 #include "base/check.h"
-#include "expr/expr.h"
 #include "expr/kind.h"
+#include "expr/node.h"
 #include "expr/type_node.h"
 #include "options/language.h"
 
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 673c5ddd9..ab2c8a218 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -209,7 +209,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
             "--tear-down-incremental doesn't work in interactive mode");
       }
       if(!opts.wasSetByUserIncrementalSolving()) {
-        cmd.reset(new SetOptionCommand("incremental", SExpr(true)));
+        cmd.reset(new SetOptionCommand("incremental", "true"));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
       }
@@ -246,7 +246,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) {
         // For tear-down-incremental values greater than 1, need incremental
         // on too.
-        cmd.reset(new SetOptionCommand("incremental", SExpr(true)));
+        cmd.reset(new SetOptionCommand("incremental", "true"));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
         // if(opts.wasSetByUserIncrementalSolving()) {
@@ -410,7 +410,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       }
     } else {
       if(!opts.wasSetByUserIncrementalSolving()) {
-        cmd.reset(new SetOptionCommand("incremental", SExpr(false)));
+        cmd.reset(new SetOptionCommand("incremental", "false"));
         cmd->setMuted(true);
         pExecutor->doCommand(cmd);
       }
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 91c7d0ded..30edf86cd 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -686,7 +686,7 @@ options { backtrack = true; }
 mainCommand[std::unique_ptr<CVC4::Command>* cmd]
 @init {
   api::Term f;
-  SExpr sexpr;
+  api::Term sexpr;
   std::string id;
   api::Sort t;
   std::vector<CVC4::api::DatatypeDecl> dts;
@@ -715,14 +715,14 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
     ( str[s] | IDENTIFIER { s = AntlrInput::tokenText($IDENTIFIER); } )
     ( symbolicExpr[sexpr]
       { if(s == "logic") {
-          cmd->reset(new SetBenchmarkLogicCommand(sexpr.getValue()));
+          cmd->reset(new SetBenchmarkLogicCommand(sexprToString(sexpr)));
         } else {
-          cmd->reset(new SetOptionCommand(s, sexpr));
+          cmd->reset(new SetOptionCommand(s, sexprToString(sexpr)));
         }
       }
-    | TRUE_TOK { cmd->reset(new SetOptionCommand(s, SExpr("true"))); }
-    | FALSE_TOK { cmd->reset(new SetOptionCommand(s, SExpr("false"))); }
-    | { cmd->reset(new SetOptionCommand(s, SExpr("true"))); }
+    | TRUE_TOK { cmd->reset(new SetOptionCommand(s, "true")); }
+    | FALSE_TOK { cmd->reset(new SetOptionCommand(s, "false")); }
+    | { cmd->reset(new SetOptionCommand(s, "true")); }
     )
 
     /* push / pop */
@@ -832,8 +832,8 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
     { UNSUPPORTED("CALL command"); }
 
   | ECHO_TOK
-    ( simpleSymbolicExpr[sexpr]
-      { cmd->reset(new EchoCommand(sexpr.getValue())); }
+    ( simpleSymbolicExpr[s]
+      { cmd->reset(new EchoCommand(s)); }
     | { cmd->reset(new EchoCommand()); }
     )
 
@@ -939,34 +939,31 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
   | toplevelDeclaration[cmd]
   ;
 
-simpleSymbolicExpr[CVC4::SExpr& sexpr]
-@declarations {
-  std::string s;
-  CVC4::Rational r;
-}
+simpleSymbolicExpr[std::string& s]
   : INTEGER_LITERAL
-    { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
+    { s = AntlrInput::tokenText($INTEGER_LITERAL); }
   | MINUS_TOK INTEGER_LITERAL
-    { sexpr = SExpr(-Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
+    { s = std::to_string(MINUS_TOK) + AntlrInput::tokenText($INTEGER_LITERAL); }
   | DECIMAL_LITERAL
-    { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
+    { s = AntlrInput::tokenText($DECIMAL_LITERAL); }
   | HEX_LITERAL
-    { sexpr = SExpr(AntlrInput::tokenText($HEX_LITERAL)); }
+    { s = AntlrInput::tokenText($HEX_LITERAL); }
   | BINARY_LITERAL
-    { sexpr = SExpr(AntlrInput::tokenText($BINARY_LITERAL)); }
+    { s = AntlrInput::tokenText($BINARY_LITERAL); }
   | str[s]
-    { sexpr = SExpr(s); }
   | IDENTIFIER
-    { sexpr = SExpr(AntlrInput::tokenText($IDENTIFIER)); }
+    { s = AntlrInput::tokenText($IDENTIFIER); }
   ;
 
-symbolicExpr[CVC4::SExpr& sexpr]
+symbolicExpr[CVC4::api::Term& sexpr]
 @declarations {
-  std::vector<SExpr> children;
+  std::string s;
+  std::vector<api::Term> children;
 }
-  : simpleSymbolicExpr[sexpr]
+  : simpleSymbolicExpr[s]
+    { sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); }
   | LPAREN (symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN
-    { sexpr = SExpr(children); }
+    { sexpr = SOLVER->mkTerm(CVC4::api::SEXPR, children); }
   ;
 
 /**
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 96a16b31f..686a0d147 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -803,7 +803,6 @@ public:
    */
   api::Term mkStringConstant(const std::string& s);
 
- private:
   /** ad-hoc string escaping
    *
    * Returns the (internal) vector of code points corresponding to processing
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index a7149ed15..c3deabbb7 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -722,29 +722,27 @@ sygusGrammar[CVC4::api::Grammar*& ret,
 setInfoInternal[std::unique_ptr<CVC4::Command>* cmd]
 @declarations {
   std::string name;
-  SExpr sexpr;
+  api::Term sexpr;
 }
   : KEYWORD symbolicExpr[sexpr]
     { name = AntlrInput::tokenText($KEYWORD);
-      PARSER_STATE->setInfo(name.c_str() + 1, sexpr);
-      cmd->reset(new SetInfoCommand(name.c_str() + 1, sexpr));
+      cmd->reset(new SetInfoCommand(name.c_str() + 1, sexprToString(sexpr)));
     }
   ;
 
 setOptionInternal[std::unique_ptr<CVC4::Command>* cmd]
 @init {
   std::string name;
-  SExpr sexpr;
+  api::Term sexpr;
 }
   : keyword[name] symbolicExpr[sexpr]
-    { PARSER_STATE->setOption(name.c_str() + 1, sexpr);
-      cmd->reset(new SetOptionCommand(name.c_str() + 1, sexpr));
+    { cmd->reset(new SetOptionCommand(name.c_str() + 1, sexprToString(sexpr)));
       // Ugly that this changes the state of the parser; but
       // global-declarations affects parsing, so we can't hold off
       // on this until some SmtEngine eventually (if ever) executes it.
       if(name == ":global-declarations")
       {
-        SYM_MAN->setGlobalDeclarations(sexpr.getValue() == "true");
+        SYM_MAN->setGlobalDeclarations(sexprToString(sexpr) == "true");
       }
     }
   ;
@@ -755,7 +753,7 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
   std::string fname;
   CVC4::api::Term expr, expr2;
   std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
-  SExpr sexpr;
+  std::string s;
   CVC4::api::Sort t;
   CVC4::api::Term func;
   std::vector<CVC4::api::Term> bvs;
@@ -786,8 +784,8 @@ smt25Command[std::unique_ptr<CVC4::Command>* cmd]
 
     /* echo */
   | ECHO_TOK
-    ( simpleSymbolicExpr[sexpr]
-      { cmd->reset(new EchoCommand(sexpr.toString())); }
+    ( simpleSymbolicExpr[s]
+      { cmd->reset(new EchoCommand(s)); }
     | { cmd->reset(new EchoCommand()); }
     )
 
@@ -1246,30 +1244,17 @@ datatypesDef[bool isCo,
   }
   ;
 
-simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
-@declarations {
-  CVC4::Kind k;
-  std::string s;
-  std::vector<unsigned int> s_vec;
-}
+simpleSymbolicExprNoKeyword[std::string& s]
   : INTEGER_LITERAL
-    { sexpr = SExpr(Integer(AntlrInput::tokenText($INTEGER_LITERAL))); }
+    { s = AntlrInput::tokenText($INTEGER_LITERAL); }
   | DECIMAL_LITERAL
-    { sexpr = SExpr(AntlrInput::tokenToRational($DECIMAL_LITERAL)); }
+    { s = AntlrInput::tokenText($DECIMAL_LITERAL); }
   | HEX_LITERAL
-    { assert( AntlrInput::tokenText($HEX_LITERAL).find("#x") == 0 );
-      std::string hexString = AntlrInput::tokenTextSubstr($HEX_LITERAL, 2);
-      sexpr = SExpr(Integer(hexString, 16));
-    }
+    { s = AntlrInput::tokenText($HEX_LITERAL); }
   | BINARY_LITERAL
-    { assert( AntlrInput::tokenText($BINARY_LITERAL).find("#b") == 0 );
-      std::string binString = AntlrInput::tokenTextSubstr($BINARY_LITERAL, 2);
-      sexpr = SExpr(Integer(binString, 2));
-    }
+    { s = AntlrInput::tokenText($BINARY_LITERAL); }
   | str[s,false]
-    { sexpr = SExpr(s); }
   | symbol[s,CHECK_NONE,SYM_SORT]
-    { sexpr = SExpr(SExpr::Keyword(s)); }
   | tok=(ASSERT_TOK | CHECK_SAT_TOK | CHECK_SAT_ASSUMING_TOK | DECLARE_FUN_TOK
         | DECLARE_SORT_TOK
         | DEFINE_FUN_TOK | DEFINE_FUN_REC_TOK | DEFINE_FUNS_REC_TOK
@@ -1279,7 +1264,7 @@ simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr]
         | RESET_TOK | RESET_ASSERTIONS_TOK | SET_LOGIC_TOK | SET_INFO_TOK
         | GET_INFO_TOK | SET_OPTION_TOK | GET_OPTION_TOK | PUSH_TOK | POP_TOK
         | DECLARE_DATATYPES_TOK | GET_MODEL_TOK | ECHO_TOK | SIMPLIFY_TOK)
-    { sexpr = SExpr(SExpr::Keyword(AntlrInput::tokenText($tok))); }
+    { s = AntlrInput::tokenText($tok); }
   ;
 
 keyword[std::string& s]
@@ -1287,20 +1272,21 @@ keyword[std::string& s]
     { s = AntlrInput::tokenText($KEYWORD); }
   ;
 
-simpleSymbolicExpr[CVC4::SExpr& sexpr]
-  : simpleSymbolicExprNoKeyword[sexpr]
-  | KEYWORD
-    { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); }
+simpleSymbolicExpr[std::string& s]
+  : simpleSymbolicExprNoKeyword[s]
+  | KEYWORD { s = AntlrInput::tokenText($KEYWORD); }
   ;
 
-symbolicExpr[CVC4::SExpr& sexpr]
+symbolicExpr[CVC4::api::Term& sexpr]
 @declarations {
-  std::vector<SExpr> children;
+  std::string s;
+  std::vector<api::Term> children;
 }
-  : simpleSymbolicExpr[sexpr]
+  : simpleSymbolicExpr[s]
+    { sexpr = SOLVER->mkString(PARSER_STATE->processAdHocStringEsc(s)); }
   | LPAREN_TOK
     ( symbolicExpr[sexpr] { children.push_back(sexpr); } )* RPAREN_TOK
-    { sexpr = SExpr(children); }
+    { sexpr = SOLVER->mkTerm(CVC4::api::SEXPR, children); }
   ;
 
 /**
@@ -1781,13 +1767,14 @@ termAtomic[CVC4::api::Term& atomTerm]
  */
 attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
 @init {
-  SExpr sexpr;
+  api::Term sexpr;
+  std::string s;
   CVC4::api::Term patexpr;
   std::vector<CVC4::api::Term> patexprs;
   CVC4::api::Term e2;
   bool hasValue = false;
 }
-  : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )?
+  : KEYWORD ( simpleSymbolicExprNoKeyword[s] { hasValue = true; } )?
   {
     attr = AntlrInput::tokenText($KEYWORD);
     PARSER_STATE->attributeNotSupported(attr);
@@ -1824,7 +1811,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
   | tok=( ATTRIBUTE_QUANTIFIER_ID_TOK ) symbolicExpr[sexpr]
     {
       api::Sort boolType = SOLVER->getBooleanSort();
-      api::Term avar = SOLVER->mkConst(boolType, sexpr.toString());
+      api::Term avar = SOLVER->mkConst(boolType, sexprToString(sexpr));
       attr = std::string(":qid");
       retExpr = MK_TERM(api::INST_ATTRIBUTE, avar);
       Command* c = new SetUserAttributeCommand("qid", avar);
@@ -1835,7 +1822,7 @@ attribute[CVC4::api::Term& expr, CVC4::api::Term& retExpr, std::string& attr]
     {
       attr = std::string(":named");
       // notify that expression was given a name
-      PARSER_STATE->notifyNamedExpression(expr, sexpr.getValue());
+      PARSER_STATE->notifyNamedExpression(expr, sexprToString(sexpr));
     }
   ;
 
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index b9279fcb0..17f5661b4 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -750,14 +750,6 @@ bool Smt2::sygus_v2() const
   return getLanguage() == language::input::LANG_SYGUS_V2;
 }
 
-void Smt2::setInfo(const std::string& flag, const SExpr& sexpr) {
-  // TODO: ???
-}
-
-void Smt2::setOption(const std::string& flag, const SExpr& sexpr) {
-  // TODO: ???
-}
-
 void Smt2::checkThatLogicIsSet()
 {
   if (!logicIsSet())
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index fd08ab241..654ff9fbf 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -261,10 +261,6 @@ class Smt2 : public Parser
    */
   bool escapeDupDblQuote() const { return v2_5() || sygus(); }
 
-  void setInfo(const std::string& flag, const SExpr& sexpr);
-
-  void setOption(const std::string& flag, const SExpr& sexpr);
-
   void checkThatLogicIsSet();
 
   /**
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g
index 447a867c8..6b66b5422 100644
--- a/src/parser/tptp/Tptp.g
+++ b/src/parser/tptp/Tptp.g
@@ -259,7 +259,7 @@ parseCommand returns [CVC4::Command* cmd = NULL]
       if(filename.substr(filename.length() - 2) == ".p") {
         filename = filename.substr(0, filename.length() - 2);
       }
-      seq->addCommand(new SetInfoCommand("filename", SExpr(filename)));
+      seq->addCommand(new SetInfoCommand("filename", filename));
       if(PARSER_STATE->hasConjecture()) {
         seq->addCommand(new QueryCommand(SOLVER->mkFalse()));
       } else {
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 4b9371181..30b09acae 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -24,10 +24,9 @@
 #include "expr/node_manager_attributes.h"  // for VarNameAttr
 #include "expr/node_visitor.h"
 #include "options/language.h"  // for LANG_AST
-#include "printer/dagification_visitor.h"
+#include "printer/let_binding.h"
 #include "smt/command.h"
 #include "smt/node_command.h"
-#include "theory/substitutions.h"
 
 using namespace std;
 
@@ -41,38 +40,17 @@ void AstPrinter::toStream(std::ostream& out,
                           size_t dag) const
 {
   if(dag != 0) {
-    DagificationVisitor dv(dag);
-    NodeVisitor<DagificationVisitor> visitor;
-    visitor.run(dv, n);
-    const theory::SubstitutionMap& lets = dv.getLets();
-    if(!lets.empty()) {
-      out << "(LET ";
-      bool first = true;
-      for(theory::SubstitutionMap::const_iterator i = lets.begin();
-          i != lets.end();
-          ++i) {
-        if(! first) {
-          out << ", ";
-        } else {
-          first = false;
-        }
-        toStream(out, (*i).second, toDepth, false);
-        out << " := ";
-        toStream(out, (*i).first, toDepth, false);
-      }
-      out << " IN ";
-    }
-    Node body = dv.getDagifiedBody();
-    toStream(out, body, toDepth);
-    if(!lets.empty()) {
-      out << ')';
-    }
+    LetBinding lbind(dag + 1);
+    toStreamWithLetify(out, n, toDepth, &lbind);
   } else {
     toStream(out, n, toDepth);
   }
 }
 
-void AstPrinter::toStream(std::ostream& out, TNode n, int toDepth) const
+void AstPrinter::toStream(std::ostream& out,
+                          TNode n,
+                          int toDepth,
+                          LetBinding* lbind) const
 {
   // null
   if(n.getKind() == kind::NULL_EXPR) {
@@ -96,12 +74,28 @@ void AstPrinter::toStream(std::ostream& out, TNode n, int toDepth) const
     // constant
     out << ' ';
     kind::metakind::NodeValueConstPrinter::toStream(out, n);
-  } else {
+  }
+  else if (n.isClosure())
+  {
+    for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+    {
+      // body is re-letified
+      if (i == 1)
+      {
+        toStreamWithLetify(out, n[i], toDepth, lbind);
+        continue;
+      }
+      toStream(out, n[i], toDepth < 0 ? toDepth : toDepth - 1, lbind);
+    }
+  }
+  else
+  {
     // operator
     if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
       out << ' ';
       if(toDepth != 0) {
-        toStream(out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1);
+        toStream(
+            out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind);
       } else {
         out << "(...)";
       }
@@ -114,7 +108,7 @@ void AstPrinter::toStream(std::ostream& out, TNode n, int toDepth) const
         out << ' ';
       }
       if(toDepth != 0) {
-        toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1);
+        toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, lbind);
       } else {
         out << "(...)";
       }
@@ -394,6 +388,50 @@ void AstPrinter::toStreamCmdComment(std::ostream& out,
   out << "CommentCommand([" << comment << "])" << std::endl;
 }
 
+void AstPrinter::toStreamWithLetify(std::ostream& out,
+                                    Node n,
+                                    int toDepth,
+                                    LetBinding* lbind) const
+{
+  if (lbind == nullptr)
+  {
+    toStream(out, n, toDepth);
+    return;
+  }
+  std::stringstream cparen;
+  std::vector<Node> letList;
+  lbind->letify(n, letList);
+  if (!letList.empty())
+  {
+    std::map<Node, uint32_t>::const_iterator it;
+    out << "(LET ";
+    cparen << ")";
+    bool first = true;
+    for (size_t i = 0, nlets = letList.size(); i < nlets; i++)
+    {
+      if (!first)
+      {
+        out << ", ";
+      }
+      else
+      {
+        first = false;
+      }
+      Node nl = letList[i];
+      uint32_t id = lbind->getId(nl);
+      out << "_let_" << id << " := ";
+      Node nlc = lbind->convert(nl, "_let_", false);
+      toStream(out, nlc, toDepth, lbind);
+    }
+    out << " IN ";
+  }
+  Node nc = lbind->convert(n, "_let_");
+  // print the body, passing the lbind object
+  toStream(out, nc, toDepth, lbind);
+  out << cparen.str();
+  lbind->popScope();
+}
+
 template <class T>
 static bool tryToStream(std::ostream& out, const Command* c)
 {
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index e4251eba0..e0bc7b6bf 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -24,6 +24,9 @@
 #include "printer/printer.h"
 
 namespace CVC4 {
+
+class LetBinding;
+
 namespace printer {
 namespace ast {
 
@@ -162,7 +165,10 @@ class AstPrinter : public CVC4::Printer
       std::ostream& out, const std::vector<Command*>& sequence) const override;
 
  private:
-  void toStream(std::ostream& out, TNode n, int toDepth) const;
+  void toStream(std::ostream& out,
+                TNode n,
+                int toDepth,
+                LetBinding* lbind = nullptr) const;
   /**
    * To stream model sort. This prints the appropriate output for type
    * tn declared via declare-sort or declare-datatype.
@@ -178,6 +184,14 @@ class AstPrinter : public CVC4::Printer
   void toStreamModelTerm(std::ostream& out,
                          const smt::Model& m,
                          Node n) const override;
+  /**
+   * To stream with let binding. This prints n, possibly in the scope
+   * of letification generated by this method based on lbind.
+   */
+  void toStreamWithLetify(std::ostream& out,
+                          Node n,
+                          int toDepth,
+                          LetBinding* lbind) const;
 }; /* class AstPrinter */
 
 }  // namespace ast
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 9e9500bdb..d3e9b48e4 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -40,7 +40,6 @@
 #include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
-#include "theory/substitutions.h"
 #include "theory/theory_model.h"
 #include "util/smt2_quote_string.h"
 
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index e6361be9e..14b9ed0aa 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -29,7 +29,7 @@
 #include "expr/expr_iomanip.h"
 #include "expr/node.h"
 #include "expr/symbol_manager.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 #include "options/options.h"
 #include "options/smt_options.h"
 #include "printer/printer.h"
@@ -45,6 +45,43 @@ using namespace std;
 
 namespace CVC4 {
 
+std::string sexprToString(api::Term sexpr)
+{
+  // if sexpr is a spec constant and not a string, return the result of calling
+  // Term::toString
+  if (sexpr.getKind() == api::CONST_BOOLEAN
+      || sexpr.getKind() == api::CONST_FLOATINGPOINT
+      || sexpr.getKind() == api::CONST_RATIONAL)
+  {
+    return sexpr.toString();
+  }
+
+  // if sexpr is a constant string, return the result of calling Term::toString.
+  // However, strip the surrounding quotes
+  if (sexpr.getKind() == api::CONST_STRING)
+  {
+    return sexpr.toString().substr(1, sexpr.toString().length() - 2);
+  }
+
+  // if sexpr is not a spec constant, make sure it is an array of sub-sexprs
+  Assert(sexpr.getKind() == api::SEXPR);
+
+  std::stringstream ss;
+  auto it = sexpr.begin();
+
+  // recursively print the sub-sexprs
+  ss << '(' << sexprToString(*it);
+  ++it;
+  while (it != sexpr.end())
+  {
+    ss << ' ' << sexprToString(*it);
+    ++it;
+  }
+  ss << ')';
+
+  return ss.str();
+}
+
 const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
 const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
 const CommandInterrupted* CommandInterrupted::s_instance =
@@ -137,11 +174,6 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps)
 
 Command::Command() : d_commandStatus(nullptr), d_muted(false) {}
 
-Command::Command(const api::Solver* solver)
-    : d_commandStatus(nullptr), d_muted(false)
-{
-}
-
 Command::Command(const Command& cmd)
 {
   d_commandStatus =
@@ -1811,7 +1843,7 @@ void BlockModelValuesCommand::invoke(api::Solver* solver, SymbolManager* sm)
     solver->blockModelValues(d_terms);
     d_commandStatus = CommandSuccess::instance();
   }
-  catch (RecoverableModalException& e)
+  catch (api::CVC4ApiRecoverableException& e)
   {
     d_commandStatus = new CommandRecoverableFailure(e.what());
   }
@@ -2520,21 +2552,21 @@ void SetBenchmarkLogicCommand::toStream(std::ostream& out,
 /* class SetInfoCommand                                                       */
 /* -------------------------------------------------------------------------- */
 
-SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr)
+SetInfoCommand::SetInfoCommand(std::string flag, const std::string& sexpr)
     : d_flag(flag), d_sexpr(sexpr)
 {
 }
 
 std::string SetInfoCommand::getFlag() const { return d_flag; }
-SExpr SetInfoCommand::getSExpr() const { return d_sexpr; }
+const std::string& SetInfoCommand::getSExpr() const { return d_sexpr; }
 void SetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
-    solver->getSmtEngine()->setInfo(d_flag, d_sexpr);
+    solver->setInfo(d_flag, d_sexpr);
     d_commandStatus = CommandSuccess::instance();
   }
-  catch (UnrecognizedOptionException&)
+  catch (api::CVC4ApiRecoverableException&)
   {
     // As per SMT-LIB spec, silently accept unknown set-info keys
     d_commandStatus = CommandSuccess::instance();
@@ -2570,23 +2602,13 @@ void GetInfoCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
-    vector<SExpr> v;
-    v.push_back(SExpr(SExpr::Keyword(string(":") + d_flag)));
-    v.emplace_back(solver->getSmtEngine()->getInfo(d_flag));
-    stringstream ss;
-    if (d_flag == "all-options" || d_flag == "all-statistics")
-    {
-      ss << PrettySExprs(true);
-    }
-    ss << SExpr(v);
-    d_result = ss.str();
+    std::vector<api::Term> v;
+    v.push_back(solver->mkString(":" + d_flag));
+    v.push_back(solver->mkString(solver->getInfo(d_flag)));
+    d_result = sexprToString(solver->mkTerm(api::SEXPR, v));
     d_commandStatus = CommandSuccess::instance();
   }
-  catch (UnrecognizedOptionException&)
-  {
-    d_commandStatus = new CommandUnsupported();
-  }
-  catch (RecoverableModalException& e)
+  catch (api::CVC4ApiRecoverableException& e)
   {
     d_commandStatus = new CommandRecoverableFailure(e.what());
   }
@@ -2630,21 +2652,21 @@ void GetInfoCommand::toStream(std::ostream& out,
 /* class SetOptionCommand                                                     */
 /* -------------------------------------------------------------------------- */
 
-SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr)
+SetOptionCommand::SetOptionCommand(std::string flag, const std::string& sexpr)
     : d_flag(flag), d_sexpr(sexpr)
 {
 }
 
 std::string SetOptionCommand::getFlag() const { return d_flag; }
-SExpr SetOptionCommand::getSExpr() const { return d_sexpr; }
+const std::string& SetOptionCommand::getSExpr() const { return d_sexpr; }
 void SetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
-    solver->getSmtEngine()->setOption(d_flag, d_sexpr);
+    solver->setOption(d_flag, d_sexpr);
     d_commandStatus = CommandSuccess::instance();
   }
-  catch (UnrecognizedOptionException&)
+  catch (api::CVC4ApiRecoverableException&)
   {
     d_commandStatus = new CommandUnsupported();
   }
@@ -2682,7 +2704,7 @@ void GetOptionCommand::invoke(api::Solver* solver, SymbolManager* sm)
     d_result = solver->getOption(d_flag);
     d_commandStatus = CommandSuccess::instance();
   }
-  catch (UnrecognizedOptionException&)
+  catch (api::CVC4ApiRecoverableException&)
   {
     d_commandStatus = new CommandUnsupported();
   }
diff --git a/src/smt/command.h b/src/smt/command.h
index 0b86f3539..bfe5e737a 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -29,8 +29,6 @@
 #include <vector>
 
 #include "api/cvc4cpp.h"
-#include "expr/expr.h"
-#include "expr/type.h"
 #include "util/result.h"
 #include "util/sexpr.h"
 
@@ -51,6 +49,16 @@ namespace smt {
 class Model;
 }
 
+/**
+ * Convert a symbolic expression to string. This method differs from
+ * Term::toString in that it does not surround constant strings with double
+ * quote symbols.
+ *
+ * @param sexpr the symbolic expression to convert
+ * @return the symbolic expression as string
+ */
+std::string sexprToString(api::Term sexpr);
+
 std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
 std::ostream& operator<<(std::ostream&, const CommandStatus&) CVC4_PUBLIC;
@@ -198,7 +206,6 @@ class CVC4_PUBLIC Command
   typedef CommandPrintSuccess printsuccess;
 
   Command();
-  Command(const api::Solver* solver);
   Command(const Command& cmd);
 
   virtual ~Command();
@@ -1285,13 +1292,13 @@ class CVC4_PUBLIC SetInfoCommand : public Command
 {
  protected:
   std::string d_flag;
-  SExpr d_sexpr;
+  std::string d_sexpr;
 
  public:
-  SetInfoCommand(std::string flag, const SExpr& sexpr);
+  SetInfoCommand(std::string flag, const std::string& sexpr);
 
   std::string getFlag() const;
-  SExpr getSExpr() const;
+  const std::string& getSExpr() const;
 
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
@@ -1330,13 +1337,13 @@ class CVC4_PUBLIC SetOptionCommand : public Command
 {
  protected:
   std::string d_flag;
-  SExpr d_sexpr;
+  std::string d_sexpr;
 
  public:
-  SetOptionCommand(std::string flag, const SExpr& sexpr);
+  SetOptionCommand(std::string flag, const std::string& sexpr);
 
   std::string getFlag() const;
-  SExpr getSExpr() const;
+  const std::string& getSExpr() const;
 
   void invoke(api::Solver* solver, SymbolManager* sm) override;
   Command* clone() const override;
diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp
index 9d3031b4d..51fcf8b5b 100644
--- a/src/smt/dump_manager.cpp
+++ b/src/smt/dump_manager.cpp
@@ -14,7 +14,6 @@
 
 #include "smt/dump_manager.h"
 
-#include "expr/expr_manager.h"
 #include "options/smt_options.h"
 #include "smt/dump.h"
 #include "smt/node_command.h"
diff --git a/src/smt/listeners.cpp b/src/smt/listeners.cpp
index 7d34f3373..356cfa8a6 100644
--- a/src/smt/listeners.cpp
+++ b/src/smt/listeners.cpp
@@ -15,7 +15,6 @@
 #include "smt/listeners.h"
 
 #include "expr/attribute.h"
-#include "expr/expr.h"
 #include "expr/node_manager_attributes.h"
 #include "options/smt_options.h"
 #include "printer/printer.h"
diff --git a/src/smt/model.cpp b/src/smt/model.cpp
index 8a9f944d2..ccf73dda0 100644
--- a/src/smt/model.cpp
+++ b/src/smt/model.cpp
@@ -49,7 +49,11 @@ Node Model::getValue(TNode n) const { return d_tmodel->getValue(n); }
 
 bool Model::hasApproximations() const { return d_tmodel->hasApproximations(); }
 
-void Model::clearModelDeclarations() { d_declareSorts.clear(); }
+void Model::clearModelDeclarations()
+{
+  d_declareTerms.clear();
+  d_declareSorts.clear();
+}
 
 void Model::addDeclarationSort(TypeNode tn) { d_declareSorts.push_back(tn); }
 
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
index 92d200d40..5c45a6a56 100644
--- a/src/smt/model_blocker.h
+++ b/src/smt/model_blocker.h
@@ -19,7 +19,7 @@
 
 #include <vector>
 
-#include "expr/expr.h"
+#include "expr/node.h"
 #include "options/smt_options.h"
 #include "theory/theory_model.h"
 
diff --git a/src/smt/model_core_builder.h b/src/smt/model_core_builder.h
index 7a28c47f2..327933f1b 100644
--- a/src/smt/model_core_builder.h
+++ b/src/smt/model_core_builder.h
@@ -19,7 +19,7 @@
 
 #include <vector>
 
-#include "expr/expr.h"
+#include "expr/node.h"
 #include "options/smt_options.h"
 #include "theory/theory_model.h"
 
diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index 118b82bec..1916f0162 100644
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -18,7 +18,6 @@
 #define CVC4__SMT__PROOF_MANAGER_H
 
 #include "context/cdlist.h"
-#include "expr/expr.h"
 #include "expr/node.h"
 #include "expr/proof_checker.h"
 #include "expr/proof_node.h"
diff --git a/src/smt/quant_elim_solver.cpp b/src/smt/quant_elim_solver.cpp
index e5ecafd4a..4636cf17a 100644
--- a/src/smt/quant_elim_solver.cpp
+++ b/src/smt/quant_elim_solver.cpp
@@ -14,6 +14,7 @@
 
 #include "smt/quant_elim_solver.h"
 
+#include "expr/skolem_manager.h"
 #include "expr/subs.h"
 #include "smt/smt_solver.h"
 #include "theory/quantifiers/cegqi/nested_qe.h"
@@ -33,7 +34,8 @@ QuantElimSolver::~QuantElimSolver() {}
 
 Node QuantElimSolver::getQuantifierElimination(Assertions& as,
                                                Node q,
-                                               bool doFull)
+                                               bool doFull,
+                                               bool isInternalSubsolver)
 {
   Trace("smt-qe") << "QuantElimSolver: get qe : " << q << std::endl;
   if (q.getKind() != EXISTS && q.getKind() != FORALL)
@@ -41,11 +43,13 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
     throw ModalException(
         "Expecting a quantified formula as argument to get-qe.");
   }
+  NodeManager* nm = NodeManager::currentNM();
+  // ensure the body is rewritten
+  q = nm->mkNode(q.getKind(), q[0], Rewriter::rewrite(q[1]));
   // do nested quantifier elimination if necessary
   q = quantifiers::NestedQe::doNestedQe(q, true);
   Trace("smt-qe") << "QuantElimSolver: after nested quantifier elimination : "
                   << q << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
   // tag the quantified formula with the quant-elim attribute
   TypeNode t = nm->booleanType();
   Node n_attr = nm->mkSkolem("qe", t, "Auxiliary variable for qe attr.");
@@ -121,6 +125,12 @@ Node QuantElimSolver::getQuantifierElimination(Assertions& as,
     // do extended rewrite to minimize the size of the formula aggressively
     theory::quantifiers::ExtendedRewriter extr(true);
     ret = extr.extendedRewrite(ret);
+    // if we are not an internal subsolver, convert to witness form, since
+    // internally generated skolems should not escape
+    if (!isInternalSubsolver)
+    {
+      ret = SkolemManager::getWitnessForm(ret);
+    }
     return ret;
   }
   // otherwise, just true/false
diff --git a/src/smt/quant_elim_solver.h b/src/smt/quant_elim_solver.h
index 96ed1f73d..ca55fc618 100644
--- a/src/smt/quant_elim_solver.h
+++ b/src/smt/quant_elim_solver.h
@@ -79,8 +79,19 @@ class QuantElimSolver
    * extended command get-qe-disjunct, which can be used
    * for incrementally computing the result of a
    * quantifier elimination.
+   *
+   * @param as The assertions of the SmtEngine
+   * @param q The quantified formula we are eliminating quantifiers from
+   * @param doFull Whether we are doing full quantifier elimination on q
+   * @param isInternalSubsolver Whether the SmtEngine we belong to is an
+   * internal subsolver. If it is not, then we convert the final result to
+   * witness form.
+   * @return The result of eliminating quantifiers from q.
    */
-  Node getQuantifierElimination(Assertions& as, Node q, bool doFull);
+  Node getQuantifierElimination(Assertions& as,
+                                Node q,
+                                bool doFull,
+                                bool isInternalSubsolver);
 
  private:
   /** The SMT solver, which is used during doQuantifierElimination. */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0f40db530..2faad7961 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -332,6 +332,7 @@ SmtEngine::~SmtEngine()
     d_absValues.reset(nullptr);
     d_asserts.reset(nullptr);
     d_dumpm.reset(nullptr);
+    d_model.reset(nullptr);
 
     d_sygusSolver.reset(nullptr);
 
@@ -468,11 +469,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
                value.getValue() == "2.6" ) {
       ilang = language::input::LANG_SMTLIB_V2_6;
     }
-    else
-    {
-      Warning() << "Warning: unsupported smt-lib-version: " << value << endl;
-      throw UnrecognizedOptionException();
-    }
     options::inputLanguage.set(ilang);
     // also update the output language
     if (!options::outputLanguage.wasSetByUser())
@@ -497,7 +493,6 @@ void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
     d_state->notifyExpectedStatus(s);
     return;
   }
-  throw UnrecognizedOptionException();
 }
 
 bool SmtEngine::isValidGetInfoFlag(const std::string& key) const
@@ -517,10 +512,6 @@ CVC4::SExpr SmtEngine::getInfo(const std::string& key) const
   SmtScope smts(this);
 
   Trace("smt") << "SMT getInfo(" << key << ")" << endl;
-  if (!isValidGetInfoFlag(key))
-  {
-    throw UnrecognizedOptionException();
-  }
   if (key == "all-statistics")
   {
     vector<SExpr> stats;
@@ -1508,7 +1499,8 @@ Node SmtEngine::getQuantifierElimination(Node q, bool doFull, bool strict)
   if(!d_logic.isPure(THEORY_ARITH) && strict){
     Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl;
   }
-  return d_quantElimSolver->getQuantifierElimination(*d_asserts, q, doFull);
+  return d_quantElimSolver->getQuantifierElimination(
+      *d_asserts, q, doFull, d_isInternalSubsolver);
 }
 
 bool SmtEngine::getInterpol(const Node& conj,
diff --git a/src/smt_util/boolean_simplification.h b/src/smt_util/boolean_simplification.h
index 78d7f8c38..d2fbeb413 100644
--- a/src/smt_util/boolean_simplification.h
+++ b/src/smt_util/boolean_simplification.h
@@ -23,7 +23,6 @@
 #include <algorithm>
 
 #include "base/check.h"
-#include "expr/expr_manager_scope.h"
 #include "expr/node.h"
 
 namespace CVC4 {
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 1e031c322..f4016d032 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -18,7 +18,6 @@
 #include <vector>
 
 #include "base/output.h"
-#include "expr/expr.h"
 #include "expr/node_algorithm.h"
 #include "options/arith_options.h"
 #include "smt/smt_statistics_registry.h"
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 7d7d0c23c..482e3bc21 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -170,31 +170,41 @@ void ExponentialSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx)
   d_data->d_im.addPendingArithLemma(lem, InferenceId::NL_T_TANGENT, nullptr, true);
 }
 
-void ExponentialSolver::doSecantLemmas(
-    TNode e, TNode poly_approx, TNode c, TNode poly_approx_c, unsigned d)
+void ExponentialSolver::doSecantLemmas(TNode e,
+                                       TNode poly_approx,
+                                       TNode center,
+                                       TNode cval,
+                                       unsigned d,
+                                       unsigned actual_d)
 {
-  d_data->doSecantLemmas(
-      getSecantBounds(e, c, d), poly_approx, c, poly_approx_c, e, d, 1);
+  d_data->doSecantLemmas(getSecantBounds(e, center, d),
+                         poly_approx,
+                         center,
+                         cval,
+                         e,
+                         Convexity::CONVEX,
+                         d,
+                         actual_d);
 }
 
 std::pair<Node, Node> ExponentialSolver::getSecantBounds(TNode e,
-                                                         TNode c,
+                                                         TNode center,
                                                          unsigned d)
 {
-  std::pair<Node, Node> bounds = d_data->getClosestSecantPoints(e, c, d);
+  std::pair<Node, Node> bounds = d_data->getClosestSecantPoints(e, center, d);
 
   // Check if we already have neighboring secant points
   if (bounds.first.isNull())
   {
     // pick c-1
     bounds.first = Rewriter::rewrite(
-        NodeManager::currentNM()->mkNode(Kind::MINUS, c, d_data->d_one));
+        NodeManager::currentNM()->mkNode(Kind::MINUS, center, d_data->d_one));
   }
   if (bounds.second.isNull())
   {
     // pick c+1
     bounds.second = Rewriter::rewrite(
-        NodeManager::currentNM()->mkNode(Kind::PLUS, c, d_data->d_one));
+        NodeManager::currentNM()->mkNode(Kind::PLUS, center, d_data->d_one));
   }
   return bounds;
 }
diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h
index b20c23e56..b4d08559a 100644
--- a/src/theory/arith/nl/transcendental/exponential_solver.h
+++ b/src/theory/arith/nl/transcendental/exponential_solver.h
@@ -87,12 +87,16 @@ class ExponentialSolver
   void doTangentLemma(TNode e, TNode c, TNode poly_approx);
 
   /** Sent secant lemmas around c for e */
-  void doSecantLemmas(
-      TNode e, TNode poly_approx, TNode c, TNode poly_approx_c, unsigned d);
+  void doSecantLemmas(TNode e,
+                      TNode poly_approx,
+                      TNode center,
+                      TNode cval,
+                      unsigned d,
+                      unsigned actual_d);
 
  private:
   /** Generate bounds for secant lemmas */
-  std::pair<Node, Node> getSecantBounds(TNode e, TNode c, unsigned d);
+  std::pair<Node, Node> getSecantBounds(TNode e, TNode center, unsigned d);
 
   /** Holds common state for transcendental solvers */
   TranscendentalState* d_data;
diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index 31fd47503..cba85b80e 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -266,19 +266,20 @@ void SineSolver::doTangentLemma(TNode e, TNode c, TNode poly_approx, int region)
   // Figure 3: T( x )
   // We use zero slope tangent planes, since the concavity of the Taylor
   // approximation cannot be easily established.
-  int concavity = regionToConcavity(region);
+  Convexity convexity = regionToConvexity(region);
   int mdir = regionToMonotonicityDir(region);
+  bool usec = (mdir == 1) == (convexity == Convexity::CONCAVE);
   Node lem = nm->mkNode(
       Kind::IMPLIES,
       nm->mkNode(
           Kind::AND,
-          nm->mkNode(Kind::GEQ,
-                     e[0],
-                     mdir == concavity ? Node(c) : regionToLowerBound(region)),
-          nm->mkNode(Kind::LEQ,
-                     e[0],
-                     mdir != concavity ? Node(c) : regionToUpperBound(region))),
-      nm->mkNode(concavity == 1 ? Kind::GEQ : Kind::LEQ, e, poly_approx));
+          nm->mkNode(
+              Kind::GEQ, e[0], usec ? Node(c) : regionToLowerBound(region)),
+          nm->mkNode(
+              Kind::LEQ, e[0], usec ? Node(c) : regionToUpperBound(region))),
+      nm->mkNode(convexity == Convexity::CONVEX ? Kind::GEQ : Kind::LEQ,
+                 e,
+                 poly_approx));
 
   Trace("nl-ext-sine") << "*** Tangent plane lemma (pre-rewrite): " << lem
                        << std::endl;
@@ -294,6 +295,7 @@ void SineSolver::doSecantLemmas(TNode e,
                                 TNode c,
                                 TNode poly_approx_c,
                                 unsigned d,
+                                unsigned actual_d,
                                 int region)
 {
   d_data->doSecantLemmas(getSecantBounds(e, c, d, region),
@@ -301,8 +303,9 @@ void SineSolver::doSecantLemmas(TNode e,
                          c,
                          poly_approx_c,
                          e,
+                         regionToConvexity(region),
                          d,
-                         regionToConcavity(region));
+                         actual_d);
 }
 
 std::pair<Node, Node> SineSolver::getSecantBounds(TNode e,
diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h
index 9f9102a53..e41e6bd4f 100644
--- a/src/theory/arith/nl/transcendental/sine_solver.h
+++ b/src/theory/arith/nl/transcendental/sine_solver.h
@@ -93,6 +93,7 @@ class SineSolver
                       TNode c,
                       TNode poly_approx_c,
                       unsigned d,
+                      unsigned actual_d,
                       int region);
 
  private:
@@ -152,15 +153,15 @@ class SineSolver
       default: return 0;
     }
   }
-  int regionToConcavity(int region)
+  Convexity regionToConvexity(int region)
   {
     switch (region)
     {
       case 1:
-      case 2: return -1;
+      case 2: return Convexity::CONCAVE;
       case 3:
-      case 4: return 1;
-      default: return 0;
+      case 4: return Convexity::CONVEX;
+      default: return Convexity::UNKNOWN;
     }
   }
 
diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp
index a373339e9..1b7257f8f 100644
--- a/src/theory/arith/nl/transcendental/taylor_generator.cpp
+++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp
@@ -212,7 +212,7 @@ void TaylorGenerator::getPolynomialApproximationBounds(
   }
 }
 
-void TaylorGenerator::getPolynomialApproximationBoundForArg(
+unsigned TaylorGenerator::getPolynomialApproximationBoundForArg(
     Kind k, Node c, unsigned d, std::vector<Node>& pbounds)
 {
   getPolynomialApproximationBounds(k, d, pbounds);
@@ -252,7 +252,9 @@ void TaylorGenerator::getPolynomialApproximationBoundForArg(
       getPolynomialApproximationBounds(k, ds, pboundss);
       pbounds[2] = pboundss[2];
     }
+    return ds;
   }
+  return d;
 }
 
 std::pair<Node, Node> TaylorGenerator::getTfModelBounds(Node tf, unsigned d, NlModel& model)
diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h
index c647f7fd2..2dbfcccde 100644
--- a/src/theory/arith/nl/transcendental/taylor_generator.h
+++ b/src/theory/arith/nl/transcendental/taylor_generator.h
@@ -79,11 +79,13 @@ class TaylorGenerator
    * polynomials may depend on c. In particular, for P_u+[x] for <k>( c ) where
    * c>0, we return the P_u+[x] from the function above for the minimum degree
    * d' >= d such that (1-c^{2*d'+1}/(2*d'+1)!) is positive.
+   * @return the actual degree of the polynomial approximations (which may be
+   * larger than d).
    */
-  void getPolynomialApproximationBoundForArg(Kind k,
-                                             Node c,
-                                             unsigned d,
-                                             std::vector<Node>& pbounds);
+  unsigned getPolynomialApproximationBoundForArg(Kind k,
+                                                 Node c,
+                                                 unsigned d,
+                                                 std::vector<Node>& pbounds);
 
   /** get transcendental function model bounds
    *
diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index 8eb69e50b..ad3f49576 100644
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -233,7 +233,8 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d)
   // mapped to for signs of c
   std::map<int, Node> poly_approx_bounds[2];
   std::vector<Node> pbounds;
-  d_tstate.d_taylor.getPolynomialApproximationBoundForArg(k, c, d, pbounds);
+  unsigned actual_d =
+      d_tstate.d_taylor.getPolynomialApproximationBoundForArg(k, c, d, pbounds);
   poly_approx_bounds[0][1] = pbounds[0];
   poly_approx_bounds[0][-1] = pbounds[1];
   poly_approx_bounds[1][1] = pbounds[2];
@@ -362,11 +363,12 @@ bool TranscendentalSolver::checkTfTangentPlanesFun(Node tf, unsigned d)
   {
     if (k == EXPONENTIAL)
     {
-      d_expSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d);
+      d_expSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d, actual_d);
     }
     else if (k == Kind::SINE)
     {
-      d_sineSlv.doSecantLemmas(tf, poly_approx, c, poly_approx_c, d, region);
+      d_sineSlv.doSecantLemmas(
+          tf, poly_approx, c, poly_approx_c, d, actual_d, region);
     }
   }
   return true;
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 41ed2c53d..69678c621 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -267,26 +267,26 @@ void TranscendentalState::getCurrentPiBounds()
 }
 
 std::pair<Node, Node> TranscendentalState::getClosestSecantPoints(TNode e,
-                                                                  TNode c,
+                                                                  TNode center,
                                                                   unsigned d)
 {
   // bounds are the minimum and maximum previous secant points
   // should not repeat secant points: secant lemmas should suffice to
   // rule out previous assignment
-  Assert(
-      std::find(d_secant_points[e][d].begin(), d_secant_points[e][d].end(), c)
-      == d_secant_points[e][d].end());
+  Assert(std::find(
+             d_secant_points[e][d].begin(), d_secant_points[e][d].end(), center)
+         == d_secant_points[e][d].end());
   // Insert into the (temporary) vector. We do not update this vector
   // until we are sure this secant plane lemma has been processed. We do
   // this by mapping the lemma to a side effect below.
   std::vector<Node> spoints = d_secant_points[e][d];
-  spoints.push_back(c);
+  spoints.push_back(center);
 
   // sort
   sortByNlModel(spoints.begin(), spoints.end(), &d_model);
   // get the resulting index of c
   unsigned index =
-      std::find(spoints.begin(), spoints.end(), c) - spoints.begin();
+      std::find(spoints.begin(), spoints.end(), center) - spoints.begin();
 
   // bounds are the next closest upper/lower bound values
   return {index > 0 ? spoints[index - 1] : Node(),
@@ -294,24 +294,40 @@ std::pair<Node, Node> TranscendentalState::getClosestSecantPoints(TNode e,
 }
 
 Node TranscendentalState::mkSecantPlane(
-    TNode arg, TNode b, TNode c, TNode approx_b, TNode approx_c)
+    TNode arg, TNode lower, TNode upper, TNode lval, TNode uval)
 {
   NodeManager* nm = NodeManager::currentNM();
   // Figure 3: S_l( x ), S_u( x ) for s = 0,1
-  Node rcoeff_n = Rewriter::rewrite(nm->mkNode(Kind::MINUS, b, c));
+  Node rcoeff_n = Rewriter::rewrite(nm->mkNode(Kind::MINUS, lower, upper));
   Assert(rcoeff_n.isConst());
   Rational rcoeff = rcoeff_n.getConst<Rational>();
   Assert(rcoeff.sgn() != 0);
-  return nm->mkNode(Kind::PLUS,
-                    approx_b,
-                    nm->mkNode(Kind::MULT,
-                               nm->mkNode(Kind::MINUS, approx_b, approx_c),
-                               nm->mkConst(rcoeff.inverse()),
-                               nm->mkNode(Kind::MINUS, arg, b)));
+  Node res =
+      nm->mkNode(Kind::PLUS,
+                 lval,
+                 nm->mkNode(Kind::MULT,
+                            nm->mkNode(Kind::DIVISION,
+                                       nm->mkNode(Kind::MINUS, lval, uval),
+                                       nm->mkNode(Kind::MINUS, lower, upper)),
+                            nm->mkNode(Kind::MINUS, arg, lower)));
+  Trace("nl-trans") << "Creating secant plane for transcendental function of "
+                    << arg << std::endl;
+  Trace("nl-trans") << "\tfrom ( " << lower << " ; " << lval << " ) to ( "
+                    << upper << " ; " << uval << " )" << std::endl;
+  Trace("nl-trans") << "\t" << res << std::endl;
+  Trace("nl-trans") << "\trewritten: " << Rewriter::rewrite(res) << std::endl;
+  return res;
 }
 
-NlLemma TranscendentalState::mkSecantLemma(
-    TNode lower, TNode upper, int concavity, TNode tf, TNode splane)
+NlLemma TranscendentalState::mkSecantLemma(TNode lower,
+                                           TNode upper,
+                                           TNode lapprox,
+                                           TNode uapprox,
+                                           int csign,
+                                           Convexity convexity,
+                                           TNode tf,
+                                           TNode splane,
+                                           unsigned actual_d)
 {
   NodeManager* nm = NodeManager::currentNM();
   // With respect to Figure 3, this is slightly different.
@@ -329,60 +345,73 @@ NlLemma TranscendentalState::mkSecantLemma(
   Node antec_n = nm->mkNode(Kind::AND,
                             nm->mkNode(Kind::GEQ, tf[0], lower),
                             nm->mkNode(Kind::LEQ, tf[0], upper));
+  Trace("nl-trans") << "Bound for secant plane: " << lower << " <= " << tf[0]
+                    << " <= " << upper << std::endl;
+  Trace("nl-trans") << "\t" << antec_n << std::endl;
+  // Convex: actual value is below the secant
+  // Concave: actual value is above the secant
   Node lem = nm->mkNode(
       Kind::IMPLIES,
       antec_n,
-      nm->mkNode(concavity == 1 ? Kind::LEQ : Kind::GEQ, tf, splane));
-  Trace("nl-ext-tftp-debug2")
-      << "*** Secant plane lemma (pre-rewrite) : " << lem << std::endl;
+      nm->mkNode(
+          convexity == Convexity::CONVEX ? Kind::LEQ : Kind::GEQ, tf, splane));
+  Trace("nl-trans-lemma") << "*** Secant plane lemma (pre-rewrite) : " << lem
+                          << std::endl;
   lem = Rewriter::rewrite(lem);
-  Trace("nl-ext-tftp-lemma") << "*** Secant plane lemma : " << lem << std::endl;
+  Trace("nl-trans-lemma") << "*** Secant plane lemma : " << lem << std::endl;
   Assert(d_model.computeAbstractModelValue(lem) == d_false);
   return NlLemma(lem, LemmaProperty::NONE, nullptr, InferenceId::NL_T_SECANT);
 }
 
 void TranscendentalState::doSecantLemmas(const std::pair<Node, Node>& bounds,
                                          TNode poly_approx,
-                                         TNode c,
-                                         TNode approx_c,
+                                         TNode center,
+                                         TNode cval,
                                          TNode tf,
+                                         Convexity convexity,
                                          unsigned d,
-                                         int concavity)
+                                         unsigned actual_d)
 {
-  Trace("nl-ext-tftp-debug2") << "...secant bounds are : " << bounds.first
-                              << " ... " << bounds.second << std::endl;
-  // take the model value of l or u (since may contain PI)
-  // Make secant from bounds.first to c
-  Node lval = d_model.computeAbstractModelValue(bounds.first);
-  Trace("nl-ext-tftp-debug2") << "...model value of bound " << bounds.first
-                              << " is " << lval << std::endl;
-  if (lval != c)
+  int csign = center.getConst<Rational>().sgn();
+  Trace("nl-trans") << "...do secant lemma with center " << center << " val "
+                    << cval << " sign " << csign << std::endl;
+  Trace("nl-trans") << "...secant bounds are : " << bounds.first << " ... "
+                    << bounds.second << std::endl;
+  // take the model value of lower (since may contain PI)
+  // Make secant from bounds.first to center
+  Node lower = d_model.computeAbstractModelValue(bounds.first);
+  Trace("nl-trans") << "...model value of bound " << bounds.first << " is "
+                    << lower << std::endl;
+  if (lower != center)
   {
     // Figure 3 : P(l), P(u), for s = 0
-    Node approx_l = Rewriter::rewrite(
-        poly_approx.substitute(d_taylor.getTaylorVariable(), lval));
-    Node splane = mkSecantPlane(tf[0], lval, c, approx_l, approx_c);
-    NlLemma nlem = mkSecantLemma(lval, c, concavity, tf, splane);
+    Node lval = Rewriter::rewrite(
+        poly_approx.substitute(d_taylor.getTaylorVariable(), lower));
+    Node splane = mkSecantPlane(tf[0], lower, center, lval, cval);
+    NlLemma nlem = mkSecantLemma(
+        lower, center, lval, cval, csign, convexity, tf, splane, actual_d);
     // The side effect says that if lem is added, then we should add the
     // secant point c for (tf,d).
-    nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c));
+    nlem.d_secantPoint.push_back(std::make_tuple(tf, d, center));
     d_im.addPendingArithLemma(nlem, true);
   }
 
-  // Make secant from c to bounds.second
-  Node uval = d_model.computeAbstractModelValue(bounds.second);
-  Trace("nl-ext-tftp-debug2") << "...model value of bound " << bounds.second
-                              << " is " << uval << std::endl;
-  if (c != uval)
+  // take the model value of upper (since may contain PI)
+  // Make secant from center to bounds.second
+  Node upper = d_model.computeAbstractModelValue(bounds.second);
+  Trace("nl-trans") << "...model value of bound " << bounds.second << " is "
+                    << upper << std::endl;
+  if (center != upper)
   {
     // Figure 3 : P(l), P(u), for s = 1
-    Node approx_u = Rewriter::rewrite(
-        poly_approx.substitute(d_taylor.getTaylorVariable(), uval));
-    Node splane = mkSecantPlane(tf[0], c, uval, approx_c, approx_u);
-    NlLemma nlem = mkSecantLemma(c, uval, concavity, tf, splane);
+    Node uval = Rewriter::rewrite(
+        poly_approx.substitute(d_taylor.getTaylorVariable(), upper));
+    Node splane = mkSecantPlane(tf[0], center, upper, cval, uval);
+    NlLemma nlem = mkSecantLemma(
+        center, upper, cval, uval, csign, convexity, tf, splane, actual_d);
     // The side effect says that if lem is added, then we should add the
     // secant point c for (tf,d).
-    nlem.d_secantPoint.push_back(std::make_tuple(tf, d, c));
+    nlem.d_secantPoint.push_back(std::make_tuple(tf, d, center));
     d_im.addPendingArithLemma(nlem, true);
   }
 }
diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index 0a4e46eca..e1510c3b3 100644
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -27,6 +27,24 @@ namespace nl {
 namespace transcendental {
 
 /**
+ * This enum indicates whether some function is convex, concave or unknown at
+ * some point.
+ */
+enum class Convexity
+{
+  CONVEX,
+  CONCAVE,
+  UNKNOWN
+};
+inline std::ostream& operator<<(std::ostream& os, Convexity c) {
+  switch (c) {
+    case Convexity::CONVEX: return os << "CONVEX";
+    case Convexity::CONCAVE: return os << "CONCAVE";
+    default: return os << "UNKNOWN";
+  }
+}
+
+/**
  * Holds common state and utilities for transcendental solvers.
  *
  * This includes common lookups and caches as well as generic utilities for
@@ -60,20 +78,24 @@ struct TranscendentalState
    * Get the two closest secant points from the once stored already.
    * "closest" is determined according to the current model.
    * @param e The transcendental term (like (exp t))
-   * @param c The point currently under consideration (probably the model of t)
+   * @param center The point currently under consideration (probably the model
+   * of t)
    * @param d The taylor degree.
    */
-  std::pair<Node, Node> getClosestSecantPoints(TNode e, TNode c, unsigned d);
+  std::pair<Node, Node> getClosestSecantPoints(TNode e,
+                                               TNode center,
+                                               unsigned d);
 
   /**
-   * Construct a secant plane between b and c
+   * Construct a secant plane as function in arg between lower and upper
    * @param arg The argument of the transcendental term
-   * @param b Left secant point
-   * @param c Right secant point
-   * @param approx Approximation for b (not yet substituted)
-   * @param approx_c Approximation for c (already substituted)
+   * @param lower Left secant point
+   * @param upper Right secant point
+   * @param lval Evaluation at lower
+   * @param uval Evaluation at upper
    */
-  Node mkSecantPlane(TNode arg, TNode b, TNode c, TNode approx, TNode approx_c);
+  Node mkSecantPlane(
+      TNode arg, TNode lower, TNode upper, TNode lval, TNode uval);
 
   /**
    * Construct a secant lemma between lower and upper for tf.
@@ -83,26 +105,34 @@ struct TranscendentalState
    * @param tf Current transcendental term
    * @param splane Secant plane as computed by mkSecantPlane()
    */
-  NlLemma mkSecantLemma(
-      TNode lower, TNode upper, int concavity, TNode tf, TNode splane);
+  NlLemma mkSecantLemma(TNode lower,
+                        TNode upper,
+                        TNode lapprox,
+                        TNode uapprox,
+                        int csign,
+                        Convexity convexity,
+                        TNode tf,
+                        TNode splane,
+                        unsigned actual_d);
 
   /**
    * Construct and send secant lemmas (if appropriate)
    * @param bounds Secant bounds
    * @param poly_approx Polynomial approximation
-   * @param c Current point
-   * @param approx_c Approximation for c
+   * @param center Current point
+   * @param cval Evaluation at c
    * @param tf Current transcendental term
    * @param d Current taylor degree
    * @param concavity Concavity in region of c
    */
   void doSecantLemmas(const std::pair<Node, Node>& bounds,
                       TNode poly_approx,
-                      TNode c,
-                      TNode approx_c,
+                      TNode center,
+                      TNode cval,
                       TNode tf,
+                      Convexity convexity,
                       unsigned d,
-                      int concavity);
+                      unsigned actual_d);
 
   Node d_true;
   Node d_false;
diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index a0def66c5..a090a58fe 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -21,7 +21,6 @@
 
 #include "expr/dtype.h"
 #include "expr/kind.h"
-#include "expr/type.h"
 #include "expr/type_node.h"
 #include "options/quantifiers_options.h"
 #include "theory/type_enumerator.h"
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 85482bf6d..858710746 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -755,18 +755,20 @@ TypeNode floatingPointTypeInfo::getTypeNode(void) const
 }
 
 FpConverter::FpConverter(context::UserContext* user)
-    :
+    : d_additionalAssertions(user)
 #ifdef CVC4_USE_SYMFPU
+      ,
       d_fpMap(user),
       d_rmMap(user),
       d_boolMap(user),
       d_ubvMap(user),
-      d_sbvMap(user),
+      d_sbvMap(user)
 #endif
-      d_additionalAssertions(user)
 {
 }
 
+FpConverter::~FpConverter() {}
+
 #ifdef CVC4_USE_SYMFPU
 Node FpConverter::ufToNode(const fpt &format, const uf &u) const
 {
diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index 59e65c9e1..6688e8607 100644
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -14,6 +14,8 @@
  ** Uses the symfpu library to convert from floating-point operations to
  ** bit-vectors and propositions allowing the theory to be solved by
  ** 'bit-blasting'.
+ **
+ ** !!! This header is not to be included in any other headers !!!
  **/
 
 #include "cvc4_private.h"
@@ -26,7 +28,7 @@
 #include "context/cdlist.h"
 #include "expr/node.h"
 #include "expr/node_builder.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 #include "theory/valuation.h"
 #include "util/bitvector.h"
 #include "util/floatingpoint_size.h"
@@ -49,10 +51,6 @@ namespace CVC4 {
 namespace theory {
 namespace fp {
 
-typedef PairHashFunction<TypeNode, TypeNode, TypeNodeHashFunction,
-                         TypeNodeHashFunction>
-    PairTypeNodeHashFunction;
-
 /**
  * This is a symfpu symbolic "back-end".  It allows the library to be used to
  * construct bit-vector expressions that compute floating-point operations.
@@ -302,6 +300,20 @@ class floatingPointTypeInfo : public FloatingPointSize
  */
 class FpConverter
 {
+ public:
+  /** Constructor. */
+  FpConverter(context::UserContext*);
+  /** Destructor. */
+  ~FpConverter();
+
+  /** Adds a node to the conversion, returns the converted node */
+  Node convert(TNode);
+
+  /** Gives the node representing the value of a given variable */
+  Node getValue(Valuation&, TNode);
+
+  context::CDList<Node> d_additionalAssertions;
+
  protected:
 #ifdef CVC4_USE_SYMFPU
   typedef symfpuSymbolic::traits traits;
@@ -338,17 +350,6 @@ class FpConverter
   /* Creates the relevant components for a variable */
   uf buildComponents(TNode current);
 #endif
-
- public:
-  context::CDList<Node> d_additionalAssertions;
-
-  FpConverter(context::UserContext *);
-
-  /** Adds a node to the conversion, returns the converted node */
-  Node convert(TNode);
-
-  /** Gives the node representing the value of a given variable */
-  Node getValue(Valuation &, TNode);
 };
 
 }  // namespace fp
diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 0b15486e2..01fab92c8 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -23,6 +23,7 @@
 #include <vector>
 
 #include "options/fp_options.h"
+#include "theory/fp/fp_converter.h"
 #include "theory/fp/theory_fp_rewriter.h"
 #include "theory/rewriter.h"
 #include "theory/theory_model.h"
@@ -108,7 +109,7 @@ TheoryFp::TheoryFp(context::Context* c,
     : Theory(THEORY_FP, c, u, out, valuation, logicInfo, pnm),
       d_notification(*this),
       d_registeredTerms(u),
-      d_conv(u),
+      d_conv(new FpConverter(u)),
       d_expansionRequested(false),
       d_conflictNode(c, Node::null()),
       d_minMap(u),
@@ -116,9 +117,9 @@ TheoryFp::TheoryFp(context::Context* c,
       d_toUBVMap(u),
       d_toSBVMap(u),
       d_toRealMap(u),
-      realToFloatMap(u),
-      floatToRealMap(u),
-      abstractionMap(u),
+      d_realToFloatMap(u),
+      d_floatToRealMap(u),
+      d_abstractionMap(u),
       d_state(c, u, valuation)
 {
   // indicate we are using the default theory state object
@@ -341,10 +342,10 @@ Node TheoryFp::abstractRealToFloat(Node node)
   Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
 
   NodeManager *nm = NodeManager::currentNM();
-  ComparisonUFMap::const_iterator i(realToFloatMap.find(t));
+  ComparisonUFMap::const_iterator i(d_realToFloatMap.find(t));
 
   Node fun;
-  if (i == realToFloatMap.end())
+  if (i == d_realToFloatMap.end())
   {
     std::vector<TypeNode> args(2);
     args[0] = node[0].getType();
@@ -353,7 +354,7 @@ Node TheoryFp::abstractRealToFloat(Node node)
                        nm->mkFunctionType(args, node.getType()),
                        "floatingpoint_abstract_real_to_float",
                        NodeManager::SKOLEM_EXACT_NAME);
-    realToFloatMap.insert(t, fun);
+    d_realToFloatMap.insert(t, fun);
   }
   else
   {
@@ -361,7 +362,7 @@ Node TheoryFp::abstractRealToFloat(Node node)
   }
   Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
 
-  abstractionMap.insert(uf, node);
+  d_abstractionMap.insert(uf, node);
 
   return uf;
 }
@@ -373,10 +374,10 @@ Node TheoryFp::abstractFloatToReal(Node node)
   Assert(t.getKind() == kind::FLOATINGPOINT_TYPE);
 
   NodeManager *nm = NodeManager::currentNM();
-  ComparisonUFMap::const_iterator i(floatToRealMap.find(t));
+  ComparisonUFMap::const_iterator i(d_floatToRealMap.find(t));
 
   Node fun;
-  if (i == floatToRealMap.end())
+  if (i == d_floatToRealMap.end())
   {
     std::vector<TypeNode> args(2);
     args[0] = t;
@@ -385,7 +386,7 @@ Node TheoryFp::abstractFloatToReal(Node node)
                        nm->mkFunctionType(args, nm->realType()),
                        "floatingpoint_abstract_float_to_real",
                        NodeManager::SKOLEM_EXACT_NAME);
-    floatToRealMap.insert(t, fun);
+    d_floatToRealMap.insert(t, fun);
   }
   else
   {
@@ -393,7 +394,7 @@ Node TheoryFp::abstractFloatToReal(Node node)
   }
   Node uf = nm->mkNode(kind::APPLY_UF, fun, node[0], node[1]);
 
-  abstractionMap.insert(uf, node);
+  d_abstractionMap.insert(uf, node);
 
   return uf;
 }
@@ -737,9 +738,9 @@ bool TheoryFp::refineAbstraction(TheoryModel *m, TNode abstract, TNode concrete)
 
 void TheoryFp::convertAndEquateTerm(TNode node) {
   Trace("fp-convertTerm") << "TheoryFp::convertTerm(): " << node << std::endl;
-  size_t oldAdditionalAssertions = d_conv.d_additionalAssertions.size();
+  size_t oldAdditionalAssertions = d_conv->d_additionalAssertions.size();
 
-  Node converted(d_conv.convert(node));
+  Node converted(d_conv->convert(node));
 
   if (converted != node) {
     Debug("fp-convertTerm")
@@ -748,11 +749,11 @@ void TheoryFp::convertAndEquateTerm(TNode node) {
         << "TheoryFp::convertTerm(): after  " << converted << std::endl;
   }
 
-  size_t newAdditionalAssertions = d_conv.d_additionalAssertions.size();
+  size_t newAdditionalAssertions = d_conv->d_additionalAssertions.size();
   Assert(oldAdditionalAssertions <= newAdditionalAssertions);
 
   while (oldAdditionalAssertions < newAdditionalAssertions) {
-    Node addA = d_conv.d_additionalAssertions[oldAdditionalAssertions];
+    Node addA = d_conv->d_additionalAssertions[oldAdditionalAssertions];
 
     Debug("fp-convertTerm") << "TheoryFp::convertTerm(): additional assertion  "
                             << addA << std::endl;
@@ -953,8 +954,8 @@ void TheoryFp::postCheck(Effort level)
     TheoryModel* m = getValuation().getModel();
     bool lemmaAdded = false;
 
-    for (abstractionMapType::const_iterator i = abstractionMap.begin();
-         i != abstractionMap.end();
+    for (AbstractionMap::const_iterator i = d_abstractionMap.begin();
+         i != d_abstractionMap.end();
          ++i)
     {
       if (m->hasTerm((*i).first))
@@ -1016,7 +1017,7 @@ TrustNode TheoryFp::explain(TNode n)
 }
 
 Node TheoryFp::getModelValue(TNode var) {
-  return d_conv.getValue(d_valuation, var);
+  return d_conv->getValue(d_valuation, var);
 }
 
 bool TheoryFp::collectModelInfo(TheoryModel* m,
@@ -1069,14 +1070,16 @@ bool TheoryFp::collectModelValues(TheoryModel* m,
   }
 
   for (std::set<TNode>::const_iterator i(relevantVariables.begin());
-       i != relevantVariables.end(); ++i) {
+       i != relevantVariables.end();
+       ++i)
+  {
     TNode node = *i;
 
     Trace("fp-collectModelInfo")
         << "TheoryFp::collectModelInfo(): relevantVariable " << node
         << std::endl;
 
-    if (!m->assertEquality(node, d_conv.getValue(d_valuation, node), true))
+    if (!m->assertEquality(node, d_conv->getValue(d_valuation, node), true))
     {
       return false;
     }
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 42c009893..fe91a39bd 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -24,7 +24,6 @@
 #include <utility>
 
 #include "context/cdo.h"
-#include "theory/fp/fp_converter.h"
 #include "theory/fp/theory_fp_rewriter.h"
 #include "theory/theory.h"
 #include "theory/uf/equality_engine.h"
@@ -33,7 +32,10 @@ namespace CVC4 {
 namespace theory {
 namespace fp {
 
-class TheoryFp : public Theory {
+class FpConverter;
+
+class TheoryFp : public Theory
+{
  public:
   /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
   TheoryFp(context::Context* c,
@@ -42,8 +44,9 @@ class TheoryFp : public Theory {
            Valuation valuation,
            const LogicInfo& logicInfo,
            ProofNodeManager* pnm = nullptr);
+
   //--------------------------------- initialization
-  /** get the official theory rewriter of this theory */
+  /** Get the official theory rewriter of this theory. */
   TheoryRewriter* getTheoryRewriter() override;
   /**
    * Returns true if we need an equality engine. If so, we initialize the
@@ -51,7 +54,7 @@ class TheoryFp : public Theory {
    * documentation in Theory::needsEqualityEngine.
    */
   bool needsEqualityEngine(EeSetupInfo& esi) override;
-  /** finish initialization */
+  /** Finish initialization. */
   void finishInit() override;
   //--------------------------------- end initialization
 
@@ -77,8 +80,10 @@ class TheoryFp : public Theory {
   Node getModelValue(TNode var) override;
   bool collectModelInfo(TheoryModel* m,
                         const std::set<Node>& relevantTerms) override;
-  /** Collect model values in m based on the relevant terms given by
-   * relevantTerms */
+  /**
+   * Collect model values in m based on the relevant terms given by
+   * relevantTerms.
+   */
   bool collectModelValues(TheoryModel* m,
                           const std::set<Node>& relevantTerms) override;
 
@@ -87,7 +92,20 @@ class TheoryFp : public Theory {
   TrustNode explain(TNode n) override;
 
  protected:
-  /** Equality engine */
+  using PairTypeNodeHashFunction = PairHashFunction<TypeNode,
+                                                    TypeNode,
+                                                    TypeNodeHashFunction,
+                                                    TypeNodeHashFunction>;
+  /** Uninterpreted functions for undefined cases of non-total operators. */
+  using ComparisonUFMap =
+      context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>;
+  /** Uninterpreted functions for lazy handling of conversions. */
+  using ConversionUFMap = context::
+      CDHashMap<std::pair<TypeNode, TypeNode>, Node, PairTypeNodeHashFunction>;
+  using ConversionAbstractionMap = ComparisonUFMap;
+  using AbstractionMap = context::CDHashMap<Node, Node, NodeHashFunction>;
+
+  /** Equality engine. */
   class NotifyClass : public eq::EqualityEngineNotify {
    protected:
     TheoryFp& d_theorySolver;
@@ -108,14 +126,15 @@ class TheoryFp : public Theory {
 
   NotifyClass d_notification;
 
-  /** General utility **/
+  /** General utility. */
   void registerTerm(TNode node);
   bool isRegistered(TNode node);
 
   context::CDHashSet<Node, NodeHashFunction> d_registeredTerms;
 
-  /** Bit-blasting conversion */
-  FpConverter d_conv;
+  /** The word-blaster. Translates FP -> BV. */
+  std::unique_ptr<FpConverter> d_conv;
+
   bool d_expansionRequested;
 
   void convertAndEquateTerm(TNode node);
@@ -133,44 +152,30 @@ class TheoryFp : public Theory {
    */
   void conflictEqConstantMerge(TNode t1, TNode t2);
 
-  context::CDO<Node> d_conflictNode;
-
-  typedef context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>
-      ComparisonUFMap;
-
-  ComparisonUFMap d_minMap;
-  ComparisonUFMap d_maxMap;
+  bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
 
   Node minUF(Node);
   Node maxUF(Node);
 
-  typedef context::CDHashMap<std::pair<TypeNode, TypeNode>, Node,
-                             PairTypeNodeHashFunction>
-      ConversionUFMap;
-
-  ConversionUFMap d_toUBVMap;
-  ConversionUFMap d_toSBVMap;
-
   Node toUBVUF(Node);
   Node toSBVUF(Node);
 
-  ComparisonUFMap d_toRealMap;
-
   Node toRealUF(Node);
 
-  /** Uninterpretted functions for lazy handling of conversions */
-  typedef ComparisonUFMap conversionAbstractionMap;
-
-  conversionAbstractionMap realToFloatMap;
-  conversionAbstractionMap floatToRealMap;
-
   Node abstractRealToFloat(Node);
   Node abstractFloatToReal(Node);
 
-  typedef context::CDHashMap<Node, Node, NodeHashFunction> abstractionMapType;
-  abstractionMapType abstractionMap;  // abstract -> original
+ private:
+  context::CDO<Node> d_conflictNode;
 
-  bool refineAbstraction(TheoryModel* m, TNode abstract, TNode concrete);
+  ComparisonUFMap d_minMap;
+  ComparisonUFMap d_maxMap;
+  ConversionUFMap d_toUBVMap;
+  ConversionUFMap d_toSBVMap;
+  ComparisonUFMap d_toRealMap;
+  ConversionAbstractionMap d_realToFloatMap;
+  ConversionAbstractionMap d_floatToRealMap;
+  AbstractionMap d_abstractionMap;  // abstract -> original
 
   /** The theory rewriter for this theory. */
   TheoryFpRewriter d_rewriter;
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 1a67a2b16..1d917b8f4 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -156,7 +156,11 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
         {
           d_parent_quant[q].push_back(qi);
           d_children_quant[qi].push_back(q);
-          Assert(hasAddedCbqiLemma(qi));
+          // may not have added the CEX lemma, but the literal is created by
+          // the following call regardless. One rare case where this can happen
+          // is if both sygus-inst and CEGQI are being run in parallel, and
+          // a parent quantified formula is not handled by CEGQI, but a child
+          // is.
           Node qicel = getCounterexampleLiteral(qi);
           dep.push_back(qi);
           dep.push_back(qicel);
@@ -164,6 +168,9 @@ bool InstStrategyCegqi::registerCbqiLemma(Node q)
       }
       if (!dep.empty())
       {
+        // This lemma states that if the child is active, then the parent must
+        // be asserted, in particular G => Q where G is the CEX literal for the
+        // child and Q is the parent.
         Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep));
         Trace("cegqi-lemma")
             << "Counterexample dependency lemma : " << dep_lemma << std::endl;
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index aa0e62891..a3938412d 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -21,8 +21,7 @@
 #include <memory>
 #include <vector>
 
-#include "expr/expr.h"
-#include "expr/expr_manager.h"
+#include "expr/node.h"
 #include "smt/smt_engine.h"
 #include "theory/quantifiers/sygus_sampler.h"
 
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.h b/src/theory/quantifiers/sygus/sygus_abduct.h
index 9fc8e703c..d39d2a377 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.h
+++ b/src/theory/quantifiers/sygus/sygus_abduct.h
@@ -19,7 +19,7 @@
 #include <string>
 #include <vector>
 #include "expr/node.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.h b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
index acafeec3c..48a5dbe06 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.h
@@ -24,7 +24,6 @@
 
 #include "expr/node.h"
 #include "expr/sygus_datatype.h"
-#include "expr/type.h"
 #include "expr/type_node.h"
 #include "theory/quantifiers/term_util.h"
 
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index 916f2d9b5..4db5f261a 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -20,7 +20,7 @@
 #include <vector>
 
 #include "expr/node.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 #include "smt/smt_engine.h"
 
 namespace CVC4 {
diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.h b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
index 2c49d9f58..545b35af0 100644
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.h
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.h
@@ -18,7 +18,7 @@
 #include <string>
 #include <vector>
 #include "expr/node.h"
-#include "expr/type.h"
+#include "expr/type_node.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 297f11690..da9fdd022 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -336,6 +336,8 @@ bool QuantifiersEngine::getBoundElements(RepSetIterator* rsi,
 
 void QuantifiersEngine::presolve() {
   Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl;
+  d_lemmas_waiting.clear();
+  d_phase_req_waiting.clear();
   for( unsigned i=0; i<d_modules.size(); i++ ){
     d_modules[i]->presolve();
   }
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index f68900ccc..e2742c812 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -22,7 +22,6 @@
 #include <memory>
 #include <vector>
 
-#include "expr/expr_manager.h"
 #include "expr/node.h"
 #include "smt/smt_engine.h"
 
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index 0b6cf6652..2726097bc 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -438,9 +438,20 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
   }
   else if (id == PfRule::RE_ELIM)
   {
-    Assert(children.size() == 1);
-    Assert(args.empty());
-    return RegExpElimination::eliminate(children[0]);
+    Assert(children.empty());
+    Assert(args.size() == 2);
+    bool isAgg;
+    if (!getBool(args[1], isAgg))
+    {
+      return Node::null();
+    }
+    Node ea = RegExpElimination::eliminate(args[0], isAgg);
+    // if we didn't eliminate, then this trivially proves the reflexive equality
+    if (ea.isNull())
+    {
+      ea = args[0];
+    }
+    return args[0].eqNode(ea);
   }
   else if (id == PfRule::STRING_CODE_INJ)
   {
diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index 1d0db0e4d..aaa9ffc48 100644
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -20,30 +20,58 @@
 #include "theory/strings/regexp_entail.h"
 #include "theory/strings/theory_strings_utils.h"
 
-using namespace CVC4;
 using namespace CVC4::kind;
-using namespace CVC4::theory;
-using namespace CVC4::theory::strings;
 
-RegExpElimination::RegExpElimination()
+namespace CVC4 {
+namespace theory {
+namespace strings {
+
+RegExpElimination::RegExpElimination(bool isAgg,
+                                     ProofNodeManager* pnm,
+                                     context::Context* c)
+    : d_isAggressive(isAgg),
+      d_pnm(pnm),
+      d_epg(pnm == nullptr
+                ? nullptr
+                : new EagerProofGenerator(pnm, c, "RegExpElimination::epg"))
 {
 }
 
-Node RegExpElimination::eliminate(Node atom)
+Node RegExpElimination::eliminate(Node atom, bool isAgg)
 {
   Assert(atom.getKind() == STRING_IN_REGEXP);
   if (atom[1].getKind() == REGEXP_CONCAT)
   {
-    return eliminateConcat(atom);
+    return eliminateConcat(atom, isAgg);
   }
   else if (atom[1].getKind() == REGEXP_STAR)
   {
-    return eliminateStar(atom);
+    return eliminateStar(atom, isAgg);
   }
   return Node::null();
 }
 
-Node RegExpElimination::eliminateConcat(Node atom)
+TrustNode RegExpElimination::eliminateTrusted(Node atom)
+{
+  Node eatom = eliminate(atom, d_isAggressive);
+  if (!eatom.isNull())
+  {
+    // Currently aggressive doesnt work due to fresh bound variables
+    if (isProofEnabled() && !d_isAggressive)
+    {
+      Node eq = atom.eqNode(eatom);
+      Node aggn = NodeManager::currentNM()->mkConst(d_isAggressive);
+      std::shared_ptr<ProofNode> pn =
+          d_pnm->mkNode(PfRule::RE_ELIM, {}, {atom, aggn}, eq);
+      d_epg->setProofFor(eq, pn);
+      return TrustNode::mkTrustRewrite(atom, eatom, d_epg.get());
+    }
+    return TrustNode::mkTrustRewrite(atom, eatom, nullptr);
+  }
+  return TrustNode::null();
+}
+
+Node RegExpElimination::eliminateConcat(Node atom, bool isAgg)
 {
   NodeManager* nm = NodeManager::currentNM();
   Node x = atom[0];
@@ -217,7 +245,7 @@ Node RegExpElimination::eliminateConcat(Node atom)
         // otherwise, we can use indexof to represent some next occurrence
         if (gap_exact[i + 1] && i + 1 != size)
         {
-          if (!options::regExpElimAgg())
+          if (!isAgg)
           {
             canProcess = false;
             break;
@@ -330,7 +358,7 @@ Node RegExpElimination::eliminateConcat(Node atom)
     }
   }
 
-  if (!options::regExpElimAgg())
+  if (!isAgg)
   {
     return Node::null();
   }
@@ -455,9 +483,9 @@ Node RegExpElimination::eliminateConcat(Node atom)
   return Node::null();
 }
 
-Node RegExpElimination::eliminateStar(Node atom)
+Node RegExpElimination::eliminateStar(Node atom, bool isAgg)
 {
-  if (!options::regExpElimAgg())
+  if (!isAgg)
   {
     return Node::null();
   }
@@ -580,3 +608,8 @@ Node RegExpElimination::returnElim(Node atom, Node atomElim, const char* id)
                    << "." << std::endl;
   return atomElim;
 }
+bool RegExpElimination::isProofEnabled() const { return d_pnm != nullptr; }
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/strings/regexp_elim.h b/src/theory/strings/regexp_elim.h
index 0c1acd29d..9d6fecc93 100644
--- a/src/theory/strings/regexp_elim.h
+++ b/src/theory/strings/regexp_elim.h
@@ -18,6 +18,8 @@
 #define CVC4__THEORY__STRINGS__REGEXP_ELIM_H
 
 #include "expr/node.h"
+#include "theory/eager_proof_generator.h"
+#include "theory/trust_node.h"
 
 namespace CVC4 {
 namespace theory {
@@ -33,14 +35,32 @@ namespace strings {
 class RegExpElimination
 {
  public:
-  RegExpElimination();
+  /**
+   * @param isAgg Whether aggressive eliminations are enabled
+   * @param pnm The proof node manager to use (for proofs)
+   * @param c The context to use (for proofs)
+   */
+  RegExpElimination(bool isAgg = false,
+                    ProofNodeManager* pnm = nullptr,
+                    context::Context* c = nullptr);
   /** eliminate membership
    *
    * This method takes as input a regular expression membership atom of the
    * form (str.in.re x R). If this method returns a non-null node ret, then ret
    * is equivalent to atom.
+   *
+   * @param atom The node to eliminate
+   * @param isAgg Whether we apply aggressive elimination techniques
+   * @return The node with regular expressions eliminated, or null if atom
+   * was unchanged.
+   */
+  static Node eliminate(Node atom, bool isAgg);
+
+  /**
+   * Return the trust node corresponding to rewriting n based on eliminate
+   * above.
    */
-  static Node eliminate(Node atom);
+  TrustNode eliminateTrusted(Node atom);
 
  private:
   /** return elimination
@@ -50,9 +70,17 @@ class RegExpElimination
    */
   static Node returnElim(Node atom, Node atomElim, const char* id);
   /** elimination for regular expression concatenation */
-  static Node eliminateConcat(Node atom);
+  static Node eliminateConcat(Node atom, bool isAgg);
   /** elimination for regular expression star */
-  static Node eliminateStar(Node atom);
+  static Node eliminateStar(Node atom, bool isAgg);
+  /** Are proofs enabled? */
+  bool isProofEnabled() const;
+  /** Are aggressive eliminations enabled? */
+  bool d_isAggressive;
+  /** Pointer to the proof node manager */
+  ProofNodeManager* d_pnm;
+  /** An eager proof generator for storing proofs in eliminate trusted above */
+  std::unique_ptr<EagerProofGenerator> d_epg;
 }; /* class RegExpElimination */
 
 }  // namespace strings
diff --git a/src/theory/strings/strings_rewriter.cpp b/src/theory/strings/strings_rewriter.cpp
index 932b5c8cc..575c33501 100644
--- a/src/theory/strings/strings_rewriter.cpp
+++ b/src/theory/strings/strings_rewriter.cpp
@@ -251,15 +251,13 @@ Node StringsRewriter::rewriteStringLeq(Node n)
   {
     String s = n1[0].getConst<String>();
     String t = n2[0].getConst<String>();
-    // only need to truncate if s is longer
-    if (s.size() > t.size())
+    size_t prefixLen = std::min(s.size(), t.size());
+    s = s.prefix(prefixLen);
+    t = t.prefix(prefixLen);
+    // if the prefixes are not the same, then we can already decide the outcome
+    if (s != t)
     {
-      s = s.prefix(t.size());
-    }
-    // if prefix is not leq, then entire string is not leq
-    if (!s.isLeq(t))
-    {
-      Node ret = nm->mkConst(false);
+      Node ret = nm->mkConst(s.isLeq(t));
       return returnRewrite(n, ret, Rewrite::STR_LEQ_CPREFIX);
     }
   }
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index a9e2c0051..d3e9e34f1 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -997,27 +997,28 @@ void TheoryStrings::checkRegisterTermsNormalForms()
 TrustNode TheoryStrings::ppRewrite(TNode atom)
 {
   Trace("strings-ppr") << "TheoryStrings::ppRewrite " << atom << std::endl;
+  TrustNode ret;
   Node atomRet = atom;
   if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP)
   {
     // aggressive elimination of regular expression membership
-    Node atomElim = d_regexp_elim.eliminate(atomRet);
-    if (!atomElim.isNull())
+    ret = d_regexp_elim.eliminateTrusted(atomRet);
+    if (!ret.isNull())
     {
-      Trace("strings-ppr") << "  rewrote " << atom << " -> " << atomElim
+      Trace("strings-ppr") << "  rewrote " << atom << " -> " << ret.getNode()
                            << " via regular expression elimination."
                            << std::endl;
-      atomRet = atomElim;
+      atomRet = ret.getNode();
     }
   }
   if( !options::stringLazyPreproc() ){
     //eager preprocess here
     std::vector< Node > new_nodes;
     StringsPreprocess* p = d_esolver.getPreprocess();
-    Node ret = p->processAssertion(atomRet, new_nodes);
-    if (ret != atomRet)
+    Node pret = p->processAssertion(atomRet, new_nodes);
+    if (pret != atomRet)
     {
-      Trace("strings-ppr") << "  rewrote " << atomRet << " -> " << ret
+      Trace("strings-ppr") << "  rewrote " << atomRet << " -> " << pret
                            << ", with " << new_nodes.size() << " lemmas."
                            << std::endl;
       for (const Node& lem : new_nodes)
@@ -1026,16 +1027,16 @@ TrustNode TheoryStrings::ppRewrite(TNode atom)
         ++(d_statistics.d_lemmasEagerPreproc);
         d_out->lemma(lem);
       }
-      atomRet = ret;
+      atomRet = pret;
+      // Don't support proofs yet, thus we must return nullptr. This is the
+      // case even if we had proven the elimination via regexp elimination
+      // above.
+      ret = TrustNode::mkTrustRewrite(atom, atomRet, nullptr);
     }else{
       Assert(new_nodes.empty());
     }
   }
-  if (atomRet != atom)
-  {
-    return TrustNode::mkTrustRewrite(atom, atomRet, nullptr);
-  }
-  return TrustNode::null();
+  return ret;
 }
 
 /** run the given inference step */
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index c5ec4d0c6..5b291f3c5 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -129,35 +129,35 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size,
 #ifdef CVC4_USE_SYMFPU
   if (signedBV)
   {
-    d_fpl = new FloatingPointLiteral(
+    d_fpl.reset(new FloatingPointLiteral(
         symfpu::convertSBVToFloat<symfpuLiteral::traits>(
             symfpuLiteral::CVC4FPSize(size),
             symfpuLiteral::CVC4RM(rm),
-            symfpuLiteral::CVC4SignedBitVector(bv)));
+            symfpuLiteral::CVC4SignedBitVector(bv))));
   }
   else
   {
-    d_fpl = new FloatingPointLiteral(
+    d_fpl.reset(new FloatingPointLiteral(
         symfpu::convertUBVToFloat<symfpuLiteral::traits>(
             symfpuLiteral::CVC4FPSize(size),
             symfpuLiteral::CVC4RM(rm),
-            symfpuLiteral::CVC4UnsignedBitVector(bv)));
+            symfpuLiteral::CVC4UnsignedBitVector(bv))));
   }
 #else
-  d_fpl = new FloatingPointLiteral(2, 2, 0.0);
+  d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0));
 #endif
 }
 
 FloatingPoint::FloatingPoint(const FloatingPointSize& fp_size,
-                             const FloatingPointLiteral* fpl)
+                             FloatingPointLiteral* fpl)
     : d_fp_size(fp_size)
 {
-  d_fpl = new FloatingPointLiteral(*fpl);
+  d_fpl.reset(fpl);
 }
 
 FloatingPoint::FloatingPoint(const FloatingPoint& fp) : d_fp_size(fp.d_fp_size)
 {
-  d_fpl = new FloatingPointLiteral(*fp.d_fpl);
+  d_fpl.reset(new FloatingPointLiteral(*fp.d_fpl));
 }
 
 FloatingPoint::FloatingPoint(const FloatingPointSize& size,
@@ -171,10 +171,10 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size,
   {
 #ifdef CVC4_USE_SYMFPU
     // In keeping with the SMT-LIB standard
-    d_fpl = new FloatingPointLiteral(
-        SymFPUUnpackedFloatLiteral::makeZero(size, false));
+    d_fpl.reset(new FloatingPointLiteral(
+        SymFPUUnpackedFloatLiteral::makeZero(size, false)));
 #else
-    d_fpl = new FloatingPointLiteral(2, 2, 0.0);
+    d_fpl.reset(new FloatingPointLiteral(2, 2, 0.0));
 #endif
   }
   else
@@ -285,8 +285,8 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size,
         negative, exactExp.signExtend(extension), sig);
 
     // Then cast...
-    d_fpl = new FloatingPointLiteral(
-        symfpu::convertFloatToFloat(exactFormat, size, rm, exactFloat.d_symuf));
+    d_fpl.reset(new FloatingPointLiteral(symfpu::convertFloatToFloat(
+        exactFormat, size, rm, exactFloat.d_symuf)));
 #else
     Unreachable() << "no concrete implementation of FloatingPointLiteral";
 #endif
@@ -295,8 +295,6 @@ FloatingPoint::FloatingPoint(const FloatingPointSize& size,
 
 FloatingPoint::~FloatingPoint()
 {
-  delete d_fpl;
-  d_fpl = nullptr;
 }
 
 FloatingPoint FloatingPoint::makeNaN(const FloatingPointSize& size)
diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h
index 754c38290..2d27b836e 100644
--- a/src/util/floatingpoint.h
+++ b/src/util/floatingpoint.h
@@ -20,6 +20,8 @@
 #ifndef CVC4__FLOATINGPOINT_H
 #define CVC4__FLOATINGPOINT_H
 
+#include <memory>
+
 #include "util/bitvector.h"
 #include "util/floatingpoint_size.h"
 #include "util/rational.h"
@@ -60,8 +62,6 @@ class CVC4_PUBLIC FloatingPoint
   /** Constructors. */
   FloatingPoint(uint32_t e, uint32_t s, const BitVector& bv);
   FloatingPoint(const FloatingPointSize& size, const BitVector& bv);
-  FloatingPoint(const FloatingPointSize& fp_size,
-                const FloatingPointLiteral* fpl);
   FloatingPoint(const FloatingPoint& fp);
   FloatingPoint(const FloatingPointSize& size,
                 const RoundingMode& rm,
@@ -118,7 +118,7 @@ class CVC4_PUBLIC FloatingPoint
   static FloatingPoint makeMaxNormal(const FloatingPointSize& size, bool sign);
 
   /** Get the wrapped floating-point value. */
-  const FloatingPointLiteral* getLiteral(void) const { return d_fpl; }
+  const FloatingPointLiteral* getLiteral(void) const { return d_fpl.get(); }
 
   /**
    * Return a string representation of this floating-point.
@@ -258,8 +258,16 @@ class CVC4_PUBLIC FloatingPoint
   FloatingPointSize d_fp_size;
 
  private:
+  /**
+   * Constructor.
+   *
+   * Note: This constructor takes ownership of 'fpl' and is not intended for
+   *       public use.
+   */
+  FloatingPoint(const FloatingPointSize& fp_size, FloatingPointLiteral* fpl);
+
   /** The floating-point literal of this floating-point value. */
-  FloatingPointLiteral* d_fpl;
+  std::unique_ptr<FloatingPointLiteral> d_fpl;
 
 }; /* class FloatingPoint */
 
diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp
index fb5c0b7b5..77ab910fa 100644
--- a/src/util/floatingpoint_literal_symfpu.cpp
+++ b/src/util/floatingpoint_literal_symfpu.cpp
@@ -65,12 +65,12 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::allOnes(
 template <bool isSigned>
 CVC4Prop wrappedBitVector<isSigned>::isAllOnes() const
 {
-  return (*this == wrappedBitVector<isSigned>::allOnes(this->getWidth()));
+  return (*this == wrappedBitVector<isSigned>::allOnes(getWidth()));
 }
 template <bool isSigned>
 CVC4Prop wrappedBitVector<isSigned>::isAllZeros() const
 {
-  return (*this == wrappedBitVector<isSigned>::zero(this->getWidth()));
+  return (*this == wrappedBitVector<isSigned>::zero(getWidth()));
 }
 
 template <bool isSigned>
@@ -110,101 +110,101 @@ template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator<<(
     const wrappedBitVector<isSigned>& op) const
 {
-  return this->BitVector::leftShift(op);
+  return BitVector::leftShift(op);
 }
 
 template <>
 wrappedBitVector<true> wrappedBitVector<true>::operator>>(
     const wrappedBitVector<true>& op) const
 {
-  return this->BitVector::arithRightShift(op);
+  return BitVector::arithRightShift(op);
 }
 
 template <>
 wrappedBitVector<false> wrappedBitVector<false>::operator>>(
     const wrappedBitVector<false>& op) const
 {
-  return this->BitVector::logicalRightShift(op);
+  return BitVector::logicalRightShift(op);
 }
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator|(
     const wrappedBitVector<isSigned>& op) const
 {
-  return this->BitVector::operator|(op);
+  return BitVector::operator|(op);
 }
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator&(
     const wrappedBitVector<isSigned>& op) const
 {
-  return this->BitVector::operator&(op);
+  return BitVector::operator&(op);
 }
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator+(
     const wrappedBitVector<isSigned>& op) const
 {
-  return this->BitVector::operator+(op);
+  return BitVector::operator+(op);
 }
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(
     const wrappedBitVector<isSigned>& op) const
 {
-  return this->BitVector::operator-(op);
+  return BitVector::operator-(op);
 }
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator*(
     const wrappedBitVector<isSigned>& op) const
 {
-  return this->BitVector::operator*(op);
+  return BitVector::operator*(op);
 }
 
 template <>
 wrappedBitVector<false> wrappedBitVector<false>::operator/(
     const wrappedBitVector<false>& op) const
 {
-  return this->BitVector::unsignedDivTotal(op);
+  return BitVector::unsignedDivTotal(op);
 }
 
 template <>
 wrappedBitVector<false> wrappedBitVector<false>::operator%(
     const wrappedBitVector<false>& op) const
 {
-  return this->BitVector::unsignedRemTotal(op);
+  return BitVector::unsignedRemTotal(op);
 }
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator-(void) const
 {
-  return this->BitVector::operator-();
+  return BitVector::operator-();
 }
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::operator~(void) const
 {
-  return this->BitVector::operator~();
+  return BitVector::operator~();
 }
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::increment() const
 {
-  return *this + wrappedBitVector<isSigned>::one(this->getWidth());
+  return *this + wrappedBitVector<isSigned>::one(getWidth());
 }
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::decrement() const
 {
-  return *this - wrappedBitVector<isSigned>::one(this->getWidth());
+  return *this - wrappedBitVector<isSigned>::one(getWidth());
 }
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::signExtendRightShift(
     const wrappedBitVector<isSigned>& op) const
 {
-  return this->BitVector::arithRightShift(BitVector(this->getWidth(), op));
+  return BitVector::arithRightShift(BitVector(getWidth(), op));
 }
 
 /*** Modular opertaions ***/
@@ -226,13 +226,13 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularRightShift(
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularIncrement() const
 {
-  return this->increment();
+  return increment();
 }
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularDecrement() const
 {
-  return this->decrement();
+  return decrement();
 }
 
 template <bool isSigned>
@@ -254,63 +254,63 @@ template <bool isSigned>
 CVC4Prop wrappedBitVector<isSigned>::operator==(
     const wrappedBitVector<isSigned>& op) const
 {
-  return this->BitVector::operator==(op);
+  return BitVector::operator==(op);
 }
 
 template <>
 CVC4Prop wrappedBitVector<true>::operator<=(
     const wrappedBitVector<true>& op) const
 {
-  return this->signedLessThanEq(op);
+  return signedLessThanEq(op);
 }
 
 template <>
 CVC4Prop wrappedBitVector<true>::operator>=(
     const wrappedBitVector<true>& op) const
 {
-  return !(this->signedLessThan(op));
+  return !(signedLessThan(op));
 }
 
 template <>
 CVC4Prop wrappedBitVector<true>::operator<(
     const wrappedBitVector<true>& op) const
 {
-  return this->signedLessThan(op);
+  return signedLessThan(op);
 }
 
 template <>
 CVC4Prop wrappedBitVector<true>::operator>(
     const wrappedBitVector<true>& op) const
 {
-  return !(this->signedLessThanEq(op));
+  return !(signedLessThanEq(op));
 }
 
 template <>
 CVC4Prop wrappedBitVector<false>::operator<=(
     const wrappedBitVector<false>& op) const
 {
-  return this->unsignedLessThanEq(op);
+  return unsignedLessThanEq(op);
 }
 
 template <>
 CVC4Prop wrappedBitVector<false>::operator>=(
     const wrappedBitVector<false>& op) const
 {
-  return !(this->unsignedLessThan(op));
+  return !(unsignedLessThan(op));
 }
 
 template <>
 CVC4Prop wrappedBitVector<false>::operator<(
     const wrappedBitVector<false>& op) const
 {
-  return this->unsignedLessThan(op);
+  return unsignedLessThan(op);
 }
 
 template <>
 CVC4Prop wrappedBitVector<false>::operator>(
     const wrappedBitVector<false>& op) const
 {
-  return !(this->unsignedLessThanEq(op));
+  return !(unsignedLessThanEq(op));
 }
 
 /*** Type conversion ***/
@@ -335,11 +335,11 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extend(
 {
   if (isSigned)
   {
-    return this->BitVector::signExtend(extension);
+    return BitVector::signExtend(extension);
   }
   else
   {
-    return this->BitVector::zeroExtend(extension);
+    return BitVector::zeroExtend(extension);
   }
 }
 
@@ -347,24 +347,24 @@ template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::contract(
     CVC4BitWidth reduction) const
 {
-  Assert(this->getWidth() > reduction);
+  Assert(getWidth() > reduction);
 
-  return this->extract((this->getWidth() - 1) - reduction, 0);
+  return extract((getWidth() - 1) - reduction, 0);
 }
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::resize(
     CVC4BitWidth newSize) const
 {
-  CVC4BitWidth width = this->getWidth();
+  CVC4BitWidth width = getWidth();
 
   if (newSize > width)
   {
-    return this->extend(newSize - width);
+    return extend(newSize - width);
   }
   else if (newSize < width)
   {
-    return this->contract(width - newSize);
+    return contract(width - newSize);
   }
   else
   {
@@ -376,15 +376,15 @@ template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::matchWidth(
     const wrappedBitVector<isSigned>& op) const
 {
-  Assert(this->getWidth() <= op.getWidth());
-  return this->extend(op.getWidth() - this->getWidth());
+  Assert(getWidth() <= op.getWidth());
+  return extend(op.getWidth() - getWidth());
 }
 
 template <bool isSigned>
 wrappedBitVector<isSigned> wrappedBitVector<isSigned>::append(
     const wrappedBitVector<isSigned>& op) const
 {
-  return this->BitVector::concat(op);
+  return BitVector::concat(op);
 }
 
 // Inclusive of end points, thus if the same, extracts just one bit
@@ -393,7 +393,7 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract(
     CVC4BitWidth upper, CVC4BitWidth lower) const
 {
   Assert(upper >= lower);
-  return this->BitVector::extract(upper, lower);
+  return BitVector::extract(upper, lower);
 }
 
 // Explicit instantiation
diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h.in
index 06a98b7ea..54156c7e7 100644
--- a/src/util/floatingpoint_literal_symfpu.h.in
+++ b/src/util/floatingpoint_literal_symfpu.h.in
@@ -236,25 +236,30 @@ class wrappedBitVector : public BitVector
 
   /** Bit-vector signed/unsigned (zero) extension. */
   wrappedBitVector<isSigned> extend(CVC4BitWidth extension) const;
+
   /**
    * Create a "contracted" bit-vector by cutting off the 'reduction' number of
    * most significant bits, i.e., by extracting the (bit-width - reduction)
    * least significant bits.
    */
   wrappedBitVector<isSigned> contract(CVC4BitWidth reduction) const;
+
   /**
    * Create a "resized" bit-vector of given size bei either extending (if new
    * size is larger) or contracting (if it is smaller) this wrapped bit-vector.
    */
   wrappedBitVector<isSigned> resize(CVC4BitWidth newSize) const;
+
   /**
    * Create an extension of this bit-vector that matches the bit-width of the
    * given bit-vector.
+   *
    * Note: The size of the given bit-vector may not be larger than the size of
-   * this bit-vector.
+   *       this bit-vector.
    */
   wrappedBitVector<isSigned> matchWidth(
       const wrappedBitVector<isSigned>& op) const;
+
   /** Bit-vector concatenation. */
   wrappedBitVector<isSigned> append(const wrappedBitVector<isSigned>& op) const;
 
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 816202fa9..1826b3156 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -126,6 +126,7 @@ set(regress_0_tests
   regress0/aufbv/fuzz14.smtv1.smt2
   regress0/aufbv/fuzz15.smtv1.smt2
   regress0/aufbv/issue3737.smt2
+  regress0/aufbv/issue3687-check-models-small.smt2
   regress0/aufbv/rewrite_bug.smtv1.smt2
   regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smtv1.smt2
   regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smtv1.smt2
@@ -584,7 +585,12 @@ set(regress_0_tests
   regress0/issue2832-qualId.smt2
   regress0/issue4010-sort-inf-var.smt2
   regress0/issue4469-unc-no-reuse-var.smt2
+  regress0/issue4707-bv-to-bool-small.smt2
+  regress0/issue5099-model-1.smt2
+  regress0/issue5099-model-2.smt2
   regress0/issue5144-resetAssertions.smt2
+  regress0/issue5540-2-dump-model.smt2
+  regress0/issue5540-model-decls.smt2
   regress0/ite.cvc
   regress0/ite2.smt2
   regress0/ite3.smt2
@@ -1016,6 +1022,7 @@ set(regress_0_tests
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2
+  regress0/strings/leq.smt2
   regress0/strings/loop001.smt2
   regress0/strings/loop-wrong-sem.smt2
   regress0/strings/model001.smt2
@@ -1416,6 +1423,7 @@ set(regress_1_tests
   regress1/issue3970-nl-ext-purify.smt2
   regress1/issue3990-sort-inference.smt2
   regress1/issue4273-ext-rew-cache.smt2
+  regress1/issue4335-unsat-core.smt2
   regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
   regress1/lemmas/pursuit-safety-8.smtv1.smt2
   regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
@@ -1622,6 +1630,8 @@ set(regress_1_tests
   regress1/quantifiers/issue5482-rtf-no-fv.smt2
   regress1/quantifiers/issue5484-qe.smt2
   regress1/quantifiers/issue5484b-qe.smt2
+  regress1/quantifiers/issue5506-qe.smt2
+  regress1/quantifiers/issue5507-qe.smt2
   regress1/quantifiers/issue993.smt2
   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
   regress1/quantifiers/lia-witness-div-pp.smt2
@@ -2167,6 +2177,8 @@ set(regress_2_tests
   regress2/hole7.cvc
   regress2/hole8.cvc
   regress2/instance_1444.smtv1.smt2
+  regress2/issue3687-check-models.smt2
+  regress2/issue4707-bv-to-bool-large.smt2
   regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2
   regress2/javafe.ast.WhileStmt.447_no_forall.smt2
   regress2/ooo.rf6.smt2
diff --git a/test/regress/regress0/aufbv/issue3687-check-models-small.smt2 b/test/regress/regress0/aufbv/issue3687-check-models-small.smt2
new file mode 100644
index 000000000..88cbd8a0b
--- /dev/null
+++ b/test/regress/regress0/aufbv/issue3687-check-models-small.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --check-models
+; EXPECT: sat
+(set-logic QF_AUFBV)
+(declare-fun a () (Array (_ BitVec 2) (_ BitVec 2)))
+(declare-fun b () (_ BitVec 2))
+(assert (distinct #b01 (select (store (store a #b01 (bvor #b01 (select a
+  #b00))) #b10 #b00) b)))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/bv/bv_to_int_5281.smt2 b/test/regress/regress0/bv/bv_to_int_5281.smt2
index 4d0da1dbb..dc2cb7f35 100644
--- a/test/regress/regress0/bv/bv_to_int_5281.smt2
+++ b/test/regress/regress0/bv/bv_to_int_5281.smt2
@@ -1,4 +1,4 @@
-; COMMAND: --check-models --incremental
+; COMMAND-LINE: --check-models --incremental
 ; EXPECT: sat
 (set-logic ALL)
 (set-option :check-models true)
diff --git a/test/regress/regress0/issue4707-bv-to-bool-small.smt2 b/test/regress/regress0/issue4707-bv-to-bool-small.smt2
new file mode 100644
index 000000000..c2f0a58ad
--- /dev/null
+++ b/test/regress/regress0/issue4707-bv-to-bool-small.smt2
@@ -0,0 +1,13 @@
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun b () (Array (_ BitVec 10) (_ BitVec 1)))
+(declare-fun c () (Array (_ BitVec 10) (_ BitVec 1)))
+(declare-fun ae () (_ BitVec 10))
+(declare-fun ag () (_ BitVec 10))
+(declare-fun ak () (_ BitVec 10))
+(assert (= (_ bv1 1) (bvand (bvcomp ae ((_ zero_extend 9) (select b (_ bv0
+  10)))) (bvsdiv (bvcomp ae ak) (bvand (ite (= (_ bv0 1) (bvcomp ag (bvshl ((_
+  zero_extend 9) (select c (bvadd ae (_ bv3 10)))) (_ bv8 10)))) (_ bv1 1) (_
+  bv0 1)) (ite (= b (store (store c (bvadd ae (_ bv3 10)) ((_ extract 0 0)
+  (bvlshr ag (_ bv8 10)))) ak (_ bv1 1))) (_ bv1 1) (_ bv0 1)))))))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/issue5099-model-1.smt2 b/test/regress/regress0/issue5099-model-1.smt2
new file mode 100644
index 000000000..dd422ab3b
--- /dev/null
+++ b/test/regress/regress0/issue5099-model-1.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: -m
+; EXPECT: sat
+; EXPECT: ((baz true))
+(set-logic QF_NIRA)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(assert (! (or (= a (div 0 b))) :named baz))
+(assert (and (> b 5)))
+(check-sat)
+(get-assignment)
diff --git a/test/regress/regress0/issue5099-model-2.smt2 b/test/regress/regress0/issue5099-model-2.smt2
new file mode 100644
index 000000000..2bd27093f
--- /dev/null
+++ b/test/regress/regress0/issue5099-model-2.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: -m
+; EXPECT: sat
+; EXPECT: ((IP true))
+(set-logic QF_NRA)
+(declare-const r11 Real)
+(declare-const r16 Real)
+(assert (! (distinct (/ 1 r16) r11) :named IP))
+(check-sat)
+(get-assignment)
\ No newline at end of file
diff --git a/test/regress/regress0/issue5540-2-dump-model.smt2 b/test/regress/regress0/issue5540-2-dump-model.smt2
new file mode 100644
index 000000000..56d3b2458
--- /dev/null
+++ b/test/regress/regress0/issue5540-2-dump-model.smt2
@@ -0,0 +1,9 @@
+; SCRUBBER: sed -e 's/Bool.*$/Bool/'
+; COMMAND-LINE: --dump-models
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: (define-fun v16 () Bool
+; EXPECT: )
+(set-logic UFLIA)
+(declare-fun v16 () Bool)
+(check-sat)
diff --git a/test/regress/regress0/issue5540-model-decls.smt2 b/test/regress/regress0/issue5540-model-decls.smt2
new file mode 100644
index 000000000..714159c9f
--- /dev/null
+++ b/test/regress/regress0/issue5540-model-decls.smt2
@@ -0,0 +1,19 @@
+; SCRUBBER: sed -e 's/Bool.*$/Bool/'
+; COMMAND-LINE: --dump-models -i
+; EXPECT:sat
+; EXPECT: (
+; EXPECT: (define-fun a () Bool
+; EXPECT: )
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: (define-fun a () Bool
+; EXPECT: )
+; EXPECT: sat
+; EXPECT: (
+; EXPECT: (define-fun a () Bool
+; EXPECT: )
+(set-logic ALL)
+(declare-fun a () Bool)
+(check-sat)
+(check-sat)
+(check-sat)
diff --git a/test/regress/regress0/strings/leq.smt2 b/test/regress/regress0/strings/leq.smt2
new file mode 100644
index 000000000..b3bd40739
--- /dev/null
+++ b/test/regress/regress0/strings/leq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --strings-exp
+(set-logic QF_SLIA)
+(declare-const x String)
+(declare-const y String)
+(assert (or
+  (not (str.<= (str.++ "A" x) (str.++ "B" y)))
+  (not (str.<= (str.++ "A" x) (str.++ "BC" y)))
+  (str.<= (str.++ "A" "D" x) (str.++ "AC" y))))
+(set-info :status unsat)
+(check-sat)
diff --git a/test/regress/regress1/issue4335-unsat-core.smt2 b/test/regress/regress1/issue4335-unsat-core.smt2
new file mode 100644
index 000000000..11e689515
--- /dev/null
+++ b/test/regress/regress1/issue4335-unsat-core.smt2
@@ -0,0 +1,187 @@
+; SCRUBBER: sed -e 's/IP_[0-9]*/IP/'
+; EXPECT: unsat
+; EXPECT: (
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: IP
+; EXPECT: )
+(set-logic ALL)
+(set-option :produce-unsat-cores true)
+(declare-const v0 Bool)
+(declare-const v1 Bool)
+(declare-const v2 Bool)
+(declare-const v3 Bool)
+(declare-const v4 Bool)
+(declare-const i1 Int)
+(declare-const r1 Real)
+(declare-const r2 Real)
+(declare-const r3 Real)
+(declare-const r7 Real)
+(declare-const r10 Real)
+(declare-const r14 Real)
+(declare-const r16 Real)
+(declare-const r17 Real)
+(declare-const r18 Real)
+(declare-const v5 Bool)
+(declare-const r20 Real)
+(declare-const arr-5074471134850140881_778238581772319464-0 (Array Bool Int))
+(assert (! (exists ((q0 Int) (q1 Real) (q2 Int)) (not (> (- i1) (select (store arr-5074471134850140881_778238581772319464-0 v0 60) (= v0 v4 v3 v3 v4))))) :named IP_1))
+(assert (! (or (forall ((q0 Int) (q1 Real) (q2 Int)) (=> (>= r20 q1 q1 26271062.0) (<= q2 q2))) (exists ((q0 Int) (q1 Real) (q2 Int)) (=> (>= (- i1) q2) (< q1 q1 5851734.0)))) :named IP_2))
+(declare-const arr-778238581772319464_-3713212254555730767-0 (Array Int (_ BitVec 8)))
+(declare-const v6 Bool)
+(declare-const v7 Bool)
+(declare-const arr--5101604640448673848_-3713212254554648242-0 (Array Real (_ BitVec 9)))
+(declare-const arr--3713212254557895817_-5101604640448673848-0 (Array (_ BitVec 10) Real))
+(assert (! (or (distinct (- i1) 35) (not v4) (= v0 v4 v3 v3 v4)) :named IP_3))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 (= v0 v4 v3 v3 v4)) :named IP_4))
+(assert (! (or (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_5))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (= v0 v4 v3 v3 v4)) :named IP_6))
+(assert (! (or (= v0 v4 v3 v3 v4) v3 (= v0 v4 v3 v3 v4)) :named IP_7))
+(assert (! (or (is_int 1193124502.0) (= v0 v4 v3 v3 v4) (not v4)) :named IP_8))
+(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) v0) :named IP_9))
+(assert (! (or (< 397 (div (- i1) 60)) v3 (= v0 v4 v3 v3 v4)) :named IP_10))
+(assert (! (or v3 v3 v3) :named IP_11))
+(assert (! (or (is_int 1193124502.0) (not v4) (= v0 v4 v3 v3 v4)) :named IP_12))
+(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_13))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) v0) :named IP_14))
+(assert (! (or (is_int 1193124502.0) v0 (not v4)) :named IP_15))
+(assert (! (or (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60))) :named IP_16))
+(assert (! (or (not v4) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_17))
+(assert (! (or (distinct (- i1) 35) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_18))
+(assert (! (or v3 (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_19))
+(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_20))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_21))
+(assert (! (or (< 397 (div (- i1) 60)) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_22))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (is_int 1193124502.0)) :named IP_23))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_24))
+(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (< 397 (div (- i1) 60))) :named IP_25))
+(assert (! (or v0 v0 (= v0 v4 v3 v3 v4)) :named IP_26))
+(assert (! (or v0 (not v4) (= v0 v4 v3 v3 v4)) :named IP_27))
+(assert (! (or (= v0 v4 v3 v3 v4) v3 v3) :named IP_28))
+(assert (! (or v3 (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_29))
+(assert (! (or (is_int 1193124502.0) (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_30))
+(assert (! (or (distinct (- i1) 35) (not v4) (distinct (- i1) 35)) :named IP_31))
+(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) v3) :named IP_32))
+(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) (not v4)) :named IP_33))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 v0) :named IP_34))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (< 397 (div (- i1) 60))) :named IP_35))
+(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (not v4)) :named IP_36))
+(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) v0) :named IP_37))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60))) :named IP_38))
+(assert (! (or (distinct (- i1) 35) v3 (= v0 v4 v3 v3 v4)) :named IP_39))
+(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (not v4)) :named IP_40))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (is_int 1193124502.0)) :named IP_41))
+(assert (! (or v0 (distinct (- i1) 35) v0) :named IP_42))
+(assert (! (or (not v4) v0 (not v4)) :named IP_43))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (not v4) (= v0 v4 v3 v3 v4)) :named IP_44))
+(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0)) :named IP_45))
+(assert (! (or v0 (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_46))
+(assert (! (or (= v0 v4 v3 v3 v4) v0 (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_47))
+(assert (! (or (is_int 1193124502.0) v0 (= v0 v4 v3 v3 v4)) :named IP_48))
+(assert (! (or v0 (< 397 (div (- i1) 60)) v3) :named IP_49))
+(assert (! (or v0 v3 (is_int 1193124502.0)) :named IP_50))
+(assert (! (or v3 (distinct (- i1) 35) v0) :named IP_51))
+(assert (! (or v3 (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0)) :named IP_52))
+(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_53))
+(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_54))
+(assert (! (or (distinct (- i1) 35) v3 (not v4)) :named IP_55))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) v0) :named IP_56))
+(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_57))
+(assert (! (or (not v4) v0 (< 397 (div (- i1) 60))) :named IP_58))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (not v4)) :named IP_59))
+(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) (is_int 1193124502.0)) :named IP_60))
+(assert (! (or (is_int 1193124502.0) v0 (distinct (- i1) 35)) :named IP_61))
+(assert (! (or (not v4) (< 397 (div (- i1) 60)) v3) :named IP_62))
+(assert (! (or (not v4) (distinct (- i1) 35) v0) :named IP_63))
+(assert (! (or (distinct (- i1) 35) (is_int 1193124502.0) v3) :named IP_64))
+(assert (! (or (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4)) :named IP_65))
+(assert (! (or (< 397 (div (- i1) 60)) v3 v3) :named IP_66))
+(assert (! (or (not v4) v3 (distinct (- i1) 35)) :named IP_67))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 v3) :named IP_68))
+(assert (! (or (distinct (- i1) 35) (distinct (- i1) 35) v0) :named IP_69))
+(assert (! (or v3 (not v4) (< 397 (div (- i1) 60))) :named IP_70))
+(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (< 397 (div (- i1) 60))) :named IP_71))
+(assert (! (or (< 397 (div (- i1) 60)) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_72))
+(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_73))
+(assert (! (or v0 v0 (is_int 1193124502.0)) :named IP_74))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_75))
+(assert (! (or v3 (not v4) v0) :named IP_76))
+(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (not v4)) :named IP_77))
+(assert (! (or v3 (is_int 1193124502.0) (< 397 (div (- i1) 60))) :named IP_78))
+(assert (! (or (is_int 1193124502.0) (not v4) v0) :named IP_79))
+(assert (! (or (not v4) v3 (not v4)) :named IP_80))
+(assert (! (or v3 v0 v0) :named IP_81))
+(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_82))
+(assert (! (or (is_int 1193124502.0) (= v0 v4 v3 v3 v4) (not v4)) :named IP_83))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0) v0) :named IP_84))
+(assert (! (or (not v4) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_85))
+(assert (! (or (= v0 v4 v3 v3 v4) v0 (= v0 v4 v3 v3 v4)) :named IP_86))
+(assert (! (or v3 (distinct (- i1) 35) (not v4)) :named IP_87))
+(assert (! (or (distinct (- i1) 35) v0 (not v4)) :named IP_88))
+(assert (! (or (distinct (- i1) 35) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_89))
+(assert (! (or (distinct (- i1) 35) (< 397 (div (- i1) 60)) (not v4)) :named IP_90))
+(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_91))
+(assert (! (or (is_int 1193124502.0) (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_92))
+(assert (! (or v0 (distinct (- i1) 35) (is_int 1193124502.0)) :named IP_93))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_94))
+(assert (! (or (= v0 v4 v3 v3 v4) (distinct (- i1) 35) (= v0 v4 v3 v3 v4)) :named IP_95))
+(assert (! (or v3 (not v4) (is_int 1193124502.0)) :named IP_96))
+(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_97))
+(assert (! (or (= v0 v4 v3 v3 v4) v3 (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_98))
+(assert (! (or (distinct (- i1) 35) (distinct v4 (= v0 v4 v3 v3 v4)) v3) :named IP_99))
+(assert (! (or v0 v0 (= v0 v4 v3 v3 v4)) :named IP_100))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_101))
+(assert (! (or (is_int 1193124502.0) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_102))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4)) :named IP_103))
+(assert (! (or (not v4) (not v4) (= v0 v4 v3 v3 v4)) :named IP_104))
+(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_105))
+(assert (! (or (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60)) (is_int 1193124502.0)) :named IP_106))
+(assert (! (or v0 (is_int 1193124502.0) (distinct (- i1) 35)) :named IP_107))
+(assert (! (or (< 397 (div (- i1) 60)) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_108))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (distinct (- i1) 35)) :named IP_109))
+(assert (! (or (= v0 v4 v3 v3 v4) v0 (not v4)) :named IP_110))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_111))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (distinct (- i1) 35)) :named IP_112))
+(assert (! (or v0 (not v4) (< 397 (div (- i1) 60))) :named IP_113))
+(assert (! (or v3 (distinct (- i1) 35) v0) :named IP_114))
+(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_115))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_116))
+(assert (! (or (< 397 (div (- i1) 60)) (is_int 1193124502.0) (not v4)) :named IP_117))
+(assert (! (or v0 (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_118))
+(assert (! (or (distinct (- i1) 35) (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_119))
+(assert (! (or (= v0 v4 v3 v3 v4) (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_120))
+(assert (! (or v3 v3 v3) :named IP_121))
+(assert (! (or (is_int 1193124502.0) (< 397 (div (- i1) 60)) v3) :named IP_122))
+(assert (! (or (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_123))
+(assert (! (or (not v4) (= v0 v4 v3 v3 v4) v3) :named IP_124))
+(assert (! (or (distinct (- i1) 35) (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60))) :named IP_125))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35) (not v4)) :named IP_126))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 v0) :named IP_127))
+(assert (! (or (is_int 1193124502.0) (distinct (- i1) 35) (is_int 1193124502.0)) :named IP_128))
+(assert (! (or v0 (= v0 v4 v3 v3 v4) (= v0 v4 v3 v3 v4)) :named IP_129))
+(assert (! (or v0 (distinct (- i1) 35) v0) :named IP_130))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (= v0 v4 v3 v3 v4) (is_int 1193124502.0)) :named IP_131))
+(assert (! (or (not v4) v3 (distinct (- i1) 35)) :named IP_132))
+(assert (! (or v0 (< 397 (div (- i1) 60)) (= v0 v4 v3 v3 v4)) :named IP_133))
+(assert (! (or (is_int 1193124502.0) (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60))) :named IP_134))
+(assert (! (or v0 (distinct v4 (= v0 v4 v3 v3 v4)) (is_int 1193124502.0)) :named IP_135))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4))) :named IP_136))
+(assert (! (or v3 (= v0 v4 v3 v3 v4) (< 397 (div (- i1) 60))) :named IP_137))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v3 (distinct (- i1) 35)) :named IP_138))
+(assert (! (or v3 (< 397 (div (- i1) 60)) (distinct (- i1) 35)) :named IP_139))
+(assert (! (or (< 397 (div (- i1) 60)) (< 397 (div (- i1) 60)) v3) :named IP_140))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (< 397 (div (- i1) 60)) v0) :named IP_141))
+(assert (! (or (< 397 (div (- i1) 60)) (not v4) v3) :named IP_142))
+(assert (! (or (< 397 (div (- i1) 60)) (distinct v4 (= v0 v4 v3 v3 v4)) (distinct (- i1) 35)) :named IP_143))
+(assert (! (or v3 (is_int 1193124502.0) v3) :named IP_144))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) v0 (< 397 (div (- i1) 60))) :named IP_145))
+(assert (! (or (distinct v4 (= v0 v4 v3 v3 v4)) (not v4) v3) :named IP_146))
+(check-sat-assuming (IP_107 IP_133))
+(get-unsat-core)
+(exit)
\ No newline at end of file
diff --git a/test/regress/regress1/quantifiers/issue5506-qe.smt2 b/test/regress/regress1/quantifiers/issue5506-qe.smt2
new file mode 100644
index 000000000..3839f2d75
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5506-qe.smt2
@@ -0,0 +1,6 @@
+; SCRUBBER: sed 's/(.*)/()/g'
+; EXPECT: ()
+; EXIT: 0
+(set-logic LIA)
+(declare-fun a () Int)
+(get-qe (forall ((b Int)) (= a 0)))
diff --git a/test/regress/regress1/quantifiers/issue5507-qe.smt2 b/test/regress/regress1/quantifiers/issue5507-qe.smt2
new file mode 100644
index 000000000..3b7ddbcf3
--- /dev/null
+++ b/test/regress/regress1/quantifiers/issue5507-qe.smt2
@@ -0,0 +1,19 @@
+; EXPECT: false
+; EXIT: 0
+(set-logic LIA)
+(declare-fun v0 () Bool)
+(declare-fun v1 () Bool)
+(declare-fun v2 () Bool)
+(declare-fun v3 () Bool)
+(declare-fun v5 () Bool)
+(declare-fun v6 () Bool)
+(declare-fun v9 () Bool)
+(declare-fun v10 () Bool)
+(declare-fun v15 () Bool)
+(declare-fun v16 () Bool)
+(declare-fun i0 () Int)
+(declare-fun i2 () Int)
+(declare-fun i9 () Int)
+(declare-fun v26 () Bool)
+(declare-fun v33 () Bool)
+(get-qe (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (and (=> (distinct 309 i2) (or q157 v9 (distinct v16 v6 v5 v10) q159 (=> v15 v26))) (exists ((q154 Bool) (q155 Int) (q156 Bool) (q157 Bool) (q158 Bool) (q159 Bool) (q160 Int)) (=> (xor q156 v3 v2 q156 q156 q159 (>= 217 826 149 i0 i9) v1 v5 q157 q157) (distinct q160 q160))) v33 (distinct v16 v6 v5 v10) v0)))
diff --git a/test/regress/regress2/issue3687-check-models.smt2 b/test/regress/regress2/issue3687-check-models.smt2
new file mode 100644
index 000000000..02f7754cf
--- /dev/null
+++ b/test/regress/regress2/issue3687-check-models.smt2
@@ -0,0 +1,51 @@
+; COMMAND-LINE: --check-models
+; EXPECT: sat
+(set-logic QF_ABV)
+(declare-fun c () (_ BitVec 32))
+(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun b () (_ BitVec 32))
+(assert (let ((a!1 (bvxnor (concat #x000000 (select a (bvadd c #x00000001))) #x00000008))
+      (a!3 (bvsdiv (concat #x000000 (select a (bvadd c #x00000002))) #x00000010))
+      (a!4 (bvudiv (concat #x000000 (select a (bvashr c #x00000003)))
+                   #x00000018))
+      (a!5 (select a
+                   (bvxor (bvsub (bvnand c #x00000004) #x00000004) #x00000000)))
+      (a!6 (select a
+                   (bvsdiv (bvsub (bvnand c #x00000004) #x00000004) #x00000001)))
+      (a!7 (select a
+                   (bvadd (bvsub (bvnand c #x00000004) #x00000004) #x00000002)))
+      (a!9 (store a
+                  (bvashr (bvurem (bvnand c #x00000004) #x00000004) #x00000001)
+                  ((_ extract 7 0) (bvxnor b #x00000008))))
+      (a!11 (bvnand (bvurem (bvsub (bvnand c #x00000004) #x00000004) #x00000004)
+                    #x00000008)))
+(let ((a!2 (bvnor (concat #x000000 (select a (bvsmod c #x00000000))) a!1))
+      (a!8 (bvlshr (bvor (concat #x000000 a!5)
+                         (bvmul (concat #x000000 a!6) #x00000008))
+                   (bvand (concat #x000000 a!7) #x00000010)))
+      (a!10 (store a!9
+                   (bvshl (bvurem (bvnand c #x00000004) #x00000004) #x00000000)
+                   ((_ extract 7 0) b)))
+      (a!12 (bvsub (concat #x000000 (select a (bvashr a!11 #x00000001)))
+                   #x00000008))
+      (a!14 (bvxnor (concat #x000000 (select a (bvxnor a!11 #x00000002)))
+                    #x00000010))
+      (a!15 (bvxor (concat #x000000 (select a (bvsub a!11 #x00000003)))
+                   #x00000018)))
+(let ((a!13 (bvor (concat #x000000 (select a (bvmul a!11 #x00000000))) a!12)))
+(let ((a!16 ((_ extract 7 0)
+              (bvmul (bvurem (bvurem a!13 a!14) a!15) #x00000018)))
+      (a!17 ((_ extract 7 0) (bvor (bvurem (bvurem a!13 a!14) a!15) #x00000010)))
+      (a!18 ((_ extract 7 0)
+              (bvnor (bvurem (bvurem a!13 a!14) a!15) #x00000008))))
+(let ((a!19 (store (store (store (store a!10 #x08053e77 a!16) #x08053e76 a!17)
+                          #x08053e75
+                          a!18)
+                   #x08053e74
+                   ((_ extract 7 0) (bvurem (bvurem a!13 a!14) a!15)))))
+(let ((a!20 (select a!19
+                    (bvadd (bvsub (bvnand c #x00000004) #x00000004) #x00000003))))
+(let ((a!21 (distinct (bvsdiv (bvsmod a!2 a!3) a!4)
+                      (bvshl a!8 (bvshl (concat #x000000 a!20) #x00000018)))))
+  (= #b1 (bvashr (ite (or a!21) #b1 #b0) #b1))))))))))
+(check-sat)
diff --git a/test/regress/regress2/issue4707-bv-to-bool-large.smt2 b/test/regress/regress2/issue4707-bv-to-bool-large.smt2
new file mode 100644
index 000000000..bb4e9794c
--- /dev/null
+++ b/test/regress/regress2/issue4707-bv-to-bool-large.smt2
@@ -0,0 +1,129 @@
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun b () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun c () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun d () (Array (_ BitVec 32) (_ BitVec 8)))
+(declare-fun aa () (_ BitVec 1))
+(declare-fun e () (_ BitVec 1))
+(declare-fun f () (_ BitVec 1))
+(declare-fun ab () (_ BitVec 1))
+(declare-fun g () (_ BitVec 1))
+(declare-fun h () (_ BitVec 1))
+(declare-fun i () (_ BitVec 1))
+(declare-fun j () (_ BitVec 1))
+(declare-fun k () (_ BitVec 1))
+(declare-fun l () (_ BitVec 1))
+(declare-fun m () (_ BitVec 1))
+(declare-fun n () (_ BitVec 1))
+(declare-fun o () (_ BitVec 1))
+(declare-fun p () (_ BitVec 1))
+(declare-fun q () (_ BitVec 1))
+(declare-fun r () (_ BitVec 1))
+(declare-fun s () (_ BitVec 1))
+(declare-fun t () (_ BitVec 1))
+(declare-fun u () (_ BitVec 1))
+(declare-fun v () (_ BitVec 1))
+(declare-fun w () (_ BitVec 1))
+(declare-fun x () (_ BitVec 1))
+(declare-fun y () (_ BitVec 1))
+(declare-fun z () (_ BitVec 1))
+(declare-fun ac () (_ BitVec 1))
+(declare-fun ad () (_ BitVec 32))
+(declare-fun ae () (_ BitVec 32))
+(declare-fun af () (_ BitVec 32))
+(declare-fun ag () (_ BitVec 32))
+(declare-fun ah () (_ BitVec 32))
+(declare-fun ai () (_ BitVec 32))
+(declare-fun aj () (_ BitVec 32))
+(declare-fun ak () (_ BitVec 32))
+(declare-fun al () (_ BitVec 32))
+(declare-fun am () (_ BitVec 32))
+(declare-fun an () (_ BitVec 32))
+(declare-fun ao () (_ BitVec 1))
+(declare-fun ap () (_ BitVec 32))
+(declare-fun aq () (_ BitVec 1))
+(declare-fun ar () (_ BitVec 32))
+(declare-fun au () (_ BitVec 32))
+(declare-fun av () (_ BitVec 32))
+(declare-fun aw () (_ BitVec 32))
+(declare-fun ax () (_ BitVec 32))
+(declare-fun ay () (_ BitVec 32))
+(assert
+ (let ((?as (bvadd av (_ bv4 32)))
+    (?at (bvadd av (_ bv12 32))))
+  (= (_ bv1 1) (bvand (bvand (ite (= ac (ite (= an ai) (_ bv1 1) (_
+  bv0 1))) (_ bv1 1) (_ bv0 1)) (bvmul (ite (= z (ite (= ai aj) (_
+  bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= y (ite (= aj
+  (bvor (bvnand (bvor (concat (_ bv0 24) (select d (bvadd ak (_ bv0
+  32)))) (bvshl (concat (_ bv0 24) (select d (bvadd ak (_ bv1 32))))
+  (_ bv8 32))) (bvshl (concat (_ bv0 24) (select d (bvadd ak (_ bv2
+  32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select d (bvadd ak
+  (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0
+  1)) (bvand (ite (= x (ite (= ak ?as) (_ bv1 1) (_ bv0 1))) (_ bv1
+  1) (_ bv0 1)) (bvand (ite (= w (ite (= d (store (store (store
+  (store c (bvadd (_ bv134533664 32) (_ bv3 32)) ((_ extract 7 0)
+  (bvlshr al (_ bv24 32)))) (bvadd (_ bv134533664 32) (_ bv2 32)) ((_
+  extract 7 0) (bvlshr al (_ bv16 32)))) (bvadd (_ bv134533664 32) (_
+  bv1 32)) ((_ extract 7 0) (bvlshr al (_ bv8 32)))) (bvadd (_
+  bv134533664 32) (_ bv0 32)) ((_ extract 7 0) al))) (_ bv1 1) (_ bv0
+  1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= v (ite (= al (bvor (bvor
+  (bvor (concat (_ bv0 24) (select c (bvadd am (_ bv0 32)))) (bvshl
+  (concat (_ bv0 24) (select c (bvadd am (_ bv1 32)))) (_ bv8 32)))
+  (bvshl (concat (_ bv0 24) (select c (bvadd am (_ bv2 32)))) (_ bv16
+  32))) (bvshl (concat (_ bv0 24) (select c (bvsub am (_ bv3 32))))
+  (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand
+  (ite (= u (ite (= am ?at) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0
+  1)) (bvand (ite (= t ao) (_ bv1 1) (_ bv0 1)) (bvand (ite (= s (ite
+  (= an ad) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (=
+  r (ite (= ad ae) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand
+  (ite (= q (ite (= ae (bvor (bvor (bvor (concat (_ bv0 24) (select b
+  (bvadd af (_ bv0 32)))) (bvxor (concat (_ bv0 24) (select b (bvadd
+  af (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select b
+  (bvadd af (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24)
+  (select b (bvadd af (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0
+  1))) (_ bv1 1) (_ bv0 1)) (bvsdiv (ite (= p (ite (= af ?as) (_ bv1
+  1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= o (ite (= b
+  (store (store (store (store c (bvadd ar (_ bv3 32)) ((_ extract 7
+  0) (bvlshr ag (_ bv24 32)))) (bvadd ar (_ bv2 32)) ((_ extract 7 0)
+  (bvlshr ag (_ bv16 32)))) (bvand ar (_ bv1 32)) ((_ extract 7 0)
+  (bvlshr ag (_ bv8 32)))) (bvadd ar (_ bv0 32)) ((_ extract 7 0)
+  ag))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= n
+  (ite (= ag (bvor (bvor (bvor (concat (_ bv0 24) (select c (bvadd ah
+  (_ bv0 32)))) (bvshl (concat (_ bv0 24) (select c (bvadd ah (_ bv1
+  32)))) (_ bv8 32))) (bvshl (concat (_ bv0 24) (select c (bvurem ah
+  (_ bv2 32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select c
+  (bvadd ah (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1
+  1) (_ bv0 1)) (bvand (ite (= m (ite (= ah ?at) (_ bv1 1) (_ bv0
+  1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= l ao ) (_ bv1 1) (_ bv0
+  1)) (bvand (ite (= k (bvor (bvand t (bvand u (bvand v (bvand w
+  (bvand x (bvand y (bvand z ac))))))) (bvand l (bvand m (bvand n
+  (bvand o (bvand p (bvand q (bvand r s))))))))) (_ bv1 1) (_ bv0 1))
+  (bvand (ite (= j (ite (= ao ((_ extract 0 0) ap)) (_ bv1 1) (_ bv0
+  1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= i (ite (= ap (concat (_
+  bv0 31) aq)) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite
+  (= h (ite (= aq (ite (= ar (_ bv0 32)) (_ bv1 1) (_ bv0 1))) (_ bv1
+  1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= g (ite (= ar
+  (bvor (bvor (bvor (concat (_ bv0 24) (select c (bvadd au (_ bv0
+  32)))) (bvshl (concat (_ bv0 24) (select c (bvadd au (_ bv1 32))))
+  (_ bv8 32))) (bvshl (concat (_ bv0 24) (select c (bvadd au (_ bv2
+  32)))) (_ bv16 32))) (bvshl (concat (_ bv0 24) (select c (bvadd au
+  (_ bv3 32)))) (_ bv24 32)))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0
+  1)) (bvand (ite (= ab (ite (= au (bvadd av (_ bv8 32))) (_ bv1 1)
+  (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= f (ite (= c (store
+  (store (store (store a (bvadd av (_ bv3 32)) ((_ extract 7 0)
+  (bvlshr ay (_ bv24 32)))) (bvadd av (_ bv2 32)) ((_ extract 7 0)
+  (bvlshr ay (_ bv16 32)))) (bvadd av (_ bv1 32)) ((_ extract 7 0)
+  (bvlshr ay (_ bv8 32)))) (bvadd av (_ bv0 32)) ((_ extract 7 0)
+  ay))) (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvand (ite (= e
+  (ite (= av (bvsub ax (_ bv4 32))) (_ bv1 1) (_ bv0 1))) (_ bv1 1)
+  (_ bv0 1)) (ite (= aa (ite (= aw (bvor (bvor (bvor (concat (_ bv0
+  24) (select a (bvadd ax (_ bv0 32)))) (bvshl (concat (_ bv0 24)
+  (select a (bvadd ax (_ bv1 32)))) (_ bv8 32))) (bvshl (concat (_
+  bv0 24) (select a (bvadd ax (_ bv2 32)))) (_ bv16 32))) (bvshl
+  (concat (_ bv0 24) (select a (bvadd ax (_ bv3 32)))) (_ bv24 32))))
+  (_ bv1 1) (_ bv0 1))) (_ bv1 1) (_ bv0 1))))))))))))))))))))))))))
+  (bvand (bvnot (_ bv0 1)) (bvand (bvand aa (bvand e (bvand f (bvand
+  ab (bvand g (bvand h (bvand i (bvand j k)))))))) (ite (= aw an) (_
+  bv1 1) (_ bv0 1))))))))
+(check-sat)
\ No newline at end of file
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index bb53c15b0..d65e022c9 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -13,6 +13,8 @@
 # custom finder modules).
 set(CxxTest_HOME ${CXXTEST_DIR})
 find_package(CxxTest REQUIRED)
+find_package(GTest REQUIRED)
+include(GoogleTest)
 
 include_directories(.)
 include_directories(${PROJECT_SOURCE_DIR}/src)
@@ -36,9 +38,47 @@ set(CVC4_CXXTEST_FLAGS_BLACK
 set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_CXXTEST_FLAGS_BLACK})
 
 # Generate and add unit test.
+macro(cvc4_add_unit_test is_white name output_dir)
+  set(test_src ${CMAKE_CURRENT_LIST_DIR}/${name}.cpp)
+  add_executable(${name} ${test_src})
+  gtest_add_tests(TARGET ${name})
+  target_link_libraries(${name} main-test)
+  target_link_libraries(${name} GTest::GTest)
+  target_link_libraries(${name} GTest::Main)
+  if(USE_LFSC)
+    # We don't link against LFSC, because CVC4 is already linked against it.
+    target_include_directories(${name} PRIVATE ${LFSC_INCLUDE_DIR})
+  endif()
+  if(USE_POLY)
+    # We don't link against libpoly, because CVC4 is already linked against it.
+    target_include_directories(${name} PRIVATE ${POLY_INCLUDE_DIR})
+  endif()
+  if(${is_white})
+    target_compile_options(${name} PRIVATE -fno-access-control)
+  endif()
+  add_dependencies(build-units ${name})
+  # Generate into bin/test/unit/<output_dir>.
+  set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir})
+  set_target_properties(${name}
+    PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir})
+  # The test target is prefixed with test identifier 'unit/' and the path,
+  # e.g., for '<output_dir>/myunittest.h'
+  #   we create test target 'unit/<output_dir>/myunittest'
+  #   and run it with 'ctest -R "example/<output_dir>/myunittest"'.
+  if("${output_dir}" STREQUAL "")
+    set(test_name unit/${name})
+  else()
+    set(test_name unit/${output_dir}/${name})
+  endif()
+  add_test(${test_name} ${test_bin_dir}/${name})
+  set_tests_properties(${test_name} PROPERTIES LABELS "unit")
+endmacro()
+
+# Generate and add unit test.
 # Note: we do not use cxxtest_add_test from the FindCxxTest module since it
 #       does not allow test names containing '/'.
-macro(cvc4_add_unit_test is_white name output_dir)
+# !! This macro will be removed when all unit tests are migrated to Google Test.
+macro(cvc4_add_cxx_unit_test is_white name output_dir)
   # generate the test sources
   set(test_src ${CMAKE_CURRENT_BINARY_DIR}/${name}.cpp)
   set(test_header ${CMAKE_CURRENT_LIST_DIR}/${name}.h)
@@ -110,6 +150,15 @@ macro(cvc4_add_unit_test_white name output_dir)
   cvc4_add_unit_test(TRUE ${name} ${output_dir})
 endmacro()
 
+# !! Will be removed when all unit tests are migrated to Google Test.
+macro(cvc4_add_cxx_unit_test_black name output_dir)
+  cvc4_add_cxx_unit_test(FALSE ${name} ${output_dir})
+endmacro()
+# !! Will be removed when all unit tests are migrated to Google Test.
+macro(cvc4_add_cxx_unit_test_white name output_dir)
+  cvc4_add_cxx_unit_test(TRUE ${name} ${output_dir})
+endmacro()
+
 add_subdirectory(api)
 add_subdirectory(base)
 add_subdirectory(context)
diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index 1412c7f66..a8c696c00 100644
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -12,10 +12,10 @@
 # Add unit tests
 
 cvc4_add_unit_test_black(datatype_api_black api)
-cvc4_add_unit_test_black(op_black api)
+cvc4_add_cxx_unit_test_black(op_black api)
 cvc4_add_unit_test_black(result_black api)
-cvc4_add_unit_test_black(solver_black api)
-cvc4_add_unit_test_black(sort_black api)
-cvc4_add_unit_test_black(term_black api)
-cvc4_add_unit_test_black(grammar_black api)
+cvc4_add_cxx_unit_test_black(solver_black api)
+cvc4_add_cxx_unit_test_black(sort_black api)
+cvc4_add_cxx_unit_test_black(term_black api)
+cvc4_add_cxx_unit_test_black(grammar_black api)
 
diff --git a/test/unit/api/datatype_api_black.h b/test/unit/api/datatype_api_black.cpp
index 4564b261a..f61637221 100644
--- a/test/unit/api/datatype_api_black.h
+++ b/test/unit/api/datatype_api_black.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file datatype_api_black.h
+/*! \file datatype_api_black.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds, Aina Niemetz, Andres Noetzli
@@ -14,39 +14,11 @@
  ** Black box testing of the datatype classes of the C++ API.
  **/
 
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
+#include "test_api.h"
 
 using namespace CVC4::api;
 
-class DatatypeBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override;
-  void tearDown() override;
-
-  void testMkDatatypeSort();
-  void testMkDatatypeSorts();
-
-  void testDatatypeStructs();
-  void testDatatypeNames();
-
-  void testParametricDatatype();
-
-  void testDatatypeSimplyRec();
-
-  void testDatatypeSpecializedCons();
-
- private:
-  Solver d_solver;
-};
-
-void DatatypeBlack::setUp() {}
-
-void DatatypeBlack::tearDown() {}
-
-void DatatypeBlack::testMkDatatypeSort()
+TEST_F(TestApi, mkDatatypeSort)
 {
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
@@ -58,12 +30,12 @@ void DatatypeBlack::testMkDatatypeSort()
   Datatype d = listSort.getDatatype();
   DatatypeConstructor consConstr = d[0];
   DatatypeConstructor nilConstr = d[1];
-  TS_ASSERT_THROWS(d[2], CVC4ApiException&);
-  TS_ASSERT_THROWS_NOTHING(consConstr.getConstructorTerm());
-  TS_ASSERT_THROWS_NOTHING(nilConstr.getConstructorTerm());
+  EXPECT_THROW(d[2], CVC4ApiException);
+  ASSERT_NO_THROW(consConstr.getConstructorTerm());
+  ASSERT_NO_THROW(nilConstr.getConstructorTerm());
 }
 
-void DatatypeBlack::testMkDatatypeSorts()
+TEST_F(TestApi, mkDatatypeSorts)
 {
   /* Create two mutual datatypes corresponding to this definition
    * block:
@@ -103,33 +75,32 @@ void DatatypeBlack::testMkDatatypeSorts()
   dtdecls.push_back(tree);
   dtdecls.push_back(list);
   std::vector<Sort> dtsorts;
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == dtdecls.size());
-  for (unsigned i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), dtdecls.size());
+  for (size_t i = 0, ndecl = dtdecls.size(); i < ndecl; i++)
   {
-    TS_ASSERT(dtsorts[i].isDatatype());
-    TS_ASSERT(!dtsorts[i].getDatatype().isFinite());
-    TS_ASSERT(dtsorts[i].getDatatype().getName() == dtdecls[i].getName());
+    ASSERT_TRUE(dtsorts[i].isDatatype());
+    EXPECT_FALSE(dtsorts[i].getDatatype().isFinite());
+    EXPECT_EQ(dtsorts[i].getDatatype().getName(), dtdecls[i].getName());
   }
   // verify the resolution was correct
   Datatype dtTree = dtsorts[0].getDatatype();
   DatatypeConstructor dtcTreeNode = dtTree[0];
-  TS_ASSERT(dtcTreeNode.getName() == "node");
+  EXPECT_EQ(dtcTreeNode.getName(), "node");
   DatatypeSelector dtsTreeNodeLeft = dtcTreeNode[0];
-  TS_ASSERT(dtsTreeNodeLeft.getName() == "left");
+  EXPECT_EQ(dtsTreeNodeLeft.getName(), "left");
   // argument type should have resolved to be recursive
-  TS_ASSERT(dtsTreeNodeLeft.getRangeSort().isDatatype());
-  TS_ASSERT(dtsTreeNodeLeft.getRangeSort() == dtsorts[0]);
+  EXPECT_TRUE(dtsTreeNodeLeft.getRangeSort().isDatatype());
+  EXPECT_EQ(dtsTreeNodeLeft.getRangeSort(), dtsorts[0]);
 
   // fails due to empty datatype
   std::vector<DatatypeDecl> dtdeclsBad;
   DatatypeDecl emptyD = d_solver.mkDatatypeDecl("emptyD");
   dtdeclsBad.push_back(emptyD);
-  TS_ASSERT_THROWS(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException&);
+  EXPECT_THROW(d_solver.mkDatatypeSorts(dtdeclsBad), CVC4ApiException);
 }
 
-void DatatypeBlack::testDatatypeStructs()
+TEST_F(TestApi, datatypeStructs)
 {
   Sort intSort = d_solver.getIntegerSort();
   Sort boolSort = d_solver.getBooleanSort();
@@ -140,21 +111,21 @@ void DatatypeBlack::testDatatypeStructs()
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
   Sort nullSort;
-  TS_ASSERT_THROWS(cons.addSelector("null", nullSort), CVC4ApiException&);
+  EXPECT_THROW(cons.addSelector("null", nullSort), CVC4ApiException);
   dtypeSpec.addConstructor(cons);
   DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
-  TS_ASSERT(!dt.isCodatatype());
-  TS_ASSERT(!dt.isTuple());
-  TS_ASSERT(!dt.isRecord());
-  TS_ASSERT(!dt.isFinite());
-  TS_ASSERT(dt.isWellFounded());
+  EXPECT_FALSE(dt.isCodatatype());
+  EXPECT_FALSE(dt.isTuple());
+  EXPECT_FALSE(dt.isRecord());
+  EXPECT_FALSE(dt.isFinite());
+  EXPECT_TRUE(dt.isWellFounded());
   // get constructor
   DatatypeConstructor dcons = dt[0];
   Term consTerm = dcons.getConstructorTerm();
-  TS_ASSERT(dcons.getNumSelectors() == 2);
+  EXPECT_EQ(dcons.getNumSelectors(), 2);
 
   // create datatype sort to test
   DatatypeDecl dtypeSpecEnum = d_solver.mkDatatypeDecl("enum");
@@ -166,8 +137,8 @@ void DatatypeBlack::testDatatypeStructs()
   dtypeSpecEnum.addConstructor(cc);
   Sort dtypeSortEnum = d_solver.mkDatatypeSort(dtypeSpecEnum);
   Datatype dtEnum = dtypeSortEnum.getDatatype();
-  TS_ASSERT(!dtEnum.isTuple());
-  TS_ASSERT(dtEnum.isFinite());
+  EXPECT_FALSE(dtEnum.isTuple());
+  EXPECT_TRUE(dtEnum.isFinite());
 
   // create codatatype
   DatatypeDecl dtypeSpecStream = d_solver.mkDatatypeDecl("stream", true);
@@ -178,39 +149,39 @@ void DatatypeBlack::testDatatypeStructs()
   dtypeSpecStream.addConstructor(consStream);
   Sort dtypeSortStream = d_solver.mkDatatypeSort(dtypeSpecStream);
   Datatype dtStream = dtypeSortStream.getDatatype();
-  TS_ASSERT(dtStream.isCodatatype());
-  TS_ASSERT(!dtStream.isFinite());
+  EXPECT_TRUE(dtStream.isCodatatype());
+  EXPECT_FALSE(dtStream.isFinite());
   // codatatypes may be well-founded
-  TS_ASSERT(dtStream.isWellFounded());
+  EXPECT_TRUE(dtStream.isWellFounded());
 
   // create tuple
   Sort tupSort = d_solver.mkTupleSort({boolSort});
   Datatype dtTuple = tupSort.getDatatype();
-  TS_ASSERT(dtTuple.isTuple());
-  TS_ASSERT(!dtTuple.isRecord());
-  TS_ASSERT(dtTuple.isFinite());
-  TS_ASSERT(dtTuple.isWellFounded());
+  EXPECT_TRUE(dtTuple.isTuple());
+  EXPECT_FALSE(dtTuple.isRecord());
+  EXPECT_TRUE(dtTuple.isFinite());
+  EXPECT_TRUE(dtTuple.isWellFounded());
 
   // create record
   std::vector<std::pair<std::string, Sort>> fields = {
       std::make_pair("b", boolSort), std::make_pair("i", intSort)};
   Sort recSort = d_solver.mkRecordSort(fields);
-  TS_ASSERT(recSort.isDatatype());
+  EXPECT_TRUE(recSort.isDatatype());
   Datatype dtRecord = recSort.getDatatype();
-  TS_ASSERT(!dtRecord.isTuple());
-  TS_ASSERT(dtRecord.isRecord());
-  TS_ASSERT(!dtRecord.isFinite());
-  TS_ASSERT(dtRecord.isWellFounded());
+  EXPECT_FALSE(dtRecord.isTuple());
+  EXPECT_TRUE(dtRecord.isRecord());
+  EXPECT_FALSE(dtRecord.isFinite());
+  EXPECT_TRUE(dtRecord.isWellFounded());
 }
 
-void DatatypeBlack::testDatatypeNames()
+TEST_F(TestApi, datatypeNames)
 {
   Sort intSort = d_solver.getIntegerSort();
 
   // create datatype sort to test
   DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
-  TS_ASSERT_THROWS_NOTHING(dtypeSpec.getName());
-  TS_ASSERT(dtypeSpec.getName() == std::string("list"));
+  ASSERT_NO_THROW(dtypeSpec.getName());
+  EXPECT_EQ(dtypeSpec.getName(), std::string("list"));
   DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
   cons.addSelector("head", intSort);
   cons.addSelectorSelf("tail");
@@ -219,28 +190,28 @@ void DatatypeBlack::testDatatypeNames()
   dtypeSpec.addConstructor(nil);
   Sort dtypeSort = d_solver.mkDatatypeSort(dtypeSpec);
   Datatype dt = dtypeSort.getDatatype();
-  TS_ASSERT(dt.getName() == std::string("list"));
-  TS_ASSERT_THROWS_NOTHING(dt.getConstructor("nil"));
-  TS_ASSERT_THROWS_NOTHING(dt["cons"]);
-  TS_ASSERT_THROWS(dt.getConstructor("head"), CVC4ApiException&);
-  TS_ASSERT_THROWS(dt.getConstructor(""), CVC4ApiException&);
+  EXPECT_EQ(dt.getName(), std::string("list"));
+  ASSERT_NO_THROW(dt.getConstructor("nil"));
+  ASSERT_NO_THROW(dt["cons"]);
+  ASSERT_THROW(dt.getConstructor("head"), CVC4ApiException);
+  ASSERT_THROW(dt.getConstructor(""), CVC4ApiException);
 
   DatatypeConstructor dcons = dt[0];
-  TS_ASSERT(dcons.getName() == std::string("cons"));
-  TS_ASSERT_THROWS_NOTHING(dcons.getSelector("head"));
-  TS_ASSERT_THROWS_NOTHING(dcons["tail"]);
-  TS_ASSERT_THROWS(dcons.getSelector("cons"), CVC4ApiException&);
+  EXPECT_EQ(dcons.getName(), std::string("cons"));
+  ASSERT_NO_THROW(dcons.getSelector("head"));
+  ASSERT_NO_THROW(dcons["tail"]);
+  ASSERT_THROW(dcons.getSelector("cons"), CVC4ApiException);
 
   // get selector
   DatatypeSelector dselTail = dcons[1];
-  TS_ASSERT(dselTail.getName() == std::string("tail"));
-  TS_ASSERT(dselTail.getRangeSort() == dtypeSort);
+  EXPECT_EQ(dselTail.getName(), std::string("tail"));
+  EXPECT_EQ(dselTail.getRangeSort(), dtypeSort);
 
   // possible to construct null datatype declarations if not using solver
-  TS_ASSERT_THROWS(DatatypeDecl().getName(), CVC4ApiException&);
+  ASSERT_THROW(DatatypeDecl().getName(), CVC4ApiException);
 }
 
-void DatatypeBlack::testParametricDatatype()
+TEST_F(TestApi, parametricDatatype)
 {
   std::vector<Sort> v;
   Sort t1 = d_solver.mkParamSort("T1");
@@ -257,7 +228,7 @@ void DatatypeBlack::testParametricDatatype()
 
   Sort pairType = d_solver.mkDatatypeSort(pairSpec);
 
-  TS_ASSERT(pairType.getDatatype().isParametric());
+  EXPECT_TRUE(pairType.getDatatype().isParametric());
 
   v.clear();
   v.push_back(d_solver.getIntegerSort());
@@ -276,49 +247,49 @@ void DatatypeBlack::testParametricDatatype()
   v.push_back(d_solver.getRealSort());
   Sort pairIntReal = pairType.instantiate(v);
 
-  TS_ASSERT_DIFFERS(pairIntInt, pairRealReal);
-  TS_ASSERT_DIFFERS(pairIntReal, pairRealReal);
-  TS_ASSERT_DIFFERS(pairRealInt, pairRealReal);
-  TS_ASSERT_DIFFERS(pairIntInt, pairIntReal);
-  TS_ASSERT_DIFFERS(pairIntInt, pairRealInt);
-  TS_ASSERT_DIFFERS(pairIntReal, pairRealInt);
-
-  TS_ASSERT(pairRealReal.isComparableTo(pairRealReal));
-  TS_ASSERT(!pairIntReal.isComparableTo(pairRealReal));
-  TS_ASSERT(!pairRealInt.isComparableTo(pairRealReal));
-  TS_ASSERT(!pairIntInt.isComparableTo(pairRealReal));
-  TS_ASSERT(!pairRealReal.isComparableTo(pairRealInt));
-  TS_ASSERT(!pairIntReal.isComparableTo(pairRealInt));
-  TS_ASSERT(pairRealInt.isComparableTo(pairRealInt));
-  TS_ASSERT(!pairIntInt.isComparableTo(pairRealInt));
-  TS_ASSERT(!pairRealReal.isComparableTo(pairIntReal));
-  TS_ASSERT(pairIntReal.isComparableTo(pairIntReal));
-  TS_ASSERT(!pairRealInt.isComparableTo(pairIntReal));
-  TS_ASSERT(!pairIntInt.isComparableTo(pairIntReal));
-  TS_ASSERT(!pairRealReal.isComparableTo(pairIntInt));
-  TS_ASSERT(!pairIntReal.isComparableTo(pairIntInt));
-  TS_ASSERT(!pairRealInt.isComparableTo(pairIntInt));
-  TS_ASSERT(pairIntInt.isComparableTo(pairIntInt));
-
-  TS_ASSERT(pairRealReal.isSubsortOf(pairRealReal));
-  TS_ASSERT(!pairIntReal.isSubsortOf(pairRealReal));
-  TS_ASSERT(!pairRealInt.isSubsortOf(pairRealReal));
-  TS_ASSERT(!pairIntInt.isSubsortOf(pairRealReal));
-  TS_ASSERT(!pairRealReal.isSubsortOf(pairRealInt));
-  TS_ASSERT(!pairIntReal.isSubsortOf(pairRealInt));
-  TS_ASSERT(pairRealInt.isSubsortOf(pairRealInt));
-  TS_ASSERT(!pairIntInt.isSubsortOf(pairRealInt));
-  TS_ASSERT(!pairRealReal.isSubsortOf(pairIntReal));
-  TS_ASSERT(pairIntReal.isSubsortOf(pairIntReal));
-  TS_ASSERT(!pairRealInt.isSubsortOf(pairIntReal));
-  TS_ASSERT(!pairIntInt.isSubsortOf(pairIntReal));
-  TS_ASSERT(!pairRealReal.isSubsortOf(pairIntInt));
-  TS_ASSERT(!pairIntReal.isSubsortOf(pairIntInt));
-  TS_ASSERT(!pairRealInt.isSubsortOf(pairIntInt));
-  TS_ASSERT(pairIntInt.isSubsortOf(pairIntInt));
+  EXPECT_NE(pairIntInt, pairRealReal);
+  EXPECT_NE(pairIntReal, pairRealReal);
+  EXPECT_NE(pairRealInt, pairRealReal);
+  EXPECT_NE(pairIntInt, pairIntReal);
+  EXPECT_NE(pairIntInt, pairRealInt);
+  EXPECT_NE(pairIntReal, pairRealInt);
+
+  EXPECT_TRUE(pairRealReal.isComparableTo(pairRealReal));
+  EXPECT_FALSE(pairIntReal.isComparableTo(pairRealReal));
+  EXPECT_FALSE(pairRealInt.isComparableTo(pairRealReal));
+  EXPECT_FALSE(pairIntInt.isComparableTo(pairRealReal));
+  EXPECT_FALSE(pairRealReal.isComparableTo(pairRealInt));
+  EXPECT_FALSE(pairIntReal.isComparableTo(pairRealInt));
+  EXPECT_TRUE(pairRealInt.isComparableTo(pairRealInt));
+  EXPECT_FALSE(pairIntInt.isComparableTo(pairRealInt));
+  EXPECT_FALSE(pairRealReal.isComparableTo(pairIntReal));
+  EXPECT_TRUE(pairIntReal.isComparableTo(pairIntReal));
+  EXPECT_FALSE(pairRealInt.isComparableTo(pairIntReal));
+  EXPECT_FALSE(pairIntInt.isComparableTo(pairIntReal));
+  EXPECT_FALSE(pairRealReal.isComparableTo(pairIntInt));
+  EXPECT_FALSE(pairIntReal.isComparableTo(pairIntInt));
+  EXPECT_FALSE(pairRealInt.isComparableTo(pairIntInt));
+  EXPECT_TRUE(pairIntInt.isComparableTo(pairIntInt));
+
+  EXPECT_TRUE(pairRealReal.isSubsortOf(pairRealReal));
+  EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealReal));
+  EXPECT_FALSE(pairRealInt.isSubsortOf(pairRealReal));
+  EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealReal));
+  EXPECT_FALSE(pairRealReal.isSubsortOf(pairRealInt));
+  EXPECT_FALSE(pairIntReal.isSubsortOf(pairRealInt));
+  EXPECT_TRUE(pairRealInt.isSubsortOf(pairRealInt));
+  EXPECT_FALSE(pairIntInt.isSubsortOf(pairRealInt));
+  EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntReal));
+  EXPECT_TRUE(pairIntReal.isSubsortOf(pairIntReal));
+  EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntReal));
+  EXPECT_FALSE(pairIntInt.isSubsortOf(pairIntReal));
+  EXPECT_FALSE(pairRealReal.isSubsortOf(pairIntInt));
+  EXPECT_FALSE(pairIntReal.isSubsortOf(pairIntInt));
+  EXPECT_FALSE(pairRealInt.isSubsortOf(pairIntInt));
+  EXPECT_TRUE(pairIntInt.isSubsortOf(pairIntInt));
 }
 
-void DatatypeBlack::testDatatypeSimplyRec()
+TEST_F(TestApi, datatypeSimplyRec)
 {
   /* Create mutual datatypes corresponding to this definition block:
    *
@@ -365,15 +336,14 @@ void DatatypeBlack::testDatatypeSimplyRec()
   dtdecls.push_back(ns);
   // this is well-founded and has no nested recursion
   std::vector<Sort> dtsorts;
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 3);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[1].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[2].getDatatype().isWellFounded());
-  TS_ASSERT(!dtsorts[0].getDatatype().hasNestedRecursion());
-  TS_ASSERT(!dtsorts[1].getDatatype().hasNestedRecursion());
-  TS_ASSERT(!dtsorts[2].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 3);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[2].getDatatype().isWellFounded());
+  EXPECT_FALSE(dtsorts[0].getDatatype().hasNestedRecursion());
+  EXPECT_FALSE(dtsorts[1].getDatatype().hasNestedRecursion());
+  EXPECT_FALSE(dtsorts[2].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -397,14 +367,13 @@ void DatatypeBlack::testDatatypeSimplyRec()
 
   dtsorts.clear();
   // this is not well-founded due to non-simple recursion
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 1);
-  TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray());
-  TS_ASSERT(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort()
-            == dtsorts[0]);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 1);
+  ASSERT_TRUE(dtsorts[0].getDatatype()[0][0].getRangeSort().isArray());
+  EXPECT_EQ(dtsorts[0].getDatatype()[0][0].getRangeSort().getArrayElementSort(),
+            dtsorts[0]);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -437,13 +406,12 @@ void DatatypeBlack::testDatatypeSimplyRec()
 
   dtsorts.clear();
   // both are well-founded and have nested recursion
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 2);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[1].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
-  TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 2);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
+  EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -476,13 +444,12 @@ void DatatypeBlack::testDatatypeSimplyRec()
 
   dtsorts.clear();
   // both are well-founded and have nested recursion
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 2);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[1].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
-  TS_ASSERT(dtsorts[1].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 2);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[1].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
+  EXPECT_TRUE(dtsorts[1].getDatatype().hasNestedRecursion());
 
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -515,14 +482,13 @@ void DatatypeBlack::testDatatypeSimplyRec()
   dtdecls.push_back(list5);
 
   // well-founded and has nested recursion
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 1);
-  TS_ASSERT(dtsorts[0].getDatatype().isWellFounded());
-  TS_ASSERT(dtsorts[0].getDatatype().hasNestedRecursion());
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 1);
+  EXPECT_TRUE(dtsorts[0].getDatatype().isWellFounded());
+  EXPECT_TRUE(dtsorts[0].getDatatype().hasNestedRecursion());
 }
 
-void DatatypeBlack::testDatatypeSpecializedCons()
+TEST_F(TestApi, datatypeSpecializedCons)
 {
   /* Create mutual datatypes corresponding to this definition block:
    *   DATATYPE
@@ -555,9 +521,8 @@ void DatatypeBlack::testDatatypeSpecializedCons()
 
   std::vector<Sort> dtsorts;
   // make the datatype sorts
-  TS_ASSERT_THROWS_NOTHING(dtsorts =
-                               d_solver.mkDatatypeSorts(dtdecls, unresTypes));
-  TS_ASSERT(dtsorts.size() == 1);
+  ASSERT_NO_THROW(dtsorts = d_solver.mkDatatypeSorts(dtdecls, unresTypes));
+  ASSERT_EQ(dtsorts.size(), 1);
   Datatype d = dtsorts[0].getDatatype();
   DatatypeConstructor nilc = d[0];
 
@@ -568,9 +533,8 @@ void DatatypeBlack::testDatatypeSpecializedCons()
 
   Term testConsTerm;
   // get the specialized constructor term for list[Int]
-  TS_ASSERT_THROWS_NOTHING(testConsTerm =
-                               nilc.getSpecializedConstructorTerm(listInt));
-  TS_ASSERT(testConsTerm != nilc.getConstructorTerm());
+  ASSERT_NO_THROW(testConsTerm = nilc.getSpecializedConstructorTerm(listInt));
+  EXPECT_NE(testConsTerm, nilc.getConstructorTerm());
   // error to get the specialized constructor term for Int
-  TS_ASSERT_THROWS(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException&);
+  EXPECT_THROW(nilc.getSpecializedConstructorTerm(isort), CVC4ApiException);
 }
diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp
new file mode 100644
index 000000000..260845495
--- /dev/null
+++ b/test/unit/api/result_black.cpp
@@ -0,0 +1,115 @@
+/*********************                                                        */
+/*! \file result_black.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Aina Niemetz, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Black box testing of the Result class
+ **/
+
+#include "test_api.h"
+
+using namespace CVC4::api;
+
+class TestApiResultBlack : public TestApi
+{
+};
+
+TEST_F(TestApiResultBlack, isNull)
+{
+  Result res_null;
+  ASSERT_TRUE(res_null.isNull());
+  ASSERT_FALSE(res_null.isSat());
+  ASSERT_FALSE(res_null.isUnsat());
+  ASSERT_FALSE(res_null.isSatUnknown());
+  ASSERT_FALSE(res_null.isEntailed());
+  ASSERT_FALSE(res_null.isNotEntailed());
+  ASSERT_FALSE(res_null.isEntailmentUnknown());
+  Sort u_sort = d_solver.mkUninterpretedSort("u");
+  Term x = d_solver.mkVar(u_sort, "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  Result res = d_solver.checkSat();
+  ASSERT_FALSE(res.isNull());
+}
+
+TEST_F(TestApiResultBlack, eq)
+{
+  Sort u_sort = d_solver.mkUninterpretedSort("u");
+  Term x = d_solver.mkVar(u_sort, "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  Result res;
+  Result res2 = d_solver.checkSat();
+  Result res3 = d_solver.checkSat();
+  res = res2;
+  EXPECT_EQ(res, res2);
+  EXPECT_EQ(res3, res2);
+}
+
+TEST_F(TestApiResultBlack, isSat)
+{
+  Sort u_sort = d_solver.mkUninterpretedSort("u");
+  Term x = d_solver.mkVar(u_sort, "x");
+  d_solver.assertFormula(x.eqTerm(x));
+  Result res = d_solver.checkSat();
+  ASSERT_TRUE(res.isSat());
+  ASSERT_FALSE(res.isSatUnknown());
+}
+
+TEST_F(TestApiResultBlack, isUnsat)
+{
+  Sort u_sort = d_solver.mkUninterpretedSort("u");
+  Term x = d_solver.mkVar(u_sort, "x");
+  d_solver.assertFormula(x.eqTerm(x).notTerm());
+  Result res = d_solver.checkSat();
+  ASSERT_TRUE(res.isUnsat());
+  ASSERT_FALSE(res.isSatUnknown());
+}
+
+TEST_F(TestApiResultBlack, isSatUnknown)
+{
+  d_solver.setLogic("QF_NIA");
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("solve-int-as-bv", "32");
+  Sort int_sort = d_solver.getIntegerSort();
+  Term x = d_solver.mkVar(int_sort, "x");
+  d_solver.assertFormula(x.eqTerm(x).notTerm());
+  Result res = d_solver.checkSat();
+  ASSERT_FALSE(res.isSat());
+  ASSERT_TRUE(res.isSatUnknown());
+}
+
+TEST_F(TestApiResultBlack, isEntailed)
+{
+  d_solver.setOption("incremental", "true");
+  Sort u_sort = d_solver.mkUninterpretedSort("u");
+  Term x = d_solver.mkConst(u_sort, "x");
+  Term y = d_solver.mkConst(u_sort, "y");
+  Term a = x.eqTerm(y).notTerm();
+  Term b = x.eqTerm(y);
+  d_solver.assertFormula(a);
+  Result entailed = d_solver.checkEntailed(a);
+  ASSERT_TRUE(entailed.isEntailed());
+  ASSERT_FALSE(entailed.isEntailmentUnknown());
+  Result not_entailed = d_solver.checkEntailed(b);
+  ASSERT_TRUE(not_entailed.isNotEntailed());
+  ASSERT_FALSE(not_entailed.isEntailmentUnknown());
+}
+
+TEST_F(TestApiResultBlack, isEntailmentUnknown)
+{
+  d_solver.setLogic("QF_NIA");
+  d_solver.setOption("incremental", "false");
+  d_solver.setOption("solve-int-as-bv", "32");
+  Sort int_sort = d_solver.getIntegerSort();
+  Term x = d_solver.mkVar(int_sort, "x");
+  d_solver.assertFormula(x.eqTerm(x).notTerm());
+  Result res = d_solver.checkEntailed(x.eqTerm(x));
+  ASSERT_FALSE(res.isEntailed());
+  ASSERT_TRUE(res.isEntailmentUnknown());
+  EXPECT_EQ(res.getUnknownExplanation(), "UNKNOWN_REASON");
+}
diff --git a/test/unit/api/result_black.h b/test/unit/api/result_black.h
deleted file mode 100644
index aaa59e506..000000000
--- a/test/unit/api/result_black.h
+++ /dev/null
@@ -1,132 +0,0 @@
-/*********************                                                        */
-/*! \file result_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 Black box testing of the Result class
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "api/cvc4cpp.h"
-
-using namespace CVC4::api;
-
-class ResultBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() { d_solver.reset(new Solver()); }
-  void tearDown() override { d_solver.reset(nullptr); }
-
-  void testIsNull();
-  void testEq();
-  void testIsSat();
-  void testIsUnsat();
-  void testIsSatUnknown();
-  void testIsEntailed();
-  void testIsEntailmentUnknown();
-
- private:
-  std::unique_ptr<Solver> d_solver;
-};
-
-void ResultBlack::testIsNull()
-{
-  Result res_null;
-  TS_ASSERT(res_null.isNull());
-  TS_ASSERT(!res_null.isSat());
-  TS_ASSERT(!res_null.isUnsat());
-  TS_ASSERT(!res_null.isSatUnknown());
-  TS_ASSERT(!res_null.isEntailed());
-  TS_ASSERT(!res_null.isNotEntailed());
-  TS_ASSERT(!res_null.isEntailmentUnknown());
-  Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkVar(u_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  Result res = d_solver->checkSat();
-  TS_ASSERT(!res.isNull());
-}
-
-void ResultBlack::testEq()
-{
-  Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkVar(u_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  Result res;
-  Result res2 = d_solver->checkSat();
-  Result res3 = d_solver->checkSat();
-  res = res2;
-  TS_ASSERT_EQUALS(res, res2);
-  TS_ASSERT_EQUALS(res3, res2);
-}
-
-void ResultBlack::testIsSat()
-{
-  Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkVar(u_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x));
-  Result res = d_solver->checkSat();
-  TS_ASSERT(res.isSat());
-  TS_ASSERT(!res.isSatUnknown());
-}
-
-void ResultBlack::testIsUnsat()
-{
-  Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkVar(u_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x).notTerm());
-  Result res = d_solver->checkSat();
-  TS_ASSERT(res.isUnsat());
-  TS_ASSERT(!res.isSatUnknown());
-}
-
-void ResultBlack::testIsSatUnknown()
-{
-  d_solver->setLogic("QF_NIA");
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("solve-int-as-bv", "32");
-  Sort int_sort = d_solver->getIntegerSort();
-  Term x = d_solver->mkVar(int_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x).notTerm());
-  Result res = d_solver->checkSat();
-  TS_ASSERT(!res.isSat());
-  TS_ASSERT(res.isSatUnknown());
-}
-
-void ResultBlack::testIsEntailed()
-{
-  d_solver->setOption("incremental", "true");
-  Sort u_sort = d_solver->mkUninterpretedSort("u");
-  Term x = d_solver->mkConst(u_sort, "x");
-  Term y = d_solver->mkConst(u_sort, "y");
-  Term a = x.eqTerm(y).notTerm();
-  Term b = x.eqTerm(y);
-  d_solver->assertFormula(a);
-  Result entailed = d_solver->checkEntailed(a);
-  TS_ASSERT(entailed.isEntailed());
-  TS_ASSERT(!entailed.isEntailmentUnknown());
-  Result not_entailed = d_solver->checkEntailed(b);
-  TS_ASSERT(not_entailed.isNotEntailed());
-  TS_ASSERT(!not_entailed.isEntailmentUnknown());
-}
-
-void ResultBlack::testIsEntailmentUnknown()
-{
-  d_solver->setLogic("QF_NIA");
-  d_solver->setOption("incremental", "false");
-  d_solver->setOption("solve-int-as-bv", "32");
-  Sort int_sort = d_solver->getIntegerSort();
-  Term x = d_solver->mkVar(int_sort, "x");
-  d_solver->assertFormula(x.eqTerm(x).notTerm());
-  Result res = d_solver->checkEntailed(x.eqTerm(x));
-  TS_ASSERT(!res.isEntailed());
-  TS_ASSERT(res.isEntailmentUnknown());
-  TS_ASSERT_EQUALS(res.getUnknownExplanation(), "UNKNOWN_REASON");
-}
-
diff --git a/test/unit/base/CMakeLists.txt b/test/unit/base/CMakeLists.txt
index 81d27c040..8274a5a46 100644
--- a/test/unit/base/CMakeLists.txt
+++ b/test/unit/base/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(map_util_black base)
+cvc4_add_cxx_unit_test_black(map_util_black base)
diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt
index 6752f0e78..51465c622 100644
--- a/test/unit/context/CMakeLists.txt
+++ b/test/unit/context/CMakeLists.txt
@@ -11,10 +11,10 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(cdlist_black context)
-cvc4_add_unit_test_black(cdmap_black context)
-cvc4_add_unit_test_white(cdmap_white context)
-cvc4_add_unit_test_black(cdo_black context)
-cvc4_add_unit_test_black(context_black context)
-cvc4_add_unit_test_black(context_mm_black context)
-cvc4_add_unit_test_white(context_white context)
+cvc4_add_cxx_unit_test_black(cdlist_black context)
+cvc4_add_cxx_unit_test_black(cdmap_black context)
+cvc4_add_cxx_unit_test_white(cdmap_white context)
+cvc4_add_cxx_unit_test_black(cdo_black context)
+cvc4_add_cxx_unit_test_black(context_black context)
+cvc4_add_cxx_unit_test_black(context_mm_black context)
+cvc4_add_cxx_unit_test_white(context_white context)
diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index c10648c03..6c0abc4ab 100644
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -11,20 +11,20 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(attribute_black expr)
-cvc4_add_unit_test_white(attribute_white expr)
-cvc4_add_unit_test_black(expr_manager_public expr)
-cvc4_add_unit_test_black(expr_public expr)
-cvc4_add_unit_test_black(kind_black expr)
-cvc4_add_unit_test_black(kind_map_black expr)
-cvc4_add_unit_test_black(node_black expr)
-cvc4_add_unit_test_black(node_algorithm_black expr)
-cvc4_add_unit_test_black(node_builder_black expr)
-cvc4_add_unit_test_black(node_manager_black expr)
-cvc4_add_unit_test_white(node_manager_white expr)
-cvc4_add_unit_test_black(node_self_iterator_black expr)
-cvc4_add_unit_test_black(node_traversal_black expr)
-cvc4_add_unit_test_white(node_white expr)
-cvc4_add_unit_test_black(symbol_table_black expr)
-cvc4_add_unit_test_black(type_cardinality_public expr)
-cvc4_add_unit_test_white(type_node_white expr)
+cvc4_add_cxx_unit_test_black(attribute_black expr)
+cvc4_add_cxx_unit_test_white(attribute_white expr)
+cvc4_add_cxx_unit_test_black(expr_manager_public expr)
+cvc4_add_cxx_unit_test_black(expr_public expr)
+cvc4_add_cxx_unit_test_black(kind_black expr)
+cvc4_add_cxx_unit_test_black(kind_map_black expr)
+cvc4_add_cxx_unit_test_black(node_black expr)
+cvc4_add_cxx_unit_test_black(node_algorithm_black expr)
+cvc4_add_cxx_unit_test_black(node_builder_black expr)
+cvc4_add_cxx_unit_test_black(node_manager_black expr)
+cvc4_add_cxx_unit_test_white(node_manager_white expr)
+cvc4_add_cxx_unit_test_black(node_self_iterator_black expr)
+cvc4_add_cxx_unit_test_black(node_traversal_black expr)
+cvc4_add_cxx_unit_test_white(node_white expr)
+cvc4_add_cxx_unit_test_black(symbol_table_black expr)
+cvc4_add_cxx_unit_test_black(type_cardinality_public expr)
+cvc4_add_cxx_unit_test_white(type_node_white expr)
diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt
index 55307db95..59c197f04 100644
--- a/test/unit/main/CMakeLists.txt
+++ b/test/unit/main/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(interactive_shell_black main)
+cvc4_add_cxx_unit_test_black(interactive_shell_black main)
diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt
index 1bdcbd5f5..4202ea0c9 100644
--- a/test/unit/parser/CMakeLists.txt
+++ b/test/unit/parser/CMakeLists.txt
@@ -11,5 +11,5 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(parser_black parser)
-cvc4_add_unit_test_black(parser_builder_black parser)
+cvc4_add_cxx_unit_test_black(parser_black parser)
+cvc4_add_cxx_unit_test_black(parser_builder_black parser)
diff --git a/test/unit/preprocessing/CMakeLists.txt b/test/unit/preprocessing/CMakeLists.txt
index 7e142f404..a2381ba90 100644
--- a/test/unit/preprocessing/CMakeLists.txt
+++ b/test/unit/preprocessing/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_white(pass_bv_gauss_white preprocessing)
+cvc4_add_cxx_unit_test_white(pass_bv_gauss_white preprocessing)
diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt
index 3b040d1fc..93c241af9 100644
--- a/test/unit/printer/CMakeLists.txt
+++ b/test/unit/printer/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(smt2_printer_black printer)
+cvc4_add_cxx_unit_test_black(smt2_printer_black printer)
diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt
index bed0575c6..f866e5ffa 100644
--- a/test/unit/prop/CMakeLists.txt
+++ b/test/unit/prop/CMakeLists.txt
@@ -11,4 +11,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_white(cnf_stream_white prop)
+cvc4_add_cxx_unit_test_white(cnf_stream_white prop)
diff --git a/src/expr/array.h b/test/unit/test_api.h
index 620e61ea0..72d0658a7 100644
--- a/src/expr/array.h
+++ b/test/unit/test_api.h
@@ -1,26 +1,27 @@
 /*********************                                                        */
-/*! \file array.h
+/*! \file datatype_api_black.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Mathias Preiner, Morgan Deters
+ **   Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 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 Array types.
- **
- ** Array types.
+ ** \brief Common header for API unit test.
  **/
 
-#include "cvc4_public.h"
+#ifndef CVC4__TEST__UNIT__TEST_API_H
+#define CVC4__TEST__UNIT__TEST_API_H
 
-#ifndef CVC4__ARRAY_H
-#define CVC4__ARRAY_H
+#include "api/cvc4cpp.h"
+#include "gtest/gtest.h"
 
-// we get ArrayType right now by #including type.h.
-// array.h is still useful for the auto-generated kinds #includes.
-#include "expr/type.h"
+class TestApi : public ::testing::Test
+{
+ protected:
+  CVC4::api::Solver d_solver;
+};
 
-#endif /* CVC4__ARRAY_H */
+#endif
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 8cfd43989..334ded2d1 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -8,23 +8,24 @@
 ## All rights reserved.  See the file COPYING in the top-level source
 ## directory for licensing information.
 ##
-cvc4_add_unit_test_black(regexp_operation_black theory)
-cvc4_add_unit_test_black(theory_black theory)
-cvc4_add_unit_test_white(evaluator_white theory)
-cvc4_add_unit_test_white(logic_info_white theory)
-cvc4_add_unit_test_white(sequences_rewriter_white theory)
-cvc4_add_unit_test_white(theory_arith_white theory)
-cvc4_add_unit_test_white(theory_bags_normal_form_white theory)
-cvc4_add_unit_test_white(theory_bags_rewriter_white theory)
-cvc4_add_unit_test_white(theory_bags_type_rules_white theory)
-cvc4_add_unit_test_white(theory_bv_rewriter_white theory)
-cvc4_add_unit_test_white(theory_bv_white theory)
-cvc4_add_unit_test_white(theory_engine_white theory)
-cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
-cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory)
-cvc4_add_unit_test_white(theory_sets_type_enumerator_white theory)
-cvc4_add_unit_test_white(theory_sets_type_rules_white theory)
-cvc4_add_unit_test_white(theory_strings_skolem_cache_black theory)
-cvc4_add_unit_test_white(theory_strings_word_white theory)
-cvc4_add_unit_test_white(theory_white theory)
-cvc4_add_unit_test_white(type_enumerator_white theory)
+cvc4_add_cxx_unit_test_black(regexp_operation_black theory)
+cvc4_add_cxx_unit_test_black(theory_black theory)
+cvc4_add_cxx_unit_test_white(evaluator_white theory)
+cvc4_add_cxx_unit_test_white(logic_info_white theory)
+cvc4_add_cxx_unit_test_white(sequences_rewriter_white theory)
+cvc4_add_cxx_unit_test_white(strings_rewriter_white theory)
+cvc4_add_cxx_unit_test_white(theory_arith_white theory)
+cvc4_add_cxx_unit_test_white(theory_bags_normal_form_white theory)
+cvc4_add_cxx_unit_test_white(theory_bags_rewriter_white theory)
+cvc4_add_cxx_unit_test_white(theory_bags_type_rules_white theory)
+cvc4_add_cxx_unit_test_white(theory_bv_rewriter_white theory)
+cvc4_add_cxx_unit_test_white(theory_bv_white theory)
+cvc4_add_cxx_unit_test_white(theory_engine_white theory)
+cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
+cvc4_add_cxx_unit_test_white(theory_quantifiers_bv_inverter_white theory)
+cvc4_add_cxx_unit_test_white(theory_sets_type_enumerator_white theory)
+cvc4_add_cxx_unit_test_white(theory_sets_type_rules_white theory)
+cvc4_add_cxx_unit_test_white(theory_strings_skolem_cache_black theory)
+cvc4_add_cxx_unit_test_white(theory_strings_word_white theory)
+cvc4_add_cxx_unit_test_white(theory_white theory)
+cvc4_add_cxx_unit_test_white(type_enumerator_white theory)
diff --git a/test/unit/theory/strings_rewriter_white.h b/test/unit/theory/strings_rewriter_white.h
new file mode 100644
index 000000000..f5c7cced8
--- /dev/null
+++ b/test/unit/theory/strings_rewriter_white.h
@@ -0,0 +1,89 @@
+/*********************                                                        */
+/*! \file strings_rewriter_white.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 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 Unit tests for the strings rewriter
+ **
+ ** Unit tests for the strings rewriter.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <memory>
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "smt/smt_engine.h"
+#include "smt/smt_engine_scope.h"
+#include "theory/rewriter.h"
+#include "theory/strings/strings_rewriter.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::smt;
+using namespace CVC4::theory;
+using namespace CVC4::theory::strings;
+
+class StringsRewriterWhite : public CxxTest::TestSuite
+{
+ public:
+  StringsRewriterWhite() {}
+
+  void setUp() override
+  {
+    Options opts;
+    opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
+    d_em = new ExprManager;
+    d_nm = NodeManager::fromExprManager(d_em);
+    d_smt = new SmtEngine(d_nm, &opts);
+    d_scope = new SmtScope(d_smt);
+    d_smt->finishInit();
+  }
+
+  void tearDown() override
+  {
+    delete d_scope;
+    delete d_smt;
+    delete d_em;
+  }
+
+  void testRewriteLeq()
+  {
+    TypeNode intType = d_nm->integerType();
+    TypeNode strType = d_nm->stringType();
+
+    Node a = d_nm->mkConst(::CVC4::String("A"));
+    Node bc = d_nm->mkConst(::CVC4::String("BC"));
+    Node x = d_nm->mkVar("x", strType);
+    Node y = d_nm->mkVar("y", strType);
+
+    Node ax = d_nm->mkNode(STRING_CONCAT, a, x);
+    Node bcy = d_nm->mkNode(STRING_CONCAT, bc, y);
+
+    {
+      Node leq = d_nm->mkNode(STRING_LEQ, ax, bcy);
+      TS_ASSERT_EQUALS(Rewriter::rewrite(leq), d_nm->mkConst(true));
+    }
+
+    {
+      Node leq = d_nm->mkNode(STRING_LEQ, bcy, ax);
+      TS_ASSERT_EQUALS(Rewriter::rewrite(leq), d_nm->mkConst(false));
+    }
+  }
+
+ private:
+  ExprManager* d_em;
+  SmtEngine* d_smt;
+  SmtScope* d_scope;
+
+  NodeManager* d_nm;
+};
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index 0fd7894fe..148ae9910 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -11,25 +11,25 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_white(array_store_all_white util)
-cvc4_add_unit_test_white(assert_white util)
-cvc4_add_unit_test_black(binary_heap_black util)
-cvc4_add_unit_test_black(bitvector_black util)
-cvc4_add_unit_test_black(boolean_simplification_black util)
-cvc4_add_unit_test_black(cardinality_public util)
-cvc4_add_unit_test_white(check_white util)
-cvc4_add_unit_test_black(configuration_black util)
-cvc4_add_unit_test_black(datatype_black util)
-cvc4_add_unit_test_black(exception_black util)
+cvc4_add_cxx_unit_test_white(array_store_all_white util)
+cvc4_add_cxx_unit_test_white(assert_white util)
+cvc4_add_cxx_unit_test_black(binary_heap_black util)
+cvc4_add_cxx_unit_test_black(bitvector_black util)
+cvc4_add_cxx_unit_test_black(boolean_simplification_black util)
+cvc4_add_cxx_unit_test_black(cardinality_public util)
+cvc4_add_cxx_unit_test_white(check_white util)
+cvc4_add_cxx_unit_test_black(configuration_black util)
+cvc4_add_cxx_unit_test_black(datatype_black util)
+cvc4_add_cxx_unit_test_black(exception_black util)
 if(CVC4_USE_SYMFPU)
-cvc4_add_unit_test_black(floatingpoint_black util)
+cvc4_add_cxx_unit_test_black(floatingpoint_black util)
 endif()
-cvc4_add_unit_test_black(integer_black util)
-cvc4_add_unit_test_white(integer_white util)
-cvc4_add_unit_test_black(output_black util)
-cvc4_add_unit_test_black(rational_black util)
-cvc4_add_unit_test_white(rational_white util)
+cvc4_add_cxx_unit_test_black(integer_black util)
+cvc4_add_cxx_unit_test_white(integer_white util)
+cvc4_add_cxx_unit_test_black(output_black util)
+cvc4_add_cxx_unit_test_black(rational_black util)
+cvc4_add_cxx_unit_test_white(rational_white util)
 if(CVC4_USE_POLY_IMP)
-cvc4_add_unit_test_black(real_algebraic_number_black util)
+cvc4_add_cxx_unit_test_black(real_algebraic_number_black util)
 endif()
-cvc4_add_unit_test_black(stats_black util)
+cvc4_add_cxx_unit_test_black(stats_black util)