Merge branch 'master' into update1.9news

70 files changed, 2050 insertions, 416 deletions

diff --git a/contrib/get-gmp-dev b/contrib/get-gmp-dev
index f8a301a89..c844db93c 100755
--- a/contrib/get-gmp-dev
+++ b/contrib/get-gmp-dev
@@ -13,7 +13,7 @@ source "$(dirname "$0")/get-script-header.sh"
 
 [ -z "${BUILD_TYPE}" ] && BUILD_TYPE="--disable-shared --enable-static"
 [ -n "$HOST" ] && HOST="--host=$HOST"
-[ -z "$GMPVERSION" ] && GMPVERSION=6.1.2
+[ -z "$GMPVERSION" ] && GMPVERSION=6.2.0
 
 GMP_DIR="$DEPS_DIR/gmp-$GMPVERSION"
 
@@ -36,7 +36,7 @@ echo "Setting up GMP $GMPVERSION..."
 echo
 setup_dep "https://gmplib.org/download/gmp/gmp-$GMPVERSION.tar.bz2" "$GMP_DIR"
 cd "$GMP_DIR"
-./configure ${HOST} --prefix="$INSTALL_DIR" --enable-cxx ${BUILD_TYPE}
+./configure ${HOST} --prefix="$INSTALL_DIR" --enable-cxx ${BUILD_TYPE} --enable-shared --enable-static
 make \
   CFLAGS="${MAKE_CFLAGS}" \
   CXXFLAGS="${MAKE_CXXFLAGS}" \
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 6168a8e22..cd74698d7 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -58,31 +58,34 @@ endmacro()
 
 cvc4_add_example(simple_vc_cxx "" "")
 cvc4_add_example(simple_vc_quant_cxx "" "")
-cvc4_add_example(translator "" ""
-    # argument to binary (for testing)
-    ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2)
+# TODO(project issue $206): Port example to new API
+# cvc4_add_example(translator "" ""
+#     # argument to binary (for testing)
+#     ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2)
 
 add_subdirectory(api)
-add_subdirectory(hashsmt)
-add_subdirectory(nra-translate)
-add_subdirectory(sets-translate)
+# TODO(project issue $206): Port example to new API
+# add_subdirectory(hashsmt)
+# add_subdirectory(nra-translate)
+# add_subdirectory(sets-translate)
 
 if(TARGET CVC4::cvc4jar)
   find_package(Java REQUIRED)
   include(UseJava)
 
-  get_target_property(CVC4_JAR CVC4::cvc4jar JAR_FILE)
-
-  add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC4_JAR}")
-
-  add_test(
-    NAME java/SimpleVC
-    COMMAND
-      ${Java_JAVA_EXECUTABLE}
-        -cp "${CVC4_JAR}:${CMAKE_BINARY_DIR}/SimpleVC.jar"
-        -Djava.library.path=${CVC4_JNI_PATH}
-        SimpleVC
-  )
+  ## disabled until bindings for the new API are in place (issue #2284)
+  # get_target_property(CVC4_JAR CVC4::cvc4jar JAR_FILE)
+  #
+  # add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC4_JAR}")
+  #
+  # add_test(
+  #   NAME java/SimpleVC
+  #   COMMAND
+  #     ${Java_JAVA_EXECUTABLE}
+  #       -cp "${CVC4_JAR}:${CMAKE_BINARY_DIR}/SimpleVC.jar"
+  #       -Djava.library.path=${CVC4_JNI_PATH}
+  #       SimpleVC
+  # )
 
   add_subdirectory(api/java)
 endif()
diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index 31f62db56..0afcec0e4 100644
--- a/examples/api/java/CMakeLists.txt
+++ b/examples/api/java/CMakeLists.txt
@@ -1,20 +1,19 @@
 set(EXAMPLES_API_JAVA
-  BitVectors
-  BitVectorsAndArrays
   ## disabled until bindings for the new API are in place (issue #2284)
-  #CVC4Streams
-  Combination
-  Datatypes
-  Exceptions
-  FloatingPointArith
-  HelloWorld
-  LinearArith
-  ## disabled until bindings for the new API are in place (issue #2284)
-  #PipedInput
-  Relations
-  Statistics
-  Strings
-  UnsatCores
+  # BitVectors
+  # BitVectorsAndArrays
+  # CVC4Streams
+  # Combination
+  # Datatypes
+  # Exceptions
+  # FloatingPointArith
+  # HelloWorld
+  # LinearArith
+  # PipedInput
+  # Relations
+  # Statistics
+  # Strings
+  # UnsatCores
 )
 
 foreach(example ${EXAMPLES_API_JAVA})
diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index 26d785edc..64c2b12c1 100644
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -16,43 +16,42 @@
  ** identical.
  **/
 
-#include <iostream>
+#include <cvc4/api/cvc4cpp.h>
 
-#include <cvc4/cvc4.h>
+#include <iostream>
 
-using namespace std;
-using namespace CVC4;
+using namespace CVC4::api;
 
 int main() {
-  ExprManager em;
-  SmtEngine smt(&em);
+  Solver slv;
 
   // Prove that for integers x and y:
   //   x > 0 AND y > 0  =>  2x + y >= 3
 
-  Type integer = em.integerType();
+  Sort integer = slv.getIntegerSort();
 
-  Expr x = em.mkVar("x", integer);
-  Expr y = em.mkVar("y", integer);
-  Expr zero = em.mkConst(Rational(0));
+  Term x = slv.mkConst(integer, "x");
+  Term y = slv.mkConst(integer, "y");
+  Term zero = slv.mkReal(0);
 
-  Expr x_positive = em.mkExpr(kind::GT, x, zero);
-  Expr y_positive = em.mkExpr(kind::GT, y, zero);
+  Term x_positive = slv.mkTerm(Kind::GT, x, zero);
+  Term y_positive = slv.mkTerm(Kind::GT, y, zero);
 
-  Expr two = em.mkConst(Rational(2));
-  Expr twox = em.mkExpr(kind::MULT, two, x);
-  Expr twox_plus_y = em.mkExpr(kind::PLUS, twox, y);
+  Term two = slv.mkReal(2);
+  Term twox = slv.mkTerm(Kind::MULT, two, x);
+  Term twox_plus_y = slv.mkTerm(Kind::PLUS, twox, y);
 
-  Expr three = em.mkConst(Rational(3));
-  Expr twox_plus_y_geq_3 = em.mkExpr(kind::GEQ, twox_plus_y, three);
+  Term three = slv.mkReal(3);
+  Term twox_plus_y_geq_3 = slv.mkTerm(Kind::GEQ, twox_plus_y, three);
 
-  Expr formula =
-    em.mkExpr(kind::AND, x_positive, y_positive).
-    impExpr(twox_plus_y_geq_3);
+  Term formula =
+      slv.mkTerm(Kind::AND, x_positive, y_positive).impTerm(twox_plus_y_geq_3);
 
-  cout << "Checking entailment of formula " << formula << " with CVC4." << endl;
-  cout << "CVC4 should report ENTAILED." << endl;
-  cout << "Result from CVC4 is: " << smt.checkEntailed(formula) << endl;
+  std::cout << "Checking entailment of formula " << formula << " with CVC4."
+            << std::endl;
+  std::cout << "CVC4 should report ENTAILED." << std::endl;
+  std::cout << "Result from CVC4 is: " << slv.checkEntailed(formula)
+            << std::endl;
 
   return 0;
 }
diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp
index 83d011993..4d5767ebb 100644
--- a/examples/simple_vc_quant_cxx.cpp
+++ b/examples/simple_vc_quant_cxx.cpp
@@ -14,64 +14,63 @@
  ** A simple demonstration of the C++ interface for quantifiers. 
  **/
 
-#include <iostream>
+#include <cvc4/api/cvc4cpp.h>
 
-#include <cvc4/cvc4.h>
+#include <iostream>
 
