Merge branch 'master' into fix1649fix1649

94 files changed, 2174 insertions, 816 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 733186d16..a2b5966e1 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -795,6 +795,8 @@ libcvc5_add_sources(
   theory/quantifiers/ematching/instantiation_engine.h
   theory/quantifiers/ematching/pattern_term_selector.cpp
   theory/quantifiers/ematching/pattern_term_selector.h
+  theory/quantifiers/ematching/relational_match_generator.cpp
+  theory/quantifiers/ematching/relational_match_generator.h
   theory/quantifiers/ematching/trigger.cpp
   theory/quantifiers/ematching/trigger.h
   theory/quantifiers/ematching/trigger_database.cpp
@@ -805,6 +807,8 @@ libcvc5_add_sources(
   theory/quantifiers/ematching/trigger_trie.h
   theory/quantifiers/ematching/var_match_generator.cpp
   theory/quantifiers/ematching/var_match_generator.h
+  theory/quantifiers/entailment_check.cpp
+  theory/quantifiers/entailment_check.h
   theory/quantifiers/equality_query.cpp
   theory/quantifiers/equality_query.h
   theory/quantifiers/expr_miner.cpp
@@ -1079,6 +1083,8 @@ libcvc5_add_sources(
   theory/strings/normal_form.h
   theory/strings/proof_checker.cpp
   theory/strings/proof_checker.h
+  theory/strings/regexp_enumerator.cpp
+  theory/strings/regexp_enumerator.h
   theory/strings/regexp_elim.cpp
   theory/strings/regexp_elim.h
   theory/strings/regexp_entail.cpp
@@ -1402,7 +1408,6 @@ if(USE_GLPK)
   if(ENABLE_STATIC_LIBRARY)
     target_link_libraries(cvc5-static PUBLIC ${GLPK_LIBRARIES})
   endif()
-  target_link_libraries(cvc5-obj PUBLIC ${GLPK_LIBRARIES})
 endif()
 if(USE_POLY)
   add_dependencies(cvc5-obj Polyxx_SHARED)
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 778f700c0..bb39ae86d 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -1682,7 +1682,7 @@ size_t Sort::getSortConstructorArity() const
 
 /* Bit-vector sort ----------------------------------------------------- */
 
-uint32_t Sort::getBVSize() const
+uint32_t Sort::getBitVectorSize() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
@@ -1695,7 +1695,7 @@ uint32_t Sort::getBVSize() const
 
 /* Floating-point sort ------------------------------------------------- */
 
-uint32_t Sort::getFPExponentSize() const
+uint32_t Sort::getFloatingPointExponentSize() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
@@ -1706,7 +1706,7 @@ uint32_t Sort::getFPExponentSize() const
   CVC5_API_TRY_CATCH_END;
 }
 
-uint32_t Sort::getFPSignificandSize() const
+uint32_t Sort::getFloatingPointSignificandSize() const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK_NOT_NULL;
@@ -5082,7 +5082,7 @@ Term Solver::mkTermFromKind(Kind kind) const
   CVC5_API_KIND_CHECK_EXPECTED(kind == PI || kind == REGEXP_EMPTY
                                    || kind == REGEXP_SIGMA || kind == SEP_EMP,
                                kind)
-      << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
+      << "PI, REGEXP_EMPTY, REGEXP_SIGMA or SEP_EMP";
   //////// all checks before this line
   Node res;
   cvc5::Kind k = extToIntKind(kind);
@@ -5822,6 +5822,18 @@ Term Solver::mkEmptyBag(const Sort& sort) const
   CVC5_API_TRY_CATCH_END;
 }
 
+Term Solver::mkSepEmp() const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  //////// all checks before this line
+  Node res = getNodeManager()->mkNullaryOperator(d_nodeMgr->booleanType(),
+                                                 cvc5::Kind::SEP_EMP);
+  (void)res.getType(true); /* kick off type checking */
+  return Term(this, res);
+  ////////
+  CVC5_API_TRY_CATCH_END;
+}
+
 Term Solver::mkSepNil(const Sort& sort) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
@@ -6030,10 +6042,11 @@ Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
   CVC5_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0";
   CVC5_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0";
   uint32_t bw = exp + sig;
-  CVC5_API_ARG_CHECK_EXPECTED(bw == val.getSort().getBVSize(), val)
+  CVC5_API_ARG_CHECK_EXPECTED(bw == val.d_node->getType().getBitVectorSize(),
+                              val)
       << "a bit-vector constant with bit-width '" << bw << "'";
   CVC5_API_ARG_CHECK_EXPECTED(
-      val.getSort().isBitVector() && val.d_node->isConst(), val)
+      val.d_node->getType().isBitVector() && val.d_node->isConst(), val)
       << "bit-vector constant";
   //////// all checks before this line
   return mkValHelper<cvc5::FloatingPoint>(
@@ -7204,7 +7217,7 @@ std::string Solver::getProof(void) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_CHECK(d_slv->getOptions().smt.produceProofs)
-      << "Cannot get proof explicitly enabled (try --produce-proofs)";
+      << "Cannot get proof unless proofs are enabled (try --produce-proofs)";
   CVC5_API_RECOVERABLE_CHECK(d_slv->getSmtMode() == SmtMode::UNSAT)
       << "Cannot get proof unless in unsat mode.";
   return d_slv->getProof();
@@ -7455,6 +7468,8 @@ bool Solver::getAbduct(const Term& conj, Term& output) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
+  CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts)
+      << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
   //////// all checks before this line
   Node result;
   bool success = d_slv->getAbduct(*conj.d_node, result);
@@ -7471,6 +7486,8 @@ bool Solver::getAbduct(const Term& conj, Grammar& grammar, Term& output) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
   CVC5_API_SOLVER_CHECK_TERM(conj);
+  CVC5_API_CHECK(d_slv->getOptions().smt.produceAbducts)
+      << "Cannot get abduct unless abducts are enabled (try --produce-abducts)";
   //////// all checks before this line
   Node result;
   bool success =
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index 3db581db6..c46b00d0e 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -700,19 +700,19 @@ class CVC5_EXPORT Sort
   /**
    * @return the bit-width of the bit-vector sort
    */
-  uint32_t getBVSize() const;
+  uint32_t getBitVectorSize() const;
 
   /* Floating-point sort ------------------------------------------------- */
 
   /**
    * @return the bit-width of the exponent of the floating-point sort
    */
-  uint32_t getFPExponentSize() const;
+  uint32_t getFloatingPointExponentSize() const;
 
   /**
    * @return the width of the significand of the floating-point sort
    */
-  uint32_t getFPSignificandSize() const;
+  uint32_t getFloatingPointSignificandSize() const;
 
   /* Datatype sort ------------------------------------------------------- */
 
@@ -1353,6 +1353,8 @@ class CVC5_EXPORT Term
   std::pair<int64_t, uint64_t> getReal64Value() const;
   /**
    * @return true if the term is a rational value.
+   *
+   * Note that a term of kind PI is not considered to be a real value.
    */
   bool isRealValue() const;
   /**
@@ -1448,6 +1450,17 @@ class CVC5_EXPORT Term
 
   /**
    * @return true if the term is a set value.
+   *
+   * A term is a set value if it is considered to be a (canonical) constant set
+   * value.  A canonical set value is one whose AST is:
+   * ```
+   *   (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
+   * ```
+   * where `c1 ... cn` are values ordered by id such that `c1 > ... > cn` (see
+   * also @ref Term::operator>(const Term&) const).
+   *
+   * Note that a universe set term (kind UNIVERSE_SET) is not considered to be
+   * a set value.
    */
   bool isSetValue() const;
   /**
@@ -2464,7 +2477,7 @@ class CVC5_EXPORT Grammar
   /**
    * Allow \p ntSymbol to be any input variable to corresponding
    * synth-fun/synth-inv with the same sort as \p ntSymbol.
-   * @param ntSymbol the non-terminal allowed to be any input constant
+   * @param ntSymbol the non-terminal allowed to be any input variable
    */
   void addAnyVariable(const Term& ntSymbol);
 
@@ -3431,6 +3444,12 @@ class CVC5_EXPORT Solver
   Term mkEmptyBag(const Sort& sort) const;
 
   /**
+   * Create a separation logic empty term.
+   * @return the separation logic empty term
+   */
+  Term mkSepEmp() const;
+
+  /**
    * Create a separation logic nil term.
    * @param sort the sort of the nil term
    * @return the separation logic nil term
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 0ff05022f..fe87df934 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -766,6 +766,9 @@ enum CVC5_EXPORT Kind : int32_t
   /**
    * Pi constant.
    *
+   * Note that PI is considered a special symbol of sort Real, but is not
+   * a real value, i.e., `Term::isRealValue() const` will return false.
+   *
    * Create with:
    *   - `Solver::mkPi() const`
    *   - `Solver::mkTerm(Kind kind) const`
@@ -2228,6 +2231,10 @@ enum CVC5_EXPORT Kind : int32_t
    * Finite universe set.
    * All set variables must be interpreted as subsets of it.
    *
+   * Note that UNIVERSE_SET is considered a special symbol of the theory of
+   * sets and is not considered as a set value,
+   * i.e., `Term::isSetValue() const` will return false.
+   *
    * Create with:
    *   - `Solver::mkUniverseSet(const Sort& sort) const`
    */
diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java
index b0bee500c..c46d60aee 100644
--- a/src/api/java/cvc5/Solver.java
+++ b/src/api/java/cvc5/Solver.java
@@ -882,6 +882,18 @@ public class Solver implements IPointer
   private native long mkEmptyBag(long pointer, long sortPointer);
 
   /**
+   * Create a separation logic empty term.
+   * @return the separation logic empty term
+   */
+  public Term mkSepEmp()
+  {
+    long termPointer = mkSepEmp(pointer);
+    return new Term(this, termPointer);
+  }
+
+  private native long mkSepEmp(long pointer);
+
+  /**
    * Create a separation logic nil term.
    * @param sort the sort of the nil term
    * @return the separation logic nil term
diff --git a/src/api/java/cvc5/Sort.java b/src/api/java/cvc5/Sort.java
index f1f541e35..434c07424 100644
--- a/src/api/java/cvc5/Sort.java
+++ b/src/api/java/cvc5/Sort.java
@@ -725,34 +725,34 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
   /**
    * @return the bit-width of the bit-vector sort
    */
-  public int getBVSize()
+  public int getBitVectorSize()
   {
-    return getBVSize(pointer);
+    return getBitVectorSize(pointer);
   }
 
-  private native int getBVSize(long pointer);
+  private native int getBitVectorSize(long pointer);
 
   /* Floating-point sort ------------------------------------------------- */
 
   /**
    * @return the bit-width of the exponent of the floating-point sort
    */
-  public int getFPExponentSize()
+  public int getFloatingPointExponentSize()
   {
-    return getFPExponentSize(pointer);
+    return getFloatingPointExponentSize(pointer);
   }
 
-  private native int getFPExponentSize(long pointer);
+  private native int getFloatingPointExponentSize(long pointer);
 
   /**
    * @return the width of the significand of the floating-point sort
    */
-  public int getFPSignificandSize()
+  public int getFloatingPointSignificandSize()
   {
-    return getFPSignificandSize(pointer);
+    return getFloatingPointSignificandSize(pointer);
   }
 
-  private native int getFPSignificandSize(long pointer);
+  private native int getFloatingPointSignificandSize(long pointer);
 
   /* Datatype sort ------------------------------------------------------- */
 
diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/cvc5_Solver.cpp
index c28ea412f..53c050c96 100644
--- a/src/api/java/jni/cvc5_Solver.cpp
+++ b/src/api/java/jni/cvc5_Solver.cpp
@@ -1061,6 +1061,22 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkEmptyBag(JNIEnv* env,
 
 /*
  * Class:     cvc5_Solver
+ * Method:    mkSepEmp
+ * Signature: (JJ)J
+ */
+JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkSepEmp(JNIEnv* env,
+                                                  jobject,
+                                                  jlong pointer)
+{
+  CVC5_JAVA_API_TRY_CATCH_BEGIN;
+  Solver* solver = reinterpret_cast<Solver*>(pointer);
+  Term* retPointer = new Term(solver->mkSepEmp());
+  return reinterpret_cast<jlong>(retPointer);
+  CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
+}
+
+/*
+ * Class:     cvc5_Solver
  * Method:    mkSepNil
  * Signature: (JJ)J
  */
@@ -2591,4 +2607,4 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullDatatypeDecl(JNIEnv* env,
   DatatypeDecl* ret = new DatatypeDecl();
   return reinterpret_cast<jlong>(ret);
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
-}
\ No newline at end of file
+}
diff --git a/src/api/java/jni/cvc5_Sort.cpp b/src/api/java/jni/cvc5_Sort.cpp
index a2754f032..36ba81249 100644
--- a/src/api/java/jni/cvc5_Sort.cpp
+++ b/src/api/java/jni/cvc5_Sort.cpp
@@ -978,46 +978,44 @@ JNIEXPORT jint JNICALL Java_cvc5_Sort_getSortConstructorArity(JNIEnv* env,
 
 /*
  * Class:     cvc5_Sort
- * Method:    getBVSize
+ * Method:    getBitVectorSize
  * Signature: (J)I
  */
-JNIEXPORT jint JNICALL Java_cvc5_Sort_getBVSize(JNIEnv* env,
-                                                jobject,
-                                                jlong pointer)
+JNIEXPORT jint JNICALL Java_cvc5_Sort_getBitVectorSize(JNIEnv* env,
+                                                       jobject,
+                                                       jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Sort* current = reinterpret_cast<Sort*>(pointer);
-  return static_cast<jint>(current->getBVSize());
+  return static_cast<jint>(current->getBitVectorSize());
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
 /*
  * Class:     cvc5_Sort
- * Method:    getFPExponentSize
+ * Method:    getFloatingPointExponentSize
  * Signature: (J)I
  */
-JNIEXPORT jint JNICALL Java_cvc5_Sort_getFPExponentSize(JNIEnv* env,
-                                                        jobject,
-                                                        jlong pointer)
+JNIEXPORT jint JNICALL
+Java_cvc5_Sort_getFloatingPointExponentSize(JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Sort* current = reinterpret_cast<Sort*>(pointer);
-  return static_cast<jint>(current->getFPExponentSize());
+  return static_cast<jint>(current->getFloatingPointExponentSize());
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
 /*
  * Class:     cvc5_Sort
- * Method:    getFPSignificandSize
+ * Method:    getFloatingPointSignificandSize
  * Signature: (J)I
  */
-JNIEXPORT jint JNICALL Java_cvc5_Sort_getFPSignificandSize(JNIEnv* env,
-                                                           jobject,
-                                                           jlong pointer)
+JNIEXPORT jint JNICALL Java_cvc5_Sort_getFloatingPointSignificandSize(
+    JNIEnv* env, jobject, jlong pointer)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Sort* current = reinterpret_cast<Sort*>(pointer);
-  return static_cast<jint>(current->getFPSignificandSize());
+  return static_cast<jint>(current->getFloatingPointSignificandSize());
   CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
 }
 
diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index ef9971c20..02b572120 100644
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -219,6 +219,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         Term mkRegexpSigma() except +
         Term mkEmptySet(Sort s) except +
         Term mkEmptyBag(Sort s) except +
+        Term mkSepEmp() except +
         Term mkSepNil(Sort sort) except +
         Term mkString(const string& s) except +
         Term mkString(const wstring& s) except +
@@ -308,6 +309,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint operator>(const Sort&) except +
         bint operator<=(const Sort&) except +
         bint operator>=(const Sort&) except +
+        bint isNull() except +
         bint isBoolean() except +
         bint isInteger() except +
         bint isReal() except +
@@ -321,6 +323,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint isConstructor() except +
         bint isSelector() except +
         bint isTester() except +
+        bint isUpdater() except +
         bint isFunction() except +
         bint isPredicate() except +
         bint isTuple() except +
@@ -357,9 +360,9 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         vector[Sort] getUninterpretedSortParamSorts() except +
         string getSortConstructorName() except +
         size_t getSortConstructorArity() except +
-        uint32_t getBVSize() except +
-        uint32_t getFPExponentSize() except +
-        uint32_t getFPSignificandSize() except +
+        uint32_t getBitVectorSize() except +
+        uint32_t getFloatingPointExponentSize() except +
+        uint32_t getFloatingPointSignificandSize() except +
         vector[Sort] getDatatypeParamSorts() except +
         size_t getDatatypeArity() except +
         size_t getTupleLength() except +
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 0f6b54dc6..4627859b9 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -95,7 +95,10 @@ cdef c_hash[c_Term] ctermhash = c_hash[c_Term]()
 
 
 cdef class Datatype:
-    """Wrapper class for :cpp:class:`cvc5::api::Datatype`."""
+    """
+        A cvc5 datatype.
+        Wrapper class for :cpp:class:`cvc5::api::Datatype`.
+    """
     cdef c_Datatype cd
     cdef Solver solver
     def __cinit__(self, Solver solver):
@@ -114,7 +117,7 @@ cdef class Datatype:
     def getConstructor(self, str name):
         """
             :param name: the name of the constructor.
-            :return: a constructor by name. 
+            :return: a constructor by name.
         """
         cdef DatatypeConstructor dc = DatatypeConstructor(self.solver)
         dc.cdc = self.cd.getConstructor(name.encode())
@@ -151,34 +154,35 @@ cdef class Datatype:
         return self.cd.getNumConstructors()
 
     def isParametric(self):
-        """:return: whether this datatype is parametric."""
+        """:return: True if this datatype is parametric."""
         return self.cd.isParametric()
 
     def isCodatatype(self):
-        """:return: whether this datatype corresponds to a co-datatype."""
+        """:return: True if this datatype corresponds to a co-datatype."""
         return self.cd.isCodatatype()
 
     def isTuple(self):
-        """:return: whether this datatype corresponds to a tuple."""
+        """:return: True if this datatype corresponds to a tuple."""
         return self.cd.isTuple()
 
     def isRecord(self):
-        """:return: whether this datatype corresponds to a record."""
+        """:return: True if this datatype corresponds to a record."""
         return self.cd.isRecord()
 
     def isFinite(self):
-        """:return: whether this datatype is finite."""
+        """:return: True if this datatype is finite."""
         return self.cd.isFinite()
 
     def isWellFounded(self):
-        """:return: whether this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::api::Datatype::isWellFounded>`)."""
+        """:return: True if this datatype is well-founded (see :cpp:func:`Datatype::isWellFounded() <cvc5::api::Datatype::isWellFounded>`)."""
         return self.cd.isWellFounded()
 
     def hasNestedRecursion(self):
-        """:return: whether this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() <cvc5::api::Datatype::hasNestedRecursion>`)."""
+        """:return: True if this datatype has nested recursion (see :cpp:func:`Datatype::hasNestedRecursion() <cvc5::api::Datatype::hasNestedRecursion>`)."""
         return self.cd.hasNestedRecursion()
 
     def isNull(self):
+        """:return: True if this Datatype is a null object."""
         return self.cd.isNull()
 
     def __str__(self):
@@ -195,7 +199,10 @@ cdef class Datatype:
 
 
 cdef class DatatypeConstructor:
-    """Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`."""
+    """
+        A cvc5 datatype constructor.
+        Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructor`.
+    """
     cdef c_DatatypeConstructor cdc
     cdef Solver solver
     def __cinit__(self, Solver solver):
@@ -270,6 +277,7 @@ cdef class DatatypeConstructor:
         return term
 
     def isNull(self):
+        """:return: True if this DatatypeConstructor is a null object."""
         return self.cdc.isNull()
 
     def __str__(self):
@@ -286,7 +294,10 @@ cdef class DatatypeConstructor:
 
 
 cdef class DatatypeConstructorDecl:
-    """Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`."""
+    """
+        A cvc5 datatype constructor declaration.
+        Wrapper class for :cpp:class:`cvc5::api::DatatypeConstructorDecl`.
+    """
     cdef c_DatatypeConstructorDecl cddc
     cdef Solver solver
 
@@ -311,6 +322,7 @@ cdef class DatatypeConstructorDecl:
         self.cddc.addSelectorSelf(name.encode())
 
     def isNull(self):
+        """:return: True if this DatatypeConstructorDecl is a null object."""
         return self.cddc.isNull()
 
     def __str__(self):
@@ -321,7 +333,10 @@ cdef class DatatypeConstructorDecl:
 
 
 cdef class DatatypeDecl:
-    """Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`."""
+    """
+        A cvc5 datatype declaration.
+        Wrapper class for :cpp:class:`cvc5::api::DatatypeDecl`.
+    """
     cdef c_DatatypeDecl cdd
     cdef Solver solver
     def __cinit__(self, Solver solver):
@@ -354,6 +369,7 @@ cdef class DatatypeDecl:
         return self.cdd.getName().decode()
 
     def isNull(self):
+        """:return: True if this DatatypeDecl is a null object."""
         return self.cdd.isNull()
 
     def __str__(self):
@@ -364,7 +380,10 @@ cdef class DatatypeDecl:
 
 
 cdef class DatatypeSelector:
-    """Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`."""
+    """
+        A cvc5 datatype selector.
+        Wrapper class for :cpp:class:`cvc5::api::DatatypeSelector`.
+    """
     cdef c_DatatypeSelector cds
     cdef Solver solver
     def __cinit__(self, Solver solver):
@@ -402,6 +421,7 @@ cdef class DatatypeSelector:
         return sort
 
     def isNull(self):
+        """:return: True if this DatatypeSelector is a null object."""
         return self.cds.isNull()
 
     def __str__(self):
@@ -412,6 +432,13 @@ cdef class DatatypeSelector:
 
 
 cdef class Op:
+    """
+        A cvc5 operator.
+        An operator is a term that represents certain operators,
+        instantiated with its required parameters, e.g.,
+        a term of kind :cpp:enumerator:`BITVECTOR_EXTRACT`.
+        Wrapper class for :cpp:class:`cvc5::api::Op`.
+    """
     cdef c_Op cop
     cdef Solver solver
     def __cinit__(self, Solver solver):
@@ -434,18 +461,33 @@ cdef class Op:
         return cophash(self.cop)
 
     def getKind(self):
+        """
+            :return: the kind of this operator.
+        """
         return kind(<int> self.cop.getKind())
 
     def isIndexed(self):
+        """
+            :return: True iff this operator is indexed.
+        """
         return self.cop.isIndexed()
 
     def isNull(self):
+        """
+            :return: True iff this operator is a null term.
+        """
         return self.cop.isNull()
 
     def getNumIndices(self):
+        """
+            :return: number of indices of this op.
+        """
         return self.cop.getNumIndices()
 
     def getIndices(self):
+        """
+            :return: the indices used to create this Op (see :cpp:func:`Op::getIndices() <cvc5::api::Op::getIndices>`).
+        """
         indices = None
         try:
             indices = self.cop.getIndices[string]().decode()
@@ -468,6 +510,10 @@ cdef class Op:
         return indices
 
 cdef class Grammar:
+    """
+        A Sygus Grammar.
+        Wrapper class for :cpp:class:`cvc5::api::Grammar`.
+    """
     cdef c_Grammar  cgrammar
     cdef Solver solver
     def __cinit__(self, Solver solver):
@@ -475,46 +521,100 @@ cdef class Grammar:
         self.cgrammar = c_Grammar()
 
     def addRule(self, Term ntSymbol, Term rule):
+        """
+            Add ``rule`` to the set of rules corresponding to ``ntSymbol``.
+
+            :param ntSymbol: the non-terminal to which the rule is added.
+            :param rule: the rule to add.
+        """
         self.cgrammar.addRule(ntSymbol.cterm, rule.cterm)
 
     def addAnyConstant(self, Term ntSymbol):
+        """
+            Allow ``ntSymbol`` to be an arbitrary constant.
+
+            :param ntSymbol: the non-terminal allowed to be constant.
+        """
         self.cgrammar.addAnyConstant(ntSymbol.cterm)
 
     def addAnyVariable(self, Term ntSymbol):
+        """
+            Allow ``ntSymbol`` to be any input variable to corresponding synth-fun/synth-inv with the same sort as ``ntSymbol``.
+
+            :param ntSymbol: the non-terminal allowed to be any input variable.
+        """
         self.cgrammar.addAnyVariable(ntSymbol.cterm)
 
     def addRules(self, Term ntSymbol, rules):
+        """
+            Add ``ntSymbol`` to the set of rules corresponding to ``ntSymbol``.
+
+            :param ntSymbol: the non-terminal to which the rules are added.
+            :param rules: the rules to add.
+        """
         cdef vector[c_Term] crules
         for r in rules:
             crules.push_back((<Term?> r).cterm)
         self.cgrammar.addRules(ntSymbol.cterm, crules)
 
 cdef class Result:
+    """
+        Encapsulation of a three-valued solver result, with explanations.
+        Wrapper class for :cpp:class:`cvc5::api::Result`.
+    """
     cdef c_Result cr
     def __cinit__(self):
         # gets populated by solver
         self.cr = c_Result()
 
     def isNull(self):
+        """
+            :return: True if Result is empty, i.e., a nullary Result,
+            and not an actual result returned from a :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` (and friends) query.
+        """
         return self.cr.isNull()
 
     def isSat(self):
+        """
+            :return: True if query was a satisfiable :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::api::Solver::checkSatAssuming>` query.
+        """
         return self.cr.isSat()
 
     def isUnsat(self):
+        """
+            :return: True if query was an usatisfiable :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::api::Solver::checkSatAssuming>` query.
+        """
         return self.cr.isUnsat()
 
     def isSatUnknown(self):
+        """
+            :return: True if query was a :cpp:func:`Solver::checkSat() <cvc5::api::Solver::checkSat>` or :cpp:func:`Solver::checkSatAssuming() <cvc5::api::Solver::checkSatAssuming>` query and cvc5 was not able to determine (un)satisfiability.
+        """
         return self.cr.isSatUnknown()
 
     def isEntailed(self):
+        """
+            :return: True if corresponding query was an entailed :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query.
+        """
         return self.cr.isEntailed()
 
     def isNotEntailed(self):
+        """
+            :return: True if corresponding query was a :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query that is not entailed.
+        """
         return self.cr.isNotEntailed()
 
     def isEntailmentUnknown(self):
+        """
+            :return: True if query was a :cpp:func:`Solver::checkEntailed() <cvc5::api::Solver::checkEntailed>` query  query and cvc5 was not able to determine if it is entailed.
+        """
         return self.cr.isEntailmentUnknown()
+    
+    def getUnknownExplanation(self):
+        """
+            :return: an explanation for an unknown query result.
+        """
+        return UnknownExplanation(<int> self.cr.getUnknownExplanation())
 
     def __eq__(self, Result other):
         return self.cr == other.cr
@@ -522,9 +622,6 @@ cdef class Result:
     def __ne__(self, Result other):
         return self.cr != other.cr
 
-    def getUnknownExplanation(self):
-        return UnknownExplanation(<int> self.cr.getUnknownExplanation())
-
     def __str__(self):
         return self.cr.toString().decode()
 
@@ -533,6 +630,20 @@ cdef class Result:
 
 
 cdef class RoundingMode:
+    """
+        Rounding modes for floating-point numbers.
+
+        For many floating-point operations, infinitely precise results may not be
+        representable with the number of available bits. Thus, the results are
+        rounded in a certain way to one of the representable floating-point numbers.
+
+        These rounding modes directly follow the SMT-LIB theory for floating-point
+        arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`.
+        The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE
+        Standard 754.
+        
+        Wrapper class for :cpp:enum:`cvc5::api::RoundingMode`.
+    """
     cdef c_RoundingMode crm
     cdef str name
     def __cinit__(self, int rm):
@@ -557,6 +668,9 @@ cdef class RoundingMode:
 
 
 cdef class UnknownExplanation:
+    """
+        Wrapper class for :cpp:enum:`cvc5::api::Result::UnknownExplanation`.
+    """
     cdef c_UnknownExplanation cue
     cdef str name
     def __cinit__(self, int ue):
@@ -907,9 +1021,10 @@ cdef class Solver:
         - ``Op mkOp(Kind kind, const string& arg)``
         - ``Op mkOp(Kind kind, uint32_t arg)``
         - ``Op mkOp(Kind kind, uint32_t arg0, uint32_t arg1)``
+        - ``Op mkOp(Kind kind, [uint32_t arg0, ...])`` (used for the TupleProject kind)
         """
         cdef Op op = Op(self)
-        cdef vector[int] v
+        cdef vector[uint32_t] v
 
         if len(args) == 0:
             op.cop = self.csolver.mkOp(k.k)
@@ -922,7 +1037,10 @@ cdef class Solver:
                 op.cop = self.csolver.mkOp(k.k, <int?> args[0])
             elif isinstance(args[0], list):
                 for a in args[0]:
-                    v.push_back((<int?> a))
+                    if a < 0 or a >= 2 ** 31:
+                        raise ValueError("Argument {} must fit in a uint32_t".format(a))
+
+                    v.push_back((<uint32_t?> a))
                 op.cop = self.csolver.mkOp(k.k, <const vector[uint32_t]&> v)   
             else:
                 raise ValueError("Unsupported signature"
@@ -1050,6 +1168,15 @@ cdef class Solver:
         term.cterm = self.csolver.mkEmptyBag(s.csort)
         return term
 
+    def mkSepEmp(self):
+        """Create a separation logic empty term.
+
+        :return: the separation logic empty term
+        """
+        cdef Term term = Term(self)
+        term.cterm = self.csolver.mkSepEmp()
+        return term
+
     def mkSepNil(self, Sort sort):
         """Create a separation logic nil term.
 
@@ -2087,6 +2214,9 @@ cdef class Sort:
     def __hash__(self):
         return csorthash(self.csort)
 
+    def isNull(self):
+        return self.csort.isNull()
+
     def isBoolean(self):
         return self.csort.isBoolean()
 
@@ -2126,6 +2256,9 @@ cdef class Sort:
     def isTester(self):
         return self.csort.isTester()
 
+    def isUpdater(self):
+        return self.csort.isUpdater()
+
     def isFunction(self):
         return self.csort.isFunction()
 
@@ -2278,14 +2411,14 @@ cdef class Sort:
     def getSortConstructorArity(self):
         return self.csort.getSortConstructorArity()
 
-    def getBVSize(self):
-        return self.csort.getBVSize()
+    def getBitVectorSize(self):
+        return self.csort.getBitVectorSize()
 
-    def getFPExponentSize(self):
-        return self.csort.getFPExponentSize()
+    def getFloatingPointExponentSize(self):
+        return self.csort.getFloatingPointExponentSize()
 
-    def getFPSignificandSize(self):
-        return self.csort.getFPSignificandSize()
+    def getFloatingPointSignificandSize(self):
+        return self.csort.getFloatingPointSignificandSize()
 
     def getDatatypeParamSorts(self):
         param_sorts = []
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index e73960676..45ce01edb 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -26,6 +26,8 @@ libcvc5_add_sources(
   bound_var_manager.h
   cardinality_constraint.cpp
   cardinality_constraint.h
+  codatatype_bound_variable.cpp
+  codatatype_bound_variable.h
   emptyset.cpp
   emptyset.h
   emptybag.cpp
@@ -95,6 +97,8 @@ libcvc5_add_sources(
   sygus_datatype.h
   uninterpreted_constant.cpp
   uninterpreted_constant.h
+  variadic_trie.cpp
+  variadic_trie.h
 )
 
 libcvc5_add_sources(GENERATED
diff --git a/src/expr/codatatype_bound_variable.cpp b/src/expr/codatatype_bound_variable.cpp
new file mode 100644
index 000000000..a6a9d8e3e
--- /dev/null
+++ b/src/expr/codatatype_bound_variable.cpp
@@ -0,0 +1,113 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Representation of bound variables in codatatype values
+ */
+
+#include "expr/codatatype_bound_variable.h"
+
+#include <algorithm>
+#include <iostream>
+#include <sstream>
+#include <string>
+
+#include "base/check.h"
+#include "expr/type_node.h"
+
+using namespace std;
+
+namespace cvc5 {
+
+CodatatypeBoundVariable::CodatatypeBoundVariable(const TypeNode& type,
+                                                 Integer index)
+    : d_type(new TypeNode(type)), d_index(index)
+{
+  PrettyCheckArgument(type.isCodatatype(),
+                      type,
+                      "codatatype bound variables can only be created for "
+                      "codatatype sorts, not `%s'",
+                      type.toString().c_str());
+  PrettyCheckArgument(
+      index >= 0,
+      index,
+      "index >= 0 required for codatatype bound variable index, not `%s'",
+      index.toString().c_str());
+}
+
+CodatatypeBoundVariable::~CodatatypeBoundVariable() {}
+
+CodatatypeBoundVariable::CodatatypeBoundVariable(
+    const CodatatypeBoundVariable& other)
+    : d_type(new TypeNode(other.getType())), d_index(other.getIndex())
+{
+}
+
+const TypeNode& CodatatypeBoundVariable::getType() const { return *d_type; }
+const Integer& CodatatypeBoundVariable::getIndex() const { return d_index; }
+bool CodatatypeBoundVariable::operator==(
+    const CodatatypeBoundVariable& cbv) const
+{
+  return getType() == cbv.getType() && d_index == cbv.d_index;
+}
+bool CodatatypeBoundVariable::operator!=(
+    const CodatatypeBoundVariable& cbv) const
+{
+  return !(*this == cbv);
+}
+
+bool CodatatypeBoundVariable::operator<(
+    const CodatatypeBoundVariable& cbv) const
+{
+  return getType() < cbv.getType()
+         || (getType() == cbv.getType() && d_index < cbv.d_index);
+}
+bool CodatatypeBoundVariable::operator<=(
+    const CodatatypeBoundVariable& cbv) const
+{
+  return getType() < cbv.getType()
+         || (getType() == cbv.getType() && d_index <= cbv.d_index);
+}
+bool CodatatypeBoundVariable::operator>(
+    const CodatatypeBoundVariable& cbv) const
+{
+  return !(*this <= cbv);
+}
+bool CodatatypeBoundVariable::operator>=(
+    const CodatatypeBoundVariable& cbv) const
+{
+  return !(*this < cbv);
+}
+
+std::ostream& operator<<(std::ostream& out, const CodatatypeBoundVariable& cbv)
+{
+  std::stringstream ss;
+  ss << cbv.getType();
+  std::string st(ss.str());
+  // must remove delimiting quotes from the name of the type
+  // this prevents us from printing symbols like |@cbv_|T|_n|
+  std::string q("|");
+  size_t pos;
+  while ((pos = st.find(q)) != std::string::npos)
+  {
+    st.replace(pos, 1, "");
+  }
+  return out << "cbv_" << st.c_str() << "_" << cbv.getIndex();
+}
+
+size_t CodatatypeBoundVariableHashFunction::operator()(
+    const CodatatypeBoundVariable& cbv) const
+{
+  return std::hash<TypeNode>()(cbv.getType())
+         * IntegerHashFunction()(cbv.getIndex());
+}
+
+}  // namespace cvc5
diff --git a/src/expr/codatatype_bound_variable.h b/src/expr/codatatype_bound_variable.h
new file mode 100644
index 000000000..9af8476d5
--- /dev/null
+++ b/src/expr/codatatype_bound_variable.h
@@ -0,0 +1,91 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Representation of bound variables in codatatype values
+ */
+
+#include "cvc5_public.h"
+
+#ifndef CVC5__EXPR__CODATATYPE_BOUND_VARIABLE_H
+#define CVC5__EXPR__CODATATYPE_BOUND_VARIABLE_H
+
+#include <iosfwd>
+#include <memory>
+
+#include "util/integer.h"
+
+namespace cvc5 {
+
+class TypeNode;
+
+/**
+ * In theory, codatatype values are represented in using a MU-notation form,
+ * where recursive values may contain free constants indexed by their de Bruijn
+ * indices. This is sometimes written:
+ *    MU x. (cons 0 x).
+ * where the MU binder is label for a term position, which x references.
+ * Instead of constructing an explicit MU binder (which is problematic for
+ * canonicity), we use de Bruijn indices for representing bound variables,
+ * whose index indicates the level in which it is nested. For example, we
+ * represent the above value as:
+ *    (cons 0 @cbv_0)
+ * In the above value, @cbv_0 is a pointer to its direct parent, so the above
+ * value represents the infinite list (cons 0 (cons 0 (cons 0 ... ))).
+ * Another example, the value:
+ *    (cons 0 (cons 1 @cbv_1))
+ * @cbv_1 is pointer to the top most node of this value, so this is value
+ * represents the infinite list (cons 0 (cons 1 (cons 0 (cons 1 ...)))). The
+ * value:
+ *    (cons 0 (cons 1 @cbv_0))
+ * on the other hand represents the lasso:
+ *    (cons 0 (cons 1 (cons 1 (cons 1 ... ))))
+ *
+ * This class is used for representing the indexed bound variables in the above
+ * values. It is considered a constant (isConst is true). However, constants
+ * of codatatype type are normalized by the rewriter (see datatypes rewriter
+ * normalizeCodatatypeConstant) to ensure their canonicity, via a variant
+ * of Hopcroft's algorithm.
+ */
+class CodatatypeBoundVariable
+{
+ public:
+  CodatatypeBoundVariable(const TypeNode& type, Integer index);
+  ~CodatatypeBoundVariable();
+
+  CodatatypeBoundVariable(const CodatatypeBoundVariable& other);
+
+  const TypeNode& getType() const;
+  const Integer& getIndex() const;
+  bool operator==(const CodatatypeBoundVariable& cbv) const;
+  bool operator!=(const CodatatypeBoundVariable& cbv) const;
+  bool operator<(const CodatatypeBoundVariable& cbv) const;
+  bool operator<=(const CodatatypeBoundVariable& cbv) const;
+  bool operator>(const CodatatypeBoundVariable& cbv) const;
+  bool operator>=(const CodatatypeBoundVariable& cbv) const;
+
+ private:
+  std::unique_ptr<TypeNode> d_type;
+  const Integer d_index;
+};
+std::ostream& operator<<(std::ostream& out, const CodatatypeBoundVariable& cbv);
+
+/**
+ * Hash function for codatatype bound variables.
+ */
+struct CodatatypeBoundVariableHashFunction
+{
+  size_t operator()(const CodatatypeBoundVariable& cbv) const;
+};
+
+}  // namespace cvc5
+
+#endif /* CVC5__UNINTERPRETED_CONSTANT_H */
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index ef354568d..709ec112f 100644
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -31,7 +31,11 @@ UninterpretedConstant::UninterpretedConstant(const TypeNode& type,
                                              Integer index)
     : d_type(new TypeNode(type)), d_index(index)
 {
-  //PrettyCheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str());
+  PrettyCheckArgument(type.isSort(),
+                      type,
+                      "uninterpreted constants can only be created for "
+                      "uninterpreted sorts, not `%s'",
+                      type.toString().c_str());
   PrettyCheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str());
 }
 
diff --git a/src/expr/variadic_trie.cpp b/src/expr/variadic_trie.cpp
new file mode 100644
index 000000000..bd27780e9
--- /dev/null
+++ b/src/expr/variadic_trie.cpp
@@ -0,0 +1,55 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Variadic trie utility
+ */
+
+#include "expr/variadic_trie.h"
+
+namespace cvc5 {
+
+bool VariadicTrie::add(Node n, const std::vector<Node>& i)
+{
+  VariadicTrie* curr = this;
+  for (const Node& ic : i)
+  {
+    curr = &(curr->d_children[ic]);
+  }
+  if (curr->d_data.isNull())
+  {
+    curr->d_data = n;
+    return true;
+  }
+  return false;
+}
+
+bool VariadicTrie::hasSubset(const std::vector<Node>& is) const
+{
+  if (!d_data.isNull())
+  {
+    return true;
+  }
+  for (const std::pair<const Node, VariadicTrie>& p : d_children)
+  {
+    Node n = p.first;
+    if (std::find(is.begin(), is.end(), n) != is.end())
+    {
+      if (p.second.hasSubset(is))
+      {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
+}  // namespace cvc5
diff --git a/src/expr/variadic_trie.h b/src/expr/variadic_trie.h
new file mode 100644
index 000000000..aa7ca1e37
--- /dev/null
+++ b/src/expr/variadic_trie.h
@@ -0,0 +1,54 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Variadic trie utility
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__EXPR__VARIADIC_TRIE_H
+#define CVC5__EXPR__VARIADIC_TRIE_H
+
+#include <map>
+#include <vector>
+
+#include "expr/node.h"
+
+namespace cvc5 {
+
+/**
+ * A trie that stores data at undetermined depth. Storing data at
+ * undetermined depth is in contrast to the NodeTrie (expr/node_trie.h), which
+ * assumes all data is stored at a fixed depth.
+ *
+ * Since data can be stored at any depth, we require both a d_children field
+ * and a d_data field.
+ */
+class VariadicTrie
+{
+ public:
+  /** the children of this node */
+  std::map<Node, VariadicTrie> d_children;
+  /** the data at this node */
+  Node d_data;
+  /**
+   * Add data with identifier n indexed by i, return true if data is not already
+   * stored at the node indexed by i.
+   */
+  bool add(Node n, const std::vector<Node>& i);
+  /** Is there any data in this trie that is indexed by any subset of is? */
+  bool hasSubset(const std::vector<Node>& is) const;
+};
+
+}  // namespace cvc5
+
+#endif /* CVC5__EXPR__VARIADIC_TRIE_H */
diff --git a/src/options/managed_streams.cpp b/src/options/managed_streams.cpp
index 81bb242cf..90090df25 100644
--- a/src/options/managed_streams.cpp
+++ b/src/options/managed_streams.cpp
@@ -100,34 +100,54 @@ std::istream* openIStream(const std::string& filename)
 }
 }  // namespace detail
 
-std::ostream* ManagedErr::defaultValue() const { return &std::cerr; }
+ManagedErr::ManagedErr() : ManagedStream(&std::cerr, "stderr") {}
 bool ManagedErr::specialCases(const std::string& value)
 {
   if (value == "stderr" || value == "--")
   {
-    d_stream.reset();
+    d_nonowned = &std::cerr;
+    d_owned.reset();
+    d_description = "stderr";
+    return true;
+  }
+  else if (value == "stdout")
+  {
+    d_nonowned = &std::cout;
+    d_owned.reset();
+    d_description = "stdout";
     return true;
   }
   return false;
 }
 
-std::istream* ManagedIn::defaultValue() const { return &std::cin; }
+ManagedIn::ManagedIn() : ManagedStream(&std::cin, "stdin") {}
 bool ManagedIn::specialCases(const std::string& value)
 {
   if (value == "stdin" || value == "--")
   {
-    d_stream.reset();
+    d_nonowned = &std::cin;
+    d_owned.reset();
+    d_description = "stdin";
     return true;
   }
   return false;
 }
 
-std::ostream* ManagedOut::defaultValue() const { return &std::cout; }
+ManagedOut::ManagedOut() : ManagedStream(&std::cout, "stdout") {}
 bool ManagedOut::specialCases(const std::string& value)
 {
   if (value == "stdout" || value == "--")
   {
-    d_stream.reset();
+    d_nonowned = &std::cout;
+    d_owned.reset();
+    d_description = "stdout";
+    return true;
+  }
+  else if (value == "stderr")
+  {
+    d_nonowned = &std::cerr;
+    d_owned.reset();
+    d_description = "stderr";
     return true;
   }
   return false;
diff --git a/src/options/managed_streams.h b/src/options/managed_streams.h
index 56bb21c2e..cf1820de6 100644
--- a/src/options/managed_streams.h
+++ b/src/options/managed_streams.h
@@ -50,7 +50,8 @@ template <typename Stream>
 class ManagedStream
 {
  public:
-  ManagedStream() {}
+  ManagedStream(Stream* nonowned, std::string description)
+  : d_nonowned(nonowned), d_description(std::move(description)) {}
   virtual ~ManagedStream() {}
 
   /**
@@ -62,11 +63,15 @@ class ManagedStream
     if (specialCases(value)) return;
     if constexpr (std::is_same<Stream, std::ostream>::value)
     {
-      d_stream.reset(detail::openOStream(value));
+      d_nonowned = nullptr;
+      d_owned.reset(detail::openOStream(value));
+      d_description = value;
     }
     else if constexpr (std::is_same<Stream, std::istream>::value)
     {
-      d_stream.reset(detail::openIStream(value));
+      d_nonowned = nullptr;
+      d_owned.reset(detail::openIStream(value));
+      d_description = value;
     }
   }
 
@@ -75,12 +80,14 @@ class ManagedStream
   operator Stream&() const { return *getPtr(); }
   operator Stream*() const { return getPtr(); }
 
+  const std::string& description() const { return d_description; }
+
  protected:
-  std::shared_ptr<Stream> d_stream;
+  Stream* d_nonowned;
+  std::shared_ptr<Stream> d_owned;
+  std::string d_description = "<null>";
 
  private:
-  /** Returns the value to be used if d_stream is not set. */
-  virtual Stream* defaultValue() const = 0;
   /**
    * Check if there is a special case for this value. If so, the implementation
    * should set d_stream appropriately and return true to skip the default
@@ -88,18 +95,18 @@ class ManagedStream
    */
   virtual bool specialCases(const std::string& value) = 0;
 
-  /** Return the pointer, either from d_stream of from defaultValue(). */
+  /** Return the pointer, either from d_nonowned or d_owned. */
   Stream* getPtr() const
   {
-    if (d_stream) return d_stream.get();
-    return defaultValue();
+    if (d_nonowned != nullptr) return d_nonowned;
+    return d_owned.get();
   }
 };
 
 template <typename Stream>
 std::ostream& operator<<(std::ostream& os, const ManagedStream<Stream>& ms)
 {
-  return os << "ManagedStream";
+  return os << ms.description();
 }
 
 /**
@@ -108,7 +115,10 @@ std::ostream& operator<<(std::ostream& os, const ManagedStream<Stream>& ms)
  */
 class ManagedErr : public ManagedStream<std::ostream>
 {
-  std::ostream* defaultValue() const override final;
+ public:
+  ManagedErr();
+
+ private:
   bool specialCases(const std::string& value) override final;
 };
 
@@ -118,7 +128,10 @@ class ManagedErr : public ManagedStream<std::ostream>
  */
 class ManagedIn : public ManagedStream<std::istream>
 {
-  std::istream* defaultValue() const override final;
+ public:
+  ManagedIn();
+
+ private:
   bool specialCases(const std::string& value) override final;
 };
 
@@ -128,7 +141,10 @@ class ManagedIn : public ManagedStream<std::istream>
  */
 class ManagedOut : public ManagedStream<std::ostream>
 {
-  std::ostream* defaultValue() const override final;
+ public:
+  ManagedOut();
+
+ private:
   bool specialCases(const std::string& value) override final;
 };
 
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index a8f631de6..57f8b64e6 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -480,17 +480,6 @@ def generate_module_option_names(module):
         'static constexpr const char* {name}__name = "{long_name}";', relevant)
 
 
-def generate_module_setdefaults_decl(module):
-    res = []
-    for option in module.options:
-        if option.name is None:
-            continue
-        funcname = option.name[0].capitalize() + option.name[1:]
-        res.append('void setDefault{}(Options& opts, {} value);'.format(
-            funcname, option.type))
-    return '\n'.join(res)
-
-
 ################################################################################
 # for options/<module>.cpp
 
@@ -581,27 +570,6 @@ def generate_module_mode_impl(module):
     return '\n'.join(res)
 
 
-TPL_SETDEFAULT_IMPL = '''void setDefault{capname}(Options& opts, {type} value)
-{{
-    if (!opts.{module}.{name}WasSetByUser) opts.{module}.{name} = value;
-}}'''
-
-
-def generate_module_setdefaults_impl(module):
-    res = []
-    for option in module.options:
-        if option.name is None:
-            continue
-        fmt = {
-            'capname': option.name[0].capitalize() + option.name[1:],
-            'type': option.type,
-            'module': module.id,
-            'name': option.name,
-        }
-        res.append(TPL_SETDEFAULT_IMPL.format(**fmt))
-    return '\n'.join(res)
-
-
 ################################################################################
 # for main/options.cpp
 
@@ -875,11 +843,9 @@ def codegen_module(module, dst_dir, tpls):
         'holder_decl': generate_module_holder_decl(module),
         'wrapper_functions': generate_module_wrapper_functions(module),
         'option_names': generate_module_option_names(module),
-        'setdefaults_decl': generate_module_setdefaults_decl(module),
         # module source
         'header': module.header,
         'modes_impl': generate_module_mode_impl(module),
-        'setdefaults_impl': generate_module_setdefaults_impl(module),
     }
     for tpl in tpls:
         filename = tpl['output'].replace('module', module.filename)
diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp
index ee5260f34..d2ece3f13 100644
--- a/src/options/module_template.cpp
+++ b/src/options/module_template.cpp
@@ -28,11 +28,4 @@ namespace cvc5::options {
 ${modes_impl}$
 // clang-format on
 
-namespace ${id}$
-{
-// clang-format off
-${setdefaults_impl}$
-// clang-format on
-}
-
 }  // namespace cvc5::options
diff --git a/src/options/module_template.h b/src/options/module_template.h
index 61d689b72..d9b591f11 100644
--- a/src/options/module_template.h
+++ b/src/options/module_template.h
@@ -56,8 +56,6 @@ namespace ${id}$
 {
 // clang-format off
 ${option_names}$
-
-${setdefaults_decl}$
 // clang-format on
 }
 
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 93b08a858..ec6c831e4 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -387,7 +387,10 @@ void OptionsHandler::checkBvSatSolver(const std::string& option,
                             + " does not support lazy bit-blasting.\n"
                             + "Try --bv-sat-solver=minisat");
     }
-    options::bv::setDefaultBitvectorToBool(*d_options, true);
+    if (!d_options->bv.bitvectorToBoolWasSetByUser)
+    {
+      d_options->bv.bitvectorToBool = true;
+    }
   }
 }
 
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 19862cab2..420496190 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -259,6 +259,7 @@ name   = "SMT Layer"
   category   = "common"
   long       = "produce-assertions"
   type       = "bool"
+  alias      = ["interactive-mode"]
   help       = "keep an assertions list (enables get-assertions command)"
 
 [[option]]
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 84c0bd17c..9f34b5647 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -737,6 +737,36 @@ void Parser::pushScope(bool isUserContext)
   d_symman->pushScope(isUserContext);
 }
 
