Merge branch 'master' into smtcompoptssmtcompopts

44 files changed, 614 insertions, 160 deletions

diff --git a/docs/api/cpp/kind.rst b/docs/api/cpp/kind.rst
index 579407c85..4c07804a4 100644
--- a/docs/api/cpp/kind.rst
+++ b/docs/api/cpp/kind.rst
@@ -4,14 +4,8 @@ Kind
 Every :cpp:class:`Term <cvc5::api::Term>` has a kind which represents its type,
 for example whether it is an equality (:cpp:enumerator:`EQUAL
 <cvc5::api::Kind::EQUAL>`), a conjunction (:cpp:enumerator:`AND
-<cvc5::api::Kind::AND>`), or a bitvector addition
-(:cpp:enumerator:`BITVECTOR_PLUS <cvc5::api::Kind::BITVECTOR_PLUS>`).
-#ifndef DOXYGEN_SKIP
-Note that the API type :cpp:enum:`cvc5::api::Kind` roughly corresponds to
-:cpp:enum:`cvc5::Kind`, but is a different type. It hides internal kinds that
-should not be exported to the API, and maps all kinds that we want to export
-to its corresponding internal kinds.
-#endif
+<cvc5::api::Kind::AND>`), or a bit-vector addition
+(:cpp:enumerator:`BITVECTOR_ADD <cvc5::api::Kind::BITVECTOR_ADD>`).
 
 .. doxygenenum:: cvc5::api::Kind
     :project: cvc5
diff --git a/docs/ext/smtliblexer.py b/docs/ext/smtliblexer.py
index 5dd54d006..2ce860e39 100644
--- a/docs/ext/smtliblexer.py
+++ b/docs/ext/smtliblexer.py
@@ -9,13 +9,17 @@ class SmtLibLexer(RegexLexer):
         'root': [
             (r'QF_BV', token.Text),
             (r'QF_UFDT', token.Text),
-            (r'ALL_SUPPORTED', token.Text),
+            (r'ALL', token.Text),
+            (r'QF_ALL', token.Text),
+            (r'set-info', token.Keyword),
             (r'set-logic', token.Keyword),
             (r'set-option', token.Keyword),
             (r'declare-codatatypes', token.Keyword),
             (r'declare-const', token.Keyword),
+            (r'declare-datatype', token.Keyword),
             (r'declare-datatypes', token.Keyword),
             (r'declare-fun', token.Keyword),
+            (r'declare-sort', token.Keyword),
             (r'define-fun', token.Keyword),
             (r'assert\b', token.Keyword),
             (r'check-sat-assuming', token.Keyword),
@@ -32,6 +36,7 @@ class SmtLibLexer(RegexLexer):
             (r':produce-models', token.Name.Attribute),
             (r':produce-unsat-cores', token.Name.Attribute),
             (r':produce-unsat-assumptions', token.Name.Attribute),
+            (r':status', token.Name.Attribute),
             (r'!', token.Name.Attribute),
             (r'BitVec', token.Name.Attribute),
             (r'RNE', token.Name.Attribute),
@@ -48,11 +53,15 @@ class SmtLibLexer(RegexLexer):
             (r'bvult', token.Operator),
             (r'bvule', token.Operator),
             (r'bvsdiv', token.Operator),
+            (r'emp', token.Operator),
             (r'extract', token.Operator),
             (r'fp.gt', token.Operator),
             (r'ite', token.Operator),
             (r'mkTuple', token.Operator),
             (r'to_fp_unsigned', token.Operator),
+            (r'pto', token.Operator),
+            (r'sep', token.Operator),
+            (r'wand', token.Operator),
             (r'\+zero', token.Operator),
             (r'#b[0-1]+', token.Text),
             (r'bv[0-9]+', token.Text),
diff --git a/docs/theories/separation-logic.rst b/docs/theories/separation-logic.rst
new file mode 100644
index 000000000..c2dcda78e
--- /dev/null
+++ b/docs/theories/separation-logic.rst
@@ -0,0 +1,154 @@
+Theory Reference: Separation Logic
+==================================
+
+cvc5 supports a syntax for separation logic as an extension of the SMT-LIB 2
+language.
+
+Signature
+---------
+
+Given a (decidable) base theory :math:`T`, cvc5 has a
+`decision procedure <https://cvc4.github.io/publications/2016/RIS+16.pdf>`__
+for quantifier-free :math:`SL(T)_{Loc,Data}` formulas, where :math:`Loc` and
+:math:`Data` are any sort belonging to :math:`T`.
+
+A :math:`SL(T)_{Loc,Data}` formula is one from the following grammar:
+
+.. code::
+
+  F : L | (emp t u) | (pto t u) | (sep F1 ... Fn) | (wand F1 F2) | ~F1 | F1 op ... op Fn
+
+where ``op`` is any classical Boolean connective, ``t`` and ``u`` are terms
+built from symbols in the signature of :math:`T` of sort :math:`Loc` and
+:math:`Data` respectively, and :math:`L` is a :math:`T`-literal.
+
+The operator ``emp`` denotes the empty heap constraint, the operator ``pto``
+denotes the points-to predicate, the operator ``sep`` denotes separation start
+and is variadic, and the operator ``wand`` denote magic wand.
+
+Semantics
+---------
+
+A satisfiability relation :math:`I,h \models_{SL} \varphi` is defined for
+:math:`SL(T)_{Loc,Data}` formulas :math:`\varphi`,
+where :math:`I` is an interpretation, and :math:`h` is a heap.
+
+The semantics of separation logic operators are as follows:
+
++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+
+| :math:`I,h \models_{SL} L`                                  | Iff  | :math:`I \models L`, if :math:`L` is a :math:`T`-literal                            |
++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+
+| :math:`I,h \models_{SL}` (emp :math:`t \ u`)                | Iff  | :math:`h = \emptyset`                                                               |
++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+
+| :math:`I,h \models_{SL}` (pto :math:`t \ u`)                | Iff  | :math:`h = \{(t^I,u^I)\} \text{ and } t^I\not=nil^I`                                |
++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+
+| :math:`I,h \models_{SL}` (sep :math:`\phi_1 \ldots \phi_n)` | Iff  | there exist heaps :math:`h_1,\ldots,h_n` s.t. :math:`h=h_1\uplus \ldots \uplus h_n` |
+|                                                             |      |                                                                                     |
+|                                                             |      | and :math:`I,h_i \models_{SL} \phi_i, i = 1,\ldots,n`                               |
++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+
+| :math:`I,h \models_{SL}` (wand :math:`\phi_1 \ \phi_2`)     | Iff  | for all heaps :math:`h'` if :math:`h'\#h` and :math:`I,h' \models_{SL} \phi_1`      |
+|                                                             |      |                                                                                     |
+|                                                             |      | then :math:`I,h'\uplus h \models_{SL} \phi_2`                                       |
++-------------------------------------------------------------+------+-------------------------------------------------------------------------------------+
+
+where :math:`h_1 \uplus \ldots \uplus h_n` denotes the disjoint union of heaps
+:math:`h_1, \ldots, h_n` and :math:`h'\#h` denotes that heaps :math:`h'` and
+:math:`h` are disjoint, and :math:`nil` is a distinguished variable of sort
+:math:`Loc`.
+All classical Boolean connectives are interpreted as expected.
+
+.. note::
+  The arguments of ``emp`` are used to denote the sort of the heap and have no
+  meaning otherwise.
+
+Syntax
+------
+
+Separation logic in cvc5 requires the ``QF_ALL`` logic.
+
+The syntax for the operators of separation logic is summarized in the following
+table.
+For the C++ API examples in this table, we assume that we have created
+a :cpp:class:`cvc5::api::Solver` object.
+
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+|                      | SMTLIB language                              | C++ API                                                            |
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+| Logic String         | ``(set-logic QF_ALL)``                       | ``solver.setLogic("QF_ALL");``                                     |
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+| Empty Heap           | ``(_ emp <Sort_1> <Sort_2>)``                | ``solver.mkTerm(Kind::SEP_EMP, x, y);``                            |
+|                      |                                              |                                                                    |
+|                      |                                              | where ``x`` and ``y`` are of sort ``<Sort_1>`` and ``<Sort_2>``    |
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+| Points-To            | ``(pto x y)``                                | ``solver.mkTerm(Kind::SEP_PTO, x, y);``                            |
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+| Separation Star      | ``(sep c1 .. cn)``                           | ``solver.mkTerm(Kind::SEP_STAR, {c1, ..., cn});``                  |
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+| Magic Wand           | ``(wand c1 c1)``                             | ``solver.mkTerm(Kind::SEP_WAND, c1, c2);``                         |
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+| Nil Element          | ``(as nil <Sort>)``                          | ``solver.mkSepNil(cvc5::api::Sort sort);``                         |
++----------------------+----------------------------------------------+--------------------------------------------------------------------+
+
+
+Examples
+--------
+
+The following input on heaps ``Int -> Int`` is unsatisfiable:
+
+.. code:: smtlib
+
+  (set-logic QF_ALL)
+  (set-info :status unsat)
+  (declare-const x Int)
+  (declare-const a Int)
+  (declare-const b Int)
+  (assert (and (pto x a) (pto x b)))
+  (assert (not (= a b)))
+  (check-sat)
+
+
+The following input on heaps ``U -> Int`` is satisfiable. Notice that the
+formula ``(not (emp x 0))`` is satisfied by heaps ``U -> Int`` (the sorts of
+``x`` and ``0`` respectively) whose domain is non-empty.
+
+.. code:: smtlib
+
+  (set-logic QF_ALL)
+  (set-info :status sat)
+  (declare-sort U 0)
+  (declare-const x U)
+  (declare-const a Int)
+  (assert (and (not (_ emp U Int)) (pto x a)))
+  (check-sat)
+
+The following input on heaps ``Int -> Node`` is satisfiable, where ``Node``
+denotes a user-defined inductive `datatypes <datatypes>`__.
+
+.. code:: smtlib
+
+  (set-logic QF_ALL)
+  (set-info :status sat)
+  (declare-const x Int)
+  (declare-const y Int)
+  (declare-const z Int)
+  (declare-datatype Node ((node (data Int) (left Int) (right Int))))
+  (assert (pto x (node 0 y z)))
+  (check-sat)
+
+.. note::
+
+  Given a separation logic input, the sorts :math:`Loc` and :math:`Data` are
+  inferred by cvc5, and must be consistent across all predicates occurring in
+  an input.
+  cvc5 does not accept an input such as:
+
+  .. code:: smtlib
+
+    (set-logic QF_ALL)
+    (declare-sort U 0)
+    (declare-const x U)
+    (assert (and (pto x 0) (pto 1 2)))
+    (check-sat)
+
+  since the sorts of the first arguments of the points-to predicates do not
+  agree.
diff --git a/docs/theory.rst b/docs/theory.rst
index 45be41b2e..f0b25aea4 100644
--- a/docs/theory.rst
+++ b/docs/theory.rst
@@ -5,3 +5,4 @@ Theory References
    :maxdepth: 1
 
    theories/datatypes
+   theories/separation-logic
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 775e04b9c..1edafb977 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -52,6 +52,8 @@ libcvc5_add_sources(
   omt/omt_optimizer.h
   preprocessing/assertion_pipeline.cpp
   preprocessing/assertion_pipeline.h
+  preprocessing/learned_literal_manager.cpp
+  preprocessing/learned_literal_manager.h
   preprocessing/passes/ackermann.cpp
   preprocessing/passes/ackermann.h
   preprocessing/passes/apply_substs.cpp
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index b4596e977..be9083960 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -33,9 +33,15 @@ namespace api {
 /**
  * The kind of a cvc5 term.
  *
- * Note that the underlying type of Kind must be signed (to enable range
- * checks for validity). The size of this type depends on the size of
- * cvc5::Kind (NodeValue::NBITS_KIND, currently 10 bits, see expr/node_value.h).
+ * \internal
+ *
+ * Note that the API type `cvc5::api::Kind` roughly corresponds to
+ * `cvc5::Kind`, but is a different type. It hides internal kinds that should
+ * not be exported to the API, and maps all kinds that we want to export to its
+ * corresponding internal kinds. The underlying type of `cvc5::api::Kind` must
+ * be signed (to enable range checks for validity). The size of this type
+ * depends on the size of `cvc5::Kind` (`NodeValue::NBITS_KIND`, currently 10
+ * bits, see expr/node_value.h).
  */
 enum CVC5_EXPORT Kind : int32_t
 {
diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 3339543f3..258005207 100644
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -740,6 +740,21 @@ cdef class Solver:
         return term
 
     def mkReal(self, val, den=None):
+        '''
+        Make a real number term.
+
+        Really, makes a rational term.
+
+        Can be used in various forms.
+        * Given a string "N/D" constructs the corresponding rational.
+        * Given a string "W.D" constructs the reduction of (W * P + D)/P, where
+          P is the appropriate power of 10.
+        * Given a float f, constructs the rational matching f's string
+          representation. This means that mkReal(0.3) gives 3/10 and not the
+          IEEE-754 approximation of 3/10.
+        * Given a string "W" or an integer, constructs that integer.
+        * Given two strings and/or integers N and D, constructs N/D.
+        '''
         cdef Term term = Term(self)
         if den is None:
             term.cterm = self.csolver.mkReal(str(val).encode())
@@ -1766,12 +1781,14 @@ cdef class Term:
         return self.cterm.isRealValue()
 
     def getRealValue(self):
-        return float(Fraction(self.cterm.getRealValue().decode()))
+        '''Returns the value of a real term as a Fraction'''
+        return Fraction(self.cterm.getRealValue().decode())
 
     def isBitVectorValue(self):
         return self.cterm.isBitVectorValue()
 
     def getBitVectorValue(self, base = 2):
+        '''Returns the value of a bit-vector term as a 0/1 string'''
         return self.cterm.getBitVectorValue(base).decode()
 
     def toPythonObj(self):
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 1e6a38815..fe7d75ca3 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -528,10 +528,6 @@ TypeNode NodeManager::mkBagType(TypeNode elementType)
 {
   CheckArgument(
       !elementType.isNull(), elementType, "unexpected NULL element type");
-  CheckArgument(elementType.isFirstClass(),
-                elementType,
-                "cannot store types that are not first-class in bags. Try "
-                "option --uf-ho.");
   Debug("bags") << "making bags type " << elementType << std::endl;
   return mkTypeNode(kind::BAG_TYPE, elementType);
 }
@@ -540,10 +536,6 @@ TypeNode NodeManager::mkSequenceType(TypeNode elementType)
 {
   CheckArgument(
       !elementType.isNull(), elementType, "unexpected NULL element type");
-  CheckArgument(elementType.isFirstClass(),
-                elementType,
-                "cannot store types that are not first-class in sequences. Try "
-                "option --uf-ho.");
   return mkTypeNode(kind::SEQUENCE_TYPE, elementType);
 }
 
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index ad0593cee..b651c055a 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1095,14 +1095,6 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                 "unexpected NULL index type");
   CheckArgument(!constituentType.isNull(), constituentType,
                 "unexpected NULL constituent type");
-  CheckArgument(indexType.isFirstClass(),
-                indexType,
-                "cannot index arrays by types that are not first-class. Try "
-                "option --uf-ho.");
-  CheckArgument(constituentType.isFirstClass(),
-                constituentType,
-                "cannot store types that are not first-class in arrays. Try "
-                "option --uf-ho.");
   Debug("arrays") << "making array type " << indexType << " "
                   << constituentType << std::endl;
   return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
@@ -1111,10 +1103,6 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
 inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
   CheckArgument(!elementType.isNull(), elementType,
                 "unexpected NULL element type");
-  CheckArgument(elementType.isFirstClass(),
-                elementType,
-                "cannot store types that are not first-class in sets. Try "
-                "option --uf-ho.");
   Debug("sets") << "making sets type " << elementType << std::endl;
   return mkTypeNode(kind::SET_TYPE, elementType);
 }
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index caa0340bd..697501d13 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -57,7 +57,7 @@ thread_local Options* pOptions;
 const char* progPath;
 
 /** Just the basename component of argv[0] */
-const std::string* progName;
+std::string progName;
 
 /** A pointer to the CommandExecutor (the signal handlers need it) */
 std::unique_ptr<cvc5::main::CommandExecutor> pExecutor;
@@ -80,7 +80,7 @@ TotalTimer::~TotalTimer()
 
 void printUsage(Options& opts, bool full) {
   stringstream ss;
-  ss << "usage: " << options::getBinaryName(opts) << " [options] [input-file]"
+  ss << "usage: " << progName << " [options] [input-file]"
      << endl
      << endl
      << "Without an input file, or with `-', cvc5 reads from standard input."
@@ -106,13 +106,11 @@ int runCvc5(int argc, char* argv[], Options& opts)
   progPath = argv[0];
 
   // Parse the options
-  vector<string> filenames = Options::parseOptions(&opts, argc, argv);
+  std::vector<string> filenames =
+      Options::parseOptions(&opts, argc, argv, progName);
 
   auto limit = install_time_limit(opts);
 
-  string progNameStr = options::getBinaryName(opts);
-  progName = &progNameStr;
-
   if (opts.driver.help)
   {
     printUsage(opts, true);
diff --git a/src/main/main.h b/src/main/main.h
index 54abbdbe9..14d99f79c 100644
--- a/src/main/main.h
+++ b/src/main/main.h
@@ -34,7 +34,7 @@ class CommandExecutor;
 extern const char* progPath;
 
 /** Just the basename component of argv[0] */
-extern const std::string* progName;
+extern std::string progName;
 
 /** A reference for use by the signal handlers to print statistics */
 extern std::unique_ptr<cvc5::main::CommandExecutor> pExecutor;
diff --git a/src/main/signal_handlers.cpp b/src/main/signal_handlers.cpp
index d0628e2a7..b65600eb5 100644
--- a/src/main/signal_handlers.cpp
+++ b/src/main/signal_handlers.cpp
@@ -136,14 +136,14 @@ void segv_handler(int sig, siginfo_t* info, void* c)
     safe_print(STDERR_FILENO,
                "Spinning so that a debugger can be connected.\n");
     safe_print(STDERR_FILENO, "Try:  gdb ");
-    safe_print(STDERR_FILENO, *progName);
+    safe_print(STDERR_FILENO, progName);
     safe_print(STDERR_FILENO, " ");
     safe_print<int64_t>(STDERR_FILENO, getpid());
     safe_print(STDERR_FILENO, "\n");
     safe_print(STDERR_FILENO, " or:  gdb --pid=");
     safe_print<int64_t>(STDERR_FILENO, getpid());
     safe_print(STDERR_FILENO, " ");
-    safe_print(STDERR_FILENO, *progName);
+    safe_print(STDERR_FILENO, progName);
     safe_print(STDERR_FILENO, "\n");
     for (;;)
     {
@@ -191,14 +191,14 @@ void ill_handler(int sig, siginfo_t* info, void*)
     safe_print(STDERR_FILENO,
                "Spinning so that a debugger can be connected.\n");
     safe_print(STDERR_FILENO, "Try:  gdb ");
-    safe_print(STDERR_FILENO, *progName);
+    safe_print(STDERR_FILENO, progName);
     safe_print(STDERR_FILENO, " ");
     safe_print<int64_t>(STDERR_FILENO, getpid());
     safe_print(STDERR_FILENO, "\n");
     safe_print(STDERR_FILENO, " or:  gdb --pid=");
     safe_print<int64_t>(STDERR_FILENO, getpid());
     safe_print(STDERR_FILENO, " ");
-    safe_print(STDERR_FILENO, *progName);
+    safe_print(STDERR_FILENO, progName);
     safe_print(STDERR_FILENO, "\n");
     for (;;)
     {
diff --git a/src/omt/integer_optimizer.h b/src/omt/integer_optimizer.h
index 34605cc71..0b62c0816 100644
--- a/src/omt/integer_optimizer.h
+++ b/src/omt/integer_optimizer.h
@@ -36,13 +36,12 @@ class OMTOptimizerInteger : public OMTOptimizer
  private:
   /**
    * Handles the optimization query specified by objType
-   * isMinimize = true will trigger minimization, 
+   * isMinimize = true will trigger minimization,
    * otherwise trigger maximization
    **/
-  smt::OptimizationResult optimize(
-      SmtEngine* optChecker,
-      TNode target,
-      bool isMinimize);
+  smt::OptimizationResult optimize(SmtEngine* optChecker,
+                                   TNode target,
+                                   bool isMinimize);
 };
 
 }  // namespace cvc5::omt
diff --git a/src/omt/omt_optimizer.cpp b/src/omt/omt_optimizer.cpp
index 08f1809ec..2145492db 100644
--- a/src/omt/omt_optimizer.cpp
+++ b/src/omt/omt_optimizer.cpp
@@ -30,7 +30,7 @@ bool OMTOptimizer::nodeSupportsOptimization(TNode node)
 }
 
 std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForObjective(
-    OptimizationObjective& objective)
+    const OptimizationObjective& objective)
 {
   // the datatype of the target node
   TypeNode objectiveType = objective.getTarget().getType(true);
@@ -53,7 +53,10 @@ std::unique_ptr<OMTOptimizer> OMTOptimizer::getOptimizerForObjective(
 }
 
 Node OMTOptimizer::mkStrongIncrementalExpression(
-    NodeManager* nm, TNode lhs, TNode rhs, OptimizationObjective& objective)
+    NodeManager* nm,
+    TNode lhs,
+    TNode rhs,
+    const OptimizationObjective& objective)
 {
   constexpr const char lhsTypeError[] =
       "lhs type does not match or is not implicitly convertable to the target "
@@ -114,10 +117,11 @@ Node OMTOptimizer::mkStrongIncrementalExpression(
   Unreachable();
 }
 
-Node OMTOptimizer::mkWeakIncrementalExpression(NodeManager* nm,
-                                               TNode lhs,
-                                               TNode rhs,
-                                               OptimizationObjective& objective)
+Node OMTOptimizer::mkWeakIncrementalExpression(
+    NodeManager* nm,
+    TNode lhs,
+    TNode rhs,
+    const OptimizationObjective& objective)
 {
   constexpr const char lhsTypeError[] =
       "lhs type does not match or is not implicitly convertable to the target "
diff --git a/src/omt/omt_optimizer.h b/src/omt/omt_optimizer.h
index 1052865b0..1e8d9e763 100644
--- a/src/omt/omt_optimizer.h
+++ b/src/omt/omt_optimizer.h
@@ -46,7 +46,7 @@ class OMTOptimizer
    *   and this is the optimizer for targetNode
    **/
   static std::unique_ptr<OMTOptimizer> getOptimizerForObjective(
-      smt::OptimizationObjective& objective);
+      const smt::OptimizationObjective& objective);
 
   /**
    * Given the lhs and rhs expressions, with an optimization objective,
@@ -70,7 +70,7 @@ class OMTOptimizer
       NodeManager* nm,
       TNode lhs,
       TNode rhs,
-      smt::OptimizationObjective& objective);
+      const smt::OptimizationObjective& objective);
 
   /**
    * Given the lhs and rhs expressions, with an optimization objective,
@@ -94,7 +94,7 @@ class OMTOptimizer
       NodeManager* nm,
       TNode lhs,
       TNode rhs,
-      smt::OptimizationObjective& objective);
+      const smt::OptimizationObjective& objective);
 
   /**
    * Minimize the target node with constraints encoded in optChecker
diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 7b2cde54a..f9d1c1a18 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -2,11 +2,6 @@ id     = "BASE"
 name   = "Base"
 
 [[option]]
-  name       = "binary_name"
-  category   = "undocumented"
-  type       = "std::string"
-
-[[option]]
   name       = "in"
   category   = "undocumented"
   type       = "std::istream*"
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index d06c64517..c1c843802 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -252,26 +252,29 @@ void OptionsHandler::setStats(const std::string& option, bool value)
     throw OptionException(ss.str());
   }
 #endif /* CVC5_STATISTICS_ON */
-  Assert(option.substr(0, 2) == "--");
-  std::string opt = option.substr(2);
+  std::string opt = option;
+  if (option.substr(0, 2) == "--")
+  {
+    opt = opt.substr(2);
+  }
   if (value)
   {
-    if (option == options::base::statisticsAll__name)
+    if (opt == options::base::statisticsAll__name)
     {
       d_options->base.statistics = true;
     }
-    else if (option == options::base::statisticsEveryQuery__name)
+    else if (opt == options::base::statisticsEveryQuery__name)
     {
       d_options->base.statistics = true;
     }
-    else if (option == options::base::statisticsExpert__name)
+    else if (opt == options::base::statisticsExpert__name)
     {
       d_options->base.statistics = true;
     }
   }
   else
   {
-    if (option == options::base::statistics__name)
+    if (opt == options::base::statistics__name)
     {
       d_options->base.statisticsAll = false;
       d_options->base.statisticsEveryQuery = false;
diff --git a/src/options/options_public.cpp b/src/options/options_public.cpp
index 7d72496aa..35e891f5a 100644
--- a/src/options/options_public.cpp
+++ b/src/options/options_public.cpp
@@ -103,10 +103,6 @@ int32_t getVerbosity(const Options& opts) { return opts.base.verbosity; }
 std::istream* getIn(const Options& opts) { return opts.base.in; }
 std::ostream* getErr(const Options& opts) { return opts.base.err; }
 std::ostream* getOut(const Options& opts) { return opts.base.out; }
-const std::string& getBinaryName(const Options& opts)
-{
-  return opts.base.binary_name;
-}
 
 void setInputLanguage(InputLanguage val, Options& opts)
 {
diff --git a/src/options/options_public.h b/src/options/options_public.h
index 9b549601f..1d2f9edba 100644
--- a/src/options/options_public.h
+++ b/src/options/options_public.h
@@ -55,7 +55,6 @@ int32_t getVerbosity(const Options& opts) CVC5_EXPORT;
 std::istream* getIn(const Options& opts) CVC5_EXPORT;
 std::ostream* getErr(const Options& opts) CVC5_EXPORT;
 std::ostream* getOut(const Options& opts) CVC5_EXPORT;
-const std::string& getBinaryName(const Options& opts) CVC5_EXPORT;
 
 void setInputLanguage(InputLanguage val, Options& opts) CVC5_EXPORT;
 void setOut(std::ostream* val, Options& opts) CVC5_EXPORT;
diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp
index 0d6b7f01b..e909a5f0a 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -364,7 +364,8 @@ public:
  */
 std::vector<std::string> Options::parseOptions(Options* options,
                                                int argc,
-                                               char* argv[])
+                                               char* argv[],
+                                               std::string& binaryName)
 {
   Assert(options != NULL);
   Assert(argv != NULL);
@@ -386,7 +387,7 @@ std::vector<std::string> Options::parseOptions(Options* options,
   if(x != NULL) {
     progName = x + 1;
   }
-  options->base.binary_name = std::string(progName);
+  binaryName = std::string(progName);
 
   std::vector<std::string> nonoptions;
   options->parseOptionsRecursive(argc, argv, &nonoptions);
diff --git a/src/options/options_template.h b/src/options/options_template.h
index 76c599d23..e9a4a6999 100644
--- a/src/options/options_template.h
+++ b/src/options/options_template.h
@@ -174,7 +174,8 @@ public:
    */
   static std::vector<std::string> parseOptions(Options* options,
                                                int argc,
-                                               char* argv[]);
+                                               char* argv[],
+                                               std::string& binaryName);
 
   /**
    * Get the setting for all options.
diff --git a/src/preprocessing/learned_literal_manager.cpp b/src/preprocessing/learned_literal_manager.cpp
new file mode 100644
index 000000000..5b301592a
--- /dev/null
+++ b/src/preprocessing/learned_literal_manager.cpp
@@ -0,0 +1,52 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Learned literal manager
+ */
+
+#include "preprocessing/learned_literal_manager.h"
+
+#include "theory/rewriter.h"
+
+namespace cvc5 {
+namespace preprocessing {
+
+LearnedLiteralManager::LearnedLiteralManager(theory::TrustSubstitutionMap& tls,
+                                             context::UserContext* u,
+                                             ProofNodeManager* pnm)
+    : d_topLevelSubs(tls), d_learnedLits(u)
+{
+}
+
+void LearnedLiteralManager::notifyLearnedLiteral(Node lit)
+{
+  d_learnedLits.insert(lit);
+  Trace("pp-llm") << "LLM:notifyLearnedLiteral: " << lit << std::endl;
+}
+
+std::vector<Node> LearnedLiteralManager::getLearnedLiterals() const
+{
+  std::vector<Node> currLearnedLits;
+  for (const auto& lit: d_learnedLits)
+  {
+    // update based on substitutions
+    Node tlsNode = d_topLevelSubs.get().apply(lit);
+    tlsNode = theory::Rewriter::rewrite(tlsNode);
+    currLearnedLits.push_back(tlsNode);
+    Trace("pp-llm") << "Learned literal : " << tlsNode << " from " << lit
+                    << std::endl;
+  }
+  return currLearnedLits;
+}
+
+}  // namespace preprocessing
+}  // namespace cvc5
diff --git a/src/preprocessing/learned_literal_manager.h b/src/preprocessing/learned_literal_manager.h
new file mode 100644
index 000000000..2148b3f7c
--- /dev/null
+++ b/src/preprocessing/learned_literal_manager.h
@@ -0,0 +1,71 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Andrew Reynolds
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Learned literal manager
+ */
+
+#include "cvc5_private.h"
+
+#ifndef CVC5__PREPROCESSING__LEARNED_LITERAL_MANAGER_H
+#define CVC5__PREPROCESSING__LEARNED_LITERAL_MANAGER_H
+
+#include "context/cdhashset.h"
+#include "expr/node.h"
+#include "theory/trust_substitutions.h"
+
+namespace cvc5 {
+namespace preprocessing {
+
+/**
+ * This class maintains the list of learned literals that have been inferred
+ * during preprocessing but we have not fully processed e.g. via substitutions.
+ *
+ * In particular, notice that if an equality (= x t) is learned at top level,
+ * we may add x -> t to top level substitutions if t does not contain x; we can
+ * henceforth forget that (= x t) is a learned literal. On the other hand, if
+ * a literal like (> x t) is learned at top-level, it may be useful to remember
+ * this information. This class is concerned with the latter kind of literals.
+ */
+class LearnedLiteralManager
+{
+ public:
+  LearnedLiteralManager(theory::TrustSubstitutionMap& tls,
+                        context::UserContext* u,
+                        ProofNodeManager* pnm);
+  /**
+   * Notify learned literal. This method is called when a literal is
+   * entailed by the current set of assertions.
+   *
+   * It should be rewritten, and such that top level substitutions have
+   * been applied to it.
+   */
+  void notifyLearnedLiteral(Node lit);
+  /**
+   * Get learned literals, which returns the current set of learned literals
+   * provided to this class. These literals are refreshed so that the current
+   * top-level substitutions are applied to them, and then are rewritten.
+   */
+  std::vector<Node> getLearnedLiterals() const;
+
+ private:
+  /** Learned literal map */
+  typedef context::CDHashSet<Node> NodeSet;
+  /* The top level substitutions */
+  theory::TrustSubstitutionMap& d_topLevelSubs;
+  /** Learned literals */
+  NodeSet d_learnedLits;
+};
+
+}  // namespace preprocessing
+}  // namespace cvc5
+
+#endif /* CVC5__PREPROCESSING__LEARNED_LITERAL_MANAGER_H */
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 1381ef87c..b6cdfb67b 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -43,6 +43,7 @@ Env::Env(NodeManager* nm, Options* opts)
       d_logic(),
       d_statisticsRegistry(std::make_unique<StatisticsRegistry>()),
       d_options(),
+      d_originalOptions(opts),
       d_resourceManager()
 {
   if (opts != nullptr)
@@ -97,6 +98,8 @@ StatisticsRegistry& Env::getStatisticsRegistry()
 
 const Options& Env::getOptions() const { return d_options; }
 
+const Options& Env::getOriginalOptions() const { return *d_originalOptions; }
+
 ResourceManager* Env::getResourceManager() const
 {
   return d_resourceManager.get();
diff --git a/src/smt/env.h b/src/smt/env.h
index 29a360209..57b5ad9c7 100644
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -94,6 +94,9 @@ class Env
   /** Get the options object (const version only) owned by this Env. */
   const Options& getOptions() const;
 
+  /** Get the original options object (const version only). */
+  const Options& getOriginalOptions() const;
+
   /** Get the resource manager owned by this Env. */
   ResourceManager* getResourceManager() const;
 
@@ -180,6 +183,12 @@ class Env
    * consider during solving and initialization.
    */
   Options d_options;
+  /**
+   * A pointer to the original options object as stored in the api::Solver.
+   * The referenced objects holds the options as initially parsed before being
+   * changed, e.g., by setDefaults().
+   */
+  const Options* d_originalOptions;
   /** Manager for limiting time and abstract resource usage. */
   std::unique_ptr<ResourceManager> d_resourceManager;
 }; /* class Env */
diff --git a/src/smt/optimization_solver.cpp b/src/smt/optimization_solver.cpp
index ffc49710a..e85ea82ef 100644
--- a/src/smt/optimization_solver.cpp
+++ b/src/smt/optimization_solver.cpp
@@ -15,6 +15,8 @@
 
 #include "smt/optimization_solver.h"
 
+#include "context/cdhashmap.h"
+#include "context/cdlist.h"
 #include "omt/omt_optimizer.h"
 #include "options/smt_options.h"
 #include "smt/assertions.h"
@@ -29,7 +31,7 @@ namespace smt {
 OptimizationSolver::OptimizationSolver(SmtEngine* parent)
     : d_parent(parent),
       d_optChecker(),
-      d_objectives(),
+      d_objectives(parent->getUserContext()),
       d_results(),
       d_objectiveCombination(LEXICOGRAPHIC)
 {
@@ -37,10 +39,14 @@ OptimizationSolver::OptimizationSolver(SmtEngine* parent)
 
 OptimizationResult::ResultType OptimizationSolver::checkOpt()
 {
+  // if the results of the previous call have different size than the
+  // objectives, then we should clear the pareto optimization context
+  if (d_results.size() != d_objectives.size()) d_optChecker.reset();
+  // initialize the result vector
+  d_results.clear();
   for (size_t i = 0, numObj = d_objectives.size(); i < numObj; ++i)
   {
-    // reset the optimization results
-    d_results[i] = OptimizationResult();
+    d_results.emplace_back();
   }
   switch (d_objectiveCombination)
   {
@@ -66,14 +72,6 @@ void OptimizationSolver::addObjective(TNode target,
   }
   d_optChecker.reset();
   d_objectives.emplace_back(target, type, bvSigned);
-  d_results.emplace_back(OptimizationResult::UNKNOWN, Node());
-}
-
-void OptimizationSolver::resetObjectives()
-{
-  d_optChecker.reset();
-  d_objectives.clear();
-  d_results.clear();
 }
 
 std::vector<OptimizationResult> OptimizationSolver::getValues()
diff --git a/src/smt/optimization_solver.h b/src/smt/optimization_solver.h
index 64591d8f1..6d138deb2 100644
--- a/src/smt/optimization_solver.h
+++ b/src/smt/optimization_solver.h
@@ -18,6 +18,8 @@
 #ifndef CVC5__SMT__OPTIMIZATION_SOLVER_H
 #define CVC5__SMT__OPTIMIZATION_SOLVER_H
 
+#include "context/cdhashmap_forward.h"
+#include "context/cdlist.h"
 #include "expr/node.h"
 #include "expr/type_node.h"
 #include "util/result.h"
@@ -74,14 +76,14 @@ class OptimizationResult
    * @return an enum showing whether the result is optimal, unbounded,
    *   unsat or unknown.
    **/
-  ResultType getType() { return d_type; }
+  ResultType getType() const { return d_type; }
   /**
    * Returns the optimal value.
    * @return Node containing the optimal value,
    *   if getType() is not OPTIMAL, it might return an empty node or a node
    *   containing non-optimal value
    **/
-  Node getValue() { return d_value; }
+  Node getValue() const { return d_value; }
 
  private:
   /** the indicating whether the result is optimal or something else **/
@@ -124,13 +126,13 @@ class OptimizationObjective
   ~OptimizationObjective() = default;
 
   /** A getter for d_type **/
-  ObjectiveType getType() { return d_type; }
+  ObjectiveType getType() const { return d_type; }
 
   /** A getter for d_target **/
-  Node getTarget() { return d_target; }
+  Node getTarget() const { return d_target; }
 
   /** A getter for d_bvSigned **/
-  bool bvIsSigned() { return d_bvSigned; }
+  bool bvIsSigned() const { return d_bvSigned; }
 
  private:
   /**
@@ -173,7 +175,7 @@ class OptimizationSolver
    *
    * Lexicographic: optimize the objectives one-by-one, in the order they are
    * added:
-   *   v_x = max(x) s.t. phi(x, y) = sat 
+   *   v_x = max(x) s.t. phi(x, y) = sat
    *   v_y = max(y) s.t. phi(v_x, y) = sat
    *
    * Pareto: optimize multiple goals to a state such that
@@ -215,11 +217,6 @@ class OptimizationSolver
                     bool bvSigned = false);
 
   /**
-   * Clear all the added optimization objectives
-   **/
-  void resetObjectives();
-
-  /**
    * Returns the values of the optimized objective after checkOpt is called
    * @return a vector of Optimization Result,
    *   each containing the outcome and the value.
@@ -293,7 +290,7 @@ class OptimizationSolver
   std::unique_ptr<SmtEngine> d_optChecker;
 
   /** The objectives to optimize for **/
-  std::vector<OptimizationObjective> d_objectives;
+  context::CDList<OptimizationObjective> d_objectives;
 
   /** The results of the optimizations from the last checkOpt call **/
   std::vector<OptimizationResult> d_results;
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index b0f6e63bf..5ecc33778 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -716,7 +716,22 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va
     Trace("bound-int-rsi") << "Look up the value for " << d_set[q][i] << " " << i << std::endl;
     int vo = rsi->getVariableOrder(i);
     Assert(q[0][vo] == d_set[q][i]);
-    Node t = rsi->getCurrentTerm(vo, true);
+    TypeNode tn = d_set[q][i].getType();
+    // If the type of tn is not closed enumerable, we must map the value back
+    // to a term that appears in the same equivalence class as the constant.
+    // Notice that this is to ensure that unhandled values (e.g. uninterpreted
+    // constants, datatype values) do not enter instantiations/lemmas, which
+    // can lead to refutation unsoundness. However, it is important that we
+    // conversely do *not* map terms to values in other cases. In particular,
+    // replacing a constant c with a term t can lead to solution unsoundness
+    // if we are instantiating a quantified formula that corresponds to a
+    // reduction for t, since then the reduction is using circular reasoning:
+    // the current value of t is being used to reason about the range of
+    // its axiomatization. This is limited to reductions in the theory of
+    // strings, which use quantification on integers only. Note this
+    // impacts only quantified formulas with 2+ dimensions and dependencies
+    // between dimensions, e.g. str.indexof_re reduction.
+    Node t = rsi->getCurrentTerm(vo, !tn.isClosedEnumerable());
     Trace("bound-int-rsi") << "term : " << t << std::endl;
     vars.push_back( d_set[q][i] );
     subs.push_back( t );
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index d0eee1886..f6af5b680 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -429,14 +429,17 @@ Node RepSetIterator::getCurrentTerm(unsigned i, bool valTerm) const
                      << d_domain_elements[i].size() << std::endl;
   Assert(0 <= curr && curr < d_domain_elements[i].size());
   Node t = d_domain_elements[i][curr];
+  Trace("rsi-debug") << "rsi : term = " << t << std::endl;
   if (valTerm)
   {
     Node tt = d_rs->getTermForRepresentative(t);
     if (!tt.isNull())
     {
+  Trace("rsi-debug") << "rsi : return rep term = " << tt << std::endl;
       return tt;
     }
   }
+  Trace("rsi-debug") << "rsi : return" << std::endl;
   return t;
 }
 
diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index b0d538064..dbb6d4cf3 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -323,7 +323,7 @@ Node StringsPreprocess::reduce(Node t,
     //         n <= i < ite(skk = -1, len(s), skk) ^ 0 < l <= len(s) - i =>
     //           ~in_re(substr(s, i, l), r)) ^
     //       (skk != -1 =>
-    //          exists l. 0 <= l < len(s) - skk ^ in_re(substr(s, skk, l), r))
+    //          exists l. 0 <= l <= len(s) - skk ^ in_re(substr(s, skk, l), r))
     //
     // Note that this reduction relies on eager reduction lemmas being sent to
     // properly limit the range of skk.
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 1afb8cc31..36b05b145 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -148,56 +148,54 @@ void TheoryUF::postCheck(Effort level)
   }
 }
 
-bool TheoryUF::preNotifyFact(
-    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
+void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
 {
+  if (d_state.isInConflict())
+  {
+    return;
+  }
   if (d_thss != nullptr)
   {
     bool isDecision =
         d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
     d_thss->assertNode(fact, isDecision);
-    if (d_state.isInConflict())
-    {
-      return true;
-    }
   }
-  if (atom.getKind() == kind::CARDINALITY_CONSTRAINT
-      || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT)
+  switch (atom.getKind())
   {
-    if (d_thss == nullptr)
+    case kind::EQUAL:
     {
-      if (!getLogicInfo().hasCardinalityConstraints())
+      if (options::ufHo() && options::ufHoExt())
       {
-        std::stringstream ss;
-        ss << "Cardinality constraint " << atom
-           << " was asserted, but the logic does not allow it." << std::endl;
-        ss << "Try using a logic containing \"UFC\"." << std::endl;
-        throw Exception(ss.str());
-      }
-      else
-      {
-        // support for cardinality constraints is not enabled, set incomplete
-        d_im.setIncomplete(IncompleteId::UF_CARD_DISABLED);
+        if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction())
+        {
+          // apply extensionality eagerly using the ho extension
+          d_ho->applyExtensionality(fact);
+        }
       }
     }
-    // don't need to assert cardinality constraints if not producing models
-    return !options::produceModels();
-  }
-  return false;
-}
-
-void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
-{
-  if (!d_state.isInConflict() && atom.getKind() == kind::EQUAL)
-  {
-    if (options::ufHo() && options::ufHoExt())
+    break;
+    case kind::CARDINALITY_CONSTRAINT:
+    case kind::COMBINED_CARDINALITY_CONSTRAINT:
     {
-      if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction())
+      if (d_thss == nullptr)
       {
-        // apply extensionality eagerly using the ho extension
-        d_ho->applyExtensionality(fact);
+        if (!getLogicInfo().hasCardinalityConstraints())
+        {
+          std::stringstream ss;
+          ss << "Cardinality constraint " << atom
+             << " was asserted, but the logic does not allow it." << std::endl;
+          ss << "Try using a logic containing \"UFC\"." << std::endl;
+          throw Exception(ss.str());
+        }
+        else
+        {
+          // support for cardinality constraints is not enabled, set incomplete
+          d_im.setIncomplete(IncompleteId::UF_CARD_DISABLED);
+        }
       }
     }
+    break;
+    default: break;
   }
 }
 //--------------------------------- end standard check
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index c811e08e8..c953cfe5c 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -128,12 +128,6 @@ private:
   bool needsCheckLastEffort() override;
   /** Post-check, called after the fact queue of the theory is processed. */
   void postCheck(Effort level) override;
-  /** Pre-notify fact, return true if processed. */
-  bool preNotifyFact(TNode atom,
-                     bool pol,
-                     TNode fact,
-                     bool isPrereg,
-                     bool isInternal) override;
   /** Notify fact */
   void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
   //--------------------------------- end standard check
diff --git a/test/python/unit/api/test_term.py b/test/python/unit/api/test_term.py
index 32813e17f..e78188079 100644
--- a/test/python/unit/api/test_term.py
+++ b/test/python/unit/api/test_term.py
@@ -15,6 +15,7 @@ import pytest
 import pycvc5
 from pycvc5 import kinds
 from pycvc5 import Sort, Term
+from fractions import Fraction
 
 
 @pytest.fixture
@@ -1145,12 +1146,27 @@ def test_get_real(solver):
     assert 0 == real1.getRealValue()
     assert 0 == real2.getRealValue()
     assert -17 == real3.getRealValue()
-    assert -3 / 5 == real4.getRealValue()
-    assert 127 / 10 == real5.getRealValue()
-    assert 1 / 4294967297 == real6.getRealValue()
+    assert Fraction(-3, 5) == real4.getRealValue()
+    assert Fraction(127, 10) == real5.getRealValue()
+    assert Fraction(1, 4294967297) == real6.getRealValue()
     assert 4294967297 == real7.getRealValue()
-    assert 1 / 18446744073709551617 == real8.getRealValue()
-    assert float(18446744073709551617) == real9.getRealValue()
+    assert Fraction(1, 18446744073709551617) == real8.getRealValue()
+    assert Fraction(18446744073709551617, 1) == real9.getRealValue()
+
+    # Check denominator too large for float
+    num = 1
+    den = 2 ** 64 + 1
+    real_big = solver.mkReal(num, den)
+    assert real_big.isRealValue()
+    assert Fraction(num, den) == real_big.getRealValue()
+
+    # Check that we're treating floats as decimal aproximations rather than
+    # IEEE-754-specified values.
+    real_decimal = solver.mkReal(0.3)
+    assert real_decimal.isRealValue()
+    assert Fraction("0.3") == real_decimal.getRealValue()
+    assert Fraction(0.3) == Fraction(5404319552844595, 18014398509481984)
+    assert Fraction(0.3) != real_decimal.getRealValue()
 
 
 def test_get_boolean(solver):
diff --git a/test/python/unit/api/test_to_python_obj.py b/test/python/unit/api/test_to_python_obj.py
index 2ba685d50..bb30fae8f 100644
--- a/test/python/unit/api/test_to_python_obj.py
+++ b/test/python/unit/api/test_to_python_obj.py
@@ -22,8 +22,8 @@ def testGetBool():
     solver = pycvc5.Solver()
     t = solver.mkTrue()
     f = solver.mkFalse()
-    assert t.toPythonObj() == True
-    assert f.toPythonObj() == False
+    assert t.toPythonObj() is True
+    assert f.toPythonObj() is False
 
 
 def testGetInt():
@@ -115,4 +115,4 @@ def testGetValueReal():
     xval = solver.getValue(x)
     yval = solver.getValue(y)
     assert xval.toPythonObj() == Fraction("6")
-    assert yval.toPythonObj() == float(Fraction("8.33"))
+    assert yval.toPythonObj() == Fraction("8.33")
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d112bdf1d..4ee8e513e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -737,6 +737,7 @@ set(regress_0_tests
   regress0/options/ast-and-sexpr.smt2
   regress0/options/invalid_dump.smt2
   regress0/options/set-and-get-options.smt2
+  regress0/options/statistics.smt2
   regress0/parallel-let.smt2
   regress0/parser/as.smt2
   regress0/parser/bv_arity_smt2.6.smt2
@@ -2125,7 +2126,11 @@ set(regress_1_tests
   regress1/strings/issue6337-replace-re.smt2
   regress1/strings/issue6567-empty-re-range.smt2
   regress1/strings/issue6604-2.smt2
+  regress1/strings/issue6635-rre.smt2
   regress1/strings/issue6653-2-update-c-len.smt2
+  regress1/strings/issue6653-4-rre.smt2
+  regress1/strings/issue6653-rre.smt2
+  regress1/strings/issue6653-rre-small.smt2
   regress1/strings/kaluza-fl.smt2
   regress1/strings/loop002.smt2
   regress1/strings/loop003.smt2
diff --git a/test/regress/regress0/options/statistics.smt2 b/test/regress/regress0/options/statistics.smt2
new file mode 100644
index 000000000..ae9d93b6f
--- /dev/null
+++ b/test/regress/regress0/options/statistics.smt2
@@ -0,0 +1,43 @@
+; REQUIRES: statistics
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: true
+; EXPECT: true
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: false
+; EXPECT: true
+; EXPECT: false
+; EXPECT: false
+; EXPECT: true
+(set-logic QF_UF)
+(get-option :stats)
+(get-option :stats-all)
+(get-option :stats-every-query)
+(get-option :stats-expert)
+
+(set-option :stats-all true)
+
+(get-option :stats)
+(get-option :stats-all)
+(get-option :stats-every-query)
+(get-option :stats-expert)
+
+(set-option :stats false)
+
+(get-option :stats)
+(get-option :stats-all)
+(get-option :stats-every-query)
+(get-option :stats-expert)
+
+(set-option :stats-expert true)
+
+(get-option :stats)
+(get-option :stats-all)
+(get-option :stats-every-query)
+(get-option :stats-expert)
\ No newline at end of file
diff --git a/test/regress/regress1/strings/issue6635-rre.smt2 b/test/regress/regress1/strings/issue6635-rre.smt2
new file mode 100644
index 000000000..cbca77783
--- /dev/null
+++ b/test/regress/regress1/strings/issue6635-rre.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; EXPECT: unsat
+(set-logic ALL)
+(declare-fun a () String)
+(assert (str.in_re (str.replace_re a (re.++ (str.to_re "A") (re.union (str.to_re "") (str.to_re (str.from_code (str.len a))))) "AB") (re.+ (str.to_re "A"))))
+(check-sat)
diff --git a/test/regress/regress1/strings/issue6653-4-rre.smt2 b/test/regress/regress1/strings/issue6653-4-rre.smt2
new file mode 100644
index 000000000..8de99a334
--- /dev/null
+++ b/test/regress/regress1/strings/issue6653-4-rre.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun x () String)
+(assert (str.in_re (str.replace_re x (str.to_re "A") x) (re.++ (re.comp (str.to_re "A")) (str.to_re "A") re.allchar)))
+(check-sat)
diff --git a/test/regress/regress1/strings/issue6653-rre-small.smt2 b/test/regress/regress1/strings/issue6653-rre-small.smt2
new file mode 100644
index 000000000..c4b6a497b
--- /dev/null
+++ b/test/regress/regress1/strings/issue6653-rre-small.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --strings-exp --strings-fmf --re-elim --re-elim-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () String)
+(assert (str.in_re a (re.+ (str.to_re (str.replace_re a (str.to_re a) "A")))))
+(check-sat)
diff --git a/test/regress/regress1/strings/issue6653-rre.smt2 b/test/regress/regress1/strings/issue6653-rre.smt2
new file mode 100644
index 000000000..66b7dd64e
--- /dev/null
+++ b/test/regress/regress1/strings/issue6653-rre.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --strings-exp --re-elim --re-elim-agg
+; EXPECT: sat
+(set-logic ALL)
+(declare-fun a () String)
+(declare-fun b () String)
+(assert (str.in_re (str.replace_re b (str.to_re (str.replace_all a (str.++ b "a") b)) (str.++ b "a")) (re.+ (str.to_re "b"))))
+(assert (str.in_re a (re.* (re.range "a" "b"))))
+(check-sat)
diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp
index 94a2e5fb6..98fabc727 100644
--- a/test/unit/node/node_black.cpp
+++ b/test/unit/node/node_black.cpp
@@ -67,7 +67,8 @@ class TestNodeBlackNode : public TestNode
     char* argv[2];
     argv[0] = strdup("");
     argv[1] = strdup("--output-lang=ast");
-    Options::parseOptions(&opts, 2, argv);
+    std::string progName;
+    Options::parseOptions(&opts, 2, argv, progName);
     free(argv[0]);
     free(argv[1]);
     d_smt.reset(new SmtEngine(d_nodeManager.get(), &opts));
diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp
index 66efe7eff..c23ce79dd 100644
--- a/test/unit/theory/theory_bv_opt_white.cpp
+++ b/test/unit/theory/theory_bv_opt_white.cpp
@@ -63,7 +63,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_min)
 
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
             BitVector(32u, (uint32_t)0x3FFFFFA1));
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 TEST_F(TestTheoryWhiteBVOpt, signed_min)
@@ -87,7 +87,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_min)
 
   // expect the minimum x = -1
   ASSERT_EQ(val, BitVector(32u, (uint32_t)0x80000000));
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
@@ -114,7 +114,7 @@ TEST_F(TestTheoryWhiteBVOpt, unsigned_max)
 
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
             BitVector(32u, 2u));
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 TEST_F(TestTheoryWhiteBVOpt, signed_max)
@@ -137,7 +137,7 @@ TEST_F(TestTheoryWhiteBVOpt, signed_max)
   // expect the maxmum x =
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
             BitVector(32u, 10u));
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 TEST_F(TestTheoryWhiteBVOpt, min_boundary)
@@ -161,7 +161,7 @@ TEST_F(TestTheoryWhiteBVOpt, min_boundary)
   // expect the maximum x = 18
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<BitVector>(),
             BitVector(32u, 18u));
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 }  // namespace test
diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp
index f16db0c0e..cf0434ddc 100644
--- a/test/unit/theory/theory_int_opt_white.cpp
+++ b/test/unit/theory/theory_int_opt_white.cpp
@@ -70,7 +70,7 @@ TEST_F(TestTheoryWhiteIntOpt, max)
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
             Rational("99"));
 
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 TEST_F(TestTheoryWhiteIntOpt, min)
@@ -101,7 +101,7 @@ TEST_F(TestTheoryWhiteIntOpt, min)
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
             Rational("1"));
 
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 TEST_F(TestTheoryWhiteIntOpt, result)
@@ -129,7 +129,7 @@ TEST_F(TestTheoryWhiteIntOpt, result)
 
   // We expect our check to have returned UNSAT
   ASSERT_EQ(r, OptimizationResult::UNSAT);
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 TEST_F(TestTheoryWhiteIntOpt, open_interval)
@@ -164,7 +164,7 @@ TEST_F(TestTheoryWhiteIntOpt, open_interval)
   // expect the minimum result of cost3 = cost1 + cost2 to be 1 + 111 = 112
   ASSERT_EQ(d_optslv->getValues()[0].getValue().getConst<Rational>(),
             Rational("112"));