-using namespace std;
-using namespace CVC4;
+using namespace CVC4::api;
 
 int main() {
-  ExprManager em;
-  SmtEngine smt(&em);
+  Solver slv;
 
   // Prove that the following is unsatisfiable:
   //   forall x. P( x ) ^ ~P( 5 )
 
-  Type integer = em.integerType();
-  Type boolean = em.booleanType();
-  Type integerPredicate = em.mkFunctionType(integer, boolean);
-  
-  Expr p = em.mkVar("P", integerPredicate);
-  Expr x = em.mkBoundVar("x", integer);
-  
+  Sort integer = slv.getIntegerSort();
+  Sort boolean = slv.getBooleanSort();
+  Sort integerPredicate = slv.mkFunctionSort(integer, boolean);
+
+  Term p = slv.mkConst(integerPredicate, "P");
+  Term x = slv.mkVar(integer, "x");
+
   // make forall x. P( x )
-  Expr var_list = em.mkExpr(kind::BOUND_VAR_LIST, x);
-  Expr px = em.mkExpr(kind::APPLY_UF, p, x);
-  Expr quantpospx = em.mkExpr(kind::FORALL, var_list, px);
-  cout << "Made expression : " << quantpospx << endl;
-  
+  Term var_list = slv.mkTerm(Kind::BOUND_VAR_LIST, x);
+  Term px = slv.mkTerm(Kind::APPLY_UF, p, x);
+  Term quantpospx = slv.mkTerm(Kind::FORALL, var_list, px);
+  std::cout << "Made expression : " << quantpospx << std::endl;
+
   //make ~P( 5 )
-  Expr five = em.mkConst(Rational(5));
-  Expr pfive = em.mkExpr(kind::APPLY_UF, p, five);
-  Expr negpfive = em.mkExpr(kind::NOT, pfive);
-  cout << "Made expression : " << negpfive << endl;
-  
-  Expr formula = em.mkExpr(kind::AND, quantpospx, negpfive);
+  Term five = slv.mkReal(5);
+  Term pfive = slv.mkTerm(Kind::APPLY_UF, p, five);
+  Term negpfive = slv.mkTerm(Kind::NOT, pfive);
+  std::cout << "Made expression : " << negpfive << std::endl;
 
-  smt.assertFormula(formula);
+  Term formula = slv.mkTerm(Kind::AND, quantpospx, negpfive);
 
-  cout << "Checking SAT after asserting " << formula << " to CVC4." << endl;
-  cout << "CVC4 should report unsat." << endl;
-  cout << "Result from CVC4 is: " << smt.checkSat() << endl;
+  slv.assertFormula(formula);
 
+  std::cout << "Checking SAT after asserting " << formula << " to CVC4."
+            << std::endl;
+  std::cout << "CVC4 should report unsat." << std::endl;
+  std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl;
 
-  SmtEngine smtp(&em);
-  
-  // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x))))
-  Expr pattern = em.mkExpr(kind::INST_PATTERN, px);
-  Expr pattern_list = em.mkExpr(kind::INST_PATTERN_LIST, pattern);
-  Expr quantpospx_pattern = em.mkExpr(kind::FORALL, var_list, px, pattern_list);
-  cout << "Made expression : " << quantpospx_pattern << endl;
+  slv.resetAssertions();
 
-  Expr formula_pattern = em.mkExpr(kind::AND, quantpospx_pattern, negpfive);
+  // this version has a pattern e.g. in smt2 syntax (forall ((x Int)) (! (P x ) :pattern ((P x))))
+  Term pattern = slv.mkTerm(Kind::INST_PATTERN, px);
+  Term pattern_list = slv.mkTerm(Kind::INST_PATTERN_LIST, pattern);
+  Term quantpospx_pattern =
+      slv.mkTerm(Kind::FORALL, var_list, px, pattern_list);
+  std::cout << "Made expression : " << quantpospx_pattern << std::endl;
 
-  smtp.assertFormula(formula_pattern);
+  Term formula_pattern = slv.mkTerm(Kind::AND, quantpospx_pattern, negpfive);
 
-  cout << "Checking SAT after asserting " << formula_pattern << " to CVC4." << endl;
-  cout << "CVC4 should report unsat." << endl;
-  cout << "Result from CVC4 is: " << smtp.checkSat() << endl;
+  slv.assertFormula(formula_pattern);
 
+  std::cout << "Checking SAT after asserting " << formula_pattern << " to CVC4."
+            << std::endl;
+  std::cout << "CVC4 should report unsat." << std::endl;
+  std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl;
 
   return 0;
 }
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 6850ef450..0774d60af 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1001,6 +1001,7 @@ install(FILES
           util/divisible.h
           util/gmp_util.h
           util/hash.h
+          util/iand.h
           util/integer_cln_imp.h
           util/integer_gmp_imp.h
           util/maybe.h
diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 0c8de5291..1e14e9b3a 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -4744,6 +4744,31 @@ void Solver::pop(uint32_t nscopes) const
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
+bool Solver::getInterpolant(Term conj, Term& output) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  Expr result;
+  bool success = d_smtEngine->getInterpol(*conj.d_expr, result);
+  if (success) {
+    output = Term(output.d_solver, result);
+  }
+  return success;
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+bool Solver::getInterpolant(Term conj, const Type& gtype, Term& output) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  Expr result;
+  bool success = d_smtEngine->getInterpol(*conj.d_expr, gtype, result);
+  if (success)
+  {
+    output = Term(output.d_solver, result);
+  }
+  return success;
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
 void Solver::printModel(std::ostream& out) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 828dc6f65..76306d443 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -3023,6 +3023,29 @@ class CVC4_PUBLIC Solver
   void pop(uint32_t nscopes = 1) const;
 
   /**
+   * Get an interpolant
+   * SMT-LIB: ( get-interpol <term> )
+   * Requires to enable option 'produce-interpols'.
+   * @param conj the conjecture term
+   * @param output a Term I such that A->I and I->B are valid, where A is the
+   *        current set of assertions and B is given in the input by conj.
+   * @return true if it gets I successfully, false otherwise.
+   */
+  bool getInterpolant(Term conj, Term& output) const;
+
+  /**
+   * Get an interpolant
+   * SMT-LIB: ( get-interpol <term> )
+   * Requires to enable option 'produce-interpols'.
+   * @param conj the conjecture term
+   * @param gtype the grammar for the interpolant I
+   * @param output a Term I such that A->I and I->B are valid, where A is the
+   *        current set of assertions and B is given in the input by conj.
+   * @return true if it gets I successfully, false otherwise.
+   */
+  bool getInterpolant(Term conj, const Type& gtype, Term& output) const;
+
+  /**
    * Print the model of a satisfiable query to the given output stream.
    * Requires to enable option 'produce-models'.
    * @param out the output stream
diff --git a/src/api/python/cvc4.pxd b/src/api/python/cvc4.pxd
index ee05709b7..940922052 100644
--- a/src/api/python/cvc4.pxd
+++ b/src/api/python/cvc4.pxd
@@ -21,6 +21,7 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4":
 cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
     cdef cppclass Datatype:
         Datatype() except +
+        DatatypeConstructor operator[](size_t idx) except +
         DatatypeConstructor operator[](const string& name) except +
         DatatypeConstructor getConstructor(const string& name) except +
         Term getConstructorTerm(const string& name) except +
@@ -39,7 +40,12 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
 
     cdef cppclass DatatypeConstructor:
         DatatypeConstructor() except +
+        DatatypeSelector operator[](size_t idx) except +
         DatatypeSelector operator[](const string& name) except +
+        string getName() except +
+        Term getConstructorTerm() except +
+        Term getTesterTerm() except +
+        size_t getNumSelectors() except +
         DatatypeSelector getSelector(const string& name) except +
         Term getSelectorTerm(const string& name) except +
         string toString() except +
@@ -61,12 +67,16 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
 
     cdef cppclass DatatypeDecl:
         void addConstructor(const DatatypeConstructorDecl& ctor) except +
+        size_t getNumConstructors() except +
         bint isParametric() except +
         string toString() except +
 
 
     cdef cppclass DatatypeSelector:
         DatatypeSelector() except +
+        string getName() except +
+        Term getSelectorTerm() except +
+        Sort getRangeSort() except +
         string toString() except +
 
 
@@ -213,6 +223,10 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         Sort() except +
         bint operator==(const Sort&) except +
         bint operator!=(const Sort&) except +
+        bint operator<(const Sort&) except +
+        bint operator>(const Sort&) except +
+        bint operator<=(const Sort&) except +
+        bint operator>=(const Sort&) except +
         bint isBoolean() except +
         bint isInteger() except +
         bint isReal() except +
@@ -223,6 +237,9 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint isFloatingPoint() except +
         bint isDatatype() except +
         bint isParametricDatatype() except +
+        bint isConstructor() except +
+        bint isSelector() except +
+        bint isTester() except +
         bint isFunction() except +
         bint isPredicate() except +
         bint isTuple() except +
@@ -233,9 +250,31 @@ cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
         bint isSortConstructor() except +
         bint isFirstClass() except +
         bint isFunctionLike() except +
+        bint isSubsortOf(Sort s) except +
+        bint isComparableTo(Sort s) except +
         Datatype getDatatype() except +
         Sort instantiate(const vector[Sort]& params) except +
+        size_t getConstructorArity() except +
+        vector[Sort] getConstructorDomainSorts() except +
+        Sort getConstructorCodomainSort() except +
+        size_t getFunctionArity() except +
+        vector[Sort] getFunctionDomainSorts() except +
+        Sort getFunctionCodomainSort() except +
+        Sort getArrayIndexSort() except +
+        Sort getArrayElementSort() except +
+        Sort getSetElementSort() except +
+        string getUninterpretedSortName() except +
         bint isUninterpretedSortParameterized() except +
+        vector[Sort] getUninterpretedSortParamSorts() except +
+        string getSortConstructorName() except +
+        size_t getSortConstructorArity() except +
+        uint32_t getBVSize() except +
+        uint32_t getFPExponentSize() except +
+        uint32_t getFPSignificandSize() except +
+        vector[Sort] getDatatypeParamSorts() except +
+        size_t getDatatypeArity() except +
+        size_t getTupleLength() except +
+        vector[Sort] getTupleSorts() except +
         string toString() except +
 
     cdef cppclass SortHashFunction:
diff --git a/src/api/python/cvc4.pxi b/src/api/python/cvc4.pxi
index ab174ef0d..01660e206 100644
--- a/src/api/python/cvc4.pxi
+++ b/src/api/python/cvc4.pxi
@@ -65,9 +65,14 @@ cdef class Datatype:
     def __cinit__(self):
         pass
 
-    def __getitem__(self, str name):
+    def __getitem__(self, index):
         cdef DatatypeConstructor dc = DatatypeConstructor()
-        dc.cdc = self.cd[name.encode()]
+        if isinstance(index, int) and index >= 0:
+            dc.cdc = self.cd[(<int?> index)]
+        elif isinstance(index, str):
+            dc.cdc = self.cd[(<const string &> name.encode())]
+        else:
+            raise ValueError("Expecting a non-negative integer or string")
         return dc
 
     def getConstructor(self, str name):
@@ -104,11 +109,32 @@ cdef class DatatypeConstructor:
     def __cinit__(self):
         self.cdc = c_DatatypeConstructor()
 
-    def __getitem__(self, str name):
+    def __getitem__(self, index):
         cdef DatatypeSelector ds = DatatypeSelector()
-        ds.cds = self.cdc[name.encode()]
+        if isinstance(index, int) and index >= 0:
+            ds.cds = self.cdc[(<int?> index)]
+        elif isinstance(index, str):
+            ds.cds = self.cdc[(<const string &> name.encode())]
+        else:
+            raise ValueError("Expecting a non-negative integer or string")
         return ds
 
+    def getName(self):
+        return self.cdc.getName().decode()
+
+    def getConstructorTerm(self):
+        cdef Term term = Term()
+        term.cterm = self.cdc.getConstructorTerm()
+        return term
+
+    def getTesterTerm(self):
+        cdef Term term = Term()
+        term.cterm = self.cdc.getTesterTerm()
+        return term
+
+    def getNumSelectors(self):
+        return self.cdc.getNumSelectors()
+
     def getSelector(self, str name):
         cdef DatatypeSelector ds = DatatypeSelector()
         ds.cds = self.cdc.getSelector(name.encode())
@@ -159,6 +185,9 @@ cdef class DatatypeDecl:
     def addConstructor(self, DatatypeConstructorDecl ctor):
         self.cdd.addConstructor(ctor.cddc)
 
+    def getNumConstructors(self):
+        return self.cdd.getNumConstructors()
+
     def isParametric(self):
         return self.cdd.isParametric()
 
@@ -174,6 +203,19 @@ cdef class DatatypeSelector:
     def __cinit__(self):
         self.cds = c_DatatypeSelector()
 
+    def getName(self):
+        return self.cds.getName().decode()
+
+    def getSelectorTerm(self):
+        cdef Term term = Term()
+        term.cterm = self.cds.getSelectorTerm()
+        return term
+
+    def getRangeSort(self):
+        cdef Sort sort = Sort()
+        sort.csort = self.cds.getRangeSort()
+        return sort
+
     def __str__(self):
         return self.cds.toString().decode()
 
@@ -961,6 +1003,18 @@ cdef class Sort:
     def __ne__(self, Sort other):
         return self.csort != other.csort
 
+    def __lt__(self, Sort other):
+        return self.csort < other.csort
+
+    def __gt__(self, Sort other):
+        return self.csort > other.csort
+
+    def __le__(self, Sort other):
+        return self.csort <= other.csort
+
+    def __ge__(self, Sort other):
+        return self.csort >= other.csort
+
     def __str__(self):
         return self.csort.toString().decode()
 
@@ -1000,6 +1054,15 @@ cdef class Sort:
     def isParametricDatatype(self):
         return self.csort.isParametricDatatype()
 
+    def isConstructor(self):
+        return self.csort.isConstructor()
+
+    def isSelector(self):
+        return self.csort.isSelector()
+
+    def isTester(self):
+        return self.csort.isTester()
+
     def isFunction(self):
         return self.csort.isFunction()
 
@@ -1030,6 +1093,12 @@ cdef class Sort:
     def isFunctionLike(self):
         return self.csort.isFunctionLike()
 
+    def isSubsortOf(self, Sort sort):
+        return self.csort.isSubsortOf(sort.csort)
+
+    def isComparableTo(self, Sort sort):
+        return self.csort.isComparableTo(sort.csort)
+
     def getDatatype(self):
         cdef Datatype d = Datatype()
         d.cd = self.csort.getDatatype()
@@ -1043,9 +1112,104 @@ cdef class Sort:
         sort.csort = self.csort.instantiate(v)
         return sort
 
+    def getConstructorArity(self):
+        return self.csort.getConstructorArity()
+
+    def getConstructorDomainSorts(self):
+        domain_sorts = []
+        for s in self.csort.getConstructorDomainSorts():
+            sort = Sort()
+            sort.csort = s
+            domain_sorts.append(sort)
+        return domain_sorts
+
+    def getConstructorCodomainSort(self):
+        cdef Sort sort = Sort()
+        sort.csort = self.csort.getConstructorCodomainSort()
+        return sort
+
+    def getFunctionArity(self):
+        return self.csort.getFunctionArity()
+
+    def getFunctionDomainSorts(self):
+        domain_sorts = []
+        for s in self.csort.getFunctionDomainSorts():
+            sort = Sort()
+            sort.csort = s
+            domain_sorts.append(sort)
+        return domain_sorts
+
+    def getFunctionCodomainSort(self):
+        cdef Sort sort = Sort()
+        sort.csort = self.csort.getFunctionCodomainSort()
+        return sort
+
+    def getArrayIndexSort(self):
+        cdef Sort sort = Sort()
+        sort.csort = self.csort.getArrayIndexSort()
+        return sort
+
+    def getArrayElementSort(self):
+        cdef Sort sort = Sort()
+        sort.csort = self.csort.getArrayElementSort()
+        return sort
+
+    def getSetElementSort(self):
+        cdef Sort sort = Sort()
+        sort.csort = self.csort.getSetElementSort()
+        return sort
+
+    def getUninterpretedSortName(self):
+        return self.csort.getUninterpretedSortName().decode()
+
     def isUninterpretedSortParameterized(self):
         return self.csort.isUninterpretedSortParameterized()
 
+    def getUninterpretedSortParamSorts(self):
+        param_sorts = []
+        for s in self.csort.getUninterpretedSortParamSorts():
+            sort = Sort()
+            sort.csort = s
+            param_sorts.append(sort)
+        return param_sorts
+
+    def getSortConstructorName(self):
+        return self.csort.getSortConstructorName().decode()
+
+    def getSortConstructorArity(self):
+        return self.csort.getSortConstructorArity()
+
+    def getBVSize(self):
+        return self.csort.getBVSize()
+
+    def getFPExponentSize(self):
+        return self.csort.getFPExponentSize()
+
+    def getFPSignificandSize(self):
+        return self.csort.getFPSignificandSize()
+
+    def getDatatypeParamSorts(self):
+        param_sorts = []
+        for s in self.csort.getDatatypeParamSorts():
+            sort = Sort()
+            sort.csort = s
+            param_sorts.append(sort)
+        return param_sorts
+
+    def getDatatypeArity(self):
+        return self.csort.getDatatypeArity()
+
+    def getTupleLength(self):
+        return self.csort.getTupleLength()
+
+    def getTupleSorts(self):
+        tuple_sorts = []
+        for s in self.csort.getTupleSorts():
+            sort = Sort()
+            sort.csort = s
+            tuple_sorts.append(sort)
+        return tuple_sorts
+
 
 cdef class Term:
     cdef c_Term cterm
diff --git a/src/api/python/genkinds.py b/src/api/python/genkinds.py
index a12c9735c..77b168dea 100755
--- a/src/api/python/genkinds.py
+++ b/src/api/python/genkinds.py
@@ -83,7 +83,7 @@ cdef class kind:
     cdef str name
     def __cinit__(self, int kindint):
         self.k = int2kind[kindint]
-        self.name = int2name[kindint].decode()
+        self.name = str(int2name[kindint])
 
     def __eq__(self, kind other):
         return (<int> self.k) == (<int> other.k)
@@ -111,7 +111,7 @@ kinds.__file__ = kinds.__name__ + ".py"
 KINDS_ATTR_TEMPLATE = \
 r"""
 int2kind[<int> {kind}] = {kind}
-int2name[<int> {kind}] = "{name}".encode()
+int2name[<int> {kind}] = b"{name}"
 cdef kind {name} = kind(<int> {kind})
 setattr(kinds, "{name}", {name})
 """
diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt
index 8e919db86..8159b8ee0 100644
--- a/src/bindings/java/CMakeLists.txt
+++ b/src/bindings/java/CMakeLists.txt
@@ -81,6 +81,7 @@ set(gen_java_files
   ${CMAKE_CURRENT_BINARY_DIR}/FloatingPointType.java
   ${CMAKE_CURRENT_BINARY_DIR}/FunctionType.java
   ${CMAKE_CURRENT_BINARY_DIR}/InputLanguage.java
+  ${CMAKE_CURRENT_BINARY_DIR}/IntAnd.java
   ${CMAKE_CURRENT_BINARY_DIR}/IntToBitVector.java
   ${CMAKE_CURRENT_BINARY_DIR}/Integer.java
   ${CMAKE_CURRENT_BINARY_DIR}/IntegerHashFunction.java
diff --git a/src/cvc4.i b/src/cvc4.i
index 4fc0b092a..9fc8ed60e 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -40,6 +40,7 @@ using namespace CVC4;
 #include "smt/command.h"
 #include "util/bitvector.h"
 #include "util/floatingpoint.h"
+#include "util/iand.h"
 #include "util/integer.h"
 #include "util/sexpr.h"
 #include "util/unsafe_interrupt_exception.h"
@@ -206,6 +207,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "util/integer.i"
 %include "util/rational.i"
 %include "util/bitvector.i"
+%include "util/iand.i"
 %include "util/floatingpoint.i"
 
 // Tim: The remainder of util/.
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 1809eb2d0..3a4498ab7 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -36,6 +36,10 @@ ${includes}
 
 namespace CVC4 {
 
+namespace api {
+class Solver;
+}
+
 class Expr;
 class SmtEngine;
 class NodeManager;
@@ -45,7 +49,8 @@ struct ExprManagerMapCollection;
 class ResourceManager;
 
 class CVC4_PUBLIC ExprManager {
-private:
+ private:
+  friend api::Solver;
   /** The internal node manager */
   NodeManager* d_nodeManager;
 
@@ -83,7 +88,6 @@ private:
   /** A list of datatypes owned by this expr manager. */
   std::vector<std::unique_ptr<Datatype> > d_ownedDatatypes;
 
- public:
   /**
    * Creates an expression manager with default options.
    */
@@ -97,6 +101,7 @@ private:
    */
   explicit ExprManager(const Options& options);
 
+ public:
   /**
    * Destroys the expression manager. No will be deallocated at this point, so
    * any expression references that used to be managed by this expression
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index f736efed9..d00f1658b 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -90,6 +90,13 @@ const char* toString(PfRule id)
     case PfRule::EXISTS_INTRO: return "EXISTS_INTRO";
     case PfRule::SKOLEMIZE: return "SKOLEMIZE";
     case PfRule::INSTANTIATE: return "INSTANTIATE";
+    //================================================= Arith rules
+    case PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS: return "ARITH_SCALE_SUM_UPPER_BOUNDS";
+    case PfRule::ARITH_TRICHOTOMY: return "ARITH_TRICHOTOMY";
+    case PfRule::INT_TIGHT_LB: return "INT_TIGHT_LB";
+    case PfRule::INT_TIGHT_UB: return "INT_TIGHT_UB";
+    case PfRule::INT_TRUST: return "INT_TRUST";
+    case PfRule::ARITH_OP_ELIM_AXIOM: return "ARITH_OP_ELIM_AXIOM";
     //================================================= Unknown rule
     case PfRule::UNKNOWN: return "UNKNOWN";
     default: return "?";
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index d6e5b6f4b..ec589a16e 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -507,6 +507,70 @@ enum class PfRule : uint32_t
   // sigma maps x1 ... xn to t1 ... tn.
   INSTANTIATE,
 
+  // ======== Adding Inequalities
+  // Note: an ArithLiteral is a term of the form (>< poly const)
+  // where
+  //   >< is >=, >, ==, <, <=, or not(== ...).
+  //   poly is a polynomial
+  //   const is a rational constant
+
+  // Children: (P1:l1, ..., Pn:ln)
+  //           where each li is an ArithLiteral
+  //           not(= ...) is dis-allowed!
+  //
+  // Arguments: (k1, ..., kn), non-zero reals
+  // ---------------------
+  // Conclusion: (>< (* k t1) (* k t2))
+  //    where >< is the fusion of the combination of the ><i, (flipping each it
+  //    its ki is negative). >< is always one of <, <=
+  //    NB: this implies that lower bounds must have negative ki,
+  //                      and upper bounds must have positive ki.
+  //    t1 is the sum of the polynomials.
+  //    t2 is the sum of the constants.
+  ARITH_SCALE_SUM_UPPER_BOUNDS,
+
+  // ======== Tightening Strict Integer Upper Bounds
+  // Children: (P:(< i c))
+  //         where i has integer type.
+  // Arguments: none
+  // ---------------------
+  // Conclusion: (<= i greatestIntLessThan(c)})
+  INT_TIGHT_UB,
+
+  // ======== Tightening Strict Integer Lower Bounds
+  // Children: (P:(> i c))
+  //         where i has integer type.
+  // Arguments: none
+  // ---------------------
+  // Conclusion: (>= i leastIntGreaterThan(c)})
+  INT_TIGHT_LB,
+
+  // ======== Trichotomy of the reals
+  // Children: (A B)
+  // Arguments: (C)
+  // ---------------------
+  // Conclusion: (C),
+  //                 where (not A) (not B) and C
+  //                   are (> x c) (< x c) and (= x c)
+  //                   in some order
+  //                 note that "not" here denotes arithmetic negation, flipping
+  //                 >= to <, etc.
+  ARITH_TRICHOTOMY,
+
+  // ======== Arithmetic operator elimination
+  // Children: none
+  // Arguments: (t)
+  // ---------------------
+  // Conclusion: arith::OperatorElim::getAxiomFor(t)
+  ARITH_OP_ELIM_AXIOM,
+
+  // ======== Int Trust
+  // Children: (P1 ... Pn)
+  // Arguments: (Q)
+  // ---------------------
+  // Conclusion: (Q)
+  INT_TRUST,
+
   //================================================= Unknown rule
   UNKNOWN,
 };
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 303448d1b..c104cb3e7 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -669,6 +669,34 @@ header = "options/smt_options.h"
   help       = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)"
 
 [[option]]
+  name       = "produceInterpols"
+  category   = "undocumented"
+  long       = "produce-interpols=MODE"
+  type       = "ProduceInterpols"
+  default    = "NONE"
+  read_only  = true
+  help       = "support the get-interpol command"
+  help_mode  = "Interpolants grammar mode"
+[[option.mode.NONE]]
+  name = "none"
+  help = "don't compute interpolants"
+[[option.mode.DEFAULT]]
+  name = "default"
+  help = "use the default grammar for the theory or the user-defined grammar if given"
+[[option.mode.ASSUMPTIONS]]
+  name = "assumptions"
+  help = "use only operators that occur in the assumptions"
+[[option.mode.CONJECTURE]]
+  name = "conjecture"
+  help = "use only operators that occur in the conjecture"
+[[option.mode.SHARED]]
+  name = "shared"
+  help = "use only operators that occur both in the assumptions and the conjecture"
+[[option.mode.ALL]]
+  name = "all"
+  help = "use only operators that occur either in the assumptions or the conjecture"
+
+[[option]]
   name       = "produceAbducts"
   category   = "undocumented"
   long       = "produce-abducts"
@@ -678,6 +706,15 @@ header = "options/smt_options.h"
   help       = "support the get-abduct command"
 
 [[option]]
+  name       = "checkInterpols"
+  category   = "regular"
+  long       = "check-interpols"
+  type       = "bool"
+  default    = "false"
+  read_only  = true
+  help       = "checks whether produced solutions to get-interpol are correct"
+
+[[option]]
   name       = "checkAbducts"
   category   = "regular"
   long       = "check-abducts"
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 3e8234a86..703696cf5 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1136,6 +1136,17 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
     {
       cmd->reset(new GetAbductCommand(name,e.getExpr(), t.getType()));
     }
+  | GET_INTERPOL_TOK {
+      PARSER_STATE->checkThatLogicIsSet();
+    }
+    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
+    term[e,e2]
+    (
+      sygusGrammar[t, terms, name]
+    )?
+    {
+      cmd->reset(new GetInterpolCommand(SOLVER, name, e, t.getType()));
+    }
   | DECLARE_HEAP LPAREN_TOK
     sortSymbol[t, CHECK_DECLARED]
     sortSymbol[t, CHECK_DECLARED]
@@ -2315,6 +2326,7 @@ INCLUDE_TOK : 'include';
 GET_QE_TOK : 'get-qe';
 GET_QE_DISJUNCT_TOK : 'get-qe-disjunct';
 GET_ABDUCT_TOK : 'get-abduct';
+GET_INTERPOL_TOK : 'get-interpol';
 DECLARE_HEAP : 'declare-heap';
 
 // SyGuS commands
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index cbb2076dd..095c59374 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2091,6 +2091,90 @@ std::string GetSynthSolutionCommand::getCommandName() const
   return "get-instantiations";
 }
 
+GetInterpolCommand::GetInterpolCommand(api::Solver* solver,
+                                       const std::string& name,
+                                       api::Term conj)
+    : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false)
+{
+}
+GetInterpolCommand::GetInterpolCommand(api::Solver* solver,
+                                       const std::string& name,
+                                       api::Term conj,
+                                       const Type& gtype)
+    : Command(solver),
+      d_name(name),
+      d_conj(conj),
+      d_sygus_grammar_type(gtype),
+      d_resultStatus(false)
+{
+}
+
+api::Term GetInterpolCommand::getConjecture() const { return d_conj; }
+Type GetInterpolCommand::getGrammarType() const { return d_sygus_grammar_type; }
+api::Term GetInterpolCommand::getResult() const { return d_result; }
+
+void GetInterpolCommand::invoke(SmtEngine* smtEngine)
+{
+  try
+  {
+    if (d_sygus_grammar_type.isNull())
+    {
+      d_resultStatus = d_solver->getInterpolant(d_conj, d_result);
+    }
+    else
+    {
+      d_resultStatus =
+          d_solver->getInterpolant(d_conj, d_sygus_grammar_type, d_result);
+    }
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+void GetInterpolCommand::printResult(std::ostream& out,
+                                     uint32_t verbosity) const
+{
+  if (!ok())
+  {
+    this->Command::printResult(out, verbosity);
+  }
+  else
+  {
+    expr::ExprDag::Scope scope(out, false);
+    if (d_resultStatus)
+    {
+      out << "(define-fun " << d_name << " () Bool " << d_result << ")"
+          << std::endl;
+    }
+    else
+    {
+      out << "none" << std::endl;
+    }
+  }
+}
+
+Command* GetInterpolCommand::exportTo(ExprManager* exprManager,
+                                      ExprManagerMapCollection& variableMap)
+{
+  Unimplemented();
+}
+
+Command* GetInterpolCommand::clone() const
+{
+  GetInterpolCommand* c = new GetInterpolCommand(d_solver, d_name, d_conj);
+  c->d_result = d_result;
+  c->d_resultStatus = d_resultStatus;
+  return c;
+}
+
+std::string GetInterpolCommand::getCommandName() const
+{
+  return "get-interpol";
+}
+
 GetAbductCommand::GetAbductCommand() {}
 GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj)
     : d_name(name), d_conj(conj), d_resultStatus(false)
diff --git a/src/smt/command.h b/src/smt/command.h
index efb4f2f4a..a6a0faaae 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -28,6 +28,7 @@
 #include <string>
 #include <vector>
 
+#include "api/cvc4cpp.h"
 #include "expr/datatype.h"
 #include "expr/expr.h"
 #include "expr/type.h"
@@ -1038,6 +1039,58 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command
   SmtEngine* d_smtEngine;
 }; /* class GetSynthSolutionCommand */
 
+/** The command (get-interpol s B)
+ *
+ * This command asks for an interpolant from the current set of assertions and
+ * conjecture (goal) B.
+ *
+ * The symbol s is the name for the interpolation predicate. If we successfully
+ * find a predicate P, then the output response of this command is: (define-fun
+ * s () Bool P)
+ */
+class CVC4_PUBLIC GetInterpolCommand : public Command
+{
+ public:
+  GetInterpolCommand(api::Solver* solver,
+                     const std::string& name,
+                     api::Term conj);
+  /** The argument gtype is the grammar of the interpolation query */
+  GetInterpolCommand(api::Solver* solver,
+                     const std::string& name,
+                     api::Term conj,
+                     const Type& gtype);
+
+  /** Get the conjecture of the interpolation query */
+  api::Term getConjecture() const;
+  /** Get the grammar sygus datatype type given for the interpolation query */
+  Type getGrammarType() const;
+  /** Get the result of the query, which is the solution to the interpolation
+   * query. */
+  api::Term getResult() const;
+
+  void invoke(SmtEngine* smtEngine) override;
+  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  Command* clone() const override;
+  std::string getCommandName() const override;
+
+ protected:
+  /** The name of the interpolation predicate */
+  std::string d_name;
+  /** The conjecture of the interpolation query */
+  api::Term d_conj;
+  /**
+   * The (optional) grammar of the interpolation query, expressed as a sygus
+   * datatype type.
+   */
+  Type d_sygus_grammar_type;
+  /** the return status of the command */
+  bool d_resultStatus;
+  /** the return expression of the command */
+  api::Term d_result;
+}; /* class GetInterpolCommand */
+
 /** The command (get-abduct s B (G)?)
  *
  * This command asks for an abduct from the current set of assertions and
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index d663352f7..a7e8e6212 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -291,8 +291,10 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
   // sygus inference may require datatypes
   if (!smte.isInternalSubsolver())
   {
-    if (options::produceAbducts() || options::sygusInference()
-        || options::sygusRewSynthInput() || options::sygusInst())
+    if (options::produceAbducts()
+        || options::produceInterpols() != options::ProduceInterpols::NONE
+        || options::sygusInference() || options::sygusRewSynthInput()
+        || options::sygusInst())
     {
       // since we are trying to recast as sygus, we assume the input is sygus
       is_sygus = true;
@@ -316,6 +318,7 @@ void setDefaults(SmtEngine& smte, LogicInfo& logic)
 
   if ((options::checkModels() || options::checkSynthSol()
        || options::produceAbducts()
+       || options::produceInterpols() != options::ProduceInterpols::NONE
        || options::modelCoresMode() != options::ModelCoresMode::NONE
        || options::blockModelsMode() != options::BlockModelsMode::NONE)
       && !options::produceAssertions())
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a6d89aaf5..bb4d82fe0 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2934,6 +2934,12 @@ void SmtEngine::checkSynthSolution()
   }
 }
 
+void SmtEngine::checkInterpol(Expr interpol,
+                              const std::vector<Expr>& easserts,
+                              const Node& conj)
+{
+}
+
 void SmtEngine::checkAbduct(Expr a)
 {
   Assert(a.getType().isBoolean());
@@ -3152,6 +3158,19 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
   }
 }
 
+bool SmtEngine::getInterpol(const Expr& conj,
+                            const Type& grammarType,
+                            Expr& interpol)
+{
+  return false;
+}
+
+bool SmtEngine::getInterpol(const Expr& conj, Expr& interpol)
+{
+  Type grammarType;
+  return getInterpol(conj, grammarType, interpol);
+}
+
 bool SmtEngine::getAbduct(const Expr& conj, const Type& grammarType, Expr& abd)
 {
   SmtScope smts(this);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 8a9a60251..afb39b41b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -166,7 +166,9 @@ class CVC4_PUBLIC SmtEngine
     // immediately after a check-sat returning "unsat"
     SMT_MODE_UNSAT,
     // immediately after a successful call to get-abduct
-    SMT_MODE_ABDUCT
+    SMT_MODE_ABDUCT,
+    // immediately after a successful call to get-interpol
+    SMT_MODE_INTERPOL
   };
 
   /** Construct an SmtEngine with the given expression manager.  */
@@ -619,6 +621,23 @@ class CVC4_PUBLIC SmtEngine
   Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict = true);
 
   /**
+   * This method asks this SMT engine to find an interpolant with respect to
+   * the current assertion stack (call it A) and the conjecture (call it B). If
+   * this method returns true, then interpolant is set to a formula I such that
+   * A ^ ~I and I ^ ~B are both unsatisfiable.
+   *
+   * The argument grammarType is a sygus datatype type that encodes the syntax
+   * restrictions on the shapes of possible solutions.
+   *
+   * This method invokes a separate copy of the SMT engine for solving the
+   * corresponding sygus problem for generating such a solution.
+   */
+  bool getInterpol(const Expr& conj, const Type& grammarType, Expr& interpol);
+
+  /** Same as above, but without user-provided grammar restrictions */
+  bool getInterpol(const Expr& conj, Expr& interpol);
+
+  /**
    * This method asks this SMT engine to find an abduct with respect to the
    * current assertion stack (call it A) and the conjecture (call it B).
    * If this method returns true, then abd is set to a formula C such that
@@ -935,6 +954,18 @@ class CVC4_PUBLIC SmtEngine
    * unsatisfiable. If not, then the found solutions are wrong.
    */
   void checkSynthSolution();