+void Parser::pushGetValueScope()
+{
+  pushScope();
+  // we must bind all relevant uninterpreted constants, which coincide with
+  // the set of uninterpreted constants that are printed in the definition
+  // of a model.
+  std::vector<api::Sort> declareSorts = d_symman->getModelDeclareSorts();
+  Trace("parser") << "Push get value scope, with " << declareSorts.size()
+                  << " declared sorts" << std::endl;
+  for (const api::Sort& s : declareSorts)
+  {
+    std::vector<api::Term> elements = d_solver->getModelDomainElements(s);
+    for (const api::Term& e : elements)
+    {
+      // Uninterpreted constants are abstract values, which by SMT-LIB are
+      // required to be annotated with their type, e.g. (as @uc_Foo_0 Foo).
+      // Thus, the element is not printed simply as its name.
+      std::string en = e.toString();
+      size_t index = en.find("(as ");
+      if (index == 0)
+      {
+        index = en.find(" ", 4);
+        en = en.substr(4, index - 4);
+      }
+      Trace("parser") << "Get value scope : " << en << " -> " << e << std::endl;
+      defineVar(en, e);
+    }
+  }
+}
+
 void Parser::popScope()
 {
   d_symman->popScope();
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 4b04c77b7..19e5b8531 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -716,6 +716,14 @@ public:
    */
   void pushScope(bool isUserContext = false);
 
+  /** Push scope for get-value
+   *
+   * This pushes a scope by a call to pushScope that binds all relevant bindings
+   * required for parsing the SMT-LIB command `get-value`. This includes
+   * all uninterpreted constant values in user-defined uninterpreted sorts.
+   */
+  void pushGetValueScope();
+
   void popScope();
 
   virtual void reset();
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 478edb651..e3aee250e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -343,7 +343,13 @@ command [std::unique_ptr<cvc5::Command>* cmd]
   | DECLARE_DATATYPE_TOK datatypeDefCommand[false, cmd]
   | DECLARE_DATATYPES_TOK datatypesDefCommand[false, cmd]
   | /* value query */
-    GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); }
+    GET_VALUE_TOK 
+    {
+      PARSER_STATE->checkThatLogicIsSet();
+      // bind all symbols specific to the model, e.g. uninterpreted constant
+      // values
+      PARSER_STATE->pushGetValueScope();
+    }
     ( LPAREN_TOK termList[terms,expr] RPAREN_TOK
       { cmd->reset(new GetValueCommand(terms)); }
     | ~LPAREN_TOK
@@ -352,6 +358,7 @@ command [std::unique_ptr<cvc5::Command>* cmd]
                                  "parentheses?");
       }
     )
+    { PARSER_STATE->popScope(); }
   | /* get-assignment */
     GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { cmd->reset(new GetAssignmentCommand()); }
@@ -793,7 +800,7 @@ smt25Command[std::unique_ptr<cvc5::Command>* cmd]
 
     /* echo */
   | ECHO_TOK
-    ( simpleSymbolicExpr[s]
+    ( str[s, true]
       { cmd->reset(new EchoCommand(s)); }
     | { cmd->reset(new EchoCommand()); }
     )
@@ -1648,7 +1655,7 @@ identifier[cvc5::ParseOp& p]
         if (!f.getSort().isConstructor())
         {
           PARSER_STATE->parseError(
-              "Bad syntax for test (_ is X), X must be a constructor.");
+              "Bad syntax for (_ is X), X must be a constructor.");
         }
         // get the datatype that f belongs to
         api::Sort sf = f.getSort().getConstructorCodomainSort();
@@ -1662,7 +1669,7 @@ identifier[cvc5::ParseOp& p]
         if (!f.getSort().isSelector())
         {
           PARSER_STATE->parseError(
-              "Bad syntax for test (_ update X), X must be a selector.");
+              "Bad syntax for (_ update X), X must be a selector.");
         }
         std::string sname = f.toString();
         // get the datatype that f belongs to
@@ -1673,13 +1680,6 @@ identifier[cvc5::ParseOp& p]
         // get the updater term
         p.d_expr = ds.getUpdaterTerm();
       }