-  d_optslv->resetObjectives();
+  d_smtEngine->resetAssertions();
 }
 
 }  // namespace test
diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp
index 1950d9ae2..73c6d9e7e 100644
--- a/test/unit/theory/theory_opt_multigoal_white.cpp
+++ b/test/unit/theory/theory_opt_multigoal_white.cpp
@@ -240,5 +240,69 @@ TEST_F(TestTheoryWhiteOptMultigoal, pareto)
   ASSERT_EQ(possibleResults.size(), 0);
 }
 
+TEST_F(TestTheoryWhiteOptMultigoal, pushpop)
+{
+  d_smtEngine->resetAssertions();
+  Node x = d_nodeManager->mkVar(*d_BV32Type);
+  Node y = d_nodeManager->mkVar(*d_BV32Type);
+  Node z = d_nodeManager->mkVar(*d_BV32Type);
+
+  // 18 <= x
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(
+      kind::BITVECTOR_ULE, d_nodeManager->mkConst(BitVector(32u, 18u)), x));
+
+  // y <= x
+  d_smtEngine->assertFormula(d_nodeManager->mkNode(kind::BITVECTOR_SLE, y, x));
+
+  // Lexico optimization
+  OptimizationSolver optSolver(d_smtEngine.get());
+
+  optSolver.setObjectiveCombination(OptimizationSolver::LEXICOGRAPHIC);
+
+  // minimize x
+  optSolver.addObjective(x, OptimizationObjective::MINIMIZE, false);
+
+  // push
+  d_smtEngine->push();
+
+  // maximize y with `signed` comparison over bit-vectors.
+  optSolver.addObjective(y, OptimizationObjective::MAXIMIZE, true);
+  // maximize z
+  optSolver.addObjective(z, OptimizationObjective::MAXIMIZE, false);
+
+  OptimizationResult::ResultType r = optSolver.checkOpt();
+
+  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+
+  std::vector<OptimizationResult> results = optSolver.getValues();
+
+  // x == 18
+  ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
+
+  // y == 18
+  ASSERT_EQ(results[1].getValue().getConst<BitVector>(), BitVector(32u, 18u));
+
+  // z == 0xFFFFFFFF
+  ASSERT_EQ(results[2].getValue().getConst<BitVector>(),
+            BitVector(32u, (unsigned)0xFFFFFFFF));
+
+  // pop
+  d_smtEngine->pop();
+
+  // now we only have one objective: (minimize x)
+  r = optSolver.checkOpt();
+  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  results = optSolver.getValues();
+  ASSERT_EQ(results.size(), 1);
+  ASSERT_EQ(results[0].getValue().getConst<BitVector>(), BitVector(32u, 18u));
+
+  // resetting the assertions also resets the optimization objectives
+  d_smtEngine->resetAssertions();
+  r = optSolver.checkOpt();
+  ASSERT_EQ(r, OptimizationResult::OPTIMAL);
+  results = optSolver.getValues();
+  ASSERT_EQ(results.size(), 0);
+}
+
 }  // namespace test
 }  // namespace cvc5