+
+  /**
+   * Check that a solution to an interpolation problem is indeed a solution.
+   *
+   * The check is made by determining that the assertions imply the solution of
+   * the interpolation problem (interpol), and the solution implies the goal
+   * (conj). If these criteria are not met, an internal error is thrown.
+   */
+  void checkInterpol(Expr interpol,
+                     const std::vector<Expr>& easserts,
+                     const Node& conj);
+
   /**
    * Check that a solution to an abduction conjecture is indeed a solution.
    *
@@ -1058,6 +1089,7 @@ class CVC4_PUBLIC SmtEngine
   void debugCheckFunctionBody(Expr formula,
                               const std::vector<Expr>& formals,
                               Expr func);
+
   /**
    * Get abduct internal.
    *
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index e50b79bbc..188ef47e6 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -25,6 +25,7 @@
 #include "theory/arith/arith_utilities.h"
 #include "theory/arith/normal_form.h"
 #include "theory/theory.h"
+#include "util/iand.h"
 
 namespace CVC4 {
 namespace theory {
@@ -101,8 +102,8 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){
     case kind::PLUS:
       return preRewritePlus(t);
     case kind::MULT:
-    case kind::NONLINEAR_MULT:
-      return preRewriteMult(t);  
+    case kind::NONLINEAR_MULT: return preRewriteMult(t);
+    case kind::IAND: return RewriteResponse(REWRITE_DONE, t);
     case kind::EXPONENTIAL:
     case kind::SINE:
     case kind::COSINE:
@@ -165,8 +166,8 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
     case kind::PLUS:
       return postRewritePlus(t);
     case kind::MULT:
-    case kind::NONLINEAR_MULT:
-      return postRewriteMult(t);    
+    case kind::NONLINEAR_MULT: return postRewriteMult(t);
+    case kind::IAND: return postRewriteIAnd(t);
     case kind::EXPONENTIAL:
     case kind::SINE:
     case kind::COSINE:
@@ -371,6 +372,47 @@ RewriteResponse ArithRewriter::postRewriteMult(TNode t){
   return RewriteResponse(REWRITE_DONE, res.getNode());
 }
 
+RewriteResponse ArithRewriter::postRewriteIAnd(TNode t)
+{
+  Assert(t.getKind() == kind::IAND);
+  NodeManager* nm = NodeManager::currentNM();
+  // if constant, we eliminate
+  if (t[0].isConst() && t[1].isConst())
+  {
+    size_t bsize = t.getOperator().getConst<IntAnd>().d_size;
+    Node iToBvop = nm->mkConst(IntToBitVector(bsize));
+    Node arg1 = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvop, t[0]);
+    Node arg2 = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvop, t[1]);
+    Node bvand = nm->mkNode(kind::BITVECTOR_AND, arg1, arg2);
+    Node ret = nm->mkNode(kind::BITVECTOR_TO_NAT, bvand);
+    return RewriteResponse(REWRITE_AGAIN_FULL, ret);
+  }
+  else if (t[0] > t[1])
+  {
+    // ((_ iand k) x y) ---> ((_ iand k) y x) if x > y by node ordering
+    Node ret = nm->mkNode(kind::IAND, t.getOperator(), t[1], t[0]);
+    return RewriteResponse(REWRITE_AGAIN, ret);
+  }
+  else if (t[0] == t[1])
+  {
+    // ((_ iand k) x x) ---> x
+    return RewriteResponse(REWRITE_DONE, t[0]);
+  }
+  // simplifications involving constants
+  for (unsigned i = 0; i < 2; i++)
+  {
+    if (!t[i].isConst())
+    {
+      continue;
+    }
+    if (t[i].getConst<Rational>().sgn() == 0)
+    {
+      // ((_ iand k) 0 y) ---> 0
+      return RewriteResponse(REWRITE_DONE, t[i]);
+    }
+  }
+  return RewriteResponse(REWRITE_DONE, t);
+}
 
 RewriteResponse ArithRewriter::preRewriteTranscendental(TNode t) {
   return RewriteResponse(REWRITE_DONE, t);
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 0563aa1de..1dc756514 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -52,7 +52,9 @@ class ArithRewriter : public TheoryRewriter
 
   static RewriteResponse preRewriteMult(TNode t);
   static RewriteResponse postRewriteMult(TNode t);
-  
+
+  static RewriteResponse postRewriteIAnd(TNode t);
+
   static RewriteResponse preRewriteTranscendental(TNode t);
   static RewriteResponse postRewriteTranscendental(TNode t);
 
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 4c35e5d19..858098b70 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -47,6 +47,7 @@ ArithCongruenceManager::ArithCongruenceManager(
   d_ee.addFunctionKind(kind::NONLINEAR_MULT);
   d_ee.addFunctionKind(kind::EXPONENTIAL);
   d_ee.addFunctionKind(kind::SINE);
+  d_ee.addFunctionKind(kind::IAND);
 }
 
 ArithCongruenceManager::~ArithCongruenceManager() {}
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 409534050..e563d8f66 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -133,4 +133,18 @@ nullaryoperator PI "pi"
 
 typerule PI ::CVC4::theory::arith::RealNullaryOperatorTypeRule
 
+# Integer AND, which is parameterized by a (positive) bitwidth k.
+# ((_ iand k) i1 i2) is equivalent to:
+# (bv2int (bvand ((_ int2bv k) i1) ((_ int2bv k) i2)))
+# for all integers i1, i2.
+constant IAND_OP \
+	::CVC4::IntAnd \
+	"::CVC4::UnsignedHashFunction< ::CVC4::IntAnd >" \
+	"util/iand.h" \
+	"operator for integer AND; payload is an instance of the CVC4::IntAnd class"
+parameterized IAND IAND_OP 2 "integer version of AND operator; first parameter is an IAND_OP, second and third are integer terms"
+
+typerule IAND_OP ::CVC4::theory::arith::IAndOpTypeRule
+typerule IAND ::CVC4::theory::arith::IAndTypeRule
+
 endtheory
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index c7b4b3625..f964f1628 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -71,6 +71,12 @@ bool Variable::isLeafMember(Node n){
 
 VarList::VarList(Node n) : NodeWrapper(n) { Assert(isSorted(begin(), end())); }
 
+bool Variable::isIAndMember(Node n)
+{
+  return n.getKind() == kind::IAND && Polynomial::isMember(n[0])
+         && Polynomial::isMember(n[1]);
+}
+
 bool Variable::isDivMember(Node n){
   switch(n.getKind()){
   case kind::DIVISION:
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 3ab5d907a..484bdbf44 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -239,6 +239,7 @@ public:
      case kind::INTS_DIVISION_TOTAL:
      case kind::INTS_MODULUS_TOTAL:
      case kind::DIVISION_TOTAL: return isDivMember(n);
+     case kind::IAND: return isIAndMember(n);
      case kind::EXPONENTIAL:
      case kind::SINE:
      case kind::COSINE:
@@ -264,6 +265,7 @@ public:
  }
 
   static bool isLeafMember(Node n);
+  static bool isIAndMember(Node n);
   static bool isDivMember(Node n);
   bool isDivLike() const{
     return isDivMember(getNode());
diff --git a/src/theory/arith/proof_checker.cpp b/src/theory/arith/proof_checker.cpp
new file mode 100644
index 000000000..5b7a3d63a
--- /dev/null
+++ b/src/theory/arith/proof_checker.cpp
@@ -0,0 +1,269 @@
+/*********************                                                        */
+/*! \file proof_checker.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of arithmetic proof checker
+ **/
+
+#include "theory/arith/proof_checker.h"
+
+#include <iostream>
+#include <set>
+
+#include "expr/skolem_manager.h"
+#include "theory/arith/arith_utilities.h"
+#include "theory/arith/constraint.h"
+#include "theory/arith/normal_form.h"
+#include "theory/arith/operator_elim.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+void ArithProofRuleChecker::registerTo(ProofChecker* pc)
+{
+  pc->registerChecker(PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS, this);
+  pc->registerChecker(PfRule::ARITH_TRICHOTOMY, this);
+  pc->registerChecker(PfRule::INT_TIGHT_UB, this);
+  pc->registerChecker(PfRule::INT_TIGHT_LB, this);
+  pc->registerChecker(PfRule::INT_TRUST, this);
+  pc->registerChecker(PfRule::ARITH_OP_ELIM_AXIOM, this);
+}
+
+Node ArithProofRuleChecker::checkInternal(PfRule id,
+                                          const std::vector<Node>& children,
+                                          const std::vector<Node>& args)
+{
+  if (Debug.isOn("arith::pf::check"))
+  {
+    Debug("arith::pf::check") << "Arith PfRule:" << id << std::endl;
+    Debug("arith::pf::check") << "  children: " << std::endl;
+    for (const auto& c : children)
+    {
+      Debug("arith::pf::check") << "  * " << c << std::endl;
+    }
+    Debug("arith::pf::check") << "  args:" << std::endl;
+    for (const auto& c : args)
+    {
+      Debug("arith::pf::check") << "  * " << c << std::endl;
+    }
+  }
+  switch (id)
+  {
+    case PfRule::ARITH_SCALE_SUM_UPPER_BOUNDS:
+    {
+      // Children: (P1:l1, ..., Pn:ln)
+      //           where each li is an ArithLiteral
+      //           not(= ...) is dis-allowed!
+      //
+      // Arguments: (k1, ..., kn), non-zero reals
+      // ---------------------
+      // Conclusion: (>< (* k t1) (* k t2))
+      //    where >< is the fusion of the combination of the ><i, (flipping each
+      //    it its ki is negative). >< is always one of <, <= NB: this implies
+      //    that lower bounds must have negative ki,
+      //                      and upper bounds must have positive ki.
+      //    t1 is the sum of the polynomials.
+      //    t2 is the sum of the constants.
+      Assert(children.size() == args.size());
+      if (children.size() < 2)
+      {
+        return Node::null();
+      }
+
+      // Whether a strict inequality is in the sum.
+      auto nm = NodeManager::currentNM();
+      bool strict = false;
+      NodeBuilder<> leftSum(Kind::PLUS);
+      NodeBuilder<> rightSum(Kind::PLUS);
+      for (size_t i = 0; i < children.size(); ++i)
+      {
+        Rational scalar = args[i].getConst<Rational>();
+        if (scalar == 0)
+        {
+          Debug("arith::pf::check") << "Error: zero scalar" << std::endl;
+          return Node::null();
+        }
+
+        // Adjust strictness
+        switch (children[i].getKind())
+        {
+          case Kind::GT:
+          case Kind::LT:
+          {
+            strict = true;
+            break;
+          }
+          case Kind::GEQ:
+          case Kind::LEQ:
+          case Kind::EQUAL:
+          {
+            break;
+          }
+          default:
+          {
+            Debug("arith::pf::check")
+                << "Bad kind: " << children[i].getKind() << std::endl;
+          }
+        }
+        // Check sign
+        switch (children[i].getKind())
+        {
+          case Kind::GT:
+          case Kind::GEQ:
+          {
+            if (scalar > 0)
+            {
+              Debug("arith::pf::check")
+                  << "Positive scalar for lower bound: " << scalar << " for "
+                  << children[i] << std::endl;
+              return Node::null();
+            }
+            break;
+          }
+          case Kind::LEQ:
+          case Kind::LT:
+          {
+            if (scalar < 0)
+            {
+              Debug("arith::pf::check")
+                  << "Negative scalar for upper bound: " << scalar << " for "
+                  << children[i] << std::endl;
+              return Node::null();
+            }
+            break;
+          }
+          case Kind::EQUAL:
+          {
+            break;
+          }
+          default:
+          {
+            Debug("arith::pf::check")
+                << "Bad kind: " << children[i].getKind() << std::endl;
+          }
+        }
+        leftSum << nm->mkNode(
+            Kind::MULT, children[i][0], nm->mkConst<Rational>(scalar));
+        rightSum << nm->mkNode(
+            Kind::MULT, children[i][1], nm->mkConst<Rational>(scalar));
+      }
+      Node r = nm->mkNode(strict ? Kind::LT : Kind::LEQ,
+                          leftSum.constructNode(),
+                          rightSum.constructNode());
+      return r;
+    }
+    case PfRule::INT_TIGHT_LB:
+    {
+      // Children: (P:(> i c))
+      //         where i has integer type.
+      // Arguments: none
+      // ---------------------
+      // Conclusion: (>= i leastIntGreaterThan(c)})
+      if (children.size() != 1
+          || (children[0].getKind() != Kind::GT
+              && children[0].getKind() != Kind::GEQ)
+          || !children[0][0].getType().isInteger()
+          || children[0][1].getKind() != Kind::CONST_RATIONAL)
+      {
+        Debug("arith::pf::check") << "Illformed input: " << children;
+        return Node::null();
+      }
+      else
+      {
+        Rational originalBound = children[0][1].getConst<Rational>();
+        Rational newBound = leastIntGreaterThan(originalBound);
+        auto nm = NodeManager::currentNM();
+        Node rational = nm->mkConst<Rational>(newBound);
+        return nm->mkNode(kind::GEQ, children[0][0], rational);
+      }
+    }
+    case PfRule::INT_TIGHT_UB:
+    {
+      // ======== Tightening Strict Integer Upper Bounds
+      // Children: (P:(< i c))
+      //         where i has integer type.
+      // Arguments: none
+      // ---------------------
+      // Conclusion: (<= i greatestIntLessThan(c)})
+      if (children.size() != 1
+          || (children[0].getKind() != Kind::LT
+              && children[0].getKind() != Kind::LEQ)
+          || !children[0][0].getType().isInteger()
+          || children[0][1].getKind() != Kind::CONST_RATIONAL)
+      {
+        Debug("arith::pf::check") << "Illformed input: " << children;
+        return Node::null();
+      }
+      else
+      {
+        Rational originalBound = children[0][1].getConst<Rational>();
+        Rational newBound = greatestIntLessThan(originalBound);
+        auto nm = NodeManager::currentNM();
+        Node rational = nm->mkConst<Rational>(newBound);
+        return nm->mkNode(kind::LEQ, children[0][0], rational);
+      }
+    }
+    case PfRule::ARITH_TRICHOTOMY:
+    {
+      Node a = negateProofLiteral(children[0]);
+      Node b = negateProofLiteral(children[1]);
+      Node c = args[0];
+      if (a[0] == b[0] && b[0] == c[0] && a[1] == b[1] && b[1] == c[1])
+      {
+        std::set<Kind> cmps;
+        cmps.insert(a.getKind());
+        cmps.insert(b.getKind());
+        cmps.insert(c.getKind());
+        if (cmps.count(Kind::EQUAL) == 0)
+        {
+          Debug("arith::pf::check") << "Error: No = " << std::endl;
+          return Node::null();
+        }
+        if (cmps.count(Kind::GT) == 0)
+        {
+          Debug("arith::pf::check") << "Error: No > " << std::endl;
+          return Node::null();
+        }
+        if (cmps.count(Kind::LT) == 0)
+        {
+          Debug("arith::pf::check") << "Error: No < " << std::endl;
+          return Node::null();
+        }
+        return args[0];
+      }
+      else
+      {
+        Debug("arith::pf::check")
+            << "Error: Different polynomials / values" << std::endl;
+        Debug("arith::pf::check") << "  a: " << a << std::endl;
+        Debug("arith::pf::check") << "  b: " << b << std::endl;
+        Debug("arith::pf::check") << "  c: " << c << std::endl;
+        return Node::null();
+      }
+      // Check that all have the same constant:
+    }
+    case PfRule::INT_TRUST:
+    {
+      Assert(args.size() == 1);
+      return args[0];
+    }
+    case PfRule::ARITH_OP_ELIM_AXIOM:
+    {
+      Assert(children.empty());
+      Assert(args.size() == 1);
+      return OperatorElim::getAxiomFor(args[0]);
+    }
+    default: return Node::null();
+  }
+}
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/arith/proof_checker.h b/src/theory/arith/proof_checker.h
new file mode 100644
index 000000000..b8a5d0df7
--- /dev/null
+++ b/src/theory/arith/proof_checker.h
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file proof_checker.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Arithmetic proof checker utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__ARITH__PROOF_CHECKER_H
+#define CVC4__THEORY__ARITH__PROOF_CHECKER_H
+
+#include "expr/node.h"
+#include "expr/proof_checker.h"
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+/** A checker for arithmetic reasoning in proofs */
+class ArithProofRuleChecker : public ProofRuleChecker
+{
+ public:
+  ArithProofRuleChecker() {}
+  ~ArithProofRuleChecker() {}
+
+  /** Register all rules owned by this rule checker into pc. */
+  void registerTo(ProofChecker* pc) override;
+
+ protected:
+  /** Return the conclusion of the given proof step, or null if it is invalid */
+  Node checkInternal(PfRule id,
+                     const std::vector<Node>& children,
+                     const std::vector<Node>& args) override;
+};
+
+}  // namespace arith
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__ARITH__PROOF_CHECKER_H */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 30b8ed01d..8b4747927 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -48,6 +48,7 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u,
     getExtTheory()->addFunctionKind(kind::EXPONENTIAL);
     getExtTheory()->addFunctionKind(kind::SINE);
     getExtTheory()->addFunctionKind(kind::PI);