-    | TUPLE_SEL_TOK m=INTEGER_LITERAL
-      {
-        // we adopt a special syntax (_ tupSel n)
-        p.d_kind = api::APPLY_SELECTOR;
-        // put m in expr so that the caller can deal with this case
-        p.d_expr = SOLVER->mkInteger(AntlrInput::tokenToUnsigned($m));
-      }
     | TUPLE_PROJECT_TOK nonemptyNumeralList[numerals]
       {
         // we adopt a special syntax (_ tuple_project i_1 ... i_n) where
@@ -1697,9 +1697,10 @@ identifier[cvc5::ParseOp& p]
       {
         std::string opName = AntlrInput::tokenText($sym);
         api::Kind k = PARSER_STATE->getIndexedOpKind(opName);
-        if (k == api::APPLY_UPDATER)
+        if (k == api::APPLY_SELECTOR || k == api::APPLY_UPDATER)
         {
-          // we adopt a special syntax (_ tuple_update n) for tuple updaters
+          // we adopt a special syntax (_ tuple_select n) and (_ tuple_update n)
+          // for tuple selectors and updaters
           if (numerals.size() != 1)
           {
             PARSER_STATE->parseError(
@@ -2314,7 +2315,6 @@ FORALL_TOK        : 'forall';
 
 CHAR_TOK : { PARSER_STATE->isTheoryEnabled(theory::THEORY_STRINGS) }? 'char';
 TUPLE_CONST_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple';
-TUPLE_SEL_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_select';
 TUPLE_PROJECT_TOK: { PARSER_STATE->isTheoryEnabled(theory::THEORY_DATATYPES) }? 'tuple_project';
 
 HO_ARROW_TOK : { PARSER_STATE->isHoEnabled() }? '->';
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index b186c2b2a..be7bdcb0f 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -135,6 +135,11 @@ void Smt2::addDatatypesOperators()
   {
     Parser::addOperator(api::APPLY_UPDATER);
     addOperator(api::DT_SIZE, "dt.size");
+    // Notice that tuple operators, we use the generic APPLY_SELECTOR and
+    // APPLY_UPDATER kinds. These are processed based on the context
+    // in which they are parsed, e.g. when parsing identifiers.
+    addIndexedOperator(
+        api::APPLY_SELECTOR, api::APPLY_SELECTOR, "tuple_select");
     addIndexedOperator(api::APPLY_UPDATER, api::APPLY_UPDATER, "tuple_update");
   }
 }
@@ -258,14 +263,16 @@ void Smt2::addFloatingPointOperators() {
 }
 
 void Smt2::addSepOperators() {
+  defineVar("sep.emp", d_solver->mkSepEmp());
+  // the Boolean sort is a placeholder here since we don't have type info
+  // without type annotation
+  defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort()));
   addOperator(api::SEP_STAR, "sep");
   addOperator(api::SEP_PTO, "pto");
   addOperator(api::SEP_WAND, "wand");
-  addOperator(api::SEP_EMP, "emp");
   Parser::addOperator(api::SEP_STAR);
   Parser::addOperator(api::SEP_PTO);
   Parser::addOperator(api::SEP_WAND);
-  Parser::addOperator(api::SEP_EMP);
 }
 
 void Smt2::addCoreSymbols()
@@ -288,7 +295,7 @@ void Smt2::addOperator(api::Kind kind, const std::string& name)
   Debug("parser") << "Smt2::addOperator( " << kind << ", " << name << " )"
                   << std::endl;
   Parser::addOperator(kind);
-  operatorKindMap[name] = kind;
+  d_operatorKindMap[name] = kind;
 }
 
 void Smt2::addIndexedOperator(api::Kind tKind,
@@ -302,11 +309,11 @@ void Smt2::addIndexedOperator(api::Kind tKind,
 api::Kind Smt2::getOperatorKind(const std::string& name) const
 {
   // precondition: isOperatorEnabled(name)
-  return operatorKindMap.find(name)->second;
+  return d_operatorKindMap.find(name)->second;
 }
 
 bool Smt2::isOperatorEnabled(const std::string& name) const {
-  return operatorKindMap.find(name) != operatorKindMap.end();
+  return d_operatorKindMap.find(name) != d_operatorKindMap.end();
 }
 
 bool Smt2::isTheoryEnabled(theory::TheoryId theory) const
@@ -437,7 +444,7 @@ void Smt2::reset() {
   d_logicSet = false;
   d_seenSetLogic = false;
   d_logic = LogicInfo();
-  operatorKindMap.clear();
+  d_operatorKindMap.clear();
   d_lastNamedTerm = std::pair<api::Term, std::string>();
 }
 
@@ -546,7 +553,7 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
 
     if (d_logic.areTranscendentalsUsed())
     {
-      defineVar("real.pi", d_solver->mkTerm(api::PI));
+      defineVar("real.pi", d_solver->mkPi());
       addTranscendentalOperators();
     }
     if (!strictModeEnabled())
@@ -672,12 +679,8 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
     addFloatingPointOperators();
   }
 
-  if (d_logic.isTheoryEnabled(theory::THEORY_SEP)) {
-    // the Boolean sort is a placeholder here since we don't have type info
-    // without type annotation
-    defineVar("sep.nil", d_solver->mkSepNil(d_solver->getBooleanSort()));
-    defineVar("sep.emp", d_solver->mkTerm(api::SEP_EMP));
-
+  if (d_logic.isTheoryEnabled(theory::THEORY_SEP))
+  {
     addSepOperators();
   }
 
@@ -1119,11 +1122,6 @@ api::Term Smt2::applyParseOp(ParseOp& p, std::vector<api::Term>& args)
       Debug("parser") << "applyParseOp: return uminus " << ret << std::endl;
       return ret;
     }
-    if (kind == api::EQ_RANGE && d_solver->getOption("arrays-exp") != "true")
-    {
-      parseError(
-          "eqrange predicate requires option --arrays-exp to be enabled.");
-    }
     if (kind == api::SINGLETON && args.size() == 1)
     {
       api::Term ret = d_solver->mkTerm(api::SINGLETON, args[0]);
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index fd68732fe..8d8f8febe 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -50,7 +50,7 @@ class Smt2 : public Parser
   bool d_seenSetLogic;
 
   LogicInfo d_logic;
-  std::unordered_map<std::string, api::Kind> operatorKindMap;
+  std::unordered_map<std::string, api::Kind> d_operatorKindMap;
   /**
    * Maps indexed symbols to the kind of the operator (e.g. "extract" to
    * BITVECTOR_EXTRACT).
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 32b195be2..1da2a3c7b 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -1723,15 +1723,7 @@ void Smt2Printer::toStreamCmdEmpty(std::ostream& out,
 void Smt2Printer::toStreamCmdEcho(std::ostream& out,
                                   const std::string& output) const
 {
-  std::string s = output;
-  // escape all double-quotes
-  size_t pos = 0;
-  while ((pos = s.find('"', pos)) != string::npos)
-  {
-    s.replace(pos, 1, "\"\"");
-    pos += 2;
-  }
-  out << "(echo \"" << s << "\")" << std::endl;
+  out << "(echo " << cvc5::quoteString(output) << ')' << std::endl;
 }
 
 /*
@@ -1930,14 +1922,9 @@ static void toStream(std::ostream& out, const CommandUnsupported* s, Variant v)
 #endif /* CVC5_COMPETITION_MODE */
 }
 
-static void errorToStream(std::ostream& out, std::string message, Variant v) {
-  // escape all double-quotes
-  size_t pos = 0;
-  while((pos = message.find('"', pos)) != string::npos) {
-    message.replace(pos, 1, "\"\"");
-    pos += 2;
-  }
-  out << "(error \"" << message << "\")" << endl;
+static void errorToStream(std::ostream& out, std::string message, Variant v)
+{
+  out << "(error " << cvc5::quoteString(message) << ')' << endl;
 }
 
 static void toStream(std::ostream& out, const CommandFailure* s, Variant v) {
diff --git a/src/proof/alethe/alethe_post_processor.cpp b/src/proof/alethe/alethe_post_processor.cpp
index 6312f3140..ef7735b44 100644
--- a/src/proof/alethe/alethe_post_processor.cpp
+++ b/src/proof/alethe/alethe_post_processor.cpp
@@ -55,6 +55,79 @@ bool AletheProofPostprocessCallback::update(Node res,
 
   switch (id)
   {
+    // To keep the original shape of the proof node it is necessary to rederive
+    // the original conclusion. However, the term that should be printed might
+    // be different from that conclusion. Thus, it is stored as an additional
+    // argument in the proof node. Usually, the only difference is an additional
+    // cl operator or the outmost or operator being replaced by a cl operator.
+    //
+    // When steps are added to the proof that have not been there previously,
+    // it is unwise to add them in the same manner. To illustrate this the
+    // following counterexample shows the pitfalls of this approach:
+    //
+    //  (or a (or b c))   (not a)
+    // --------------------------- RESOLUTION
+    //  (or b c)
+    //
+    //  is converted into an Alethe proof that should be printed as
+    //
+    //  (cl a (or b c))   (cl (not a))
+    // -------------------------------- RESOLUTION
+    //  (cl (or b c))
+    // --------------- OR
+    //  (cl b c)
+    //
+    // Here, (cl (or b c)) and (cl b c) cannot correspond to the same proof node
+    // (or b c). Thus, we build a new proof node using the kind SEXPR
+    // that is then printed as (cl (or b c)). We denote this wrapping of a proof
+    // node by using an extra pair of parenthesis, i.e. ((or b c)) is the proof
+    // node printed as (cl (or b c)).
+    //
+    //
+    // Some proof rules have a close correspondence in Alethe. There are two
+    // very frequent patterns that, to avoid repetition, are described here and
+    // referred to in the comments on the specific proof rules below.
+    //
+    // The first pattern, which will be called singleton pattern in the
+    // following, adds the original proof node F with the corresponding rule R'
+    // of the Alethe calculus and uses the same premises as the original proof
+    // node (P1:F1) ... (Pn:Fn). However, the conclusion is printed as (cl F).
+    //
+    // This means a cvc5 rule R that looks as follows:
+    //
+    //  (P1:F1) ... (Pn:Fn)
+    // --------------------- R
+    //  F
+    //
+    // is transformed into:
+    //
+    //  (P1:F1) ... (Pn:Fn)
+    // --------------------- R'
+    //  (cl F)*
+    //
+    // * the corresponding proof node is F
+    //
+    // The second pattern, which will be called clause pattern in the following,
+    // has a disjunction (or G1 ... Gn) as conclusion. It also adds the orignal
+    // proof node (or G1 ... Gn) with the corresponding rule R' of the Alethe
+    // calculus and uses the same premises as the original proof node (P1:F1)
+    // ... (Pn:Fn). However, the conclusion is printed as (cl G1 ... Gn), i.e.
+    // the or is replaced by the cl operator.
+    //
+    // This means a cvc5 rule R that looks as follows:
+    //
+    //  (P1:F1) ... (Pn:Fn)
+    // --------------------- R
+    //  (or G1 ... Gn)
+    //
+    // Is transformed into:
+    //
+    //  (P1:F1) ... (Pn:Fn)
+    // --------------------- R'
+    //  (cl G1 ... Gn)*
+    //
+    // * the corresponding proof node is (or G1 ... Gn)
+    //
     //================================================= Core rules
     //======================== Assume and Scope
     case PfRule::ASSUME:
diff --git a/src/proof/proof_node_manager.cpp b/src/proof/proof_node_manager.cpp
index a3ef944e0..8b4b332a1 100644
--- a/src/proof/proof_node_manager.cpp
+++ b/src/proof/proof_node_manager.cpp
@@ -28,7 +28,8 @@ using namespace cvc5::kind;
 
 namespace cvc5 {
 
-ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc)
+ProofNodeManager::ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc)
+    : d_rewriter(rr), d_checker(pc)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
   // we always allocate a proof checker, regardless of the proof checking mode
@@ -160,14 +161,14 @@ std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
         computedAcr = true;
         for (const Node& acc : ac)
         {
-          Node accr = theory::Rewriter::rewrite(acc);
+          Node accr = d_rewriter->rewrite(acc);
           if (accr != acc)
           {
             acr[accr] = acc;
           }
         }
       }
-      Node ar = theory::Rewriter::rewrite(a);
+      Node ar = d_rewriter->rewrite(a);
       std::unordered_map<Node, Node>::iterator itr = acr.find(ar);
       if (itr != acr.end())
       {
diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h
index 928aabb76..533f6d173 100644
--- a/src/proof/proof_node_manager.h
+++ b/src/proof/proof_node_manager.h
@@ -28,6 +28,10 @@ namespace cvc5 {
 class ProofChecker;
 class ProofNode;
 
+namespace theory {
+class Rewriter;
+}
+
 /**
  * A manager for proof node objects. This is a trusted interface for creating
  * and updating ProofNode objects.
@@ -54,7 +58,7 @@ class ProofNode;
 class ProofNodeManager
 {
  public:
-  ProofNodeManager(ProofChecker* pc = nullptr);
+  ProofNodeManager(theory::Rewriter* rr, ProofChecker* pc = nullptr);
   ~ProofNodeManager() {}
   /**
    * This constructs a ProofNode with the given arguments. The expected
@@ -184,6 +188,8 @@ class ProofNodeManager
   static ProofNode* cancelDoubleSymm(ProofNode* pn);
 
  private:
+  /** The rewriter */
+  theory::Rewriter* d_rewriter;
   /** The (optional) proof checker */
   ProofChecker* d_checker;
   /** the true node */
diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index f148d1018..5d16c12ce 100644
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -31,8 +31,7 @@ using namespace cvc5::theory;
 namespace cvc5 {
 namespace smt {
 
-CheckModels::CheckModels(Env& e) : d_env(e) {}
-CheckModels::~CheckModels() {}
+CheckModels::CheckModels(Env& e) : EnvObj(e) {}
 
 void CheckModels::checkModel(TheoryModel* m,
                              const context::CDList<Node>& al,
@@ -50,6 +49,12 @@ void CheckModels::checkModel(TheoryModel* m,
     throw RecoverableModalException(
         "Cannot run check-model on a model with approximate values.");
   }
+  Node sepHeap, sepNeq;
+  if (m->getHeapModel(sepHeap, sepNeq))
+  {
+    throw RecoverableModalException(
+        "Cannot run check-model on a model with a separation logic heap.");
+  }
 
   theory::SubstitutionMap& sm = d_env.getTopLevelSubstitutions().get();
   Trace("check-model") << "checkModel: Check assertions..." << std::endl;
@@ -71,7 +76,7 @@ void CheckModels::checkModel(TheoryModel* m,
     Notice() << "SolverEngine::checkModel(): -- substitutes to " << n
              << std::endl;
 
-    n = Rewriter::rewrite(n);
+    n = rewrite(n);
     Notice() << "SolverEngine::checkModel(): -- rewrites to " << n << std::endl;
 
     // We look up the value before simplifying. If n contains quantifiers,
diff --git a/src/smt/check_models.h b/src/smt/check_models.h
index d785b53d5..2b3447010 100644
--- a/src/smt/check_models.h
+++ b/src/smt/check_models.h
@@ -20,11 +20,10 @@
 
 #include "context/cdlist.h"
 #include "expr/node.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
-class Env;
-
 namespace theory {
 class TheoryModel;
 }
@@ -34,11 +33,10 @@ namespace smt {
 /**
  * This utility is responsible for checking the current model.
  */
-class CheckModels
+class CheckModels : protected EnvObj
 {
  public:
   CheckModels(Env& e);
-  ~CheckModels();
   /**
    * Check model m against the current set of input assertions al.
    *
@@ -48,10 +46,6 @@ class CheckModels
   void checkModel(theory::TheoryModel* m,
                   const context::CDList<Node>& al,
                   bool hardFailure);
-
- private:
-  /** Reference to the environment */
-  Env& d_env;
 };
 
 }  // namespace smt
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 311d6713a..e8ee6d59c 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -38,6 +38,7 @@
 #include "proof/unsat_core.h"
 #include "smt/dump.h"
 #include "smt/model.h"
+#include "util/smt2_quote_string.h"
 #include "util/unsafe_interrupt_exception.h"
 #include "util/utility.h"
 
@@ -302,19 +303,10 @@ void EmptyCommand::toStream(std::ostream& out,
 /* class EchoCommand                                                          */
 /* -------------------------------------------------------------------------- */
 
-EchoCommand::EchoCommand(std::string output)
-{
-  // escape all double-quotes
-  size_t pos = 0;
-  while ((pos = output.find('"', pos)) != string::npos)
-  {
-    output.replace(pos, 1, "\"\"");
-    pos += 2;
-  }
-  d_output = '"' + output + '"';
-}
+EchoCommand::EchoCommand(std::string output) : d_output(output) {}
 
 std::string EchoCommand::getOutput() const { return d_output; }
+
 void EchoCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   /* we don't have an output stream here, nothing to do */
@@ -325,7 +317,7 @@ void EchoCommand::invoke(api::Solver* solver,
                          SymbolManager* sm,
                          std::ostream& out)
 {
-  out << d_output << std::endl;
+  out << cvc5::quoteString(d_output) << std::endl;
   Trace("dtview::command") << "* ~COMMAND: echo |" << d_output << "|~"
                            << std::endl;
   d_commandStatus = CommandSuccess::instance();
@@ -335,6 +327,7 @@ void EchoCommand::invoke(api::Solver* solver,
 }
 
 Command* EchoCommand::clone() const { return new EchoCommand(d_output); }
+
 std::string EchoCommand::getCommandName() const { return "echo"; }
 
 void EchoCommand::toStream(std::ostream& out,
diff --git a/src/smt/model_blocker.cpp b/src/smt/model_blocker.cpp
index cbc388331..e8c1ff07f 100644
--- a/src/smt/model_blocker.cpp
+++ b/src/smt/model_blocker.cpp
@@ -25,6 +25,8 @@ using namespace cvc5::kind;
 
 namespace cvc5 {
 
+ModelBlocker::ModelBlocker(Env& e) : EnvObj(e) {}
+
 Node ModelBlocker::getModelBlocker(const std::vector<Node>& assertions,
                                    theory::TheoryModel* m,
                                    options::BlockModelsMode mode,
diff --git a/src/smt/model_blocker.h b/src/smt/model_blocker.h
index 42219e220..5e41de6a3 100644
--- a/src/smt/model_blocker.h
+++ b/src/smt/model_blocker.h
@@ -22,6 +22,7 @@
 
 #include "expr/node.h"
 #include "options/smt_options.h"
+#include "smt/env_obj.h"
 
 namespace cvc5 {
 
@@ -32,9 +33,10 @@ class TheoryModel;
 /**
  * A utility for blocking the current model.
  */
-class ModelBlocker
+class ModelBlocker : protected EnvObj
 {
  public:
+  ModelBlocker(Env& e);
   /** get model blocker
    *
    * This returns a disjunction of literals ~L1 V ... V ~Ln with the following
@@ -63,7 +65,7 @@ class ModelBlocker
    * our input. In other words, we do not return ~(x < 0) V ~(w < 0) since the
    * left disjunct is always false.
    */
-  static Node getModelBlocker(
+  Node getModelBlocker(
       const std::vector<Node>& assertions,
       theory::TheoryModel* m,
       options::BlockModelsMode mode,
diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 4b16b9391..3aed58b30 100644
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -150,7 +150,7 @@ Node Preprocessor::simplify(const Node& node)
     d_env.getPrinter().toStreamCmdSimplify(d_env.getDumpOut(), node);
   }
   Node ret = expandDefinitions(node);
-  ret = theory::Rewriter::rewrite(ret);
+  ret = rewrite(ret);
   return ret;
 }
 
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 2e08ab2df..4b4291075 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -41,7 +41,7 @@ PfManager::PfManager(Env& env)
       d_pchecker(new ProofChecker(
           options().proof.proofCheck == options::ProofCheckMode::EAGER,
           options().proof.proofPedantic)),
-      d_pnm(new ProofNodeManager(d_pchecker.get())),
+      d_pnm(new ProofNodeManager(env.getRewriter(), d_pchecker.get())),
       d_pppg(new PreprocessProofGenerator(
           d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")),
       d_pfpp(nullptr),
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index adc15ca2c..04a36c1c0 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -42,7 +42,7 @@ ProofPostprocessCallback::ProofPostprocessCallback(Env& env,
     : d_env(env),
       d_pnm(env.getProofNodeManager()),
       d_pppg(pppg),
-      d_wfpm(env.getProofNodeManager()),
+      d_wfpm(env),
       d_updateScopedAssumptions(updateScopedAssumptions)
 {
   d_true = NodeManager::currentNM()->mkConst(true);
@@ -654,7 +654,7 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
     // apply transitivity if necessary
     Node eq = addProofForTrans(tchildren, cdp);
 
-    cdp->addStep(args[0], PfRule::EQ_RESOLVE, {children[0], eq}, {});
+    cdp->addStep(eq[1], PfRule::EQ_RESOLVE, {children[0], eq}, {});
     return args[0];
   }
   else if (id == PfRule::MACRO_RESOLUTION
diff --git a/src/smt/solver_engine.cpp b/src/smt/solver_engine.cpp
index 911e0a960..fc6ec3915 100644
--- a/src/smt/solver_engine.cpp
+++ b/src/smt/solver_engine.cpp
@@ -417,10 +417,10 @@ void SolverEngine::setInfo(const std::string& key, const std::string& value)
 
 bool SolverEngine::isValidGetInfoFlag(const std::string& key) const
 {
-  if (key == "all-statistics" || key == "error-behavior" || key == "name"
-      || key == "version" || key == "authors" || key == "status"
-      || key == "reason-unknown" || key == "assertion-stack-levels"
-      || key == "all-options" || key == "time")
+  if (key == "all-statistics" || key == "error-behavior" || key == "filename"
+      || key == "name" || key == "version" || key == "authors"
+      || key == "status" || key == "time" || key == "reason-unknown"
+      || key == "assertion-stack-levels" || key == "all-options")
   {
     return true;
   }
@@ -455,7 +455,7 @@ std::string SolverEngine::getInfo(const std::string& key) const
   }
   if (key == "authors")
   {
-    return toSExpr(Configuration::about());
+    return toSExpr("the " + Configuration::getName() + " authors");
   }
   if (key == "status")
   {
@@ -1081,7 +1081,7 @@ Node SolverEngine::getValue(const Node& ex) const
   // AJR : necessary?
   if (!n.getType().isFunction())
   {
-    n = Rewriter::rewrite(n);
+    n = d_env->getRewriter()->rewrite(n);
   }
 
   Trace("smt") << "--- getting value of " << n << endl;
@@ -1224,7 +1224,8 @@ Result SolverEngine::blockModel()
 
   // get expanded assertions
   std::vector<Node> eassertsProc = getExpandedAssertions();
-  Node eblocker = ModelBlocker::getModelBlocker(
+  ModelBlocker mb(*d_env.get());
+  Node eblocker = mb.getModelBlocker(
       eassertsProc, m, d_env->getOptions().smt.blockModelsMode);
   Trace("smt") << "Block formula: " << eblocker << std::endl;
   return assertFormula(eblocker);
@@ -1247,7 +1248,8 @@ Result SolverEngine::blockModelValues(const std::vector<Node>& exprs)
   // get expanded assertions
   std::vector<Node> eassertsProc = getExpandedAssertions();
   // we always do block model values mode here
-  Node eblocker = ModelBlocker::getModelBlocker(
+  ModelBlocker mb(*d_env.get());
+  Node eblocker = mb.getModelBlocker(
       eassertsProc, m, options::BlockModelsMode::VALUES, exprs);
   return assertFormula(eblocker);
 }
diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 2a1d4e6c6..5db9804c6 100644
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -377,7 +377,7 @@ void SygusSolver::checkSynthSolution(Assertions& as)
       // problem are rewritten to true. If this is not the case, then the
       // assertions module of the subsolver will complain about assertions
       // with free variables.
-      Node ar = theory::Rewriter::rewrite(a);
+      Node ar = rewrite(a);
       solChecker->assertFormula(ar);
     }
     Result r = solChecker->checkSat();
diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp
index 8e998b9cf..16d297495 100644
--- a/src/smt/witness_form.cpp
+++ b/src/smt/witness_form.cpp
@@ -16,21 +16,27 @@
 #include "smt/witness_form.h"
 
 #include "expr/skolem_manager.h"
+#include "smt/env.h"
 #include "theory/rewriter.h"
 
 namespace cvc5 {
 namespace smt {
 
-WitnessFormGenerator::WitnessFormGenerator(ProofNodeManager* pnm)
-    : d_tcpg(pnm,
+WitnessFormGenerator::WitnessFormGenerator(Env& env)
+    : d_rewriter(env.getRewriter()),
+      d_tcpg(env.getProofNodeManager(),
              nullptr,
              TConvPolicy::FIXPOINT,
              TConvCachePolicy::NEVER,
              "WfGenerator::TConvProofGenerator",
              nullptr,
              true),
-      d_wintroPf(pnm, nullptr, nullptr, "WfGenerator::LazyCDProof"),
-      d_pskPf(pnm, nullptr, "WfGenerator::PurifySkolemProof")
+      d_wintroPf(env.getProofNodeManager(),
+                 nullptr,
+                 nullptr,
+                 "WfGenerator::LazyCDProof"),
+      d_pskPf(
+          env.getProofNodeManager(), nullptr, "WfGenerator::PurifySkolemProof")
 {
 }
 
@@ -114,12 +120,12 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t)
 
 bool WitnessFormGenerator::requiresWitnessFormTransform(Node t, Node s) const
 {
-  return theory::Rewriter::rewrite(t) != theory::Rewriter::rewrite(s);
+  return d_rewriter->rewrite(t) != d_rewriter->rewrite(s);
 }
 
 bool WitnessFormGenerator::requiresWitnessFormIntro(Node t) const
 {
-  Node tr = theory::Rewriter::rewrite(t);
+  Node tr = d_rewriter->rewrite(t);
   return !tr.isConst() || !tr.getConst<bool>();
 }
 
diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h
index 8522d41f0..06d60c1ed 100644
--- a/src/smt/witness_form.h
+++ b/src/smt/witness_form.h
@@ -25,6 +25,13 @@
 #include "proof/proof_generator.h"
 
 namespace cvc5 {
+
+class Env;
+
+namespace theory {
+class Rewriter;
+}
+
 namespace smt {
 
 /**
@@ -37,7 +44,7 @@ namespace smt {
 class WitnessFormGenerator : public ProofGenerator
 {
  public:
-  WitnessFormGenerator(ProofNodeManager* pnm);
+  WitnessFormGenerator(Env& env);
   ~WitnessFormGenerator() {}
   /**
    * Get proof for, which expects an equality of the form t = toWitness(t).
@@ -85,6 +92,8 @@ class WitnessFormGenerator : public ProofGenerator
    * Return a proof generator that can prove the given axiom exists.
    */
   ProofGenerator* convertExistsInternal(Node exists);
+  /** The rewriter we are using */
+  theory::Rewriter* d_rewriter;
   /** The term conversion proof generator */
   TConvProofGenerator d_tcpg;
   /** The nodes we have already added rewrite steps for in d_tcpg */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 76a0c363d..cf2373b9f 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -193,9 +193,9 @@ void TheoryArith::postCheck(Effort level)
   if (Theory::fullEffort(level))
   {
     d_arithModelCache.clear();
+    std::set<Node> termSet;
     if (d_nonlinearExtension != nullptr)
     {
-      std::set<Node> termSet;
       updateModelCache(termSet);
       d_nonlinearExtension->checkFullEffort(d_arithModelCache, termSet);
     }
@@ -204,6 +204,15 @@ void TheoryArith::postCheck(Effort level)
       // set incomplete
       d_im.setIncomplete(IncompleteId::ARITH_NL_DISABLED);
     }
+    // If we won't be doing a last call effort check (which implies that
+    // models will be computed), we must sanity check the integer model
+    // from the linear solver now. We also must update the model cache
+    // if we did not do so above.
+    if (d_nonlinearExtension == nullptr)
+    {
+      updateModelCache(termSet);
+    }
+    sanityCheckIntegerModel();
   }
 }
 
@@ -274,12 +283,6 @@ bool TheoryArith::collectModelValues(TheoryModel* m,
 
   updateModelCache(termSet);
 
-  if (sanityCheckIntegerModel())
-  {
-    // We added a lemma
-    return false;
-  }
-
   // We are now ready to assert the model.
   for (const std::pair<const Node, Node>& p : d_arithModelCache)
   {
@@ -383,9 +386,9 @@ bool TheoryArith::sanityCheckIntegerModel()
       Trace("arith-check") << p.first << " -> " << p.second << std::endl;
       if (p.first.getType().isInteger() && !p.second.getType().isInteger())
       {
-        Assert(false) << "TheoryArithPrivate generated a bad model value for "
-                        "integer variable "
-                      << p.first << " : " << p.second;
+        Warning() << "TheoryArithPrivate generated a bad model value for "
+                     "integer variable "
+                  << p.first << " : " << p.second;
         // must branch and bound
         TrustNode lem =
             d_bab.branchIntegerVariable(p.first, p.second.getConst<Rational>());
diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 9e69c9f71..93eadde43 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -296,7 +296,19 @@ Node TheoryArrays::solveWrite(TNode term, bool solve1, bool solve2, bool ppCheck
 
 TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems)
 {
-  // first, see if we need to expand definitions
+  // first, check for logic exceptions
+  Kind k = term.getKind();
+  if (!options().arrays.arraysExp)
+  {
+    if (k == kind::EQ_RANGE)
+    {
+      std::stringstream ss;
+      ss << "Term of kind " << k
+         << " not supported in default mode, try --arrays-exp";
+      throw LogicException(ss.str());
+    }
+  }
+  // see if we need to expand definitions
   TrustNode texp = d_rewriter.expandDefinition(term);
   if (!texp.isNull())
   {
@@ -309,7 +321,8 @@ TrustNode TheoryArrays::ppRewrite(TNode term, std::vector<SkolemLemma>& lems)
   d_ppEqualityEngine.addTerm(term);
   NodeManager* nm = NodeManager::currentNM();
   Node ret;
-  switch (term.getKind()) {
+  switch (k)
+  {
     case kind::SELECT: {
       // select(store(a,i,v),j) = select(a,j)
       //    IF i != j
diff --git a/src/theory/arrays/theory_arrays_type_rules.cpp b/src/theory/arrays/theory_arrays_type_rules.cpp
index e1b4813ec..433768e5d 100644
--- a/src/theory/arrays/theory_arrays_type_rules.cpp
+++ b/src/theory/arrays/theory_arrays_type_rules.cpp
@@ -18,6 +18,7 @@
 // for array-constant attributes
 #include "expr/array_store_all.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
+#include "theory/builtin/theory_builtin_type_rules.h"
 #include "theory/type_enumerator.h"
 #include "util/cardinality.h"
 
@@ -249,7 +250,24 @@ bool ArraysProperties::isWellFounded(TypeNode type)
 
 Node ArraysProperties::mkGroundTerm(TypeNode type)
 {
-  return *TypeEnumerator(type);
+  Assert(type.getKind() == kind::ARRAY_TYPE);
+  TypeNode elemType = type.getArrayConstituentType();
+  Node elem = elemType.mkGroundTerm();
+  if (elem.isConst())
+  {
+    return NodeManager::currentNM()->mkConst(ArrayStoreAll(type, elem));
+  }
+  // Note the distinction between mkGroundTerm and mkGroundValue. While
+  // an arbitrary value can be obtained by calling the type enumerator here,
+  // that is wrong for types that are not closed enumerable since it may
+  // return a term containing values that should not appear in e.g. assertions.
+  // For example, arrays whose element type is an uninterpreted sort will
+  // incorrectly introduce uninterpreted sort values if this is done.
+  // It is currently infeasible to construct an ArrayStoreAll with the element
+  // type's mkGroundTerm as an argument when that term is not constant.
+  // Thus, we must simply return a fresh Skolem here, using the same utility
+  // as that of uninterpreted sorts.
+  return builtin::SortProperties::mkGroundTerm(type);
 }
 
 TypeNode ArrayPartialSelectTypeRule::computeType(NodeManager* nodeManager,
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index c446504fd..fd957baaa 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -16,12 +16,12 @@
 #include "theory/datatypes/datatypes_rewriter.h"
 
 #include "expr/ascription_type.h"
+#include "expr/codatatype_bound_variable.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
 #include "expr/sygus_datatype.h"
-#include "expr/uninterpreted_constant.h"
 #include "options/datatypes_options.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
@@ -729,7 +729,7 @@ Node DatatypesRewriter::collectRef(Node n,
       else
       {
         // a loop
-        const Integer& i = n.getConst<UninterpretedConstant>().getIndex();
+        const Integer& i = n.getConst<CodatatypeBoundVariable>().getIndex();
         uint32_t index = i.toUnsignedInt();
         if (index >= sk.size())
         {
@@ -771,7 +771,7 @@ Node DatatypesRewriter::normalizeCodatatypeConstantEqc(
     {
       int debruijn = depth - it->second - 1;
       return NodeManager::currentNM()->mkConst(
-          UninterpretedConstant(n.getType(), debruijn));
+          CodatatypeBoundVariable(n.getType(), debruijn));
     }
     std::vector<Node> children;
     bool childChanged = false;
@@ -798,10 +798,10 @@ Node DatatypesRewriter::replaceDebruijn(Node n,
                                         TypeNode orig_tn,
                                         unsigned depth)
 {
-  if (n.getKind() == kind::UNINTERPRETED_CONSTANT && n.getType() == orig_tn)
+  if (n.getKind() == kind::CODATATYPE_BOUND_VARIABLE && n.getType() == orig_tn)
   {
     unsigned index =
-        n.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
+        n.getConst<CodatatypeBoundVariable>().getIndex().toUnsignedInt();
     if (index == depth)
     {
       return orig;
diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index 41d5ded76..cb3a78cf2 100644
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -145,4 +145,13 @@ parameterized TUPLE_PROJECT TUPLE_PROJECT_OP 1 \
 typerule TUPLE_PROJECT_OP  "SimpleTypeRule<RBuiltinOperator>"
 typerule TUPLE_PROJECT     ::cvc5::theory::datatypes::TupleProjectTypeRule
 
+# For representing codatatype values
+constant CODATATYPE_BOUND_VARIABLE \
+    class \
+    CodatatypeBoundVariable \
+    ::cvc5::CodatatypeBoundVariableHashFunction \
+    "expr/codatatype_bound_variable.h" \
+    "the kind of expressions representing bound variables in codatatype constants, which are de Bruijn indexed variables; payload is an instance of the cvc5::CodatatypeBoundVariable class (used in models)"
+typerule CODATATYPE_BOUND_VARIABLE ::cvc5::theory::datatypes::CodatatypeBoundVariableTypeRule
+
 endtheory
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index c892ffc11..0cbeaa515 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -18,11 +18,11 @@
 #include <sstream>
 
 #include "base/check.h"
+#include "expr/codatatype_bound_variable.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "expr/kind.h"
 #include "expr/skolem_manager.h"
-#include "expr/uninterpreted_constant.h"
 #include "options/datatypes_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
@@ -1290,10 +1290,10 @@ bool TheoryDatatypes::collectModelValues(TheoryModel* m,
 
 Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth ){
   std::map< Node, int >::iterator itv = vmap.find( n );
+  NodeManager* nm = NodeManager::currentNM();
   if( itv!=vmap.end() ){
     int debruijn = depth - 1 - itv->second;
-    return NodeManager::currentNM()->mkConst(
-        UninterpretedConstant(n.getType(), debruijn));
+    return nm->mkConst(CodatatypeBoundVariable(n.getType(), debruijn));
   }else if( n.getType().isDatatype() ){
     Node nc = eqc_cons[n];
     if( !nc.isNull() ){
@@ -1308,7 +1308,7 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c
         children.push_back( rv );
       }
       vmap.erase( n );
-      return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
+      return nm->mkNode(APPLY_CONSTRUCTOR, children);
     }
   }
   return n;
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp
index 503eaf4df..86a11357b 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.cpp
+++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp
@@ -18,6 +18,7 @@
 #include <sstream>
 
 #include "expr/ascription_type.h"
+#include "expr/codatatype_bound_variable.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
 #include "expr/type_matcher.h"
@@ -597,6 +598,13 @@ TypeNode TupleProjectTypeRule::computeType(NodeManager* nm, TNode n, bool check)
   return nm->mkTupleType(types);
 }
 
+TypeNode CodatatypeBoundVariableTypeRule::computeType(NodeManager* nodeManager,
+                                                      TNode n,
+                                                      bool check)
+{
+  return n.getConst<CodatatypeBoundVariable>().getType();
+}
+
 }  // namespace datatypes
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index cf57a6c0d..7cf98aa74 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -99,6 +99,12 @@ class TupleProjectTypeRule
   static TypeNode computeType(NodeManager* nm, TNode n, bool check);
 };
 
+class CodatatypeBoundVariableTypeRule
+{
+ public:
+  static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check);
+};
+
 }  // namespace datatypes
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 39b48ece9..6528f1052 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -16,6 +16,7 @@
 #include "theory/datatypes/type_enumerator.h"
 
 #include "expr/ascription_type.h"
+#include "expr/codatatype_bound_variable.h"
 #include "expr/dtype_cons.h"
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
@@ -108,8 +109,8 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){
    {
      if (d_child_enum)
      {
-       ret = NodeManager::currentNM()->mkConst(
-           UninterpretedConstant(d_type, d_size_limit));
+       NodeManager* nm = NodeManager::currentNM();
+       ret = nm->mkConst(CodatatypeBoundVariable(d_type, d_size_limit));
      }
      else
      {
diff --git a/src/theory/incomplete_id.cpp b/src/theory/incomplete_id.cpp
index a2a3baa0f..c763fb9a0 100644
--- a/src/theory/incomplete_id.cpp
+++ b/src/theory/incomplete_id.cpp
@@ -40,6 +40,8 @@ const char* toString(IncompleteId i)
     case IncompleteId::STRINGS_LOOP_SKIP: return "STRINGS_LOOP_SKIP";
     case IncompleteId::STRINGS_REGEXP_NO_SIMPLIFY:
       return "STRINGS_REGEXP_NO_SIMPLIFY";
+    case IncompleteId::SEQ_FINITE_DYNAMIC_CARDINALITY:
+      return "SEQ_FINITE_DYNAMIC_CARDINALITY";
     case IncompleteId::UF_HO_EXT_DISABLED: return "UF_HO_EXT_DISABLED";
     case IncompleteId::UF_CARD_DISABLED: return "UF_CARD_DISABLED";
     case IncompleteId::UF_CARD_MODE: return "UF_CARD_MODE";
diff --git a/src/theory/incomplete_id.h b/src/theory/incomplete_id.h
index 951c2a94f..aaa458d8e 100644
--- a/src/theory/incomplete_id.h
+++ b/src/theory/incomplete_id.h
@@ -52,6 +52,11 @@ enum class IncompleteId
   STRINGS_LOOP_SKIP,
   // we could not simplify a regular expression membership
   STRINGS_REGEXP_NO_SIMPLIFY,
+  // incomplete due to sequence of a dynamic finite type (e.g. a type that
+  // we know is finite, but its exact cardinality is not fixed. For example,
+  // when finite model finding is enabled, uninterpreted sorts have a
+  // cardinality that depends on their interpretation in the current model).
+  SEQ_FINITE_DYNAMIC_CARDINALITY,
   // HO extensionality axiom was disabled
   UF_HO_EXT_DISABLED,
   // UF+cardinality solver was disabled
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index b98088a71..d778a679e 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -245,6 +245,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add)
       // now, do instantiation-based merging for each of these terms
       Trace("thm-ee-debug") << "Merge equivalence classes based on instantiations of terms..." << std::endl;
       //merge all pending equalities
+      EntailmentCheck* echeck = d_treg.getEntailmentCheck();
       while( !d_upendingAdds.empty() ){
         Trace("sg-pending") << "Add " << d_upendingAdds.size() << " pending terms..." << std::endl;
         std::vector< Node > pending;
@@ -256,7 +257,7 @@ Node ConjectureGenerator::getUniversalRepresentative(TNode n, bool add)
           Trace("thm-ee-add") << "UEE : Add universal term " << t << std::endl;
           std::vector< Node > eq_terms;
           //if occurs modulo equality at ground level, it is equivalent to representative of ground equality engine
-          Node gt = getTermDatabase()->evaluateTerm(t);
+          Node gt = echeck->evaluateTerm(t);
           if( !gt.isNull() && gt!=t ){
             eq_terms.push_back( gt );
           }
@@ -1362,7 +1363,8 @@ bool ConjectureGenerator::notifySubstitution( TNode glhs, std::map< TNode, TNode
   }
   Trace("sg-cconj-debug") << "Evaluate RHS : : " << rhs << std::endl;
   //get the representative of rhs with substitution subs
-  TNode grhs = getTermDatabase()->getEntailedTerm( rhs, subs, true );
+  EntailmentCheck* echeck = d_treg.getEntailmentCheck();
+  TNode grhs = echeck->getEntailedTerm(rhs, subs, true);
   Trace("sg-cconj-debug") << "...done evaluating term, got : " << grhs << std::endl;
   if( !grhs.isNull() ){
     if( glhs!=grhs ){
diff --git a/src/theory/quantifiers/ematching/ho_trigger.cpp b/src/theory/quantifiers/ematching/ho_trigger.cpp
index a8ab760ce..d2b0b0542 100644
--- a/src/theory/quantifiers/ematching/ho_trigger.cpp
+++ b/src/theory/quantifiers/ematching/ho_trigger.cpp
@@ -238,6 +238,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
     d_lchildren.clear();
     d_arg_to_arg_rep.clear();
     d_arg_vector.clear();
+    EntailmentCheck* echeck = d_treg.getEntailmentCheck();
     for (std::pair<const TNode, std::vector<Node> >& ha : ho_var_apps_subs)
     {
       TNode var = ha.first;
@@ -291,8 +292,7 @@ bool HigherOrderTrigger::sendInstantiation(std::vector<Node>& m, InferenceId id)
           {
             if (!d_qstate.areEqual(itf->second, args[k]))
             {
-              if (!d_treg.getTermDatabase()->isEntailed(
-                      itf->second.eqNode(args[k]), true))
+              if (!echeck->isEntailed(itf->second.eqNode(args[k]), true))
               {
                 fixed_vals[k] = Node::null();
               }
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index d8e3b7950..075299583 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
 #include "theory/quantifiers/ematching/inst_match_generator_simple.h"
 #include "theory/quantifiers/ematching/pattern_term_selector.h"
+#include "theory/quantifiers/ematching/relational_match_generator.h"
 #include "theory/quantifiers/ematching/var_match_generator.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quantifiers_state.h"
@@ -618,7 +619,7 @@ InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(
     InstMatchGenerator* init;
     std::map< Node, InstMatchGenerator * >::iterator iti = pat_map_init.find( pats[pCounter] );
     if( iti==pat_map_init.end() ){
-      init = new InstMatchGenerator(tparent, pats[pCounter]);
+      init = getInstMatchGenerator(tparent, q, pats[pCounter]);
     }else{
       init = iti->second;
     }
@@ -645,6 +646,7 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent,
                                                               Node q,
                                                               Node n)
 {
+  // maybe variable match generator
   if (n.getKind() != INST_CONSTANT)
   {
     Trace("var-trigger-debug")
@@ -672,6 +674,16 @@ InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent,
       return vmg;
     }
   }
+  Trace("relational-trigger")
+      << "Is " << n << " a relational trigger?" << std::endl;
+  // relational triggers
+  bool hasPol, pol;
+  Node lit;
+  if (TriggerTermInfo::isUsableRelationTrigger(n, hasPol, pol, lit))
+  {
+    Trace("relational-trigger") << "...yes, for literal " << lit << std::endl;
+    return new RelationalMatchGenerator(tparent, lit, hasPol, pol);
+  }
   return new InstMatchGenerator(tparent, n);
 }
 
diff --git a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
index 30be83ecc..fdb0d0db3 100644
--- a/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp
@@ -339,20 +339,18 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
                           TriggerDatabase::TR_GET_OLD,
                           d_num_trigger_vars[f]);
     }
-    if (tr == nullptr)
+    // if we generated a trigger above, add it
+    if (tr != nullptr)
     {
-      // did not generate a trigger
-      continue;
-    }
-    addTrigger(tr, f);
-    if (tr->isMultiTrigger())
-    {
-      // only add a single multi-trigger
-      continue;
+      addTrigger(tr, f);
+      if (tr->isMultiTrigger())
+      {
+        // only add a single multi-trigger
+        continue;
+      }
     }
     // if we are generating additional triggers...
-    size_t index = 0;
-    if (index < patTerms.size())
+    if (patTerms.size() > 1)
     {
       // check if similar patterns exist, and if so, add them additionally
       unsigned nqfs_curr = 0;
@@ -361,7 +359,7 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
         nqfs_curr =
             d_quant_rel->getNumQuantifiersForSymbol(patTerms[0].getOperator());
       }
-      index++;
+      size_t index = 1;
       bool success = true;
       while (success && index < patTerms.size()
              && d_is_single_trigger[patTerms[index]])
@@ -527,16 +525,22 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
     Trace("auto-gen-trigger-debug")
         << "...required polarity for " << pat << " is " << rpol
         << ", eq=" << rpoleq << std::endl;
+    // Currently, we have ad-hoc treatment for relational triggers that
+    // are not handled by RelationalMatchGen.
+    bool isAdHocRelationalTrigger =
+        TriggerTermInfo::isRelationalTrigger(pat)
+        && !TriggerTermInfo::isUsableRelationTrigger(pat);
     if (rpol != 0)
     {
       Assert(rpol == 1 || rpol == -1);
-      if (TriggerTermInfo::isRelationalTrigger(pat))
+      if (isAdHocRelationalTrigger)
       {
         pat = rpol == -1 ? pat.negate() : pat;
       }
       else
       {
-        Assert(TriggerTermInfo::isAtomicTrigger(pat));
+        Assert(TriggerTermInfo::isAtomicTrigger(pat)
+               || TriggerTermInfo::isUsableRelationTrigger(pat));
         if (pat.getType().isBoolean() && rpoleq.isNull())
         {
           if (options().quantifiers.literalMatchMode
@@ -575,13 +579,10 @@ bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
       }
       Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl;
     }
-    else
+    else if (isAdHocRelationalTrigger)
     {
-      if (TriggerTermInfo::isRelationalTrigger(pat))
-      {
-        // consider both polarities
-        addPatternToPool(f, pat.negate(), num_fv, mpat);
-      }
+      // consider both polarities
+      addPatternToPool(f, pat.negate(), num_fv, mpat);
     }
     addPatternToPool(f, pat, num_fv, mpat);
   }
diff --git a/src/theory/quantifiers/ematching/relational_match_generator.cpp b/src/theory/quantifiers/ematching/relational_match_generator.cpp
new file mode 100644
index 000000000..8981a7a2d
--- /dev/null
+++ b/src/theory/quantifiers/ematching/relational_match_generator.cpp
@@ -0,0 +1,125 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Relational match generator class.
+ */
+
+#include "theory/quantifiers/ematching/relational_match_generator.h"
+
+#include "theory/quantifiers/term_util.h"
+#include "util/rational.h"
+
+using namespace cvc5::kind;
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+namespace inst {
+
+RelationalMatchGenerator::RelationalMatchGenerator(Trigger* tparent,
+                                                   Node rtrigger,
+                                                   bool hasPol,
+                                                   bool pol)
+    : InstMatchGenerator(tparent, Node::null()),
+      d_vindex(-1),
+      d_hasPol(hasPol),
+      d_pol(pol),
+      d_counter(0)
+{
+  Assert((rtrigger.getKind() == EQUAL && rtrigger[0].getType().isReal())
+         || rtrigger.getKind() == GEQ);
+  Trace("relational-match-gen")
+      << "Relational trigger: " << rtrigger << ", hasPol/pol = " << hasPol
+      << "/" << pol << std::endl;
+  for (size_t i = 0; i < 2; i++)
+  {
+    if (rtrigger[i].getKind() == INST_CONSTANT)
+    {
+      d_var = rtrigger[i];
+      d_vindex = d_var.getAttribute(InstVarNumAttribute());
+      d_rhs = rtrigger[1 - i];
+      Assert(!quantifiers::TermUtil::hasInstConstAttr(d_rhs));
+      Kind k = rtrigger.getKind();
+      d_rel = (i == 0 ? k : (k == GEQ ? LEQ : k));
+      break;
+    }
+  }
+  Trace("relational-match-gen") << "...processed " << d_var << " (" << d_vindex
+                                << ") " << d_rel << " " << d_rhs << std::endl;
+  AlwaysAssert(!d_var.isNull())
+      << "Failed to initialize RelationalMatchGenerator";
+}
+
+bool RelationalMatchGenerator::reset(Node eqc)
+{
+  d_counter = 0;
+  return true;
+}
+
+int RelationalMatchGenerator::getNextMatch(Node q, InstMatch& m)
+{
+  Trace("relational-match-gen") << "getNextMatch, rel match gen" << std::endl;
+  // try (up to) two different terms
+  Node s;
+  Node rhs = d_rhs;
+  bool rmPrev = m.get(d_vindex).isNull();
+  while (d_counter < 2)
+  {
+    bool checkPol = false;
+    if (d_counter == 0)
+    {
+      checkPol = d_pol;
+    }
+    else
+    {
+      Assert(d_counter == 1);
+      if (d_hasPol)
+      {
+        break;
+      }
+      // try the opposite polarity
+      checkPol = !d_pol;
+    }
+    NodeManager* nm = NodeManager::currentNM();
+    // falsify ( d_var <d_rel> d_rhs ) = checkPol
+    s = rhs;
+    if (!checkPol)
+    {
+      s = nm->mkNode(PLUS, s, nm->mkConst(Rational(d_rel == GEQ ? -1 : 1)));
+    }
+    d_counter++;
+    Trace("relational-match-gen")
+        << "...try set " << s << " for " << checkPol << std::endl;
+    if (m.set(d_qstate, d_vindex, s))
+    {
+      Trace("relational-match-gen") << "...success" << std::endl;
+      int ret = continueNextMatch(q, m, InferenceId::UNKNOWN);
+      if (ret > 0)
+      {
+        Trace("relational-match-gen") << "...returned " << ret << std::endl;
+        return ret;
+      }
+      Trace("relational-match-gen") << "...failed to gen inst" << std::endl;
+      // failed
+      if (rmPrev)
+      {
+        m.d_vals[d_vindex] = Node::null();
+      }
+    }
+  }
+  return -1;
+}
+
+}  // namespace inst
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/ematching/relational_match_generator.h b/src/theory/quantifiers/ematching/relational_match_generator.h
new file mode 100644
index 000000000..eead2876a
--- /dev/null
+++ b/src/theory/quantifiers/ematching/relational_match_generator.h
@@ -0,0 +1,92 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Relational match generator class.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__RELATIONAL_MATCH_GENERATOR_H
+#define CVC5__THEORY__QUANTIFIERS__RELATIONAL_MATCH_GENERATOR_H
+
+#include "expr/node.h"
+#include "theory/quantifiers/ematching/inst_match_generator.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+namespace inst {
+
+/**
+ * Match generator for relational triggers x ~ t where t is a ground term.
+ * This match generator tries a small fixed set of terms based on the kind of
+ * relation and the required polarity of the trigger in the quantified formula.
+ *
+ * For example, for quantified formula (forall ((x Int)) (=> (> x n) (P x))),
+ * we have that (> x n) is a relational trigger with required polarity "true".
+ * This generator will try the match `x -> n+1` only, where notice that n+1 is
+ * the canonical term chosen to satisfy x>n. Canonical terms for arithmetic
+ * relations (~ x n) are in set { n, n+1, n-1 }.
+ *
+ * If a relational trigger does not have a required polarity, then up to 2
+ * terms are tried, a term that satisfies the relation, and one that does not.
+ * If (>= x n) is a relational trigger with no polarity, then `x -> n` and
+ * `x -> n-1` will be generated.
+ *
+ * Currently this class handles only equality between real or integer valued
+ * terms, or inequalities (kind GEQ). It furthermore only considers ground terms
+ * t for the right hand side of relations.
+ */
+class RelationalMatchGenerator : public InstMatchGenerator
+{
+ public:
+  /**
+   * @param tparent The parent trigger that this match generator belongs to
+   * @param rtrigger The relational trigger
+   * @param hasPol Whether the trigger has an entailed polarity
+   * @param pol The entailed polarity of the relational trigger.
+   */
+  RelationalMatchGenerator(Trigger* tparent,
+                           Node rtrigger,
+                           bool hasPol,
+                           bool pol);
+
+  /** Reset */
+  bool reset(Node eqc) override;
+  /** Get the next match. */
+  int getNextMatch(Node q, InstMatch& m) override;
+
+ private:
+  /** the variable */
+  Node d_var;
+  /** The index of the variable */
+  int64_t d_vindex;
+  /** the relation kind */
+  Kind d_rel;
+  /** the right hand side */
+  Node d_rhs;
+  /** whether we have a required polarity */
+  bool d_hasPol;
+  /** the required polarity, if it exists */
+  bool d_pol;
+  /**
+   * The current number of terms we have generated since the last call to reset
+   */
+  size_t d_counter;
+};
+
+}  // namespace inst
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
+
+#endif
diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp
index 600797f4e..f31ec088a 100644
--- a/src/theory/quantifiers/ematching/trigger_term_info.cpp
+++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp
@@ -70,6 +70,46 @@ bool TriggerTermInfo::isRelationalTriggerKind(Kind k)
   return k == EQUAL || k == GEQ;
 }
 
+bool TriggerTermInfo::isUsableRelationTrigger(Node n)
+{
+  bool hasPol, pol;
+  Node lit;
+  return isUsableRelationTrigger(n, hasPol, pol, lit);
+}
+bool TriggerTermInfo::isUsableRelationTrigger(Node n,
+                                              bool& hasPol,
+                                              bool& pol,
+                                              Node& lit)
+{
+  // relational triggers (not) (= (~ x t) true|false), where ~ in { =, >= }.
+  hasPol = false;
+  pol = n.getKind() != NOT;
+  lit = pol ? n : n[0];
+  if (lit.getKind() == EQUAL && lit[1].getType().isBoolean()
+      && lit[1].isConst())
+  {
+    hasPol = true;
+    pol = lit[1].getConst<bool>() ? pol : !pol;
+    lit = lit[0];
+  }
+  // is it a relational trigger?
+  if ((lit.getKind() == EQUAL && lit[0].getType().isReal())
+      || lit.getKind() == GEQ)
+  {
+    // if one side of the relation is a variable and the other side is a ground
+    // term, we can treat this using the relational match generator
+    for (size_t i = 0; i < 2; i++)
+    {
+      if (lit[i].getKind() == INST_CONSTANT
+          && !quantifiers::TermUtil::hasInstConstAttr(lit[1 - i]))
+      {
+        return true;
+      }
+    }
+  }
+  return false;
+}
+
 bool TriggerTermInfo::isSimpleTrigger(Node n)
 {
   Node t = n.getKind() == NOT ? n[0] : n;
@@ -105,7 +145,7 @@ int32_t TriggerTermInfo::getTriggerWeight(Node n)
   {
     return 0;
   }
-  if (isAtomicTrigger(n))
+  if (isAtomicTrigger(n) || isUsableRelationTrigger(n))
   {
     return 1;
   }
diff --git a/src/theory/quantifiers/ematching/trigger_term_info.h b/src/theory/quantifiers/ematching/trigger_term_info.h
index 753d0850c..3816d0988 100644
--- a/src/theory/quantifiers/ematching/trigger_term_info.h
+++ b/src/theory/quantifiers/ematching/trigger_term_info.h
@@ -108,6 +108,19 @@ class TriggerTermInfo
   static bool isRelationalTrigger(Node n);
   /** Is k a relational trigger kind? */
   static bool isRelationalTriggerKind(Kind k);
+  /**
+   * Is n a usable relational trigger, which is true if RelationalMatchGenerator
+   * can process n.
+   */
+  static bool isUsableRelationTrigger(Node n);
+  /**
+   * Same as above, but lit / hasPol / pol are updated to the required
+   * constructor arguments for RelationalMatchGenerator.
+   */
+  static bool isUsableRelationTrigger(Node n,
+                                      bool& hasPol,
+                                      bool& pol,
+                                      Node& lit);
   /** is n a simple trigger (see inst_match_generator.h)? */
   static bool isSimpleTrigger(Node n);
   /** get trigger weight
@@ -116,7 +129,8 @@ class TriggerTermInfo
    * trigger term n, where the smaller the value, the easier.
    *
    * Returns 0 for triggers that are APPLY_UF terms.
-   * Returns 1 for other triggers whose kind is atomic.
+   * Returns 1 for other triggers whose kind is atomic, or are usable
+   * relational triggers.
    * Returns 2 otherwise.
    */
   static int32_t getTriggerWeight(Node n);
diff --git a/src/theory/quantifiers/entailment_check.cpp b/src/theory/quantifiers/entailment_check.cpp
new file mode 100644
index 000000000..543414a4e
--- /dev/null
+++ b/src/theory/quantifiers/entailment_check.cpp
@@ -0,0 +1,411 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Implementation of entailment check class.
+ */
+
+#include "theory/quantifiers/entailment_check.h"
+
+#include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_database.h"
+
+using namespace cvc5::kind;
+using namespace cvc5::context;
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+EntailmentCheck::EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb)
+    : EnvObj(env), d_qstate(qs), d_tdb(tdb)
+{
+  d_true = NodeManager::currentNM()->mkConst(true);
+  d_false = NodeManager::currentNM()->mkConst(false);
+}
+
+EntailmentCheck::~EntailmentCheck() {}
+
+Node EntailmentCheck::evaluateTerm2(TNode n,
+                                    std::map<TNode, Node>& visited,
+                                    std::map<TNode, TNode>& subs,
+                                    bool subsRep,
+                                    bool useEntailmentTests,
+                                    bool reqHasTerm)
+{
+  std::map<TNode, Node>::iterator itv = visited.find(n);
+  if (itv != visited.end())
+  {
+    return itv->second;
+  }
+  Trace("term-db-eval") << "evaluate term : " << n << std::endl;
+  Node ret = n;
+  Kind k = n.getKind();
+  if (k == FORALL)
+  {
+    // do nothing
+  }
+  else if (k == BOUND_VARIABLE)
+  {
+    std::map<TNode, TNode>::iterator it = subs.find(n);
+    if (it != subs.end())
+    {
+      if (!subsRep)
+      {
+        Assert(d_qstate.hasTerm(it->second));
+        ret = d_qstate.getRepresentative(it->second);
+      }
+      else
+      {
+        ret = it->second;
+      }
+    }
+  }
+  else if (d_qstate.hasTerm(n))
+  {
+    Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
+    ret = d_qstate.getRepresentative(n);
+    reqHasTerm = false;
+  }
+  else if (n.hasOperator())
+  {
+    std::vector<TNode> args;
+    bool ret_set = false;
+    for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+    {
+      TNode c = evaluateTerm2(
+          n[i], visited, subs, subsRep, useEntailmentTests, reqHasTerm);
+      if (c.isNull())
+      {
+        ret = Node::null();
+        ret_set = true;
+        break;
+      }
+      else if (c == d_true || c == d_false)
+      {
+        // short-circuiting
+        if ((k == AND && c == d_false) || (k == OR && c == d_true))
+        {
+          ret = c;
+          ret_set = true;
+          reqHasTerm = false;
+          break;
+        }
+        else if (k == ITE && i == 0)
+        {
+          ret = evaluateTerm2(n[c == d_true ? 1 : 2],
+                              visited,
+                              subs,
+                              subsRep,
+                              useEntailmentTests,
+                              reqHasTerm);
+          ret_set = true;
+          reqHasTerm = false;
+          break;
+        }
+      }
+      Trace("term-db-eval") << "  child " << i << " : " << c << std::endl;
+      args.push_back(c);
+    }
+    if (!ret_set)
+    {
+      // get the (indexed) operator of n, if it exists
+      TNode f = d_tdb.getMatchOperator(n);
+      // if it is an indexed term, return the congruent term
+      if (!f.isNull())
+      {
+        // if f is congruent to a term indexed by this class
+        TNode nn = d_tdb.getCongruentTerm(f, args);
+        Trace("term-db-eval") << "  got congruent term " << nn
+                              << " from DB for " << n << std::endl;
+        if (!nn.isNull())
+        {
+          ret = d_qstate.getRepresentative(nn);
+          Trace("term-db-eval") << "return rep" << std::endl;
+          ret_set = true;
+          reqHasTerm = false;
+          Assert(!ret.isNull());
+        }
+      }
+      if (!ret_set)
+      {
+        Trace("term-db-eval") << "return rewrite" << std::endl;
+        // a theory symbol or a new UF term
+        if (n.getMetaKind() == metakind::PARAMETERIZED)
+        {
+          args.insert(args.begin(), n.getOperator());
+        }
+        ret = NodeManager::currentNM()->mkNode(n.getKind(), args);
+        ret = rewrite(ret);
+        if (ret.getKind() == EQUAL)
+        {
+          if (d_qstate.areDisequal(ret[0], ret[1]))
+          {
+            ret = d_false;
+          }
+        }
+        if (useEntailmentTests)
+        {
+          if (ret.getKind() == EQUAL || ret.getKind() == GEQ)
+          {
+            Valuation& val = d_qstate.getValuation();
+            for (unsigned j = 0; j < 2; j++)
+            {
+              std::pair<bool, Node> et = val.entailmentCheck(
+                  options::TheoryOfMode::THEORY_OF_TYPE_BASED,
+                  j == 0 ? ret : ret.negate());
+              if (et.first)
+              {
+                ret = j == 0 ? d_true : d_false;
+                break;
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+  // must have the term
+  if (reqHasTerm && !ret.isNull())
+  {
+    Kind rk = ret.getKind();
+    if (rk != OR && rk != AND && rk != EQUAL && rk != ITE && rk != NOT
+        && rk != FORALL)
+    {
+      if (!d_qstate.hasTerm(ret))
+      {
+        ret = Node::null();
+      }
+    }
+  }
+  Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret
+                        << ", reqHasTerm = " << reqHasTerm << std::endl;
+  visited[n] = ret;
+  return ret;
+}
+
+TNode EntailmentCheck::getEntailedTerm2(TNode n,
+                                        std::map<TNode, TNode>& subs,
+                                        bool subsRep)
+{
+  Trace("term-db-entail") << "get entailed term : " << n << std::endl;
+  if (d_qstate.hasTerm(n))
+  {
+    Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
+    return n;
+  }
+  else if (n.getKind() == BOUND_VARIABLE)
+  {
+    std::map<TNode, TNode>::iterator it = subs.find(n);
+    if (it != subs.end())
+    {
+      Trace("term-db-entail")
+          << "...substitution is : " << it->second << std::endl;
+      if (subsRep)
+      {
+        Assert(d_qstate.hasTerm(it->second));
+        Assert(d_qstate.getRepresentative(it->second) == it->second);
+        return it->second;
+      }
+      return getEntailedTerm2(it->second, subs, subsRep);
+    }
+  }
+  else if (n.getKind() == ITE)
+  {
+    for (uint32_t i = 0; i < 2; i++)
+    {
+      if (isEntailed2(n[0], subs, subsRep, i == 0))
+      {
+        return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep);
+      }
+    }
+  }
+  else
+  {
+    if (n.hasOperator())
+    {
+      TNode f = d_tdb.getMatchOperator(n);
+      if (!f.isNull())
+      {
+        std::vector<TNode> args;
+        for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+        {
+          TNode c = getEntailedTerm2(n[i], subs, subsRep);
+          if (c.isNull())
+          {
+            return TNode::null();
+          }
+          c = d_qstate.getRepresentative(c);
+          Trace("term-db-entail") << "  child " << i << " : " << c << std::endl;
+          args.push_back(c);
+        }
+        TNode nn = d_tdb.getCongruentTerm(f, args);
+        Trace("term-db-entail")
+            << "  got congruent term " << nn << " for " << n << std::endl;
+        return nn;
+      }
+    }
+  }
+  return TNode::null();
+}
+
+Node EntailmentCheck::evaluateTerm(TNode n,
+                                   std::map<TNode, TNode>& subs,
+                                   bool subsRep,
+                                   bool useEntailmentTests,
+                                   bool reqHasTerm)
+{
+  std::map<TNode, Node> visited;
+  return evaluateTerm2(
+      n, visited, subs, subsRep, useEntailmentTests, reqHasTerm);
+}
+
+Node EntailmentCheck::evaluateTerm(TNode n,
+                                   bool useEntailmentTests,
+                                   bool reqHasTerm)
+{
+  std::map<TNode, Node> visited;
+  std::map<TNode, TNode> subs;
+  return evaluateTerm2(n, visited, subs, false, useEntailmentTests, reqHasTerm);
+}
+
+TNode EntailmentCheck::getEntailedTerm(TNode n,
+                                       std::map<TNode, TNode>& subs,
+                                       bool subsRep)
+{
+  return getEntailedTerm2(n, subs, subsRep);
+}
+
+TNode EntailmentCheck::getEntailedTerm(TNode n)
+{
+  std::map<TNode, TNode> subs;
+  return getEntailedTerm2(n, subs, false);
+}
+
+bool EntailmentCheck::isEntailed2(TNode n,
+                                  std::map<TNode, TNode>& subs,
+                                  bool subsRep,
+                                  bool pol)
+{
+  Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol
+                          << std::endl;
+  Assert(n.getType().isBoolean());
+  if (n.getKind() == EQUAL && !n[0].getType().isBoolean())
+  {
+    TNode n1 = getEntailedTerm2(n[0], subs, subsRep);
+    if (!n1.isNull())
+    {
+      TNode n2 = getEntailedTerm2(n[1], subs, subsRep);
+      if (!n2.isNull())
+      {
+        if (n1 == n2)
+        {
+          return pol;
+        }
+        else
+        {
+          Assert(d_qstate.hasTerm(n1));
+          Assert(d_qstate.hasTerm(n2));
+          if (pol)
+          {
+            return d_qstate.areEqual(n1, n2);
+          }
+          else
+          {
+            return d_qstate.areDisequal(n1, n2);
+          }
+        }
+      }
+    }
+  }
+  else if (n.getKind() == NOT)
+  {
+    return isEntailed2(n[0], subs, subsRep, !pol);
+  }
+  else if (n.getKind() == OR || n.getKind() == AND)
+  {
+    bool simPol = (pol && n.getKind() == OR) || (!pol && n.getKind() == AND);
+    for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+    {
+      if (isEntailed2(n[i], subs, subsRep, pol))
+      {
+        if (simPol)
+        {
+          return true;
+        }
+      }
+      else
+      {
+        if (!simPol)
+        {
+          return false;
+        }
+      }
+    }
+    return !simPol;
+    // Boolean equality here
+  }
+  else if (n.getKind() == EQUAL || n.getKind() == ITE)
+  {
+    for (size_t i = 0; i < 2; i++)
+    {
+      if (isEntailed2(n[0], subs, subsRep, i == 0))
+      {
+        size_t ch = (n.getKind() == EQUAL || i == 0) ? 1 : 2;
+        bool reqPol = (n.getKind() == ITE || i == 0) ? pol : !pol;
+        return isEntailed2(n[ch], subs, subsRep, reqPol);
+      }
+    }
+  }
+  else if (n.getKind() == APPLY_UF)
+  {
+    TNode n1 = getEntailedTerm2(n, subs, subsRep);
+    if (!n1.isNull())
+    {
+      Assert(d_qstate.hasTerm(n1));
+      if (n1 == d_true)
+      {
+        return pol;
+      }
+      else if (n1 == d_false)
+      {
+        return !pol;
+      }
+      else
+      {
+        return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false);
+      }
+    }
+  }
+  else if (n.getKind() == FORALL && !pol)
+  {
+    return isEntailed2(n[1], subs, subsRep, pol);
+  }
+  return false;
+}
+
+bool EntailmentCheck::isEntailed(TNode n, bool pol)
+{
+  std::map<TNode, TNode> subs;
+  return isEntailed2(n, subs, false, pol);
+}
+
+bool EntailmentCheck::isEntailed(TNode n,
+                                 std::map<TNode, TNode>& subs,
+                                 bool subsRep,
+                                 bool pol)
+{
+  return isEntailed2(n, subs, subsRep, pol);
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/entailment_check.h b/src/theory/quantifiers/entailment_check.h
new file mode 100644
index 000000000..ecf74fe85
--- /dev/null
+++ b/src/theory/quantifiers/entailment_check.h
@@ -0,0 +1,156 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Entailment check class
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H
+#define CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H
+
+#include <map>
+#include <vector>
+
+#include "expr/node.h"
+#include "smt/env_obj.h"
+
+namespace cvc5 {
+namespace theory {
+namespace quantifiers {
+
+class QuantifiersState;
+class TermDb;
+
+/**
+ * Entailment check utility, which determines whether formulas are entailed
+ * in the current context. The main focus of this class is on UF formulas.
+ * It works by looking at the term argument trie data structures in term
+ * database. For details, see e.g. Section 4.1 of Reynolds et al TACAS 2018.
+ */
+class EntailmentCheck : protected EnvObj
+{
+ public:
+  EntailmentCheck(Env& env, QuantifiersState& qs, TermDb& tdb);
+  ~EntailmentCheck();
+  /** evaluate term
+   *
+   * Returns a term n' such that n * subs = n' is entailed based on the current
+   * set of equalities, where ( n * subs ) is term n under the substitution
+   * subs.
+   *
+   * This function may generate new terms. In particular, we typically rewrite
+   * subterms of n of maximal size (in terms of the AST) to terms that exist
+   * in the equality engine.
+   *
+   * useEntailmentTests is whether to call the theory engine's entailmentTest
+   * on literals n for which this call fails to find a term n' that is
+   * equivalent to n, for increased precision. This is not frequently used.
+   *
+   * If reqHasTerm, then we require that the returned term is a Boolean
+   * combination of terms that exist in the equality engine used by this call.
+   * If no such term is constructable, this call returns null. The motivation
+   * for setting this to true is to "fail fast" if we require the return value
+   * of this function to only involve existing terms. This is used e.g. in
+   * the "propagating instances" portion of conflict-based instantiation
+   * (quant_conflict_find.h).
+   *
+   * @param n The term under consideration
+   * @param subs The substitution under consideration
+   * @param subsRep Whether the range of subs are representatives in the current
+   * equality engine
+   * @param useEntailmentTests Whether to use entailment tests to show
+   * n * subs is equivalent to true/false.
+   * @param reqHasTerm Whether we require the returned term to be a Boolean
+   * combination of terms known to the current equality engine
+   * @return the term n * subs evaluates to
+   */
+  Node evaluateTerm(TNode n,
+                    std::map<TNode, TNode>& subs,
+                    bool subsRep,
+                    bool useEntailmentTests = false,
+                    bool reqHasTerm = false);
+  /** Same as above, without a substitution */
+  Node evaluateTerm(TNode n,
+                    bool useEntailmentTests = false,
+                    bool reqHasTerm = false);
+  /** get entailed term
+   *
+   * If possible, returns a term n' such that:
+   * (1) n' exists in the current equality engine (as specified by the state),
+   * (2) n = n' is entailed in the current context.
+   * It returns null if no such term can be found.
+   * Wrt evaluateTerm, this version does not construct new terms, and
+   * thus is less aggressive.
+   */
+  TNode getEntailedTerm(TNode n);
+  /** get entailed term
+   *
+   * If possible, returns a term n' such that:
+   * (1) n' exists in the current equality engine (as specified by the state),
+   * (2) n * subs = n' is entailed in the current context, where * denotes
+   * substitution application.
+   * It returns null if no such term can be found.
+   * subsRep is whether the substitution maps to terms that are representatives
+   * according to the quantifiers state.
+   * Wrt evaluateTerm, this version does not construct new terms, and
+   * thus is less aggressive.
+   */
+  TNode getEntailedTerm(TNode n, std::map<TNode, TNode>& subs, bool subsRep);
+  /** is entailed
+   * Checks whether the current context entails n with polarity pol, based on
+   * the equality information in the quantifiers state. Returns true if the
+   * entailment can be successfully shown.
+   */
+  bool isEntailed(TNode n, bool pol);
+  /** is entailed
+   *
+   * Checks whether the current context entails ( n * subs ) with polarity pol,
+   * based on the equality information in the quantifiers state,
+   * where * denotes substitution application.
+   * subsRep is whether the substitution maps to terms that are representatives
+   * according to in the quantifiers state.
+   */
+  bool isEntailed(TNode n,
+                  std::map<TNode, TNode>& subs,
+                  bool subsRep,
+                  bool pol);
+
+ protected:
+  /** helper for evaluate term */
+  Node evaluateTerm2(TNode n,
+                     std::map<TNode, Node>& visited,
+                     std::map<TNode, TNode>& subs,
+                     bool subsRep,
+                     bool useEntailmentTests,
+                     bool reqHasTerm);
+  /** helper for get entailed term */
+  TNode getEntailedTerm2(TNode n, std::map<TNode, TNode>& subs, bool subsRep);
+  /** helper for is entailed */
+  bool isEntailed2(TNode n,
+                   std::map<TNode, TNode>& subs,
+                   bool subsRep,
+                   bool pol);
+  /** The quantifiers state object */
+  QuantifiersState& d_qstate;
+  /** Reference to the term database */
+  TermDb& d_tdb;
+  /** boolean terms */
+  Node d_true;
+  Node d_false;
+}; /* class EntailmentCheck */
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace cvc5
+
+#endif /* CVC5__THEORY__QUANTIFIERS__ENTAILMENT_CHECK_H */
diff --git a/src/theory/quantifiers/fmf/full_model_check.cpp b/src/theory/quantifiers/fmf/full_model_check.cpp
index 7c1d36ce8..94351274a 100644
--- a/src/theory/quantifiers/fmf/full_model_check.cpp
+++ b/src/theory/quantifiers/fmf/full_model_check.cpp
@@ -951,10 +951,15 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
     Node r = n;
     if( !n.isConst() ){
       TypeNode tn = n.getType();
-      if( !fm->hasTerm(n) && tn.isFirstClass() ){
-        r = getSomeDomainElement(fm, tn );
+      if (!fm->hasTerm(n) && tn.isFirstClass())
+      {
+        // if the term is unknown, we do not assume any value for it
+        r = Node::null();
+      }
+      else
+      {
+        r = fm->getRepresentative(r);
       }
-      r = fm->getRepresentative( r );
     }
     Trace("fmc-debug") << "Add constant entry..." << std::endl;
     d.addEntry(fm, mkCondDefault(fm, f), r);
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index f756fcfd1..be04f9404 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -25,6 +25,7 @@
 #include "smt/logic_exception.h"
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/cegqi/inst_strategy_cegqi.h"
+#include "theory/quantifiers/entailment_check.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_preprocess.h"
@@ -183,7 +184,7 @@ bool Instantiate::addInstantiation(Node q,
 #endif
   }
 
-  TermDb* tdb = d_treg.getTermDatabase();
+  EntailmentCheck* ec = d_treg.getEntailmentCheck();
   // Note we check for entailment before checking for term vector duplication.
   // Although checking for term vector duplication is a faster check, it is
   // included automatically with recordInstantiationInternal, hence we prefer
@@ -206,7 +207,7 @@ bool Instantiate::addInstantiation(Node q,
     {
       subs[q[0][i]] = terms[i];
     }
-    if (tdb->isEntailed(q[1], subs, false, true))
+    if (ec->isEntailed(q[1], subs, false, true))
     {
       Trace("inst-add-debug") << " --> Currently entailed." << std::endl;
       ++(d_statistics.d_inst_duplicate_ent);
@@ -217,6 +218,7 @@ bool Instantiate::addInstantiation(Node q,
   // check based on instantiation level
   if (options::instMaxLevel() != -1)
   {
+    TermDb* tdb = d_treg.getTermDatabase();
     for (Node& t : terms)
     {
       if (!tdb->isTermEligibleForInstantiation(t, q))
@@ -409,7 +411,7 @@ bool Instantiate::addInstantiationExpFail(Node q,
     // will never succeed with 1 variable
     return false;
   }
-  TermDb* tdb = d_treg.getTermDatabase();
+  EntailmentCheck* echeck = d_treg.getEntailmentCheck();
   Trace("inst-exp-fail") << "Explain inst failure..." << terms << std::endl;
   // set up information for below
   std::vector<Node>& vars = d_qreg.d_vars[q];
@@ -445,7 +447,7 @@ bool Instantiate::addInstantiationExpFail(Node q,
     if (options::instNoEntail())
     {
       Trace("inst-exp-fail") << "  check entailment" << std::endl;
-      success = tdb->isEntailed(q[1], subs, false, true);
+      success = echeck->isEntailed(q[1], subs, false, true);
       Trace("inst-exp-fail") << "  entailed: " << success << std::endl;
     }
     // check whether the instantiation rewrites to the same thing
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 361adfd54..323398879 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -52,12 +52,6 @@ QuantInfo::~QuantInfo() {
   d_var_mg.clear();
 }
 
-QuantifiersInferenceManager& QuantInfo::getInferenceManager()
-{
-  Assert(d_parent != nullptr);
-  return d_parent->getInferenceManager();
-}
-
 void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) {
   d_parent = p;
   d_q = q;
@@ -577,30 +571,33 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
 {
   if( options::qcfEagerTest() ){
     //check whether the instantiation evaluates as expected
+    EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck();
+    std::map<TNode, TNode> subs;
+    for (size_t i = 0, tsize = terms.size(); i < tsize; i++)
+    {
+      Trace("qcf-instance-check") << "  " << terms[i] << std::endl;
+      subs[d_q[0][i]] = terms[i];
+    }
+    for (size_t i = 0, evsize = d_extra_var.size(); i < evsize; i++)
+    {
+      Node n = getCurrentExpValue(d_extra_var[i]);
+      Trace("qcf-instance-check")
+          << "  " << d_extra_var[i] << " -> " << n << std::endl;
+      subs[d_extra_var[i]] = n;
+    }
     if (p->atConflictEffort()) {
       Trace("qcf-instance-check") << "Possible conflict instance for " << d_q << " : " << std::endl;
-      std::map< TNode, TNode > subs;
-      for( unsigned i=0; i<terms.size(); i++ ){
-        Trace("qcf-instance-check") << "  " << terms[i] << std::endl;
-        subs[d_q[0][i]] = terms[i];
-      }
-      TermDb* tdb = p->getTermDatabase();
-      for( unsigned i=0; i<d_extra_var.size(); i++ ){
-        Node n = getCurrentExpValue( d_extra_var[i] );
-        Trace("qcf-instance-check") << "  " << d_extra_var[i] << " -> " << n << std::endl;
-        subs[d_extra_var[i]] = n;
-      }
-      if (!tdb->isEntailed(d_q[1], subs, false, false))
+      if (!echeck->isEntailed(d_q[1], subs, false, false))
       {
         Trace("qcf-instance-check") << "...not entailed to be false." << std::endl;
         return true;
       }
     }else{
-      Node inst =
-          getInferenceManager().getInstantiate()->getInstantiation(d_q, terms);
-      inst = Rewriter::rewrite(inst);
-      Node inst_eval = p->getTermDatabase()->evaluateTerm(
-          inst, options::qcfTConstraint(), true);
+      // see if the body of the quantified formula evaluates to a Boolean
+      // combination of known terms under the current substitution. We use
+      // the helper method evaluateTerm from the entailment check utility.
+      Node inst_eval = echeck->evaluateTerm(
+          d_q[1], subs, false, options::qcfTConstraint(), true);
       if( Trace.isOn("qcf-instance-check") ){
         Trace("qcf-instance-check") << "Possible propagating instance for " << d_q << " : " << std::endl;
         for( unsigned i=0; i<terms.size(); i++ ){
@@ -608,6 +605,10 @@ bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
         }
         Trace("qcf-instance-check") << "...evaluates to " << inst_eval << std::endl;
       }
+      // If it is the case that instantiation can be rewritten to a Boolean
+      // combination of terms that exist in the current context, then inst_eval
+      // is non-null. Moreover, we insist that inst_eval is not true, or else
+      // the instantiation is trivially entailed and hence is spurious.
       if (inst_eval.isNull()
           || (inst_eval.isConst() && inst_eval.getConst<bool>()))
       {
@@ -1219,11 +1220,11 @@ bool MatchGen::reset_round(QuantConflictFind* p)
     //  d_ground_eval[0] = p->d_false;
     //}
     // modified
-    TermDb* tdb = p->getTermDatabase();
+    EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck();
     QuantifiersState& qs = p->getState();
     for (unsigned i = 0; i < 2; i++)
     {
-      if (tdb->isEntailed(d_n, i == 0))
+      if (echeck->isEntailed(d_n, i == 0))
       {
         d_ground_eval[0] = i==0 ? p->d_true : p->d_false;
       }
@@ -1233,13 +1234,13 @@ bool MatchGen::reset_round(QuantConflictFind* p)
       }
     }
   }else if( d_type==typ_eq ){
-    TermDb* tdb = p->getTermDatabase();
+    EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck();
     QuantifiersState& qs = p->getState();
     for (unsigned i = 0, size = d_n.getNumChildren(); i < size; i++)
     {
       if (!expr::hasBoundVar(d_n[i]))
       {
-        TNode t = tdb->getEntailedTerm(d_n[i]);
+        TNode t = echeck->getEntailedTerm(d_n[i]);
         if (qs.isInConflict())
         {
           return false;
@@ -1289,13 +1290,9 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) {
     TNode n = qi->getCurrentValue( d_n );
     int vn = qi->getCurrentRepVar( qi->getVarNum( n ) );
     if( vn==-1 ){
-      //evaluate the value, see if it is compatible
-      //int e = p->evaluate( n );
-      //if( ( e==1 && d_tgt ) || ( e==0 && !d_tgt ) ){
-      //  d_child_counter = 0;
-      //}
-      //modified 
-      if( p->getTermDatabase()->isEntailed( n, d_tgt ) ){ 
+      EntailmentCheck* echeck = p->getTermRegistry().getEntailmentCheck();
+      if (echeck->isEntailed(n, d_tgt))
+      {
         d_child_counter = 0;
       }
     }else{
@@ -2168,8 +2165,8 @@ void QuantConflictFind::checkQuantifiedFormula(Node q,
         Node inst = qinst->getInstantiation(q, terms);
         Debug("qcf-check-inst")
             << "Check instantiation " << inst << "..." << std::endl;
-        Assert(!getTermDatabase()->isEntailed(inst, true));
-        Assert(getTermDatabase()->isEntailed(inst, false)
+        Assert(!getTermRegistry().getEntailmentCheck()->isEntailed(inst, true));
+        Assert(getTermRegistry().getEntailmentCheck()->isEntailed(inst, false)
                || d_effort > EFFORT_CONFLICT);
       }
       // Process the lemma: either add an instantiation or specific lemmas
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index 927a74ff2..d14e281fb 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -132,8 +132,6 @@ public:
 public:
   QuantInfo();
   ~QuantInfo();
-  /** Get quantifiers inference manager */
-  QuantifiersInferenceManager& getInferenceManager();
   std::vector< TNode > d_vars;
   std::vector< TypeNode > d_var_types;
   std::map< TNode, int > d_var_num;
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 7c7c7aade..52e90e26e 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/quantifiers/quantifiers_rewriter.h"
 
+#include "expr/ascription_type.h"
 #include "expr/bound_var_manager.h"
 #include "expr/dtype.h"
 #include "expr/dtype_cons.h"
@@ -895,12 +896,25 @@ bool QuantifiersRewriter::getVarElimLit(Node body,
       const DType& dt = datatypes::utils::datatypeOf(tester);
       const DTypeConstructor& c = dt[index];
       std::vector<Node> newChildren;
-      newChildren.push_back(c.getConstructor());
+      Node cons = c.getConstructor();
+      TypeNode tspec;
+      // take into account if parametric
+      if (dt.isParametric())
+      {
+        tspec = c.getSpecializedConstructorType(lit[0].getType());
+        cons = nm->mkNode(
+            APPLY_TYPE_ASCRIPTION, nm->mkConst(AscriptionType(tspec)), cons);
+      }
+      else
+      {
+        tspec = cons.getType();
+      }
+      newChildren.push_back(cons);
       std::vector<Node> newVars;
       BoundVarManager* bvm = nm->getBoundVarManager();
-      for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
+      for (size_t j = 0, nargs = c.getNumArgs(); j < nargs; j++)
       {
-        TypeNode tn = c[j].getRangeType();
+        TypeNode tn = tspec[j];
         Node rn = nm->mkConst(Rational(j));
         Node cacheVal = BoundVarManager::getCacheValue(body, lit, rn);
         Node v = bvm->mkBoundVar<QRewDtExpandAttribute>(cacheVal, tn);
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index c8e14e4bd..fdc0b28e0 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -39,6 +39,7 @@ Cegis::Cegis(Env& env,
              SynthConjecture* p)
     : SygusModule(env, qs, qim, tds, p),
       d_eval_unfold(tds->getEvalUnfold()),
+      d_cexClosedEnum(false),
       d_cegis_sampler(env),
       d_usingSymCons(false)
 {
@@ -47,11 +48,18 @@ Cegis::Cegis(Env& env,
 bool Cegis::initialize(Node conj, Node n, const std::vector<Node>& candidates)
 {
   d_base_body = n;
+  d_cexClosedEnum = true;
   if (d_base_body.getKind() == NOT && d_base_body[0].getKind() == FORALL)
   {
     for (const Node& v : d_base_body[0][0])
     {
       d_base_vars.push_back(v);
+      if (!v.getType().isClosedEnumerable())
+      {
+        // not closed enumerable, refinement lemmas cannot be sent to the
+        // quantifier-free datatype solver
+        d_cexClosedEnum = false;
+      }
     }
     d_base_body = d_base_body[0][1];
   }
@@ -467,14 +475,18 @@ void Cegis::addRefinementLemmaConjunct(unsigned wcounter,
 void Cegis::registerRefinementLemma(const std::vector<Node>& vars, Node lem)
 {
   addRefinementLemma(lem);
-  // Make the refinement lemma and add it to lems.
-  // This lemma is guarded by the parent's guard, which has the semantics
-  // "this conjecture has a solution", hence this lemma states:
-  // if the parent conjecture has a solution, it satisfies the specification
-  // for the given concrete point.
-  Node rlem =
-      NodeManager::currentNM()->mkNode(OR, d_parent->getGuard().negate(), lem);
-  d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE);
+  // must be closed enumerable
+  if (d_cexClosedEnum && options().quantifiers.sygusEvalUnfold)
+  {
+    // Make the refinement lemma and add it to lems.
+    // This lemma is guarded by the parent's guard, which has the semantics
+    // "this conjecture has a solution", hence this lemma states:
+    // if the parent conjecture has a solution, it satisfies the specification
+    // for the given concrete point.
+    Node rlem = NodeManager::currentNM()->mkNode(
+        OR, d_parent->getGuard().negate(), lem);
+    d_qim.addPendingLemma(rlem, InferenceId::QUANTIFIERS_SYGUS_CEGIS_REFINE);
+  }
 }
 
 bool Cegis::usingRepairConst() { return true; }
diff --git a/src/theory/quantifiers/sygus/cegis.h b/src/theory/quantifiers/sygus/cegis.h
index 8e0fffdd1..8d1f0a1b2 100644
--- a/src/theory/quantifiers/sygus/cegis.h
+++ b/src/theory/quantifiers/sygus/cegis.h
@@ -119,6 +119,13 @@ class Cegis : public SygusModule
   std::vector<Node> d_rl_vals;
   /** all variables appearing in refinement lemmas */
   std::unordered_set<Node> d_refinement_lemma_vars;
+  /**
+   * Are the counterexamples we are handling in this class of only closed
+   * enumerable types (see TypeNode::isClosedEnumerable). If this is false,
+   * then CEGIS refinement lemmas can contain terms that are unhandled by
+   * theory solvers, e.g. uninterpreted constants.
+   */
+  bool d_cexClosedEnum;
 
   /** adds lem as a refinement lemma */
   void addRefinementLemma(Node lem);
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 43c958ff9..9b4cfb9e1 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -20,6 +20,7 @@
 
 #include "expr/ascription_type.h"
 #include "expr/dtype_cons.h"
+#include "expr/node_algorithm.h"
 #include "options/quantifiers_options.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/datatypes/sygus_datatype_utils.h"
@@ -420,6 +421,8 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
   {
     // generate constant array over the first element of the constituent type
     Node c = type.mkGroundTerm();
+    // note that c should never contain an uninterpreted constant
+    Assert(!expr::hasSubtermKind(UNINTERPRETED_CONSTANT, c));
     ops.push_back(c);
   }
   else if (type.isRoundingMode())
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index b1537a390..573cab7bf 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -451,366 +451,6 @@ bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
   }
 }
 
-Node TermDb::evaluateTerm2(TNode n,
-                           std::map<TNode, Node>& visited,
-                           std::vector<Node>& exp,
-                           bool useEntailmentTests,
-                           bool computeExp,
-                           bool reqHasTerm)
-{
-  std::map< TNode, Node >::iterator itv = visited.find( n );
-  if( itv != visited.end() ){
-    return itv->second;
-  }
-  size_t prevSize = exp.size();
-  Trace("term-db-eval") << "evaluate term : " << n << std::endl;
-  Node ret = n;
-  if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){
-    //do nothing
-  }
-  else if (d_qstate.hasTerm(n))
-  {
-    Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
-    ret = d_qstate.getRepresentative(n);
-    if (computeExp)
-    {
-      if (n != ret)
-      {
-        exp.push_back(n.eqNode(ret));
-      }
-    }
-    reqHasTerm = false;
-  }
-  else if (n.hasOperator())
-  {
-    std::vector<TNode> args;
-    bool ret_set = false;
-    Kind k = n.getKind();
-    std::vector<Node> tempExp;
-    for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
-    {
-      TNode c = evaluateTerm2(n[i],
-                              visited,
-                              tempExp,
-                              useEntailmentTests,
-                              computeExp,
-                              reqHasTerm);
-      if (c.isNull())
-      {
-        ret = Node::null();
-        ret_set = true;
-        break;
-      }
-      else if (c == d_true || c == d_false)
-      {
-        // short-circuiting
-        if ((k == AND && c == d_false) || (k == OR && c == d_true))
-        {
-          ret = c;
-          ret_set = true;
-          reqHasTerm = false;
-          break;
-        }
-        else if (k == ITE && i == 0)
-        {
-          ret = evaluateTerm2(n[c == d_true ? 1 : 2],
-                              visited,
-                              tempExp,
-                              useEntailmentTests,
-                              computeExp,
-                              reqHasTerm);
-          ret_set = true;
-          reqHasTerm = false;
-          break;
-        }
-      }
-      if (computeExp)
-      {
-        exp.insert(exp.end(), tempExp.begin(), tempExp.end());
-      }
-      Trace("term-db-eval") << "  child " << i << " : " << c << std::endl;
-      args.push_back(c);
-    }
-    if (ret_set)
-    {
-      // if we short circuited
-      if (computeExp)
-      {
-        exp.clear();
-        exp.insert(exp.end(), tempExp.begin(), tempExp.end());
-      }
-    }
-    else
-    {
-      // get the (indexed) operator of n, if it exists
-      TNode f = getMatchOperator(n);
-      // if it is an indexed term, return the congruent term
-      if (!f.isNull())
-      {
-        // if f is congruent to a term indexed by this class
-        TNode nn = getCongruentTerm(f, args);
-        Trace("term-db-eval") << "  got congruent term " << nn
-                              << " from DB for " << n << std::endl;
-        if (!nn.isNull())
-        {
-          if (computeExp)
-          {
-            Assert(nn.getNumChildren() == n.getNumChildren());
-            for (unsigned i = 0, nchild = nn.getNumChildren(); i < nchild; i++)
-            {
-              if (nn[i] != n[i])
-              {
-                exp.push_back(nn[i].eqNode(n[i]));
-              }
-            }
-          }
-          ret = d_qstate.getRepresentative(nn);
-          Trace("term-db-eval") << "return rep" << std::endl;
-          ret_set = true;
-          reqHasTerm = false;
-          Assert(!ret.isNull());
-          if (computeExp)
-          {
-            if (n != ret)
-            {
-              exp.push_back(nn.eqNode(ret));
-            }
-          }
-        }
-      }
-      if( !ret_set ){
-        Trace("term-db-eval") << "return rewrite" << std::endl;
-        // a theory symbol or a new UF term
-        if (n.getMetaKind() == metakind::PARAMETERIZED)
-        {
-          args.insert(args.begin(), n.getOperator());
-        }
-        ret = NodeManager::currentNM()->mkNode(n.getKind(), args);
-        ret = rewrite(ret);
-        if (ret.getKind() == EQUAL)
-        {
-          if (d_qstate.areDisequal(ret[0], ret[1]))
-          {
-            ret = d_false;
-          }
-        }
-        if (useEntailmentTests)
-        {
-          if (ret.getKind() == EQUAL || ret.getKind() == GEQ)
-          {
-            Valuation& val = d_qstate.getValuation();
-            for (unsigned j = 0; j < 2; j++)
-            {
-              std::pair<bool, Node> et = val.entailmentCheck(
-                  options::TheoryOfMode::THEORY_OF_TYPE_BASED,
-                  j == 0 ? ret : ret.negate());
-              if (et.first)
-              {
-                ret = j == 0 ? d_true : d_false;
-                if (computeExp)
-                {
-                  exp.push_back(et.second);
-                }
-                break;
-              }
-            }
-          }
-        }
-      }
-    }
-  }
-  // must have the term
-  if (reqHasTerm && !ret.isNull())
-  {
-    Kind k = ret.getKind();
-    if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT
-        && k != FORALL)
-    {
-      if (!d_qstate.hasTerm(ret))
-      {
-        ret = Node::null();
-      }
-    }
-  }
-  Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret
-                        << ", reqHasTerm = " << reqHasTerm << std::endl;
-  // clear the explanation if failed
-  if (computeExp && ret.isNull())
-  {
-    exp.resize(prevSize);
-  }
-  visited[n] = ret;
-  return ret;
-}
-
-TNode TermDb::getEntailedTerm2(TNode n,
-                               std::map<TNode, TNode>& subs,
-                               bool subsRep,
-                               bool hasSubs)
-{
-  Trace("term-db-entail") << "get entailed term : " << n << std::endl;
-  if (d_qstate.hasTerm(n))
-  {
-    Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
-    return n;
-  }else if( n.getKind()==BOUND_VARIABLE ){
-    if( hasSubs ){
-      std::map< TNode, TNode >::iterator it = subs.find( n );
-      if( it!=subs.end() ){
-        Trace("term-db-entail") << "...substitution is : " << it->second << std::endl;
-        if( subsRep ){
-          Assert(d_qstate.hasTerm(it->second));
-          Assert(d_qstate.getRepresentative(it->second) == it->second);
-          return it->second;
-        }
-        return getEntailedTerm2(it->second, subs, subsRep, hasSubs);
-      }
-    }
-  }else if( n.getKind()==ITE ){
-    for( unsigned i=0; i<2; i++ ){
-      if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0))
-      {
-        return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs);
-      }
-    }
-  }else{
-    if( n.hasOperator() ){
-      TNode f = getMatchOperator( n );
-      if( !f.isNull() ){
-        std::vector< TNode > args;
-        for( unsigned i=0; i<n.getNumChildren(); i++ ){
-          TNode c = getEntailedTerm2(n[i], subs, subsRep, hasSubs);
-          if( c.isNull() ){
-            return TNode::null();
-          }
-          c = d_qstate.getRepresentative(c);
-          Trace("term-db-entail") << "  child " << i << " : " << c << std::endl;
-          args.push_back( c );
-        }
-        TNode nn = getCongruentTerm(f, args);
-        Trace("term-db-entail") << "  got congruent term " << nn << " for " << n << std::endl;
-        return nn;
-      }
-    }
-  }
-  return TNode::null();
-}
-
-Node TermDb::evaluateTerm(TNode n,
-                          bool useEntailmentTests,
-                          bool reqHasTerm)
-{
-  std::map< TNode, Node > visited;
-  std::vector<Node> exp;
-  return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm);
-}
-
-Node TermDb::evaluateTerm(TNode n,
-                          std::vector<Node>& exp,
-                          bool useEntailmentTests,
-                          bool reqHasTerm)
-{
-  std::map<TNode, Node> visited;
-  return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm);
-}
-
-TNode TermDb::getEntailedTerm(TNode n,
-                              std::map<TNode, TNode>& subs,
-                              bool subsRep)
-{
-  return getEntailedTerm2(n, subs, subsRep, true);
-}
-
-TNode TermDb::getEntailedTerm(TNode n)
-{
-  std::map< TNode, TNode > subs;
-  return getEntailedTerm2(n, subs, false, false);
-}
-
-bool TermDb::isEntailed2(
-    TNode n, std::map<TNode, TNode>& subs, bool subsRep, bool hasSubs, bool pol)
-{
-  Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl;
-  Assert(n.getType().isBoolean());
-  if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
-    TNode n1 = getEntailedTerm2(n[0], subs, subsRep, hasSubs);
-    if( !n1.isNull() ){
-      TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs);
-      if( !n2.isNull() ){
-        if( n1==n2 ){
-          return pol;
-        }else{
-          Assert(d_qstate.hasTerm(n1));
-          Assert(d_qstate.hasTerm(n2));
-          if( pol ){
-            return d_qstate.areEqual(n1, n2);
-          }else{
-            return d_qstate.areDisequal(n1, n2);
-          }
-        }
-      }
-    }
-  }else if( n.getKind()==NOT ){
-    return isEntailed2(n[0], subs, subsRep, hasSubs, !pol);
-  }else if( n.getKind()==OR || n.getKind()==AND ){
-    bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if (isEntailed2(n[i], subs, subsRep, hasSubs, pol))
-      {
-        if( simPol ){
-          return true;
-        }
-      }else{
-        if( !simPol ){
-          return false;
-        }
-      }
-    }
-    return !simPol;
-  //Boolean equality here
-  }else if( n.getKind()==EQUAL || n.getKind()==ITE ){
-    for( unsigned i=0; i<2; i++ ){
-      if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0))
-      {
-        unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2;
-        bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
-        return isEntailed2(n[ch], subs, subsRep, hasSubs, reqPol);
-      }
-    }
-  }else if( n.getKind()==APPLY_UF ){
-    TNode n1 = getEntailedTerm2(n, subs, subsRep, hasSubs);
-    if( !n1.isNull() ){
-      Assert(d_qstate.hasTerm(n1));
-      if( n1==d_true ){
-        return pol;
-      }else if( n1==d_false ){
-        return !pol;
-      }else{
-        return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false);
-      }
-    }
-  }else if( n.getKind()==FORALL && !pol ){
-    return isEntailed2(n[1], subs, subsRep, hasSubs, pol);
-  }
-  return false;
-}
-
-bool TermDb::isEntailed(TNode n, bool pol)
-{
-  Assert(d_consistent_ee);
-  std::map< TNode, TNode > subs;
-  return isEntailed2(n, subs, false, false, pol);
-}
-
-bool TermDb::isEntailed(TNode n,
-                        std::map<TNode, TNode>& subs,
-                        bool subsRep,
-                        bool pol)
-{
-  Assert(d_consistent_ee);
-  return isEntailed2(n, subs, subsRep, true, pol);
-}
-
 bool TermDb::isTermActive( Node n ) {
   return d_inactive_map.find( n )==d_inactive_map.end(); 
   //return !n.getAttribute(NoMatchAttribute());
diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index af0b87bd8..0e5c7bc01 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -176,78 +176,6 @@ class TermDb : public QuantifiersUtil {
   *     equivalence class of r.
   */
   bool inRelevantDomain(TNode f, unsigned i, TNode r);
-  /** evaluate term
-   *
-   * Returns a term n' such that n = n' is entailed based on the equality
-   * information ee.  This function may generate new terms. In particular,
-   * we typically rewrite subterms of n of maximal size to terms that exist in
-   * the equality engine specified by ee.
-   *
-   * useEntailmentTests is whether to call the theory engine's entailmentTest
-   * on literals n for which this call fails to find a term n' that is
-   * equivalent to n, for increased precision. This is not frequently used.
-   *
-   * The vector exp stores the explanation for why n evaluates to that term,
-   * that is, if this call returns a non-null node n', then:
-   *   exp => n = n'
-   *
-   * If reqHasTerm, then we require that the returned term is a Boolean
-   * combination of terms that exist in the equality engine used by this call.
-   * If no such term is constructable, this call returns null. The motivation
-   * for setting this to true is to "fail fast" if we require the return value
-   * of this function to only involve existing terms. This is used e.g. in
-   * the "propagating instances" portion of conflict-based instantiation
-   * (quant_conflict_find.h).
-   */
-  Node evaluateTerm(TNode n,
-                    std::vector<Node>& exp,
-                    bool useEntailmentTests = false,
-                    bool reqHasTerm = false);
-  /** same as above, without exp */
-  Node evaluateTerm(TNode n,
-                    bool useEntailmentTests = false,
-                    bool reqHasTerm = false);
-  /** get entailed term
-   *
-   * If possible, returns a term n' such that:
-   * (1) n' exists in the current equality engine (as specified by the state),
-   * (2) n = n' is entailed in the current context.
-   * It returns null if no such term can be found.
-   * Wrt evaluateTerm, this version does not construct new terms, and
-   * thus is less aggressive.
-   */
-  TNode getEntailedTerm(TNode n);
-  /** get entailed term
-   *
-   * If possible, returns a term n' such that:
-   * (1) n' exists in the current equality engine (as specified by the state),
-   * (2) n * subs = n' is entailed in the current context, where * denotes
-   * substitution application.
-   * It returns null if no such term can be found.
-   * subsRep is whether the substitution maps to terms that are representatives
-   * according to the quantifiers state.
-   * Wrt evaluateTerm, this version does not construct new terms, and
-   * thus is less aggressive.
-   */
-  TNode getEntailedTerm(TNode n, std::map<TNode, TNode>& subs, bool subsRep);
-  /** is entailed
-   * Checks whether the current context entails n with polarity pol, based on
-   * the equality information in the quantifiers state. Returns true if the
-   * entailment can be successfully shown.
-   */
-  bool isEntailed(TNode n, bool pol);
-  /** is entailed
-   *
-   * Checks whether the current context entails ( n * subs ) with polarity pol,
-   * based on the equality information in the quantifiers state,
-   * where * denotes substitution application.
-   * subsRep is whether the substitution maps to terms that are representatives
-   * according to in the quantifiers state.
-   */
-  bool isEntailed(TNode n,
-                  std::map<TNode, TNode>& subs,
-                  bool subsRep,
-                  bool pol);
   /** is the term n active in the current context?
    *
   * By default, all terms are active. A term is inactive if:
@@ -355,24 +283,6 @@ class TermDb : public QuantifiersUtil {
   //----------------------------- end implementation-specific
   /** set has term */
   void setHasTerm( Node n );
-  /** helper for evaluate term */
-  Node evaluateTerm2(TNode n,
-                     std::map<TNode, Node>& visited,
-                     std::vector<Node>& exp,
-                     bool useEntailmentTests,
-                     bool computeExp,
-                     bool reqHasTerm);
-  /** helper for get entailed term */
-  TNode getEntailedTerm2(TNode n,
-                         std::map<TNode, TNode>& subs,
-                         bool subsRep,
-                         bool hasSubs);
-  /** helper for is entailed */
-  bool isEntailed2(TNode n,
-                   std::map<TNode, TNode>& subs,
-                   bool subsRep,
-                   bool hasSubs,
-                   bool pol);
   /** compute uf eqc terms :
   * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes
   */
diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index ab999ad9b..d11fb0b8d 100644
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -18,6 +18,7 @@
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
+#include "theory/quantifiers/entailment_check.h"
 #include "theory/quantifiers/first_order_model.h"
 #include "theory/quantifiers/fmf/first_order_model_fmc.h"
 #include "theory/quantifiers/ho_term_database.h"
@@ -39,6 +40,7 @@ TermRegistry::TermRegistry(Env& env,
       d_termPools(new TermPools(env, qs)),
       d_termDb(logicInfo().isHigherOrder() ? new HoTermDb(env, qs, qr)
                                            : new TermDb(env, qs, qr)),
+      d_echeck(new EntailmentCheck(env, qs, *d_termDb.get())),
       d_sygusTdb(nullptr),
       d_qmodel(nullptr)
 {
@@ -132,6 +134,11 @@ TermDbSygus* TermRegistry::getTermDatabaseSygus() const
   return d_sygusTdb.get();
 }
 
+EntailmentCheck* TermRegistry::getEntailmentCheck() const
+{
+  return d_echeck.get();
+}
+
 TermEnumeration* TermRegistry::getTermEnumeration() const
 {
   return d_termEnum.get();
diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h
index 175d450df..60a87a91f 100644
--- a/src/theory/quantifiers/term_registry.h
+++ b/src/theory/quantifiers/term_registry.h
@@ -23,6 +23,7 @@
 
 #include "context/cdhashset.h"
 #include "smt/env_obj.h"
+#include "theory/quantifiers/entailment_check.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_database.h"
 #include "theory/quantifiers/term_enumeration.h"
@@ -83,6 +84,8 @@ class TermRegistry : protected EnvObj
   TermDb* getTermDatabase() const;
   /** get term database sygus */
   TermDbSygus* getTermDatabaseSygus() const;
+  /** get entailment check utility */
+  EntailmentCheck* getEntailmentCheck() const;
   /** get term enumeration utility */
   TermEnumeration* getTermEnumeration() const;
   /** get the term pools utility */
@@ -103,6 +106,8 @@ class TermRegistry : protected EnvObj
   std::unique_ptr<TermPools> d_termPools;
   /** term database */
   std::unique_ptr<TermDb> d_termDb;
+  /** entailment check */
+  std::unique_ptr<EntailmentCheck> d_echeck;
   /** sygus term database */
   std::unique_ptr<TermDbSygus> d_sygusTdb;
   /** extended model object */
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 6cb3bf3ff..361d90dcd 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -32,13 +32,6 @@ using namespace std;
 namespace cvc5 {
 namespace theory {
 
-/** Attribute true for nodes that have been rewritten with proofs enabled */
-struct RewriteWithProofsAttributeId
-{
-};
-typedef expr::Attribute<RewriteWithProofsAttributeId, bool>
-    RewriteWithProofsAttribute;
-
 // Note that this function is a simplified version of Theory::theoryOf for
 // (type-based) theoryOfMode. We expand and simplify it here for the sake of
 // efficiency.
@@ -173,7 +166,6 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
                          Node node,
                          TConvProofGenerator* tcpg)
 {
-  RewriteWithProofsAttribute rpfa;
 #ifdef CVC5_ASSERTIONS
   bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
 
@@ -187,7 +179,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
 
   // Check if it's been cached already
   Node cached = getPostRewriteCache(theoryId, node);
-  if (!cached.isNull() && (tcpg == nullptr || node.getAttribute(rpfa)))
+  if (!cached.isNull() && (tcpg == nullptr || hasRewrittenWithProofs(node)))
   {
     return cached;
   }
@@ -217,7 +209,8 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
       cached = getPreRewriteCache(rewriteStackTop.getTheoryId(),
                                   rewriteStackTop.d_node);
       if (cached.isNull()
-          || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa)))
+          || (tcpg != nullptr
+              && !hasRewrittenWithProofs(rewriteStackTop.d_node)))
       {
         // Rewrite until fix-point is reached
         for(;;) {
@@ -256,7 +249,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
                                  rewriteStackTop.d_node);
     // If not, go through the children
     if (cached.isNull()
-        || (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa)))
+        || (tcpg != nullptr && !hasRewrittenWithProofs(rewriteStackTop.d_node)))
     {
       // The child we need to rewrite
       unsigned child = rewriteStackTop.d_nextChild++;
@@ -343,7 +336,7 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId,
       if (tcpg != nullptr)
       {
         // if proofs are enabled, mark that we've rewritten with proofs
-        rewriteStackTop.d_original.setAttribute(rpfa, true);
+        d_tpgNodes.insert(rewriteStackTop.d_original);
         if (!cached.isNull())
         {
           // We may have gotten a different node, due to non-determinism in
@@ -474,5 +467,10 @@ void Rewriter::clearCaches()
   clearCachesInternal();
 }
 
+bool Rewriter::hasRewrittenWithProofs(TNode n) const
+{
+  return d_tpgNodes.find(n) != d_tpgNodes.end();
+}
+
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/rewriter.h b/src/theory/rewriter.h
index f96062b61..d90af4a31 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -159,6 +159,11 @@ class Rewriter {
 
   void clearCachesInternal();
 
+  /**
+   * Has n been rewritten with proofs? This checks if n is in d_tpgNodes.
+   */
+  bool hasRewrittenWithProofs(TNode n) const;
+
   /** The resource manager, for tracking resource usage */
   ResourceManager* d_resourceManager;
 
@@ -167,6 +172,12 @@ class Rewriter {
 
   /** The proof generator */
   std::unique_ptr<TConvProofGenerator> d_tpg;
+  /**
+   * Nodes rewritten with proofs. Since d_tpg contains a reference to all
+   * nodes that have been rewritten with proofs, we can keep only a TNode
+   * here.
+   */
+  std::unordered_set<TNode> d_tpgNodes;
 #ifdef CVC5_ASSERTIONS
   std::unique_ptr<std::unordered_set<Node>> d_rewriteStack = nullptr;
 #endif /* CVC5_ASSERTIONS */
diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h
index eb839e1c0..35d06a510 100644
--- a/src/theory/sets/normal_form.h
+++ b/src/theory/sets/normal_form.h
@@ -58,7 +58,7 @@ class NormalForm {
   }
 
   /**
-   * Returns true if n is considered a to be a (canonical) constant set value.
+   * Returns true if n is considered to be a (canonical) constant set value.
    * A canonical set value is one whose AST is:
    *   (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
    * where c1 ... cn are constants and the node identifier of these constants
diff --git a/src/theory/strings/base_solver.cpp b/src/theory/strings/base_solver.cpp
index b675d2444..9396e3e87 100644
--- a/src/theory/strings/base_solver.cpp
+++ b/src/theory/strings/base_solver.cpp
@@ -17,6 +17,7 @@
 #include "theory/strings/base_solver.h"
 
 #include "expr/sequence.h"
+#include "options/quantifiers_options.h"
 #include "options/strings_options.h"
 #include "theory/rewriter.h"
 #include "theory/strings/theory_strings_utils.h"
@@ -539,8 +540,41 @@ void BaseSolver::checkCardinalityType(TypeNode tn,
       // infinite cardinality, we are fine
       return;
     }
-    // TODO (cvc4-projects #23): how to handle sequence for finite types?
-    return;
+    // we check the cardinality class of the type, assuming that FMF is
+    // disabled.
+    if (isCardinalityClassFinite(etn.getCardinalityClass(), false))
+    {
+      Cardinality c = etn.getCardinality();
+      bool smallCardinality = false;
+      if (!c.isLargeFinite())
+      {
+        Integer ci = c.getFiniteCardinality();
+        if (ci.fitsUnsignedInt())
+        {
+          smallCardinality = true;
+          typeCardSize = ci.toUnsignedInt();
+        }
+      }
+      if (!smallCardinality)
+      {
+        // if it is large finite, then there is no way we could have
+        // constructed that many terms in memory, hence there is nothing
+        // to do.
+        return;
+      }
+    }
+    else
+    {
+      Assert(options().quantifiers.finiteModelFind);
+      // we are in a case where the cardinality of the type is infinite
+      // if not FMF, and finite given the Env's option value for FMF. In this
+      // case, FMF must be true, and the cardinality is finite and dynamic
+      // (i.e. it depends on the model's finite interpretation for uninterpreted
+      // sorts). We do not know how to handle this case, we set incomplete.
+      // TODO (cvc4-projects #23): how to handle sequence for finite types?
+      d_im.setIncomplete(IncompleteId::SEQ_FINITE_DYNAMIC_CARDINALITY);
+      return;
+    }
   }
   // for each collection
   for (unsigned i = 0, csize = cols.size(); i < csize; ++i)
diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 34597c8be..5eba8663a 100644
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -59,6 +59,11 @@ void InferProofCons::notifyFact(const InferInfo& ii)
   d_lazyFactMap.insert(ii.d_conc, iic);
 }
 
+void InferProofCons::notifyLemma(const InferInfo& ii)
+{
+  d_lazyFactMap[ii.d_conc] = std::make_shared<InferInfo>(ii);
+}
+
 bool InferProofCons::addProofTo(CDProof* pf,
                                 Node conc,
                                 InferenceId infer,
diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h
index 110d231cf..02b266fd7 100644
--- a/src/theory/strings/infer_proof_cons.h
+++ b/src/theory/strings/infer_proof_cons.h
@@ -69,6 +69,11 @@ class InferProofCons : public ProofGenerator
    * only for facts that are explained.
    */
   void notifyFact(const InferInfo& ii);
+  /**
+   * Same as above, but always overwrites. This is used for lemmas and
+   * conflicts, which do not necessarily have unique conclusions.
+   */
+  void notifyLemma(const InferInfo& ii);
 
   /**
    * This returns the proof for fact. This is required for using this class as
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp
index 0e971fc54..1f531a97c 100644
--- a/src/theory/strings/inference_manager.cpp
+++ b/src/theory/strings/inference_manager.cpp
@@ -42,7 +42,8 @@ InferenceManager::InferenceManager(Env& env,
       d_termReg(tr),
       d_extt(e),
       d_statistics(statistics),
-      d_ipc(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr)
+      d_ipc(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr),
+      d_ipcl(pnm ? new InferProofCons(context(), pnm, d_statistics) : nullptr)
 {
   NodeManager* nm = NodeManager::currentNM();
   d_zero = nm->mkConst(Rational(0));
@@ -279,12 +280,12 @@ void InferenceManager::processConflict(const InferInfo& ii)
 {
   Assert(!d_state.isInConflict());
   // setup the fact to reproduce the proof in the call below
-  if (d_ipc != nullptr)
+  if (d_ipcl != nullptr)
   {
-    d_ipc->notifyFact(ii);
+    d_ipcl->notifyLemma(ii);
   }
   // make the trust node
-  TrustNode tconf = mkConflictExp(ii.d_premises, d_ipc.get());
+  TrustNode tconf = mkConflictExp(ii.d_premises, d_ipcl.get());
   Assert(tconf.getKind() == TrustNodeKind::CONFLICT);
   Trace("strings-assert") << "(assert (not " << tconf.getNode()
                           << ")) ; conflict " << ii.getId() << std::endl;
@@ -335,11 +336,11 @@ TrustNode InferenceManager::processLemma(InferInfo& ii, LemmaProperty& p)
   }
   // ensure that the proof generator is ready to explain the final conclusion
   // of the lemma (ii.d_conc).
-  if (d_ipc != nullptr)
+  if (d_ipcl != nullptr)
   {
-    d_ipc->notifyFact(ii);
+    d_ipcl->notifyLemma(ii);
   }
-  TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipc.get());
+  TrustNode tlem = mkLemmaExp(ii.d_conc, exp, noExplain, d_ipcl.get());
   Trace("strings-pending") << "Process pending lemma : " << tlem.getNode()
                            << std::endl;
 
diff --git a/src/theory/strings/inference_manager.h b/src/theory/strings/inference_manager.h
index 49f10d7cb..9f4cd1986 100644
--- a/src/theory/strings/inference_manager.h
+++ b/src/theory/strings/inference_manager.h
@@ -249,8 +249,15 @@ class InferenceManager : public InferenceManagerBuffered
   ExtTheory& d_extt;
   /** Reference to the statistics for the theory of strings/sequences. */
   SequencesStatistics& d_statistics;
-  /** Conversion from inferences to proofs */
+  /** Conversion from inferences to proofs for facts */
   std::unique_ptr<InferProofCons> d_ipc;
+  /**
+   * Conversion from inferences to proofs for lemmas and conflicts. This is
+   * separate from the above proof generator to avoid rare cases where the
+   * conclusion of a lemma is a duplicate of the conclusion of another lemma,
+   * or is a fact in the current equality engine.
+   */
+  std::unique_ptr<InferProofCons> d_ipcl;
   /** Common constants */
   Node d_true;
   Node d_false;
diff --git a/src/theory/strings/kinds b/src/theory/strings/kinds
index aa95ef2f8..9faa935e1 100644
--- a/src/theory/strings/kinds
+++ b/src/theory/strings/kinds
@@ -56,6 +56,10 @@ enumerator STRING_TYPE \
     "::cvc5::theory::strings::StringEnumerator" \
     "theory/strings/type_enumerator.h"
 
+enumerator REGEXP_TYPE \
+    "::cvc5::theory::strings::RegExpEnumerator" \
+    "theory/strings/regexp_enumerator.h"
+
 constant CONST_STRING \
   class \
   String \
diff --git a/src/theory/strings/regexp_enumerator.cpp b/src/theory/strings/regexp_enumerator.cpp
new file mode 100644
index 000000000..261d0008e
--- /dev/null
+++ b/src/theory/strings/regexp_enumerator.cpp
@@ -0,0 +1,49 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Implementation of enumerator for regular expressions.
+ */
+
+#include "theory/strings/regexp_enumerator.h"
+
+namespace cvc5 {
+namespace theory {
+namespace strings {
+
+RegExpEnumerator::RegExpEnumerator(TypeNode type, TypeEnumeratorProperties* tep)
+    : TypeEnumeratorBase<RegExpEnumerator>(type), d_senum(type, tep)
+{
+}
+
+RegExpEnumerator::RegExpEnumerator(const RegExpEnumerator& enumerator)
+    : TypeEnumeratorBase<RegExpEnumerator>(enumerator.getType()),
+      d_senum(enumerator.d_senum)
+{
+}
+
+Node RegExpEnumerator::operator*()
+{
+  NodeManager* nm = NodeManager::currentNM();
+  return nm->mkNode(kind::STRING_TO_REGEXP, *d_senum);
+}
+
+RegExpEnumerator& RegExpEnumerator::operator++()
+{
+  ++d_senum;
+  return *this;
+}
+
+bool RegExpEnumerator::isFinished() { return d_senum.isFinished(); }
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace cvc5
diff --git a/src/theory/strings/regexp_enumerator.h b/src/theory/strings/regexp_enumerator.h
new file mode 100644
index 000000000..289c8b046
--- /dev/null
+++ b/src/theory/strings/regexp_enumerator.h
@@ -0,0 +1,59 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 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.
+ * ****************************************************************************
+ *
+ * Enumerators for regular expressions.
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__THEORY__STRINGS__REGEXP_ENUMERATOR_H
+#define CVC5__THEORY__STRINGS__REGEXP_ENUMERATOR_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+#include "theory/strings/type_enumerator.h"
+
+namespace cvc5 {
+namespace theory {
+namespace strings {
+
+/**
+ * Simple regular expression enumerator, generates only singleton language
+ * regular expressions from a string enumeration, in other words:
+ *   (str.to_re s1) ... (str.to_re sn) ....
+ * where s1 ... sn ... is the enumeration for strings.
+ */
+class RegExpEnumerator : public TypeEnumeratorBase<RegExpEnumerator>
+{
+ public:
+  RegExpEnumerator(TypeNode type, TypeEnumeratorProperties* tep = nullptr);
+  RegExpEnumerator(const RegExpEnumerator& enumerator);
+  ~RegExpEnumerator() {}
+  /** get the current term */
+  Node operator*() override;
+  /** increment */
+  RegExpEnumerator& operator++() override;
+  /** is this enumerator finished? */
+  bool isFinished() override;
+
+ private:
+  /** underlying string enumerator */
+  StringEnumerator d_senum;
+};
+
+}  // namespace strings
+}  // namespace theory
+}  // namespace cvc5
+
+#endif /* CVC5__THEORY__STRINGS__TYPE_ENUMERATOR_H */
diff --git a/src/theory/strings/regexp_solver.cpp b/src/theory/strings/regexp_solver.cpp
index 614a5e6e0..898c0f1b7 100644
--- a/src/theory/strings/regexp_solver.cpp
+++ b/src/theory/strings/regexp_solver.cpp
@@ -546,7 +546,10 @@ bool RegExpSolver::checkPDerivative(
       {
         std::vector<Node> noExplain;
         noExplain.push_back(atom);
-        noExplain.push_back(x.eqNode(d_emptyString));
+        if (x != d_emptyString)
+        {
+          noExplain.push_back(x.eqNode(d_emptyString));
+        }
         std::vector<Node> iexp = nf_exp;
         iexp.insert(iexp.end(), noExplain.begin(), noExplain.end());
         d_im.sendInference(iexp, noExplain, d_false, InferenceId::STRINGS_RE_DELTA_CONF);
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 33dbe9ffa..1a0549a0a 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -224,7 +224,7 @@ bool TheoryEngineModelBuilder::isExcludedCdtValue(
     {
       Trace("model-builder-debug") << "  ...matches with " << eqc << " -> "
                                    << eqc_m << std::endl;
-      if (eqc_m.getKind() == kind::UNINTERPRETED_CONSTANT)
+      if (eqc_m.getKind() == kind::CODATATYPE_BOUND_VARIABLE)
       {
         Trace("model-builder-debug") << "*** " << val
                                      << " is excluded datatype for " << eqc
diff --git a/src/theory/uf/ho_extension.cpp b/src/theory/uf/ho_extension.cpp
index 096a47c86..fd7cd467e 100644
--- a/src/theory/uf/ho_extension.cpp
+++ b/src/theory/uf/ho_extension.cpp
@@ -43,13 +43,16 @@ HoExtension::HoExtension(Env& env,
 Node HoExtension::ppRewrite(Node node)
 {
   // convert HO_APPLY to APPLY_UF if fully applied
-  if (node[0].getType().getNumChildren() == 2)
+  if (node.getKind() == HO_APPLY)
   {
-    Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl;
-    Node ret = getApplyUfForHoApply(node);
-    Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret
-                   << std::endl;
-    return ret;
+    if (node[0].getType().getNumChildren() == 2)
+    {
+      Trace("uf-ho") << "uf-ho : expanding definition : " << node << std::endl;
+      Node ret = getApplyUfForHoApply(node);
+      Trace("uf-ho") << "uf-ho : ppRewrite : " << node << " to " << ret
+                     << std::endl;
+      return ret;
+    }
   }
   return node;
 }
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index cd974d3e4..ca7dc6a73 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -212,7 +212,7 @@ TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
   Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node
                       << std::endl;
   Kind k = node.getKind();
-  if (k == kind::HO_APPLY)
+  if (k == kind::HO_APPLY || (node.isVar() && node.getType().isFunction()))
   {
     if (!logicInfo().isHigherOrder())
     {
diff --git a/src/util/smt2_quote_string.cpp b/src/util/smt2_quote_string.cpp
index 82750c48b..e2ab4a74c 100644
--- a/src/util/smt2_quote_string.cpp
+++ b/src/util/smt2_quote_string.cpp
@@ -42,4 +42,16 @@ std::string quoteSymbol(const std::string& s){
   return s;
 }
 
+std::string quoteString(const std::string& s) {
+  // escape all double-quotes
+  std::string output = s;
+  size_t pos = 0;
+  while ((pos = output.find('"', pos)) != std::string::npos)
+  {
+    output.replace(pos, 1, "\"\"");
+    pos += 2;
+  }
+  return '"' + output + '"';
+}
+
 }  // namespace cvc5
diff --git a/src/util/smt2_quote_string.h b/src/util/smt2_quote_string.h
index 98b2f89dd..f8be53c0c 100644
--- a/src/util/smt2_quote_string.h
+++ b/src/util/smt2_quote_string.h
@@ -27,6 +27,11 @@ namespace cvc5 {
  */
 std::string quoteSymbol(const std::string& s);
 
+/**
+ * SMT-LIB 2 quoting for strings
+ */
+std::string quoteString(const std::string& s);
+
 }  // namespace cvc5
 
 #endif /* CVC5__UTIL__SMT2_QUOTE_STRING_H */