+    getExtTheory()->addFunctionKind(kind::IAND);
   }
 }
 
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 2d3d8a28b..77efcfff7 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -87,6 +87,49 @@ public:
   }
 };/* class RealNullaryOperatorTypeRule */
 
+class IAndOpTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    if (n.getKind() != kind::IAND_OP)
+    {
+      InternalError() << "IAND_OP typerule invoked for IAND_OP kind";
+    }
+    TypeNode iType = nodeManager->integerType();
+    std::vector<TypeNode> argTypes;
+    argTypes.push_back(iType);
+    argTypes.push_back(iType);
+    return nodeManager->mkFunctionType(argTypes, iType);
+  }
+}; /* class IAndOpTypeRule */
+
+class IAndTypeRule
+{
+ public:
+  inline static TypeNode computeType(NodeManager* nodeManager,
+                                     TNode n,
+                                     bool check)
+  {
+    if (n.getKind() != kind::IAND)
+    {
+      InternalError() << "IAND typerule invoked for IAND kind";
+    }
+    if (check)
+    {
+      TypeNode arg1 = n[0].getType(check);
+      TypeNode arg2 = n[1].getType(check);
+      if (!arg1.isInteger() || !arg2.isInteger())
+      {
+        throw TypeCheckingExceptionPrivate(n, "expecting integer terms");
+      }
+    }
+    return nodeManager->integerType();
+  }
+}; /* class BitVectorConversionTypeRule */
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 49c7461e6..fda08bb0e 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -1673,7 +1673,6 @@ bool SygusExtension::checkValue(Node n,
   }
   TypeNode tn = n.getType();
   const DType& dt = tn.getDType();
-  Assert(dt.isSygus());
 
   // ensure that the expected size bound is met
   int cindex = utils::indexOf(vn.getOperator());
diff --git a/src/theory/quantifiers/candidate_rewrite_database.cpp b/src/theory/quantifiers/candidate_rewrite_database.cpp
index 0454b6412..fc3474df4 100644
--- a/src/theory/quantifiers/candidate_rewrite_database.cpp
+++ b/src/theory/quantifiers/candidate_rewrite_database.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/candidate_rewrite_database.h"
 
+#include "api/cvc4cpp.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
@@ -137,8 +138,15 @@ bool CandidateRewriteDatabase::addTerm(Node sol,
         // options as the SmtEngine we belong to, where we ensure that
         // produce-models is set.
         bool needExport = false;
-        ExprManager em(nm->getOptions());
-        std::unique_ptr<SmtEngine> rrChecker;
+
+        // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+        // This is only temporarily until we have separate options for each
+        // SmtEngine instance. We should reuse the same ExprManager with
+        // a different SmtEngine (and different options) here, eventually.
+        // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+        api::Solver slv(&nm->getOptions());
+        ExprManager* em = slv.getExprManager();
+        SmtEngine* rrChecker = slv.getSmtEngine();
         ExprManagerMapCollection varMap;
         initializeChecker(rrChecker, em, varMap, crr, needExport);
         Result r = rrChecker->checkSat();
@@ -175,7 +183,7 @@ bool CandidateRewriteDatabase::addTerm(Node sol,
               Assert(!refv.isNull() && refv.getKind() != BOUND_VARIABLE);
               if (needExport)
               {
-                Expr erefv = refv.toExpr().exportTo(&em, varMap);
+                Expr erefv = refv.toExpr().exportTo(em, varMap);
                 val = Node::fromExpr(rrChecker->getValue(erefv).exportTo(
                     nm->toExprManager(), varMap));
               }
diff --git a/src/theory/quantifiers/expr_miner.cpp b/src/theory/quantifiers/expr_miner.cpp
index 01a46d84a..b209fc6ff 100644
--- a/src/theory/quantifiers/expr_miner.cpp
+++ b/src/theory/quantifiers/expr_miner.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/expr_miner.h"
 
+#include "api/cvc4cpp.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
@@ -68,8 +69,8 @@ Node ExprMiner::convertToSkolem(Node n)
   return n.substitute(sfvs.begin(), sfvs.end(), sks.begin(), sks.end());
 }
 
-void ExprMiner::initializeChecker(std::unique_ptr<SmtEngine>& checker,
-                                  ExprManager& em,
+void ExprMiner::initializeChecker(SmtEngine* checker,
+                                  ExprManager* em,
                                   ExprManagerMapCollection& varMap,
                                   Node query,
                                   bool& needExport)
@@ -110,10 +111,16 @@ Result ExprMiner::doCheck(Node query)
       return Result(Result::SAT);
     }
   }
+  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+  // This is only temporarily until we have separate options for each
+  // SmtEngine instance. We should reuse the same ExprManager with
+  // a different SmtEngine (and different options) here, eventually.
+  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
   NodeManager* nm = NodeManager::currentNM();
   bool needExport = false;
-  ExprManager em(nm->getOptions());
-  std::unique_ptr<SmtEngine> smte;
+  api::Solver slv(&nm->getOptions());
+  ExprManager* em = slv.getExprManager();
+  SmtEngine* smte = slv.getSmtEngine();
   ExprManagerMapCollection varMap;
   initializeChecker(smte, em, varMap, queryr, needExport);
   return smte->checkSat();
diff --git a/src/theory/quantifiers/expr_miner.h b/src/theory/quantifiers/expr_miner.h
index d69ef45b4..eebcebf88 100644
--- a/src/theory/quantifiers/expr_miner.h
+++ b/src/theory/quantifiers/expr_miner.h
@@ -89,8 +89,8 @@ class ExprMiner
    * (for instance, model values) must be exported to the current expression
    * manager.
    */
-  void initializeChecker(std::unique_ptr<SmtEngine>& smte,
-                         ExprManager& em,
+  void initializeChecker(SmtEngine* smte,
+                         ExprManager* em,
                          ExprManagerMapCollection& varMap,
                          Node query,
                          bool& needExport);
diff --git a/src/theory/quantifiers/query_generator.cpp b/src/theory/quantifiers/query_generator.cpp
index 9f08ebec7..4cf65b24a 100644
--- a/src/theory/quantifiers/query_generator.cpp
+++ b/src/theory/quantifiers/query_generator.cpp
@@ -16,6 +16,8 @@
 #include "theory/quantifiers/query_generator.h"
 
 #include <fstream>
+
+#include "api/cvc4cpp.h"
 #include "options/quantifiers_options.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
@@ -157,9 +159,16 @@ void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
     Trace("sygus-qgen-check") << "  query: check " << qy << "..." << std::endl;
     NodeManager* nm = NodeManager::currentNM();
     // make the satisfiability query
+    //
+    // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+    // This is only temporarily until we have separate options for each
+    // SmtEngine instance. We should reuse the same ExprManager with
+    // a different SmtEngine (and different options) here, eventually.
+    // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
     bool needExport = false;
-    ExprManager em(nm->getOptions());
-    std::unique_ptr<SmtEngine> queryChecker;
+    api::Solver slv(&nm->getOptions());
+    ExprManager* em = slv.getExprManager();
+    SmtEngine* queryChecker = slv.getSmtEngine();
     ExprManagerMapCollection varMap;
     initializeChecker(queryChecker, em, varMap, qy, needExport);
     Result r = queryChecker->checkSat();
diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index de75af083..5784e42c0 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -735,8 +735,9 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
   {
     addSuccess = false;
     // try a new core
-    std::unique_ptr<SmtEngine> checkSol;
-    initializeSubsolver(checkSol);
+    std::unique_ptr<SmtEngine> checkSol(
+        new SmtEngine(NodeManager::currentNM()->toExprManager()));
+    initializeSubsolver(checkSol.get());
     Trace("sygus-ccore") << "----- Check candidate " << an << std::endl;
     std::vector<Node> rasserts = asserts;
     rasserts.push_back(d_sc);
@@ -775,8 +776,9 @@ Node CegisCoreConnective::constructSolutionFromPool(Component& ccheck,
         {
           // In terms of Variant #2, this is the check "if S ^ U is unsat"
           Trace("sygus-ccore") << "----- Check side condition" << std::endl;
-          std::unique_ptr<SmtEngine> checkSc;
-          initializeSubsolver(checkSc);
+          std::unique_ptr<SmtEngine> checkSc(
+              new SmtEngine(NodeManager::currentNM()->toExprManager()));
+          initializeSubsolver(checkSc.get());
           std::vector<Node> scasserts;
           scasserts.insert(scasserts.end(), uasserts.begin(), uasserts.end());
           scasserts.push_back(d_sc);
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 1c34bd73a..d34903805 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -14,6 +14,7 @@
 
 #include "theory/quantifiers/sygus/sygus_repair_const.h"
 
+#include "api/cvc4cpp.h"
 #include "options/base_options.h"
 #include "options/quantifiers_options.h"
 #include "printer/printer.h"
@@ -100,36 +101,6 @@ bool SygusRepairConst::isActive() const
   return !d_base_inst.isNull() && d_allow_constant_grammar;
 }
 
-void SygusRepairConst::initializeChecker(std::unique_ptr<SmtEngine>& checker,
-                                         ExprManager& em,
-                                         ExprManagerMapCollection& varMap,
-                                         Node query,
-                                         bool& needExport)
-{
-  if (options::sygusRepairConstTimeout.wasSetByUser())
-  {
-    // To support a separate timeout for the subsolver, we need to create
-    // a separate ExprManager with its own options. This requires that
-    // the expressions sent to the subsolver can be exported from on
-    // ExprManager to another.
-    initializeSubsolverWithExport(checker,
-                                  em,
-                                  varMap,
-                                  query.toExpr(),
-                                  true,
-                                  options::sygusRepairConstTimeout());
-    // renable options disabled by sygus
-    checker->setOption("miniscope-quant", true);
-    checker->setOption("miniscope-quant-fv", true);
-    checker->setOption("quant-split", true);
-  }
-  else
-  {
-    needExport = false;
-    initializeSubsolver(checker, query.toExpr());
-  }
-}
-
 bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
                                       const std::vector<Node>& candidate_values,
                                       std::vector<Node>& repair_cv,
@@ -258,11 +229,48 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
 
   Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
   // make the satisfiability query
+  //
+  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+  // This is only temporarily until we have separate options for each
+  // SmtEngine instance. We should reuse the same ExprManager with
+  // a different SmtEngine (and different options) here, eventually.
+  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
   bool needExport = true;
+  std::unique_ptr<SmtEngine> simpleSmte;
+  std::unique_ptr<api::Solver> slv;
+  ExprManager* em = nullptr;
+  SmtEngine* repcChecker = nullptr;
   ExprManagerMapCollection varMap;
-  ExprManager em(nm->getOptions());
-  std::unique_ptr<SmtEngine> repcChecker;
-  initializeChecker(repcChecker, em, varMap, fo_body, needExport);
+
+  if (options::sygusRepairConstTimeout.wasSetByUser())
+  {
+    // To support a separate timeout for the subsolver, we need to create
+    // a separate ExprManager with its own options. This requires that
+    // the expressions sent to the subsolver can be exported from on
+    // ExprManager to another.
+    slv.reset(new api::Solver(&nm->getOptions()));
+    em = slv->getExprManager();
+    repcChecker = slv->getSmtEngine();
+    initializeSubsolverWithExport(repcChecker,
+                                  em,
+                                  varMap,
+                                  fo_body.toExpr(),
+                                  true,
+                                  options::sygusRepairConstTimeout());
+    // renable options disabled by sygus
+    repcChecker->setOption("miniscope-quant", true);
+    repcChecker->setOption("miniscope-quant-fv", true);
+    repcChecker->setOption("quant-split", true);
+  }
+  else
+  {
+    needExport = false;
+    em = nm->toExprManager();
+    simpleSmte.reset(new SmtEngine(em));
+    repcChecker = simpleSmte.get();
+    initializeSubsolver(repcChecker, fo_body.toExpr());
+  }
+
   Result r = repcChecker->checkSat();
   Trace("sygus-repair-const") << "...got : " << r << std::endl;
   if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
@@ -279,7 +287,7 @@ bool SygusRepairConst::repairSolution(Node sygusBody,
     Node fov_m;
     if (needExport)
     {
-      Expr e_fov = fov.toExpr().exportTo(&em, varMap);
+      Expr e_fov = fov.toExpr().exportTo(em, varMap);
       fov_m = Node::fromExpr(
           repcChecker->getValue(e_fov).exportTo(nm->toExprManager(), varMap));
     }
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.h b/src/theory/quantifiers/sygus/sygus_repair_const.h
index dc721b42d..e02ca1f3e 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.h
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.h
@@ -209,26 +209,6 @@ class SygusRepairConst
    * If n is in the given logic, this method returns true.
    */
   bool getFitToLogicExcludeVar(LogicInfo& logic, Node n, Node& exvar);
-  /** initialize checker
-   *
-   * This function initializes the smt engine checker to check the
-   * satisfiability of the argument "query"
-   *
-   * The arguments em and varMap are used for supporting cases where we
-   * want checker to use a different expression manager instead of the current
-   * expression manager. The motivation for this so that different options can
-   * be set for the subcall.
-   *
-   * We update the flag needExport to true if checker is using the expression
-   * manager em. In this case, subsequent expressions extracted from smte
-   * (for instance, model values) must be exported to the current expression
-   * manager.
-   */
-  void initializeChecker(std::unique_ptr<SmtEngine>& checker,
-                         ExprManager& em,
-                         ExprManagerMapCollection& varMap,
-                         Node query,
-                         bool& needExport);
 };
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index f8349c834..590fdaa56 100644
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -169,8 +169,9 @@ void SynthEngine::assignConjecture(Node q)
     if (!sip.isPurelySingleInvocation() && sip.isNonGroundSingleInvocation())
     {
       // create new smt engine to do quantifier elimination
-      std::unique_ptr<SmtEngine> smt_qe;
-      initializeSubsolver(smt_qe);
+      std::unique_ptr<SmtEngine> smt_qe(
+          new SmtEngine(NodeManager::currentNM()->toExprManager()));
+      initializeSubsolver(smt_qe.get());
       Trace("cegqi-qep") << "Property is non-ground single invocation, run "
                             "QE to obtain single invocation."
                          << std::endl;
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index f38d2fbdb..6dce6ce1e 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1091,13 +1091,6 @@ bool QuantifiersEngine::getInstWhenNeedsCheck( Theory::Effort e ) {
   {
     performCheck = true;
   }
-  if( e==Theory::EFFORT_LAST_CALL ){
-    //with bounded integers, skip every other last call,
-    // since matching loops may occur with infinite quantification
-    if( d_ierCounter_lc%2==0 && options::fmfBound() ){
-      performCheck = false;
-    }
-  }
   return performCheck;
 }
 
diff --git a/src/theory/smt_engine_subsolver.cpp b/src/theory/smt_engine_subsolver.cpp
index 3386f3691..f529d3fea 100644
--- a/src/theory/smt_engine_subsolver.cpp
+++ b/src/theory/smt_engine_subsolver.cpp
@@ -15,6 +15,7 @@
 
 #include "theory/smt_engine_subsolver.h"
 
+#include "api/cvc4cpp.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/rewriter.h"
@@ -40,16 +41,14 @@ Result quickCheck(Node& query)
   return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
 }
 
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte)
+void initializeSubsolver(SmtEngine* smte)
 {
-  NodeManager* nm = NodeManager::currentNM();
-  smte.reset(new SmtEngine(nm->toExprManager()));
   smte->setIsInternalSubsolver();
   smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
 }
 
-void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte,
-                                   ExprManager& em,
+void initializeSubsolverWithExport(SmtEngine* smte,
+                                   ExprManager* em,
                                    ExprManagerMapCollection& varMap,
                                    Node query,
                                    bool needsTimeout,
@@ -62,14 +61,13 @@ void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte,
   // OptionException.
   try
   {
-    smte.reset(new SmtEngine(&em));
     smte->setIsInternalSubsolver();
     if (needsTimeout)
     {
       smte->setTimeLimit(timeout, true);
     }
     smte->setLogic(smt::currentSmtEngine()->getLogicInfo());
-    Expr equery = query.toExpr().exportTo(&em, varMap);
+    Expr equery = query.toExpr().exportTo(em, varMap);
     smte->assertFormula(equery);
   }
   catch (const CVC4::ExportUnsupportedException& e)
@@ -82,13 +80,13 @@ void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte,
   }
 }
 
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, Node query)
+void initializeSubsolver(SmtEngine* smte, Node query)
 {
   initializeSubsolver(smte);
   smte->assertFormula(query.toExpr());
 }
 
-Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte, Node query)
+Result checkWithSubsolver(SmtEngine* smte, Node query)
 {
   Assert(query.getType().isBoolean());
   Result r = quickCheck(query);
@@ -130,19 +128,33 @@ Result checkWithSubsolver(Node query,
     }
     return r;
   }
-  std::unique_ptr<SmtEngine> smte;
+
+  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+  // This is only temporarily until we have separate options for each
+  // SmtEngine instance. We should reuse the same ExprManager with
+  // a different SmtEngine (and different options) here, eventually.
+  // !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
+  std::unique_ptr<SmtEngine> simpleSmte;
+  std::unique_ptr<api::Solver> slv;
+  ExprManager* em = nullptr;
+  SmtEngine* smte = nullptr;
   ExprManagerMapCollection varMap;
   NodeManager* nm = NodeManager::currentNM();
-  ExprManager em(nm->getOptions());
   bool needsExport = false;
   if (needsTimeout)
   {
+    slv.reset(new api::Solver(&nm->getOptions()));
+    em = slv->getExprManager();
+    smte = slv->getSmtEngine();
     needsExport = true;
     initializeSubsolverWithExport(
         smte, em, varMap, query, needsTimeout, timeout);
   }
   else
   {
+    em = nm->toExprManager();
+    simpleSmte.reset(new SmtEngine(em));
+    smte = simpleSmte.get();
     initializeSubsolver(smte, query);
   }
   r = smte->checkSat();
@@ -153,7 +165,7 @@ Result checkWithSubsolver(Node query,
       Expr val;
       if (needsExport)
       {
-        Expr ev = v.toExpr().exportTo(&em, varMap);
+        Expr ev = v.toExpr().exportTo(em, varMap);
         val = smte->getValue(ev).exportTo(nm->toExprManager(), varMap);
       }
       else
diff --git a/src/theory/smt_engine_subsolver.h b/src/theory/smt_engine_subsolver.h
index 23308e12e..b606657bb 100644
--- a/src/theory/smt_engine_subsolver.h
+++ b/src/theory/smt_engine_subsolver.h
@@ -34,7 +34,7 @@ namespace theory {
  * This function initializes the smt engine smte as a subsolver, e.g. it
  * creates a new SMT engine and sets the options of the current SMT engine.
  */
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte);
+void initializeSubsolver(SmtEngine* smte);
 
 /**
  * Initialize Smt subsolver with exporting
@@ -52,14 +52,14 @@ void initializeSubsolver(std::unique_ptr<SmtEngine>& smte);
  * manager.
  *
  * @param smte The smt engine pointer to initialize
- * @param em Reference to the expression manager to use
+ * @param em Reference to the expression manager used by smte
  * @param varMap Map used for exporting expressions
  * @param query The query to check
  * @param needsTimeout Whether we would like to set a timeout
  * @param timeout The timeout (in milliseconds)
  */
-void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte,
-                                   ExprManager& em,
+void initializeSubsolverWithExport(SmtEngine* smte,
+                                   ExprManager* em,
                                    ExprManagerMapCollection& varMap,
                                    Node query,
                                    bool needsTimeout = false,
@@ -73,7 +73,7 @@ void initializeSubsolverWithExport(std::unique_ptr<SmtEngine>& smte,
  * exporting since the Options and ExprManager are tied together.
  * TODO: eliminate this dependency (cvc4-projects #120).
  */
-void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, Node query);
+void initializeSubsolver(SmtEngine* smte, Node query);
 
 /**
  * This returns the result of checking the satisfiability of formula query.
@@ -81,7 +81,7 @@ void initializeSubsolver(std::unique_ptr<SmtEngine>& smte, Node query);
  * If necessary, smte is initialized to the SMT engine that checked its
  * satisfiability.
  */
-Result checkWithSubsolver(std::unique_ptr<SmtEngine>& smte, Node query);
+Result checkWithSubsolver(SmtEngine* smte, Node query);
 
 /**
  * This returns the result of checking the satisfiability of formula query.
diff --git a/src/theory/strings/regexp_entail.cpp b/src/theory/strings/regexp_entail.cpp
index f005b2b42..7e1f42f37 100644
--- a/src/theory/strings/regexp_entail.cpp
+++ b/src/theory/strings/regexp_entail.cpp
@@ -48,6 +48,8 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
         do_next = false;
         Node xc = mchildren[mchildren.size() - 1];
         Node rc = children[children.size() - 1];
+        Trace("regexp-ext-rewrite-debug")
+            << "* " << xc << " in " << rc << std::endl;
         Assert(rc.getKind() != REGEXP_CONCAT);
         Assert(xc.getKind() != STRING_CONCAT);
         if (rc.getKind() == STRING_TO_REGEXP)
@@ -57,7 +59,15 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
             children.pop_back();
             mchildren.pop_back();
             do_next = true;
-            Trace("regexp-ext-rewrite-debug") << "...strip equal" << std::endl;
+            Trace("regexp-ext-rewrite-debug") << "- strip equal" << std::endl;
+          }
+          else if (rc[0].isConst() && Word::isEmpty(rc[0]))
+          {
+            Trace("regexp-ext-rewrite-debug")
+                << "- ignore empty RE" << std::endl;
+            // ignore and continue
+            children.pop_back();
+            do_next = true;
           }
           else if (xc.isConst() && rc[0].isConst())
           {
@@ -65,8 +75,8 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
             size_t index;
             Node s = Word::splitConstant(xc, rc[0], index, t == 0);
             Trace("regexp-ext-rewrite-debug")
-                << "CRE: Regexp const split : " << xc << " " << rc[0] << " -> "
-                << s << " " << index << " " << t << std::endl;
+                << "- CRE: Regexp const split : " << xc << " " << rc[0]
+                << " -> " << s << " " << index << " " << t << std::endl;
             if (s.isNull())
             {
               Trace("regexp-ext-rewrite-debug")
@@ -76,7 +86,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
             else
             {
               Trace("regexp-ext-rewrite-debug")
-                  << "...strip equal const" << std::endl;
+                  << "- strip equal const" << std::endl;
               children.pop_back();
               mchildren.pop_back();
               if (index == 0)
@@ -88,6 +98,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
                 children.push_back(nm->mkNode(STRING_TO_REGEXP, s));
               }
             }
+            Trace("regexp-ext-rewrite-debug") << "- split const" << std::endl;
             do_next = true;
           }
         }
@@ -97,7 +108,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
           CVC4::String s = xc.getConst<String>();
           if (Word::isEmpty(xc))
           {
-            Trace("regexp-ext-rewrite-debug") << "...ignore empty" << std::endl;
+            Trace("regexp-ext-rewrite-debug") << "- ignore empty" << std::endl;
             // ignore and continue
             mchildren.pop_back();
             do_next = true;
@@ -127,6 +138,8 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
             }
             else
             {
+              Trace("regexp-ext-rewrite-debug")
+                  << "...return false" << std::endl;
               return nm->mkConst(false);
             }
           }
@@ -135,19 +148,23 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
             // see if any/each child does not work
             bool result_valid = true;
             Node result;
-            Node emp_s = nm->mkConst(::CVC4::String(""));
+            Node emp_s = nm->mkConst(String(""));
             for (unsigned i = 0; i < rc.getNumChildren(); i++)
             {
               std::vector<Node> mchildren_s;
               std::vector<Node> children_s;
               mchildren_s.push_back(xc);
               utils::getConcat(rc[i], children_s);
+              Trace("regexp-ext-rewrite-debug") << push;
               Node ret = simpleRegexpConsume(mchildren_s, children_s, t);
+              Trace("regexp-ext-rewrite-debug") << pop;
               if (!ret.isNull())
               {
                 // one conjunct cannot be satisfied, return false
                 if (rc.getKind() == REGEXP_INTER)
                 {
+                  Trace("regexp-ext-rewrite-debug")
+                      << "...return " << ret << std::endl;
                   return ret;
                 }
               }
@@ -182,10 +199,15 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
               {
                 // all disjuncts cannot be satisfied, return false
                 Assert(rc.getKind() == REGEXP_UNION);
+                Trace("regexp-ext-rewrite-debug")
+                    << "...return false" << std::endl;
                 return nm->mkConst(false);
               }
               else
               {
+                Trace("regexp-ext-rewrite-debug")
+                    << "- same result, try again, children now " << children
+                    << std::endl;
                 // all branches led to the same result
                 children.pop_back();
                 mchildren.pop_back();
@@ -210,17 +232,19 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
             std::vector<Node> children_s;
             utils::getConcat(rc[0], children_s);
             Trace("regexp-ext-rewrite-debug")
-                << "...recursive call on body of star" << std::endl;
+                << "- recursive call on body of star" << std::endl;
+            Trace("regexp-ext-rewrite-debug") << push;
             Node ret = simpleRegexpConsume(mchildren_s, children_s, t);
+            Trace("regexp-ext-rewrite-debug") << pop;
             if (!ret.isNull())
             {
               Trace("regexp-ext-rewrite-debug")
-                  << "CRE : regexp star infeasable " << xc << " " << rc
+                  << "- CRE : regexp star infeasable " << xc << " " << rc
                   << std::endl;
               children.pop_back();
               if (!children.empty())
               {
-                Trace("regexp-ext-rewrite-debug") << "...continue" << std::endl;
+                Trace("regexp-ext-rewrite-debug") << "- continue" << std::endl;
                 do_next = true;
               }
             }
@@ -244,16 +268,22 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
                     std::reverse(mchildren_ss.begin(), mchildren_ss.end());
                     std::reverse(children_ss.begin(), children_ss.end());
                   }
-                  if (simpleRegexpConsume(mchildren_ss, children_ss, t)
-                          .isNull())
+                  Trace("regexp-ext-rewrite-debug")
+                      << "- recursive call required repeat star" << std::endl;
+                  Trace("regexp-ext-rewrite-debug") << push;
+                  Node rets = simpleRegexpConsume(mchildren_ss, children_ss, t);
+                  Trace("regexp-ext-rewrite-debug") << pop;
+                  if (rets.isNull())
                   {
                     can_skip = true;
                   }
                 }
                 if (!can_skip)
                 {
+                  TypeNode stype = nm->stringType();
+                  Node prev = utils::mkConcat(mchildren, stype);
                   Trace("regexp-ext-rewrite-debug")
-                      << "...can't skip" << std::endl;
+                      << "- can't skip" << std::endl;
                   // take the result of fully consuming once
                   if (t == 1)
                   {
@@ -262,12 +292,15 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
                   mchildren.clear();
                   mchildren.insert(
                       mchildren.end(), mchildren_s.begin(), mchildren_s.end());
-                  do_next = true;
+                  Node curr = utils::mkConcat(mchildren, stype);
+                  do_next = (prev != curr);
+                  Trace("regexp-ext-rewrite-debug")
+                      << "- do_next = " << do_next << std::endl;
                 }
                 else
                 {
                   Trace("regexp-ext-rewrite-debug")
-                      << "...can skip " << rc << " from " << xc << std::endl;
+                      << "- can skip " << rc << " from " << xc << std::endl;
                 }
               }
             }
@@ -276,7 +309,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
         if (!do_next)
         {
           Trace("regexp-ext-rewrite")
-              << "Cannot consume : " << xc << " " << rc << std::endl;
+              << "- cannot consume : " << xc << " " << rc << std::endl;
         }
       }
     }
@@ -286,6 +319,7 @@ Node RegExpEntail::simpleRegexpConsume(std::vector<Node>& mchildren,
       std::reverse(mchildren.begin(), mchildren.end());
     }
   }
+  Trace("regexp-ext-rewrite-debug") << "...finished, return null" << std::endl;
   return Node::null();
 }
 
diff --git a/src/theory/strings/sequences_rewriter.cpp b/src/theory/strings/sequences_rewriter.cpp
index 9df03f32c..20b892d0f 100644
--- a/src/theory/strings/sequences_rewriter.cpp
+++ b/src/theory/strings/sequences_rewriter.cpp
@@ -1315,9 +1315,13 @@ Node SequencesRewriter::rewriteMembership(TNode node)
           }
           else
           {
+            Node prev = retNode;
             retNode = nm->mkNode(
                 STRING_IN_REGEXP, utils::mkConcat(mchildren, stype), r);
-            success = true;
+            // Iterate again if the node changed. It may not have changed if
+            // nothing was consumed from mchildren (e.g. if the body of the
+            // re.* accepts the empty string.
+            success = (retNode != prev);
           }
         }
       }
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index eba5fb8c9..028288dbc 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -17,6 +17,7 @@ libcvc4_add_sources(
   floatingpoint.cpp
   gmp_util.h
   hash.h
+  iand.h
   index.cpp
   index.h
   maybe.h
diff --git a/src/util/iand.h b/src/util/iand.h
new file mode 100644
index 000000000..b5bc92960
--- /dev/null
+++ b/src/util/iand.h
@@ -0,0 +1,47 @@
+/*********************                                                        */
+/*! \file iand.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Anrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The integer AND operator.
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef CVC4__IAND_H
+#define CVC4__IAND_H
+
+#include <cstdint>
+#include <iosfwd>
+
+#include "base/exception.h"
+#include "util/integer.h"
+
+namespace CVC4 {
+
+struct CVC4_PUBLIC IntAnd
+{
+  unsigned d_size;
+  IntAnd(unsigned size) : d_size(size) {}
+  operator unsigned() const { return d_size; }
+}; /* struct IntAnd */
+
+/* -----------------------------------------------------------------------
+ ** Output stream
+ * ----------------------------------------------------------------------- */
+
+inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia) CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia)
+{
+  return os << "[" << ia.d_size << "]";
+}
+
+}  // namespace CVC4
+
+#endif /* CVC4__IAND_H */
diff --git a/src/util/iand.i b/src/util/iand.i
new file mode 100644
index 000000000..92c5a1223
--- /dev/null
+++ b/src/util/iand.i
@@ -0,0 +1,9 @@
+%{
+#include "util/iand.h"
+%}
+
+%rename(toUnsigned) CVC4::IntAnd::operator unsigned() const;
+
+%ignore CVC4::operator<<(std::ostream&, const IntAnd&);
+
+%include "util/iand.h"
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7863c5ec0..9a58457e6 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -966,6 +966,7 @@ set(regress_0_tests
   regress0/strings/issue3657-evalLeq.smt2
   regress0/strings/issue4070.smt2
   regress0/strings/issue4376.smt2
+  regress0/strings/issue4662-consume-nterm.smt2
   regress0/strings/itos-entail.smt2
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2
@@ -1526,6 +1527,7 @@ set(regress_1_tests
   regress1/quantifiers/dump-inst-i.smt2
   regress1/quantifiers/dump-inst-proof.smt2
   regress1/quantifiers/dump-inst.smt2
+  regress1/quantifiers/eqrange_ex_1.smt2
   regress1/quantifiers/ext-ex-deq-trigger.smt2
   regress1/quantifiers/extract-nproc.smt2
   regress1/quantifiers/f993-loss-easy.smt2
diff --git a/test/regress/regress0/strings/issue4662-consume-nterm.smt2 b/test/regress/regress0/strings/issue4662-consume-nterm.smt2
new file mode 100644
index 000000000..a87279b4c
--- /dev/null
+++ b/test/regress/regress0/strings/issue4662-consume-nterm.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_S)
+(set-info :status unsat)
+(declare-fun a () String)
+(define-fun b () RegLan (str.to_re "A"))
+(assert (str.in_re (str.++ "B" a) (re.+ (re.++ (re.opt b) (re.opt b)))))
+(check-sat)
diff --git a/test/regress/regress1/quantifiers/eqrange_ex_1.smt2 b/test/regress/regress1/quantifiers/eqrange_ex_1.smt2
new file mode 100644
index 000000000..ca53d7cf5
--- /dev/null
+++ b/test/regress/regress1/quantifiers/eqrange_ex_1.smt2
@@ -0,0 +1,160 @@
+(set-logic ALL)
+(set-info :status unsat)
+(set-option :produce-models true)
+(define-fun even_parity ((v (_ BitVec 8))) Bool (= (bvxor ((_ extract 0 0) v) ((_ extract 1 1) v) ((_ extract 2 2) v) ((_ extract 3 3) v) ((_ extract 4 4) v) ((_ extract 5 5) v) ((_ extract 6 6) v) ((_ extract 7 7) v)) #b0))
+(define-fun mem_readbv64 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64))) (_ BitVec 64) (concat (select m (bvadd a (_ bv7 64))) (concat (select m (bvadd a (_ bv6 64))) (concat (select m (bvadd a (_ bv5 64))) (concat (select m (bvadd a (_ bv4 64))) (concat (select m (bvadd a (_ bv3 64))) (concat (select m (bvadd a (_ bv2 64))) (concat (select m (bvadd a (_ bv1 64))) (select m a)))))))))
+(define-fun mem_writebv32 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64)) (v (_ BitVec 32))) (Array (_ BitVec 64) (_ BitVec 8)) (store (store (store (store m a ((_ extract 7 0) v)) (bvadd a (_ bv1 64)) ((_ extract 15 8) v)) (bvadd a (_ bv2 64)) ((_ extract 23 16) v)) (bvadd a (_ bv3 64)) ((_ extract 31 24) v)))
+(define-fun mem_writebv64 ((m (Array (_ BitVec 64) (_ BitVec 8))) (a (_ BitVec 64)) (v (_ BitVec 64))) (Array (_ BitVec 64) (_ BitVec 8)) (store (store (store (store (store (store (store (store m a ((_ extract 7 0) v)) (bvadd a (_ bv1 64)) ((_ extract 15 8) v)) (bvadd a (_ bv2 64)) ((_ extract 23 16) v)) (bvadd a (_ bv3 64)) ((_ extract 31 24) v)) (bvadd a (_ bv4 64)) ((_ extract 39 32) v)) (bvadd a (_ bv5 64)) ((_ extract 47 40) v)) (bvadd a (_ bv6 64)) ((_ extract 55 48) v)) (bvadd a (_ bv7 64)) ((_ extract 63 56) v)))
+(declare-fun fnstart_rcx () (_ BitVec 64))
+(declare-fun fnstart_rdx () (_ BitVec 64))
+(declare-fun fnstart_rbx () (_ BitVec 64))
+(declare-fun fnstart_rsp () (_ BitVec 64))
+(declare-fun fnstart_rbp () (_ BitVec 64))
+(declare-fun fnstart_rsi () (_ BitVec 64))
+(declare-fun fnstart_rdi () (_ BitVec 64))
+(declare-fun fnstart_r8 () (_ BitVec 64))
+(declare-fun fnstart_r9 () (_ BitVec 64))
+(declare-fun fnstart_r12 () (_ BitVec 64))
+(declare-fun fnstart_r13 () (_ BitVec 64))
+(declare-fun fnstart_r14 () (_ BitVec 64))
+(declare-fun fnstart_r15 () (_ BitVec 64))
+(declare-const stack_alloc_min (_ BitVec 64))
+(assert (= (bvand stack_alloc_min #x0000000000000fff) (_ bv0 64)))
+(assert (bvult (_ bv4096 64) stack_alloc_min))
+(define-fun stack_guard_min () (_ BitVec 64) (bvsub stack_alloc_min (_ bv4096 64)))
+(assert (bvult stack_guard_min stack_alloc_min))
+(declare-const stack_max (_ BitVec 64))
+(assert (= (bvand stack_max #x0000000000000fff) (_ bv0 64)))
+(assert (bvult stack_alloc_min stack_max))
+(assert (bvule stack_alloc_min fnstart_rsp))
+(assert (bvule fnstart_rsp (bvsub stack_max (_ bv8 64))))
+(define-fun on_stack ((a (_ BitVec 64)) (sz (_ BitVec 64))) Bool (let ((e (bvadd a sz))) (and (bvule stack_guard_min a) (bvule a e) (bvule e stack_max))))
+(define-fun not_in_stack_range ((a (_ BitVec 64)) (sz (_ BitVec 64))) Bool (let ((e (bvadd a sz))) (and (bvule a e) (or (bvule e stack_alloc_min) (bvule stack_max a)))))
+(assert (bvult fnstart_rsp (bvsub stack_max (_ bv8 64))))
+(assert (= ((_ extract 3 0) fnstart_rsp) (_ bv8 4)))
+(define-fun mc_only_stack_range ((a (_ BitVec 64)) (sz (_ BitVec 64))) Bool (let ((e (bvadd a sz))) (on_stack a sz)))
+(define-fun a201340_rip () (_ BitVec 64) #x0000000000201340)
+(declare-fun a201340_rax () (_ BitVec 64))
+(define-fun a201340_rcx () (_ BitVec 64) fnstart_rcx)
+(define-fun a201340_rdx () (_ BitVec 64) fnstart_rdx)
+(define-fun a201340_rbx () (_ BitVec 64) fnstart_rbx)
+(define-fun a201340_rsp () (_ BitVec 64) fnstart_rsp)
+(define-fun a201340_rbp () (_ BitVec 64) fnstart_rbp)
+(define-fun a201340_rsi () (_ BitVec 64) fnstart_rsi)
+(define-fun a201340_rdi () (_ BitVec 64) fnstart_rdi)
+(define-fun a201340_r8 () (_ BitVec 64) fnstart_r8)
+(define-fun a201340_r9 () (_ BitVec 64) fnstart_r9)
+(declare-fun a201340_r10 () (_ BitVec 64))
+(declare-fun a201340_r11 () (_ BitVec 64))
+(define-fun a201340_r12 () (_ BitVec 64) fnstart_r12)
+(define-fun a201340_r13 () (_ BitVec 64) fnstart_r13)
+(define-fun a201340_r14 () (_ BitVec 64) fnstart_r14)
+(define-fun a201340_r15 () (_ BitVec 64) fnstart_r15)
+(declare-fun a201340_cf () Bool)
+(declare-fun a201340_pf () Bool)
+(declare-fun a201340_af () Bool)
+(declare-fun a201340_zf () Bool)
+(declare-fun a201340_sf () Bool)
+(declare-fun a201340_tf () Bool)
+(declare-fun a201340_if () Bool)
+(define-fun a201340_df () Bool false)
+(declare-fun a201340_of () Bool)
+(declare-fun a201340_ie () Bool)
+(declare-fun a201340_de () Bool)
+(declare-fun a201340_ze () Bool)
+(declare-fun a201340_oe () Bool)
+(declare-fun a201340_ue () Bool)
+(declare-fun a201340_pe () Bool)
+(declare-fun a201340_ef () Bool)
+(declare-fun a201340_es () Bool)
+(declare-fun a201340_c0 () Bool)
+(declare-fun a201340_c1 () Bool)
+(declare-fun a201340_c2 () Bool)
+(declare-fun a201340_RESERVED_STATUS_11 () Bool)
+(declare-fun a201340_RESERVED_STATUS_12 () Bool)
+(declare-fun a201340_RESERVED_STATUS_13 () Bool)
+(declare-fun a201340_c3 () Bool)
+(declare-fun a201340_RESERVED_STATUS_15 () Bool)
+(define-fun a201340_x87top () (_ BitVec 3) (_ bv7 3))
+(declare-fun a201340_tag0 () (_ BitVec 2))
+(declare-fun a201340_tag1 () (_ BitVec 2))
+(declare-fun a201340_tag2 () (_ BitVec 2))
+(declare-fun a201340_tag3 () (_ BitVec 2))
+(declare-fun a201340_tag4 () (_ BitVec 2))
+(declare-fun a201340_tag5 () (_ BitVec 2))
+(declare-fun a201340_tag6 () (_ BitVec 2))
+(declare-fun a201340_tag7 () (_ BitVec 2))
+(declare-fun a201340_mm0 () (_ BitVec 80))
+(declare-fun a201340_mm1 () (_ BitVec 80))
+(declare-fun a201340_mm2 () (_ BitVec 80))
+(declare-fun a201340_mm3 () (_ BitVec 80))
+(declare-fun a201340_mm4 () (_ BitVec 80))
+(declare-fun a201340_mm5 () (_ BitVec 80))
+(declare-fun a201340_mm6 () (_ BitVec 80))
+(declare-fun a201340_mm7 () (_ BitVec 80))
+(declare-fun a201340_zmm0 () (_ BitVec 512))
+(declare-fun a201340_zmm1 () (_ BitVec 512))
+(declare-fun a201340_zmm2 () (_ BitVec 512))
+(declare-fun a201340_zmm3 () (_ BitVec 512))
+(declare-fun a201340_zmm4 () (_ BitVec 512))
+(declare-fun a201340_zmm5 () (_ BitVec 512))
+(declare-fun a201340_zmm6 () (_ BitVec 512))
+(declare-fun a201340_zmm7 () (_ BitVec 512))
+(declare-fun a201340_zmm8 () (_ BitVec 512))
+(declare-fun a201340_zmm9 () (_ BitVec 512))
+(declare-fun a201340_zmm10 () (_ BitVec 512))
+(declare-fun a201340_zmm11 () (_ BitVec 512))
+(declare-fun a201340_zmm12 () (_ BitVec 512))
+(declare-fun a201340_zmm13 () (_ BitVec 512))
+(declare-fun a201340_zmm14 () (_ BitVec 512))
+(declare-fun a201340_zmm15 () (_ BitVec 512))
+(declare-fun a201340_zmm16 () (_ BitVec 512))
+(declare-fun a201340_zmm17 () (_ BitVec 512))
+(declare-fun a201340_zmm18 () (_ BitVec 512))
+(declare-fun a201340_zmm19 () (_ BitVec 512))
+(declare-fun a201340_zmm20 () (_ BitVec 512))
+(declare-fun a201340_zmm21 () (_ BitVec 512))
+(declare-fun a201340_zmm22 () (_ BitVec 512))
+(declare-fun a201340_zmm23 () (_ BitVec 512))
+(declare-fun a201340_zmm24 () (_ BitVec 512))
+(declare-fun a201340_zmm25 () (_ BitVec 512))
+(declare-fun a201340_zmm26 () (_ BitVec 512))
+(declare-fun a201340_zmm27 () (_ BitVec 512))
+(declare-fun a201340_zmm28 () (_ BitVec 512))
+(declare-fun a201340_zmm29 () (_ BitVec 512))
+(declare-fun a201340_zmm30 () (_ BitVec 512))
+(declare-fun a201340_zmm31 () (_ BitVec 512))
+(declare-const x86mem_0 (Array (_ BitVec 64) (_ BitVec 8)))
+(define-fun return_addr () (_ BitVec 64) (mem_readbv64 x86mem_0 fnstart_rsp))
+(assert (= a201340_rbx fnstart_rbx))
+(assert (= a201340_rsp fnstart_rsp))
+(assert (= a201340_rbp fnstart_rbp))
+(assert (= a201340_r12 fnstart_r12))
+(assert (= a201340_r13 fnstart_r13))
+(assert (= a201340_r14 fnstart_r14))
+(assert (= a201340_r15 fnstart_r15))
+; LLVM: %t0 = call i64 (i64) @add(i64 42)
+(define-fun x86local_0 () (_ BitVec 64) (bvsub a201340_rsp (_ bv8 64)))
+(assert (mc_only_stack_range x86local_0 (_ bv8 64)))
+(define-fun x86mem_1 () (Array (_ BitVec 64) (_ BitVec 8)) (mem_writebv64 x86mem_0 x86local_0 a201340_rbp))
+(define-fun x86local_1 () Bool (distinct ((_ extract 64 64) (bvsub (bvsub ((_ sign_extend 1) x86local_0) (bvneg ((_ sign_extend 1) (_ bv16 64)))) (ite false (_ bv1 65) (_ bv0 65)))) ((_ extract 63 63) (bvsub (bvsub ((_ sign_extend 1) x86local_0) (bvneg ((_ sign_extend 1) (_ bv16 64)))) (ite false (_ bv1 65) (_ bv0 65))))))
+(define-fun x86local_2 () Bool (bvult x86local_0 (_ bv16 64)))
+(define-fun x86local_3 () (_ BitVec 64) (bvsub x86local_0 (_ bv16 64)))
+(define-fun x86local_4 () Bool (bvslt x86local_3 (_ bv0 64)))
+(define-fun x86local_5 () Bool (= x86local_3 (_ bv0 64)))
+(define-fun x86local_6 () (_ BitVec 8) ((_ extract 7 0) x86local_3))
+(define-fun x86local_7 () Bool (even_parity x86local_6))
+(define-fun x86local_8 () (_ BitVec 64) (bvadd x86local_0 (_ bv18446744073709551612 64)))
+(assert (mc_only_stack_range x86local_8 (_ bv4 64)))
+(define-fun x86mem_2 () (Array (_ BitVec 64) (_ BitVec 8)) (mem_writebv32 x86mem_1 x86local_8 (_ bv0 32)))
+(define-fun x86local_9 () (_ BitVec 64) (bvsub x86local_3 (_ bv8 64)))
+(assert (mc_only_stack_range x86local_9 (_ bv8 64)))
+(define-fun x86mem_3 () (Array (_ BitVec 64) (_ BitVec 8)) (mem_writebv64 x86mem_2 x86local_9 #x0000000000201359))
+(assert (= #x0000000000201320 #x0000000000201320))
+(assert (= (_ bv42 64) (_ bv42 64)))
+(assert (= (mem_readbv64 x86mem_3 x86local_9) #x0000000000201359))
+(declare-const x86mem_4 (Array (_ BitVec 64) (_ BitVec 8)))
+(assert (eqrange x86mem_4 x86mem_3 (bvadd x86local_9 (_ bv8 64)) (bvadd fnstart_rsp (_ bv7 64))))
+; LLVM: br label %block_0_201359
+(check-sat-assuming ((not (= (mem_readbv64 x86mem_4 (bvsub fnstart_rsp (_ bv8 64))) fnstart_rbp))))
+(exit)
diff --git a/test/system/CMakeLists.txt b/test/system/CMakeLists.txt
index 420ce8e6f..041d14295 100644
--- a/test/system/CMakeLists.txt
+++ b/test/system/CMakeLists.txt
@@ -32,5 +32,5 @@ cvc4_add_system_test(reset_assertions)
 cvc4_add_system_test(sep_log_api)
 cvc4_add_system_test(smt2_compliance)
 cvc4_add_system_test(statistics)
-cvc4_add_system_test(two_smt_engines)
+cvc4_add_system_test(two_solvers)
 # TODO: Move CVC4JavaTest.java to test/java and delete run_java_test (after full cmake migration)
diff --git a/test/system/boilerplate.cpp b/test/system/boilerplate.cpp
index 93f5dceb8..315cec7bf 100644
--- a/test/system/boilerplate.cpp
+++ b/test/system/boilerplate.cpp
@@ -19,18 +19,14 @@
 #include <iostream>
 #include <sstream>
 
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
+#include "api/cvc4cpp.h"
 
-using namespace CVC4;
+using namespace CVC4::api;
 using namespace std;
 
 int main() {
-  ExprManager em;
-  Options opts;
-  SmtEngine smt(&em);
-  Result r = smt.checkEntailed(em.mkConst(true));
-
-  return (Result::ENTAILED == r) ? 0 : 1;
+  Solver slv;
+  Result r = slv.checkEntailed(slv.mkBoolean(true));
+  return r.isEntailed() ? 0 : 1;
 }
 
diff --git a/test/system/reset_assertions.cpp b/test/system/reset_assertions.cpp
index 2a94dbd98..dc9bd24f6 100644
--- a/test/system/reset_assertions.cpp
+++ b/test/system/reset_assertions.cpp
@@ -20,34 +20,31 @@
 #include <iostream>
 #include <sstream>
 
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
+#include "api/cvc4cpp.h"
 
-using namespace CVC4;
+using namespace CVC4::api;
 
 int main()
 {
-  ExprManager em;
-  SmtEngine smt(&em);
-
-  smt.setOption("incremental", SExpr(true));
-
-  Type real = em.realType();
-  Expr x = em.mkVar("x", real);
-  Expr four = em.mkConst(Rational(4));
-  Expr xEqFour = em.mkExpr(Kind::EQUAL, x, four);
-  smt.assertFormula(xEqFour);
-  std::cout << smt.checkSat() << std::endl;
-
-  smt.resetAssertions();
-
-  Type elementType = em.integerType();
-  Type indexType = em.integerType();
-  Type arrayType = em.mkArrayType(indexType, elementType);
-  Expr array = em.mkVar("array", arrayType);
-  Expr arrayAtFour = em.mkExpr(Kind::SELECT, array, four);
-  Expr ten = em.mkConst(Rational(10));
-  Expr arrayAtFour_eq_ten = em.mkExpr(Kind::EQUAL, arrayAtFour, ten);
-  smt.assertFormula(arrayAtFour_eq_ten);
-  std::cout << smt.checkSat() << std::endl;
+  Solver slv;
+  slv.setOption("incremental", "true");
+
+  Sort real = slv.getRealSort();
+  Term x = slv.mkConst(real, "x");
+  Term four = slv.mkReal(4);
+  Term xEqFour = slv.mkTerm(Kind::EQUAL, x, four);
+  slv.assertFormula(xEqFour);
+  std::cout << slv.checkSat() << std::endl;
+
+  slv.resetAssertions();
+
+  Sort elementType = slv.getIntegerSort();
+  Sort indexType = slv.getIntegerSort();
+  Sort arrayType = slv.mkArraySort(indexType, elementType);
+  Term array = slv.mkConst(arrayType, "array");
+  Term arrayAtFour = slv.mkTerm(Kind::SELECT, array, four);
+  Term ten = slv.mkReal(10);
+  Term arrayAtFour_eq_ten = slv.mkTerm(Kind::EQUAL, arrayAtFour, ten);
+  slv.assertFormula(arrayAtFour_eq_ten);
+  std::cout << slv.checkSat() << std::endl;
 }
diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp
index 025aaed11..234246112 100644
--- a/test/system/statistics.cpp
+++ b/test/system/statistics.cpp
@@ -15,48 +15,52 @@
  ** minimally functional.
  **/
 
+#include "util/statistics.h"
+
 #include <iostream>
 #include <sstream>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr.h"
 #include "smt/smt_engine.h"
 #include "util/sexpr.h"
-#include "util/statistics.h"
 
 using namespace CVC4;
 using namespace std;
 
 int main() {
-  ExprManager em;
-  Options opts;
-  SmtEngine smt(&em);
-  smt.setOption("incremental", SExpr("true"));
-  Expr x = em.mkVar("x", em.integerType());
-  Expr y = em.mkVar("y", em.integerType());
-  smt.assertFormula(em.mkExpr(kind::GT, em.mkExpr(kind::PLUS, x, y), em.mkConst(Rational(5))));
-  Expr q = em.mkExpr(kind::GT, x, em.mkConst(Rational(0)));
-  Result r = smt.checkEntailed(q);
+  api::Solver slv;
+  ExprManager* em = slv.getExprManager();
+  SmtEngine* smt = slv.getSmtEngine();
+  smt->setOption("incremental", SExpr("true"));
+  Expr x = em->mkVar("x", em->integerType());
+  Expr y = em->mkVar("y", em->integerType());
+  smt->assertFormula(em->mkExpr(
+      kind::GT, em->mkExpr(kind::PLUS, x, y), em->mkConst(Rational(5))));
+  Expr q = em->mkExpr(kind::GT, x, em->mkConst(Rational(0)));
+  Result r = smt->checkEntailed(q);
 
   if (r != Result::NOT_ENTAILED)
   {
     exit(1);
   }
 
-  Statistics stats = smt.getStatistics();
+  Statistics stats = smt->getStatistics();
   for(Statistics::iterator i = stats.begin(); i != stats.end(); ++i) {
     cout << "stat " << (*i).first << " is " << (*i).second << endl;
   }
 
-  smt.assertFormula(em.mkExpr(kind::LT, y, em.mkConst(Rational(5))));
-  r = smt.checkEntailed(q);
-  Statistics stats2 = smt.getStatistics();
+  smt->assertFormula(em->mkExpr(kind::LT, y, em->mkConst(Rational(5))));
+  r = smt->checkEntailed(q);
+  Statistics stats2 = smt->getStatistics();
   bool different = false;
   for(Statistics::iterator i = stats2.begin(); i != stats2.end(); ++i) {
     cout << "stat1 " << (*i).first << " is " << stats.getStatistic((*i).first) << endl;
     cout << "stat2 " << (*i).first << " is " << (*i).second << endl;
-    if(smt.getStatistic((*i).first) != (*i).second) {
-      cout << "SMT engine reports different value for statistic "
-           << (*i).first << ": " << smt.getStatistic((*i).first) << endl;
+    if (smt->getStatistic((*i).first) != (*i).second)
+    {
+      cout << "SMT engine reports different value for statistic " << (*i).first
+           << ": " << smt->getStatistic((*i).first) << endl;
       exit(1);
     }
     different = different || stats.getStatistic((*i).first) != (*i).second;
diff --git a/test/system/two_smt_engines.cpp b/test/system/two_solvers.cpp
index 71676482e..c5bea4860 100644
--- a/test/system/two_smt_engines.cpp
+++ b/test/system/two_solvers.cpp
@@ -17,20 +17,16 @@
 #include <iostream>
 #include <sstream>
 
-#include "expr/expr.h"
-#include "smt/smt_engine.h"
+#include "api/cvc4cpp.h"
 
-using namespace CVC4;
+using namespace CVC4::api;
 using namespace std;
 
 int main() {
-  ExprManager em;
-  Options opts;
-  SmtEngine smt(&em);
-  SmtEngine smt2(&em);
-  Result r = smt.checkEntailed(em.mkConst(true));
-  Result r2 = smt2.checkEntailed(em.mkConst(true));
-
-  return r == Result::ENTAILED && r2 == Result::ENTAILED ? 0 : 1;
+  Solver s1;
+  Solver s2;
+  Result r = s1.checkEntailed(s1.mkBoolean(true));
+  Result r2 = s2.checkEntailed(s2.mkBoolean(true));
+  return r.isEntailed() && r2.isEntailed() ? 0 : 1;
 }
 
diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py
new file mode 100644
index 000000000..507aff2ae
--- /dev/null
+++ b/test/unit/api/python/test_sort.py
@@ -0,0 +1,322 @@
+import pytest
+
+import pycvc4
+from pycvc4 import kinds
+
+
+def testGetDatatype():
+    solver = pycvc4.Solver()
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+
+    # expecting no Error
+    dtypeSort.getDatatype()
+
+    bvSort = solver.mkBitVectorSort(32)
+    with pytest.raises(Exception):
+        # expect an exception
+        bvSort.getDatatype()
+
+
+def testDatatypeSorts():
+    solver = pycvc4.Solver()
+    intSort = solver.getIntegerSort()
+    # create datatype sort to test
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", intSort)
+    cons.addSelectorSelf("tail")
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+    dt = dtypeSort.getDatatype()
+    assert not dtypeSort.isConstructor()
+
+    with pytest.raises(Exception):
+        dtypeSort.getConstructorCodomainSort()
+
+    with pytest.raises(Exception):
+        dtypeSort.getConstructorDomainSorts()
+
+    with pytest.raises(Exception):
+        dtypeSort.getConstructorArity()
+
+    # get constructor
+    dcons = dt[0]
+    consTerm = dcons.getConstructorTerm()
+    consSort = consTerm.getSort()
+    assert consSort.isConstructor()
+    assert not consSort.isTester()
+    assert not consSort.isSelector()
+    assert consSort.getConstructorArity() == 2
+    consDomSorts = consSort.getConstructorDomainSorts()
+    assert consDomSorts[0] == intSort
+    assert consDomSorts[1] == dtypeSort
+    assert consSort.getConstructorCodomainSort() == dtypeSort
+
+    # get tester
+    isConsTerm = dcons.getTesterTerm()
+    assert isConsTerm.getSort().isTester()
+
+    # get selector
+    dselTail = dcons[1]
+    tailTerm = dselTail.getSelectorTerm()
+    assert tailTerm.getSort().isSelector()
+
+
+def testInstantiate():
+    solver = pycvc4.Solver()
+    # instantiate parametric datatype, check should not fail
+    sort = solver.mkParamSort("T")
+    paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort)
+    paramCons = solver.mkDatatypeConstructorDecl("cons")
+    paramNil = solver.mkDatatypeConstructorDecl("nil")
+    paramCons.addSelector("head", sort)
+    paramDtypeSpec.addConstructor(paramCons)
+    paramDtypeSpec.addConstructor(paramNil)
+    paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec)
+    paramDtypeSort.instantiate([solver.getIntegerSort()])
+
+    # instantiate non-parametric datatype sort, check should fail
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+
+    with pytest.raises(Exception):
+        dtypeSort.instantiate([solver.getIntegerSort()])
+
+
+def testGetFunctionArity():
+    solver = pycvc4.Solver()
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),
+                                            solver.getIntegerSort())
+    funSort.getFunctionArity()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getFunctionArity()
+
+
+def testGetFunctionDomainSorts():
+    solver = pycvc4.Solver()
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),
+                                            solver.getIntegerSort())
+    funSort.getFunctionDomainSorts()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getFunctionDomainSorts()
+
+
+def testGetFunctionCodomainSort():
+    solver = pycvc4.Solver()
+    funSort = solver.mkFunctionSort(solver.mkUninterpretedSort("u"),
+                                            solver.getIntegerSort())
+    funSort.getFunctionCodomainSort()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getFunctionCodomainSort()
+
+def testGetArrayIndexSort():
+    solver = pycvc4.Solver()
+    elementSort = solver.mkBitVectorSort(32)
+    indexSort = solver.mkBitVectorSort(32)
+    arraySort = solver.mkArraySort(indexSort, elementSort)
+    arraySort.getArrayIndexSort()
+
+    with pytest.raises(Exception):
+        indexSort.getArrayIndexSort()
+
+def testGetArrayElementSort():
+    solver = pycvc4.Solver()
+    elementSort = solver.mkBitVectorSort(32)
+    indexSort = solver.mkBitVectorSort(32)
+    arraySort = solver.mkArraySort(indexSort, elementSort)
+    arraySort.getArrayElementSort()
+
+    with pytest.raises(Exception):
+        indexSort.getArrayElementSort()
+
+def testGetSetElementSort():
+    solver = pycvc4.Solver()
+    setSort = solver.mkSetSort(solver.getIntegerSort())
+    setSort.getSetElementSort()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getSetElementSort()
+
+def testGetUninterpretedSortName():
+    solver = pycvc4.Solver()
+    uSort = solver.mkUninterpretedSort("u")
+    uSort.getUninterpretedSortName()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getUninterpretedSortName()
+
+def testIsUninterpretedSortParameterized():
+    solver = pycvc4.Solver()
+    uSort = solver.mkUninterpretedSort("u")
+    uSort.isUninterpretedSortParameterized()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.isUninterpretedSortParameterized()
+
+def testGetUninterpretedSortParamSorts():
+    solver = pycvc4.Solver()
+    uSort = solver.mkUninterpretedSort("u")
+    uSort.getUninterpretedSortParamSorts()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getUninterpretedSortParamSorts()
+
+def testGetUninterpretedSortConstructorName():
+    solver = pycvc4.Solver()
+    sSort = solver.mkSortConstructorSort("s", 2)
+    sSort.getSortConstructorName()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getSortConstructorName()
+
+def testGetUninterpretedSortConstructorArity():
+    solver = pycvc4.Solver()
+    sSort = solver.mkSortConstructorSort("s", 2)
+    sSort.getSortConstructorArity()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getSortConstructorArity()
+
+def testGetBVSize():
+    solver = pycvc4.Solver()
+    bvSort = solver.mkBitVectorSort(32)
+    bvSort.getBVSize()
+    setSort = solver.mkSetSort(solver.getIntegerSort())
+
+    with pytest.raises(Exception):
+        setSort.getBVSize()
+
+def testGetFPExponentSize():
+    solver = pycvc4.Solver()
+    fpSort = solver.mkFloatingPointSort(4, 8)
+    fpSort.getFPExponentSize()
+    setSort = solver.mkSetSort(solver.getIntegerSort())
+
+    with pytest.raises(Exception):
+        setSort.getFPExponentSize()
+
+def testGetFPSignificandSize():
+    solver = pycvc4.Solver()
+    fpSort = solver.mkFloatingPointSort(4, 8)
+    fpSort.getFPSignificandSize()
+    setSort = solver.mkSetSort(solver.getIntegerSort())
+
+    with pytest.raises(Exception):
+        setSort.getFPSignificandSize()
+
+def testGetDatatypeParamSorts():
+    solver = pycvc4.Solver()
+    # create parametric datatype, check should not fail
+    sort = solver.mkParamSort("T")
+    paramDtypeSpec = solver.mkDatatypeDecl("paramlist", sort)
+    paramCons = solver.mkDatatypeConstructorDecl("cons")
+    paramNil = solver.mkDatatypeConstructorDecl("nil")
+    paramCons.addSelector("head", sort)
+    paramDtypeSpec.addConstructor(paramCons)
+    paramDtypeSpec.addConstructor(paramNil)
+    paramDtypeSort = solver.mkDatatypeSort(paramDtypeSpec)
+    paramDtypeSort.getDatatypeParamSorts()
+    # create non-parametric datatype sort, check should fail
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+
+    with pytest.raises(Exception):
+        dtypeSort.getDatatypeParamSorts()
+
+
+def testGetDatatypeArity():
+    solver = pycvc4.Solver()
+    # create datatype sort, check should not fail
+    dtypeSpec = solver.mkDatatypeDecl("list")
+    cons = solver.mkDatatypeConstructorDecl("cons")
+    cons.addSelector("head", solver.getIntegerSort())
+    dtypeSpec.addConstructor(cons)
+    nil = solver.mkDatatypeConstructorDecl("nil")
+    dtypeSpec.addConstructor(nil)
+    dtypeSort = solver.mkDatatypeSort(dtypeSpec)
+    dtypeSort.getDatatypeArity()
+    # create bv sort, check should fail
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getDatatypeArity()
+
+def testGetTupleLength():
+    solver = pycvc4.Solver()
+    tupleSort = solver.mkTupleSort([solver.getIntegerSort(), solver.getIntegerSort()])
+    tupleSort.getTupleLength()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getTupleLength()
+
+def testGetTupleSorts():
+    solver = pycvc4.Solver()
+    tupleSort = solver.mkTupleSort([solver.getIntegerSort(), solver.getIntegerSort()])
+    tupleSort.getTupleSorts()
+    bvSort = solver.mkBitVectorSort(32)
+
+    with pytest.raises(Exception):
+        bvSort.getTupleSorts()
+
+def testSortCompare():
+    solver = pycvc4.Solver()
+    boolSort = solver.getBooleanSort()
+    intSort = solver.getIntegerSort()
+    bvSort = solver.mkBitVectorSort(32)
+    bvSort2 = solver.mkBitVectorSort(32)
+    assert bvSort >= bvSort2
+    assert bvSort <= bvSort2
+    assert (intSort > boolSort) != (intSort < boolSort)
+    assert (intSort > bvSort or intSort == bvSort) == (intSort >= bvSort)
+
+def testSortSubtyping():
+    solver = pycvc4.Solver()
+    intSort = solver.getIntegerSort()
+    realSort = solver.getRealSort()
+    assert intSort.isSubsortOf(realSort)
+    assert not realSort.isSubsortOf(intSort)
+    assert intSort.isComparableTo(realSort)
+    assert realSort.isComparableTo(intSort)
+
+    arraySortII = solver.mkArraySort(intSort, intSort)
+    arraySortIR = solver.mkArraySort(intSort, realSort)
+    assert not arraySortII.isComparableTo(intSort)
+    # we do not support subtyping for arrays
+    assert not arraySortII.isComparableTo(arraySortIR)
+
+    setSortI = solver.mkSetSort(intSort)
+    setSortR = solver.mkSetSort(realSort)
+    # we support subtyping for sets
+    assert setSortI.isSubsortOf(setSortR)
+    assert setSortR.isComparableTo(setSortI)
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index f080f5348..ddff63352 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -95,6 +95,7 @@ class SolverBlack : public CxxTest::TestSuite
   void testUFIteration();
 
   void testGetInfo();
+  void testGetInterpolant();
   void testGetOp();
   void testGetOption();
   void testGetUnsatAssumptions1();
@@ -1309,6 +1310,11 @@ void SolverBlack::testGetInfo()
   TS_ASSERT_THROWS(d_solver->getInfo("asdf"), CVC4ApiException&);
 }
 
+void SolverBlack::testGetInterpolant()
+{
+  // TODO
+}
+
 void SolverBlack::testGetOp()
 {
   Sort bv32 = d_solver->mkBitVectorSort(32);
diff --git a/test/unit/expr/attribute_black.h b/test/unit/expr/attribute_black.h
index f07612119..f671fc869 100644
--- a/test/unit/expr/attribute_black.h
+++ b/test/unit/expr/attribute_black.h
@@ -17,15 +17,16 @@
 #include <cxxtest/TestSuite.h>
 
 //Used in some of the tests
-#include <vector>
 #include <sstream>
+#include <vector>
 
+#include "api/cvc4cpp.h"
+#include "expr/attribute.h"
 #include "expr/expr_manager.h"
-#include "expr/node_value.h"
+#include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
-#include "expr/node.h"
-#include "expr/attribute.h"
+#include "expr/node_value.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 
@@ -35,27 +36,20 @@ using namespace CVC4::smt;
 using namespace std;
 
 class AttributeBlack : public CxxTest::TestSuite {
-private:
-
-  ExprManager* d_exprManager;
-  NodeManager* d_nodeManager;
-  SmtEngine* d_smtEngine;
-  SmtScope* d_scope;
-
  public:
   void setUp() override
   {
-    d_exprManager = new ExprManager();
+    d_slv = new api::Solver();
+    d_exprManager = d_slv->getExprManager();
     d_nodeManager = NodeManager::fromExprManager(d_exprManager);
-    d_smtEngine = new SmtEngine(d_exprManager);
+    d_smtEngine = d_slv->getSmtEngine();
     d_scope = new SmtScope(d_smtEngine);
   }
 
   void tearDown() override
   {
     delete d_scope;
-    delete d_smtEngine;
-    delete d_exprManager;
+    delete d_slv;
   }
 
   struct PrimitiveIntAttributeId {};
@@ -135,4 +129,10 @@ private:
     delete node;
   }
 
+ private:
+  api::Solver* d_slv;
+  ExprManager* d_exprManager;
+  NodeManager* d_nodeManager;
+  SmtEngine* d_smtEngine;
+  SmtScope* d_scope;
 };
diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
index d28553e08..c632b913e 100644
--- a/test/unit/expr/expr_manager_public.h
+++ b/test/unit/expr/expr_manager_public.h
@@ -19,56 +19,28 @@
 #include <sstream>
 #include <string>
 
-#include "expr/expr_manager.h"
-#include "expr/expr.h"
+#include "api/cvc4cpp.h"
 #include "base/exception.h"
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
 using namespace std;
 
 class ExprManagerPublic : public CxxTest::TestSuite {
-private:
-
-  ExprManager* d_exprManager;
-
-  void checkAssociative(Expr expr, Kind kind, unsigned int numChildren) {
-    std::vector<Expr> worklist;
-    worklist.push_back(expr);
-
-    unsigned int childrenFound = 0;
-
-    while( !worklist.empty() ) {
-      Expr current = worklist.back();
-      worklist.pop_back();
-      if( current.getKind() == kind ) {
-        for( unsigned int i = 0; i < current.getNumChildren(); ++i ) {
-          worklist.push_back( current[i] );
-        }
-      } else {
-        childrenFound++;
-      }
-    }
-
-    TS_ASSERT_EQUALS( childrenFound, numChildren );
-  }
-
-  std::vector<Expr> mkVars(Type type, unsigned int n) {
-    std::vector<Expr> vars;
-    for( unsigned int i = 0; i < n; ++i ) {
-      vars.push_back( d_exprManager->mkVar(type) );
-    }
-    return vars;
-  }
-
  public:
-  void setUp() override { d_exprManager = new ExprManager; }
+  void setUp() override
+  {
+    d_slv = new api::Solver();
+    d_exprManager = d_slv->getExprManager();
+  }
 
   void tearDown() override
   {
     try
     {
-      delete d_exprManager;
+      delete d_slv;
     }
     catch (Exception& e)
     {
@@ -128,4 +100,44 @@ private:
                      IllegalArgumentException&);
   }
 
+ private:
+  void checkAssociative(Expr expr, Kind kind, unsigned int numChildren)
+  {
+    std::vector<Expr> worklist;
+    worklist.push_back(expr);
+
+    unsigned int childrenFound = 0;
+
+    while (!worklist.empty())
+    {
+      Expr current = worklist.back();
+      worklist.pop_back();
+      if (current.getKind() == kind)
+      {
+        for (unsigned int i = 0; i < current.getNumChildren(); ++i)
+        {
+          worklist.push_back(current[i]);
+        }
+      }
+      else
+      {
+        childrenFound++;
+      }
+    }
+
+    TS_ASSERT_EQUALS(childrenFound, numChildren);
+  }
+
+  std::vector<Expr> mkVars(Type type, unsigned int n)
+  {
+    std::vector<Expr> vars;
+    for (unsigned int i = 0; i < n; ++i)
+    {
+      vars.push_back(d_exprManager->mkVar(type));
+    }
+    return vars;
+  }
+
+  api::Solver* d_slv;
+  ExprManager* d_exprManager;
 };
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 09452cc7a..86de45fe9 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -19,9 +19,10 @@
 #include <sstream>
 #include <string>
 
+#include "api/cvc4cpp.h"
 #include "base/exception.h"
-#include "expr/expr_manager.h"
 #include "expr/expr.h"
+#include "expr/expr_manager.h"
 #include "options/options.h"
 
 using namespace CVC4;
@@ -29,27 +30,6 @@ using namespace CVC4::kind;
 using namespace std;
 
 class ExprPublic : public CxxTest::TestSuite {
-private:
-
-  Options opts;
-
-  ExprManager* d_em;
-
-  Expr* a_bool;
-  Expr* b_bool;
-  Expr* c_bool_and;
-  Expr* and_op;
-  Expr* plus_op;
-  Type* fun_type;
-  Expr* fun_op;
-  Expr* d_apply_fun_bool;
-  Expr* null;
-
-  Expr* i1;
-  Expr* i2;
-  Expr* r1;
-  Expr* r2;
-
  public:
   void setUp() override
   {
@@ -62,7 +42,8 @@ private:
       free(argv[0]);
       free(argv[1]);
 
-      d_em = new ExprManager(opts);
+      d_slv = new api::Solver(&opts);
+      d_em = d_slv->getExprManager();
 
       a_bool = new Expr(d_em->mkVar("a", d_em->booleanType()));
       b_bool = new Expr(d_em->mkVar("b", d_em->booleanType()));
@@ -105,7 +86,7 @@ private:
       delete b_bool;
       delete a_bool;
 
-      delete d_em;
+      delete d_slv;
     }
     catch (Exception& e)
     {
@@ -466,4 +447,25 @@ private:
     TS_ASSERT(r1->getExprManager() == d_em);
     TS_ASSERT(r2->getExprManager() == d_em);
   }
+
+ private:
+  Options opts;
+
+  api::Solver* d_slv;
+  ExprManager* d_em;
+
+  Expr* a_bool;
+  Expr* b_bool;
+  Expr* c_bool_and;
+  Expr* and_op;
+  Expr* plus_op;
+  Type* fun_type;
+  Expr* fun_op;
+  Expr* d_apply_fun_bool;
+  Expr* null;
+
+  Expr* i1;
+  Expr* i2;
+  Expr* r1;
+  Expr* r2;
 };
diff --git a/test/unit/expr/node_algorithm_black.h b/test/unit/expr/node_algorithm_black.h
index 1f799cd40..7505215e7 100644
--- a/test/unit/expr/node_algorithm_black.h
+++ b/test/unit/expr/node_algorithm_black.h
@@ -32,13 +32,6 @@ using namespace CVC4::kind;
 
 class NodeAlgorithmBlack : public CxxTest::TestSuite
 {
- private:
-  NodeManager* d_nodeManager;
-  NodeManagerScope* d_scope;
-  TypeNode* d_intTypeNode;
-  TypeNode* d_boolTypeNode;
-  TypeNode* d_bvTypeNode;
-
  public:
   void setUp() override
   {
@@ -51,8 +44,9 @@ class NodeAlgorithmBlack : public CxxTest::TestSuite
 
   void tearDown() override
   {
-    delete d_intTypeNode;
+    delete d_bvTypeNode;
     delete d_boolTypeNode;
+    delete d_intTypeNode;
     delete d_scope;
     delete d_nodeManager;
   }
@@ -216,4 +210,11 @@ class NodeAlgorithmBlack : public CxxTest::TestSuite
     TS_ASSERT_EQUALS(subs.size(), 1);
     TS_ASSERT_EQUALS(subs[x], a);
   }
+
+ private:
+  NodeManager* d_nodeManager;
+  NodeManagerScope* d_scope;
+  TypeNode* d_intTypeNode;
+  TypeNode* d_boolTypeNode;
+  TypeNode* d_bvTypeNode;
 };
diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h
index 17bab05a4..12a55560d 100644
--- a/test/unit/expr/symbol_table_black.h
+++ b/test/unit/expr/symbol_table_black.h
@@ -19,6 +19,7 @@
 #include <sstream>
 #include <string>
 
+#include "api/cvc4cpp.h"
 #include "base/check.h"
 #include "base/exception.h"
 #include "context/context.h"
@@ -33,16 +34,13 @@ using namespace CVC4::context;
 using namespace std;
 
 class SymbolTableBlack : public CxxTest::TestSuite {
-private:
-
-  ExprManager* d_exprManager;
-
  public:
   void setUp() override
   {
     try
     {
-      d_exprManager = new ExprManager;
+      d_slv = new api::Solver();
+      d_exprManager = d_slv->getExprManager();
     }
     catch (Exception& e)
     {
@@ -54,7 +52,7 @@ private:
   void tearDown() override
   {
     try {
-      delete d_exprManager;
+      delete d_slv;
     }
     catch (Exception& e)
     {
@@ -164,4 +162,8 @@ private:
     // TODO: What kind of exception gets thrown here?
     TS_ASSERT_THROWS(symtab.popScope(), ScopeException&);
   }
+
+ private:
+  api::Solver* d_slv;
+  ExprManager* d_exprManager;
 };/* class SymbolTableBlack */
diff --git a/test/unit/expr/type_cardinality_public.h b/test/unit/expr/type_cardinality_public.h
index 29d9f5dc2..49d6bd9fd 100644
--- a/test/unit/expr/type_cardinality_public.h
+++ b/test/unit/expr/type_cardinality_public.h
@@ -17,12 +17,13 @@
 #include <cxxtest/TestSuite.h>
 
 #include <iostream>
-#include <string>
 #include <sstream>
+#include <string>
 
+#include "api/cvc4cpp.h"
+#include "expr/expr_manager.h"
 #include "expr/kind.h"
 #include "expr/type.h"
-#include "expr/expr_manager.h"
 #include "util/cardinality.h"
 
 using namespace CVC4;
@@ -30,12 +31,14 @@ using namespace CVC4::kind;
 using namespace std;
 
 class TypeCardinalityPublic : public CxxTest::TestSuite {
-  ExprManager* d_em;
-
  public:
-  void setUp() override { d_em = new ExprManager(); }
+  void setUp() override
+  {
+    d_slv = new api::Solver();
+    d_em = d_slv->getExprManager();
+  }
 
-  void tearDown() override { delete d_em; }
+  void tearDown() override { delete d_slv; }
 
   void testTheBasics()
   {
@@ -226,4 +229,7 @@ class TypeCardinalityPublic : public CxxTest::TestSuite {
     }
   }
 
+ private:
+  api::Solver* d_slv;
+  ExprManager* d_em;
 };/* TypeCardinalityPublic */
diff --git a/test/unit/theory/regexp_operation_black.h b/test/unit/theory/regexp_operation_black.h
index f42207c49..6e01392ab 100644
--- a/test/unit/theory/regexp_operation_black.h
+++ b/test/unit/theory/regexp_operation_black.h
@@ -14,17 +14,19 @@
  ** Unit tests for symbolic regular expression operations.
  **/
 
+#include <cxxtest/TestSuite.h>
+
+#include <iostream>
+#include <memory>
+#include <vector>
+
+#include "api/cvc4cpp.h"
 #include "expr/node.h"
 #include "expr/node_manager.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/strings/regexp_operation.h"
 
-#include <cxxtest/TestSuite.h>
-#include <iostream>
-#include <memory>
-#include <vector>
-
 using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::smt;
@@ -40,8 +42,9 @@ class RegexpOperationBlack : public CxxTest::TestSuite
   {
     Options opts;
     opts.setOutputLanguage(language::output::LANG_SMTLIB_V2);
-    d_em = new ExprManager(opts);
-    d_smt = new SmtEngine(d_em);
+    d_slv = new api::Solver();
+    d_em = d_slv->getExprManager();
+    d_smt = d_slv->getSmtEngine();
     d_scope = new SmtScope(d_smt);
     d_regExpOpr = new RegExpOpr();
 
@@ -56,8 +59,7 @@ class RegexpOperationBlack : public CxxTest::TestSuite
   {
     delete d_regExpOpr;
     delete d_scope;
-    delete d_smt;
-    delete d_em;
+    delete d_slv;
   }
 
   void includes(Node r1, Node r2)
@@ -147,6 +149,7 @@ class RegexpOperationBlack : public CxxTest::TestSuite
   }
 
  private:
+  api::Solver* d_slv;
   ExprManager* d_em;
   SmtEngine* d_smt;
   SmtScope* d_scope;
diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index 37999b73a..45d13d416 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -17,14 +17,15 @@
 #include <cxxtest/TestSuite.h>
 
 //Used in some of the tests
-#include <vector>
 #include <sstream>
+#include <vector>
 
+#include "api/cvc4cpp.h"
 #include "expr/expr_manager.h"
-#include "expr/node_value.h"
+#include "expr/node.h"
 #include "expr/node_builder.h"
 #include "expr/node_manager.h"
-#include "expr/node.h"
+#include "expr/node_value.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
 #include "theory/rewriter.h"
@@ -40,8 +41,9 @@ class TheoryBlack : public CxxTest::TestSuite {
  public:
   void setUp() override
   {
-    d_em = new ExprManager();
-    d_smt = new SmtEngine(d_em);
+    d_slv = new api::Solver();
+    d_em = d_slv->getExprManager();
+    d_smt = d_slv->getSmtEngine();
     d_scope = new SmtScope(d_smt);
     // Ensure that the SMT engine is fully initialized (required for the
     // rewriter)
@@ -53,8 +55,7 @@ class TheoryBlack : public CxxTest::TestSuite {
   void tearDown() override
   {
     delete d_scope;
-    delete d_smt;
-    delete d_em;
+    delete d_slv;
   }
 
   void testArrayConst() {
@@ -149,6 +150,7 @@ class TheoryBlack : public CxxTest::TestSuite {
   }
 
  private:
+  api::Solver* d_slv;
   ExprManager* d_em;
   SmtEngine* d_smt;
   NodeManager* d_nm;
diff --git a/test/unit/util/array_store_all_black.h b/test/unit/util/array_store_all_black.h
index 3b00fa192..bf0163317 100644
--- a/test/unit/util/array_store_all_black.h
+++ b/test/unit/util/array_store_all_black.h
@@ -16,6 +16,7 @@
 
 #include <cxxtest/TestSuite.h>
 
+#include "api/cvc4cpp.h"
 #include "expr/array_store_all.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
@@ -27,18 +28,14 @@ using namespace CVC4;
 using namespace std;
 
 class ArrayStoreAllBlack : public CxxTest::TestSuite {
-  ExprManager* d_em;
-
  public:
   void setUp() override
   {
-    d_em = new ExprManager();
+    d_slv = new api::Solver();
+    d_em = d_slv->getExprManager();
   }
 
-  void tearDown() override
-  {
-    delete d_em;
-  }
+  void tearDown() override { delete d_slv; }
 
   void testStoreAll() {
     Type usort = d_em->mkSort("U");
@@ -80,4 +77,7 @@ class ArrayStoreAllBlack : public CxxTest::TestSuite {
                                    d_em->mkConst(Rational(0)))));
   }
 
+ private:
+  api::Solver* d_slv;
+  ExprManager* d_em;
 }; /* class ArrayStoreAllBlack */
diff --git a/test/unit/util/datatype_black.h b/test/unit/util/datatype_black.h
index f69cc12ea..ac27acfb5 100644
--- a/test/unit/util/datatype_black.h
+++ b/test/unit/util/datatype_black.h
@@ -15,8 +15,10 @@
  **/
 
 #include <cxxtest/TestSuite.h>
+
 #include <sstream>
 
+#include "api/cvc4cpp.h"
 #include "expr/datatype.h"
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
@@ -27,14 +29,11 @@ using namespace CVC4;
 using namespace std;
 
 class DatatypeBlack : public CxxTest::TestSuite {
-
-  ExprManager* d_em;
-  ExprManagerScope* d_scope;
-
  public:
   void setUp() override
   {
-    d_em = new ExprManager();
+    d_slv = new api::Solver();
+    d_em = d_slv->getExprManager();
     d_scope = new ExprManagerScope(*d_em);
     Debug.on("datatypes");
     Debug.on("groundterms");
@@ -43,7 +42,7 @@ class DatatypeBlack : public CxxTest::TestSuite {
   void tearDown() override
   {
     delete d_scope;
-    delete d_em;
+    delete d_slv;
   }
 
   void testEnumeration() {
@@ -436,4 +435,8 @@ class DatatypeBlack : public CxxTest::TestSuite {
     TS_ASSERT_EQUALS(TypeNode::leastCommonTypeNode(TypeNode::fromType(pairIntInt), TypeNode::fromType(pairIntInt)).toType(), pairIntInt);
   }
 
+ private:
+  api::Solver* d_slv;
+  ExprManager* d_em;
+  ExprManagerScope* d_scope;
 };/* class DatatypeBlack */