Merge branch 'master' into fixABCfixABC

32 files changed, 795 insertions, 431 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 65ccabd89..9753f86a7 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -202,6 +202,8 @@ libcvc4_add_sources(
   smt/logic_exception.h
   smt/logic_request.cpp
   smt/logic_request.h
+  smt/interpolation_solver.cpp
+  smt/interpolation_solver.h
   smt/managed_ostreams.cpp
   smt/managed_ostreams.h
   smt/model.cpp
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index c219deefe..e40b828b5 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -168,6 +168,13 @@ Node BVToInt::eliminationPass(Node n)
   while (!toVisit.empty())
   {
     current = toVisit.back();
+    // assert that the node is binarized
+    kind::Kind_t k = current.getKind();
+    uint64_t numChildren = current.getNumChildren();
+    Assert((numChildren == 2)
+           || !(k == kind::BITVECTOR_PLUS || k == kind::BITVECTOR_MULT
+                || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR
+                || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT));
     toVisit.pop_back();
     bool inEliminationCache =
         (d_eliminationCache.find(current) != d_eliminationCache.end());
@@ -217,7 +224,7 @@ Node BVToInt::eliminationPass(Node n)
       if (d_rebuildCache[current].get().isNull())
       {
         // current wasn't rebuilt yet.
-        uint64_t numChildren = current.getNumChildren();
+        numChildren = current.getNumChildren();
         if (numChildren == 0)
         {
           // We only eliminate operators that are not nullary.
@@ -257,7 +264,10 @@ Node BVToInt::eliminationPass(Node n)
  */
 Node BVToInt::bvToInt(Node n)
 {
+  n = makeBinary(n);
   n = eliminationPass(n);
+  // binarize again, in case the elimination pass introduced
+  // non-binary terms (as can happen by RepeatEliminate, for example).
   n = makeBinary(n);
   vector<Node> toVisit;
   toVisit.push_back(n);
@@ -340,69 +350,26 @@ Node BVToInt::translateWithChildren(Node original,
   // ultbv and sltbv were supposed to be eliminated before this point.
   Assert(oldKind != kind::BITVECTOR_ULTBV);
   Assert(oldKind != kind::BITVECTOR_SLTBV);
+  uint64_t originalNumChildren = original.getNumChildren();
   Node returnNode;
   switch (oldKind)
   {
     case kind::BITVECTOR_PLUS:
     {
+      Assert(originalNumChildren == 2);
       uint64_t bvsize = original[0].getType().getBitVectorSize();
-      /**
-       * we avoid modular arithmetics by the addition of an
-       * indicator variable sigma.
-       * Tr(a+b) is Tr(a)+Tr(b)-(sigma*2^k),
-       * with k being the bit width,
-       * and sigma being either 0 or 1.
-       */
-      Node sigma = d_nm->mkSkolem(
-          "__bvToInt_sigma_var",
-          d_nm->integerType(),
-          "Variable introduced in bvToInt pass to avoid integer mod");
       Node plus = d_nm->mkNode(kind::PLUS, translated_children);
-      Node multSig = d_nm->mkNode(kind::MULT, sigma, pow2(bvsize));
-      returnNode = d_nm->mkNode(kind::MINUS, plus, multSig);
-      d_rangeAssertions.insert(d_nm->mkNode(kind::LEQ, d_zero, sigma));
-      d_rangeAssertions.insert(d_nm->mkNode(kind::LEQ, sigma, d_one));
-      d_rangeAssertions.insert(
-          mkRangeConstraint(returnNode, bvsize));
+      Node p2 = pow2(bvsize);
+      returnNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, plus, p2);
       break;
     }
     case kind::BITVECTOR_MULT:
     {
+      Assert(originalNumChildren == 2);
       uint64_t bvsize = original[0].getType().getBitVectorSize();
-      /**
-       * we use a similar trick to the one used for addition.
-       * Tr(a*b) is Tr(a)*Tr(b)-(sigma*2^k),
-       * with k being the bit width,
-       * and sigma is between [0, 2^k - 1).
-       */
-      Node sigma = d_nm->mkSkolem(
-          "__bvToInt_sigma_var",
-          d_nm->integerType(),
-          "Variable introduced in bvToInt pass to avoid integer mod");
       Node mult = d_nm->mkNode(kind::MULT, translated_children);
-      Node multSig = d_nm->mkNode(kind::MULT, sigma, pow2(bvsize));
-      returnNode = d_nm->mkNode(kind::MINUS, mult, multSig);
-      d_rangeAssertions.insert(
-          mkRangeConstraint(returnNode, bvsize));
-      if (translated_children[0].isConst() || translated_children[1].isConst())
-      {
-        /*
-         * based on equation (23), section 3.2.3 of:
-         * Bozzano et al.
-         * Encoding RTL Constructs for MathSAT: a Preliminary Report.
-         */
-        // this is an optimization when one of the children is constant
-        Node c = translated_children[0].isConst() ? translated_children[0]
-                                                  : translated_children[1];
-        d_rangeAssertions.insert(d_nm->mkNode(kind::LEQ, d_zero, sigma));
-        // the value of sigma is bounded by (c - 1)
-        // where c is the constant multiplicand
-        d_rangeAssertions.insert(d_nm->mkNode(kind::LT, sigma, c));
-      }
-      else
-      {
-        d_rangeAssertions.insert(mkRangeConstraint(sigma, bvsize));
-      }
+      Node p2 = pow2(bvsize);
+      returnNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, mult, p2);
       break;
     }
     case kind::BITVECTOR_UDIV_TOTAL:
@@ -654,7 +621,7 @@ Node BVToInt::translateWithChildren(Node original,
     {
       /**
        * higher order logic allows comparing between functions
-       * The current translation does not support this,
+       * The translation does not support this,
        * as the translated functions may be different outside
        * of the bounds that were relevant for the original
        * bit-vectors.
@@ -877,7 +844,7 @@ Node BVToInt::reconstructNode(Node originalNode,
   {
     builder << originalNode.getOperator();
   }
-  for (uint i = 0; i < originalNode.getNumChildren(); i++)
+  for (size_t i = 0; i < originalNode.getNumChildren(); i++)
   {
     Node originalChild = originalNode[i];
     Node translatedChild = translated_children[i];
diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
new file mode 100644
index 000000000..d2193d226
--- /dev/null
+++ b/src/smt/interpolation_solver.cpp
@@ -0,0 +1,142 @@
+/*********************                                                        */
+/*! \file interpolation_solver.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Ying Sheng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The solver for interpolation queries
+ **/
+
+#include "smt/interpolation_solver.h"
+
+#include "options/smt_options.h"
+#include "smt/smt_engine.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/sygus_interpol.h"
+#include "theory/smt_engine_subsolver.h"
+
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace smt {
+
+InterpolationSolver::InterpolationSolver(SmtEngine* parent) : d_parent(parent)
+{
+}
+
+InterpolationSolver::~InterpolationSolver() {}
+
+bool InterpolationSolver::getInterpol(const Node& conj,
+                                      const TypeNode& grammarType,
+                                      Node& interpol)
+{
+  if (options::produceInterpols() == options::ProduceInterpols::NONE)
+  {
+    const char* msg =
+        "Cannot get interpolation when produce-interpol options is off.";
+    throw ModalException(msg);
+  }
+  Trace("sygus-interpol") << "SmtEngine::getInterpol: conjecture " << conj
+                          << std::endl;
+  std::vector<Expr> easserts = d_parent->getExpandedAssertions();
+  std::vector<Node> axioms;
+  for (unsigned i = 0, size = easserts.size(); i < size; i++)
+  {
+    axioms.push_back(Node::fromExpr(easserts[i]));
+  }
+  // must expand definitions
+  Node conjn = d_parent->expandDefinitions(conj);
+  std::string name("A");
+
+  quantifiers::SygusInterpol interpolSolver;
+  if (interpolSolver.SolveInterpolation(
+          name, axioms, conjn, grammarType, interpol))
+  {
+    if (options::checkInterpols())
+    {
+      checkInterpol(interpol.toExpr(), easserts, conj);
+    }
+    return true;
+  }
+  return false;
+}
+
+bool InterpolationSolver::getInterpol(const Node& conj, Node& interpol)
+{
+  TypeNode grammarType;
+  return getInterpol(conj, grammarType, interpol);
+}
+
+void InterpolationSolver::checkInterpol(Expr interpol,
+                                        const std::vector<Expr>& easserts,
+                                        const Node& conj)
+{
+  Assert(interpol.getType().isBoolean());
+  Trace("check-interpol") << "SmtEngine::checkInterpol: get expanded assertions"
+                          << std::endl;
+
+  // two checks: first, axioms imply interpol, second, interpol implies conj.
+  for (unsigned j = 0; j < 2; j++)
+  {
+    if (j == 1)
+    {
+      Trace("check-interpol") << "SmtEngine::checkInterpol: conjecture is "
+                              << conj.toExpr() << std::endl;
+    }
+    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+                            << ": make new SMT engine" << std::endl;
+    // Start new SMT engine to check solution
+    std::unique_ptr<SmtEngine> itpChecker;
+    initializeSubsolver(itpChecker);
+    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+                            << ": asserting formulas" << std::endl;
+    if (j == 0)
+    {
+      for (const Expr& e : easserts)
+      {
+        itpChecker->assertFormula(e);
+      }
+      Expr negitp = interpol.notExpr();
+      itpChecker->assertFormula(negitp);
+    }
+    else
+    {
+      itpChecker->assertFormula(interpol);
+      Assert(!conj.isNull());
+      itpChecker->assertFormula(conj.toExpr().notExpr());
+    }
+    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+                            << ": check the assertions" << std::endl;
+    Result r = itpChecker->checkSat();
+    Trace("check-interpol") << "SmtEngine::checkInterpol: phase " << j
+                            << ": result is " << r << std::endl;
+    std::stringstream serr;
+    if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
+    {
+      if (j == 0)
+      {
+        serr << "SmtEngine::checkInterpol(): negated produced solution cannot "
+                "be shown "
+                "satisfiable with assertions, result was "
+             << r;
+      }
+      else
+      {
+        serr
+            << "SmtEngine::checkInterpol(): negated conjecture cannot be shown "
+               "satisfiable with produced solution, result was "
+            << r;
+      }
+      InternalError() << serr.str();
+    }
+  }
+}
+
+}  // namespace smt
+}  // namespace CVC4
diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h
new file mode 100644
index 000000000..8e6d2cd14
--- /dev/null
+++ b/src/smt/interpolation_solver.h
@@ -0,0 +1,86 @@
+/*********************                                                        */
+/*! \file interpolation_solver.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Ying Sheng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief The solver for interpolation queries
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__SMT__INTERPOLATION_SOLVER_H
+#define CVC4__SMT__INTERPOLATION_SOLVER_H
+
+#include "expr/node.h"
+#include "expr/type_node.h"
+
+namespace CVC4 {
+
+class SmtEngine;
+
+namespace smt {
+
+/**
+ * A solver for interpolation queries.
+ *
+ * This class is responsible for responding to get-interpol commands. It spawns
+ * a subsolver SmtEngine for a sygus conjecture that captures the interpolation
+ * query, and implements supporting utility methods such as checkInterpol.
+ */
+class InterpolationSolver
+{
+ public:
+  InterpolationSolver(SmtEngine* parent);
+  ~InterpolationSolver();
+
+  /**
+   * 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.
+   *
+   * @param conj The conjecture of the interpolation problem.
+   * @param grammarType A sygus datatype type that encodes the syntax
+   * restrictions on the shape of possible solutions.
+   * @param interpol This argument is updated to contain the solution to the
+   * interpolation problem.
+   *
+   * This method invokes a separate copy of the SMT engine for solving the
+   * corresponding sygus problem for generating such a solution.
+   */
+  bool getInterpol(const Node& conj,
+                   const TypeNode& grammarType,
+                   Node& interpol);
+
+  /**
+   * Same as above, but without user-provided grammar restrictions. A default
+   * grammar is chosen internally using the sygus grammar constructor utility.
+   */
+  bool getInterpol(const Node& conj, Node& interpol);
+
+  /**
+   * 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);
+
+ private:
+  /** The parent SMT engine */
+  SmtEngine* d_parent;
+};
+
+}  // namespace smt
+}  // namespace CVC4
+
+#endif /* CVC4__SMT__INTERPOLATION_SOLVER_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7f824bff3..d271ca05d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -75,6 +75,7 @@
 #include "smt/defined_function.h"
 #include "smt/dump_manager.h"
 #include "smt/expr_names.h"
+#include "smt/interpolation_solver.h"
 #include "smt/listeners.h"
 #include "smt/logic_request.h"
 #include "smt/model_blocker.h"
@@ -134,6 +135,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_definedFunctions(nullptr),
       d_sygusSolver(nullptr),
       d_abductSolver(nullptr),
+      d_interpolSolver(nullptr),
       d_quantElimSolver(nullptr),
       d_assignments(nullptr),
       d_logic(),
@@ -299,6 +301,10 @@ void SmtEngine::finishInit()
   {
     d_abductSolver.reset(new AbductionSolver(this));
   }
+  if (options::produceInterpols() != options::ProduceInterpols::NONE)
+  {
+    d_interpolSolver.reset(new InterpolationSolver(this));
+  }
 
   d_pp->finishInit();
 
@@ -1755,12 +1761,6 @@ void SmtEngine::checkModel(bool hardFailure) {
   Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
 }
 
-void SmtEngine::checkInterpol(Expr interpol,
-                              const std::vector<Expr>& easserts,
-                              const Node& conj)
-{
-}
-
 // TODO(#1108): Simplify the error reporting of this method.
 UnsatCore SmtEngine::getUnsatCore() {
   Trace("smt") << "SMT getUnsatCore()" << endl;
@@ -1818,7 +1818,11 @@ bool SmtEngine::getInterpol(const Node& conj,
                             const TypeNode& grammarType,
                             Node& interpol)
 {
-  return false;
+  bool success = d_interpolSolver->getInterpol(conj, grammarType, interpol);
+  // notify the state of whether the get-interpol call was successfuly, which
+  // impacts the SMT mode.
+  d_state->notifyGetInterpol(success);
+  return success;
 }
 
 bool SmtEngine::getInterpol(const Node& conj, Node& interpol)
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index e95e36c3d..eec17a5f8 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -105,6 +105,7 @@ class Preprocessor;
 class SmtSolver;
 class SygusSolver;
 class AbductionSolver;
+class InterpolationSolver;
 class QuantElimSolver;
 /**
  * Representation of a defined function.  We keep these around in
@@ -1101,6 +1102,8 @@ class CVC4_PUBLIC SmtEngine
 
   /** The solver for abduction queries */
   std::unique_ptr<smt::AbductionSolver> d_abductSolver;
+  /** The solver for interpolation queries */
+  std::unique_ptr<smt::InterpolationSolver> d_interpolSolver;
   /** The solver for quantifier elimination queries */
   std::unique_ptr<smt::QuantElimSolver> d_quantElimSolver;
   /**
diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index 07f1d3321..4f3782e2a 100644
--- a/src/smt/smt_engine_state.cpp
+++ b/src/smt/smt_engine_state.cpp
@@ -122,6 +122,20 @@ void SmtEngineState::notifyGetAbduct(bool success)
   }
 }
 
+void SmtEngineState::notifyGetInterpol(bool success)
+{
+  if (success)
+  {
+    // successfully generated an interpolant, update to interpol state
+    d_smtMode = SmtMode::INTERPOL;
+  }
+  else
+  {
+    // failed, we revert to the assert state
+    d_smtMode = SmtMode::ASSERT;
+  }
+}
+
 void SmtEngineState::setup()
 {
   // push a context
diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h
index efb86ca88..1a2ae7ee8 100644
--- a/src/smt/smt_engine_state.h
+++ b/src/smt/smt_engine_state.h
@@ -96,6 +96,18 @@ class SmtEngineState
    */
   void notifyGetAbduct(bool success);
   /**
+   * Notify that we finished an interpolation query, where success is whether
+   * the command was successful. This is managed independently of the above
+   * calls for notifying check-sat. In other words, if a get-interpol command
+   * is issued to an SmtEngine, it may use a satisfiability call (if desired)
+   * to solve the interpolation query. This method is called *in addition* to
+   * the above calls to notifyCheckSat / notifyCheckSatResult in this case.
+   * In particular, it is called after these two methods are completed.
+   * This overwrites the SMT mode to the "INTERPOL" mode if the call to
+   * interpolation was successful.
+   */
+  void notifyGetInterpol(bool success);
+  /**
    * Setup the context, which makes a single push to maintain a global
    * context around everything.
    */
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 585f13d82..afa640650 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -602,21 +602,7 @@ bool TheoryDatatypes::propagateLit(TNode literal)
 {
   Debug("dt::propagate") << "TheoryDatatypes::propagateLit(" << literal << ")"
                          << std::endl;
-  // If already in conflict, no more propagation
-  if (d_state.isInConflict())
-  {
-    Debug("dt::propagate") << "TheoryDatatypes::propagateLit(" << literal
-                           << "): already in conflict" << std::endl;
-    return false;
-  }
-  Trace("dt-prop") << "dtPropagate " << literal << std::endl;
-  // Propagate out
-  bool ok = d_out->propagate(literal);
-  if (!ok) {
-    Trace("dt-conflict") << "CONFLICT: Eq engine propagate conflict " << std::endl;
-    d_state.notifyInConflict();
-  }
-  return ok;
+  return d_im.propagateLit(literal);
 }
 
 void TheoryDatatypes::addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions ) {
@@ -671,8 +657,7 @@ void TheoryDatatypes::explain(TNode literal, std::vector<TNode>& assumptions){
 
 TrustNode TheoryDatatypes::explain(TNode literal)
 {
-  Node exp = explainLit(literal);
-  return TrustNode::mkTrustPropExp(literal, exp, nullptr);
+  return d_im.explainLit(literal);
 }
 
 Node TheoryDatatypes::explainLit(TNode literal)
@@ -692,11 +677,9 @@ Node TheoryDatatypes::explain( std::vector< Node >& lits ) {
 
 /** Conflict when merging two constants */
 void TheoryDatatypes::conflict(TNode a, TNode b){
-  Node eq = a.eqNode(b);
-  d_conflictNode = explainLit(eq);
-  Trace("dt-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl;
-  d_out->conflict( d_conflictNode );
-  d_state.notifyInConflict();
+  Trace("dt-conflict") << "CONFLICT: Eq engine conflict merge : " << a
+                       << " == " << b << std::endl;
+  d_im.conflictEqConstantMerge(a, b);
 }
 
 /** called when a new equivalance class is created */
@@ -744,10 +727,11 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
           std::vector< Node > rew;
           if (utils::checkClash(cons1, cons2, rew))
           {
-            d_conflictNode = explainLit(unifEq);
-            Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
-            d_out->conflict( d_conflictNode );
-            d_state.notifyInConflict();
+            std::vector<Node> conf;
+            conf.push_back(unifEq);
+            Trace("dt-conflict")
+                << "CONFLICT: Clash conflict : " << conf << std::endl;
+            d_im.conflictExp(conf, nullptr);
             return;
           }
           else
@@ -946,13 +930,12 @@ void TheoryDatatypes::addTester(
     {
       if( !eqc->d_constructor.get().isNull() ){
         //conflict because equivalence class contains a constructor
-        std::vector< TNode > assumptions;
-        explain( t, assumptions );
-        explainEquality( eqc->d_constructor.get(), t_arg, true, assumptions );
-        d_conflictNode = mkAnd( assumptions );
-        Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl;
-        d_out->conflict( d_conflictNode );
-        d_state.notifyInConflict();
+        std::vector<Node> conf;
+        conf.push_back(t);
+        conf.push_back(eqc->d_constructor.get().eqNode(t_arg));
+        Trace("dt-conflict")
+            << "CONFLICT: Tester eq conflict " << conf << std::endl;
+        d_im.conflictExp(conf, nullptr);
         return;
       }else{
         makeConflict = true;
@@ -1051,15 +1034,13 @@ void TheoryDatatypes::addTester(
     }
   }
   if( makeConflict ){
-    d_state.notifyInConflict();
     Debug("datatypes-labels") << "Explain " << j << " " << t << std::endl;
-    std::vector< TNode > assumptions;
-    explain( j, assumptions );
-    explain( t, assumptions );
-    explainEquality( jt[0], t_arg, true, assumptions );
-    d_conflictNode = mkAnd( assumptions );
-    Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl;
-    d_out->conflict( d_conflictNode );
+    std::vector<Node> conf;
+    conf.push_back(j);
+    conf.push_back(t);
+    conf.push_back(jt[0].eqNode(t_arg));
+    Trace("dt-conflict") << "CONFLICT: Tester conflict : " << conf << std::endl;
+    d_im.conflictExp(conf, nullptr);
   }
 }
 
@@ -1112,13 +1093,12 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
         unsigned tindex = d_labels_tindex[n][i];
         if (tindex == constructorIndex)
         {
-          std::vector< TNode > assumptions;
-          explain( t, assumptions );
-          explainEquality( c, t[0][0], true, assumptions );
-          d_conflictNode = mkAnd( assumptions );
-          Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl;
-          d_out->conflict( d_conflictNode );
-          d_state.notifyInConflict();
+          std::vector<Node> conf;
+          conf.push_back(t);
+          conf.push_back(c.eqNode(t[0][0]));
+          Trace("dt-conflict")
+              << "CONFLICT: Tester merge eq conflict : " << conf << std::endl;
+          d_im.conflictExp(conf, nullptr);
           return;
         }
       }
@@ -1671,7 +1651,7 @@ void TheoryDatatypes::checkCycles() {
           //do cycle checks
           std::map< TNode, bool > visited;
           std::map< TNode, bool > proc;
-          std::vector< TNode > expl;
+          std::vector<Node> expl;
           Trace("datatypes-cycle-check") << "...search for cycle starting at " << eqc << std::endl;
           Node cn = searchForCycle( eqc, eqc, visited, proc, expl );
           Trace("datatypes-cycle-check") << "...finish." << std::endl;
@@ -1687,10 +1667,9 @@ void TheoryDatatypes::checkCycles() {
 
           if( !cn.isNull() ) {
             Assert(expl.size() > 0);
-            d_conflictNode = mkAnd( expl );
-            Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl;
-            d_out->conflict( d_conflictNode );
-            d_state.notifyInConflict();
+            Trace("dt-conflict")
+                << "CONFLICT: Cycle conflict : " << expl << std::endl;
+            d_im.conflictExp(expl, nullptr);
             return;
           }
         }
@@ -1860,16 +1839,23 @@ void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector<
 }
 
 //postcondition: if cycle detected, explanation is why n is a subterm of on
-Node TheoryDatatypes::searchForCycle( TNode n, TNode on,
-                                      std::map< TNode, bool >& visited, std::map< TNode, bool >& proc,
-                                      std::vector< TNode >& explanation, bool firstTime ) {
+Node TheoryDatatypes::searchForCycle(TNode n,
+                                     TNode on,
+                                     std::map<TNode, bool>& visited,
+                                     std::map<TNode, bool>& proc,
+                                     std::vector<Node>& explanation,
+                                     bool firstTime)
+{
   Trace("datatypes-cycle-check2") << "Search for cycle " << n << " " << on << endl;
   TNode ncons;
   TNode nn;
   if( !firstTime ){
     nn = getRepresentative( n );
     if( nn==on ){
-      explainEquality( n, nn, true, explanation );
+      if (n != nn)
+      {
+        explanation.push_back(n.eqNode(nn));
+      }
       return on;
     }
   }else{
@@ -1893,7 +1879,7 @@ Node TheoryDatatypes::searchForCycle( TNode n, TNode on,
           //add explanation for why the constructor is connected
           if (n != nncons)
           {
-            explainEquality(n, nncons, true, explanation);
+            explanation.push_back(n.eqNode(nncons));
           }
           return on;
         }else if( !cn.isNull() ){
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index bf5d33177..d34390a5f 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -293,9 +293,12 @@ private:
   Node removeUninterpretedConstants( Node n, std::map< Node, Node >& visited );
   /** for checking if cycles exist */
   void checkCycles();
-  Node searchForCycle( TNode n, TNode on,
-                       std::map< TNode, bool >& visited, std::map< TNode, bool >& proc,
-                       std::vector< TNode >& explanation, bool firstTime = true );
+  Node searchForCycle(TNode n,
+                      TNode on,
+                      std::map<TNode, bool>& visited,
+                      std::map<TNode, bool>& proc,
+                      std::vector<Node>& explanation,
+                      bool firstTime = true);
   /** for checking whether two codatatype terms must be equal */
   void separateBisimilar( std::vector< Node >& part, std::vector< std::vector< Node > >& part_out,
                           std::vector< TNode >& exp,
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index c2ca83e41..4d18c850b 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/rewriter.h"
+#include "theory/smt_engine_subsolver.h"
 
 namespace CVC4 {
 namespace theory {
@@ -30,8 +31,6 @@ namespace quantifiers {
 
 SygusInterpol::SygusInterpol() {}
 
-SygusInterpol::SygusInterpol(LogicInfo logic) : d_logic(logic) {}
-
 void SygusInterpol::collectSymbols(const std::vector<Node>& axioms,
                                    const Node& conj)
 {
@@ -75,6 +74,9 @@ void SygusInterpol::createVariables(bool needsShared)
     Node var = nm->mkBoundVar(tn);
     d_vars.push_back(var);
     Node vlv = nm->mkBoundVar(ss.str(), tn);
+    // set that this variable encodes the term s
+    SygusVarToTermAttribute sta;
+    vlv.setAttribute(sta, s);
     d_vlvs.push_back(vlv);
     if (!needsShared || d_symSetShared.find(s) != d_symSetShared.end())
     {
@@ -266,7 +268,7 @@ void SygusInterpol::mkSygusConjecture(Node itp,
   Trace("sygus-interpol") << "Generate: " << d_sygusConj << std::endl;
 }
 
-bool SygusInterpol::findInterpol(Expr& interpol, Node itp)
+bool SygusInterpol::findInterpol(Node& interpol, Node itp)
 {
   // get the synthesis solution
   std::map<Node, Node> sols;
@@ -283,31 +285,31 @@ bool SygusInterpol::findInterpol(Expr& interpol, Node itp)
   }
   Trace("sygus-interpol") << "SmtEngine::getInterpol: solution is "
                           << its->second << std::endl;
-  Node interpoln = its->second;
+  interpol = its->second;
   // replace back the created variables to original symbols.
-  Node interpoln_reduced;
-  if (interpoln.getKind() == kind::LAMBDA)
+  if (interpol.getKind() == kind::LAMBDA)
   {
-    interpoln_reduced = interpoln[1];
+    interpol = interpol[1];
   }
-  else
+
+  // get the grammar type for the interpolant
+  Node igdtbv = itp.getAttribute(SygusSynthFunVarListAttribute());
+  Assert(!igdtbv.isNull());
+  Assert(igdtbv.getKind() == kind::BOUND_VAR_LIST);
+  // convert back to original
+  // must replace formal arguments of itp with the free variables in the
+  // input problem that they correspond to.
+  std::vector<Node> vars;
+  std::vector<Node> syms;
+  SygusVarToTermAttribute sta;
+  for (const Node& bv : igdtbv)
   {
-    interpoln_reduced = interpoln;
+    vars.push_back(bv);
+    syms.push_back(bv.hasAttribute(sta) ? bv.getAttribute(sta) : bv);
   }
-  if (interpoln.getNumChildren() != 0 && interpoln[0].getNumChildren() != 0)
-  {
-    std::vector<Node> formals;
-    for (const Node& n : interpoln[0])
-    {
-      formals.push_back(n);
-    }
-    interpoln_reduced = interpoln_reduced.substitute(formals.begin(),
-                                                     formals.end(),
-                                                     d_symSetShared.begin(),
-                                                     d_symSetShared.end());
-  }
-  // convert to expression
-  interpol = interpoln_reduced.toExpr();
+  interpol =
+      interpol.substitute(vars.begin(), vars.end(), syms.begin(), syms.end());
+
   return true;
 }
 
@@ -315,14 +317,11 @@ bool SygusInterpol::SolveInterpolation(const std::string& name,
                                        const std::vector<Node>& axioms,
                                        const Node& conj,
                                        const TypeNode& itpGType,
-                                       Expr& interpol)
+                                       Node& interpol)
 {
-  NodeManager* nm = NodeManager::currentNM();
-  // we generate a new smt engine to do the interpolation query
-  d_subSolver.reset(new SmtEngine(nm->toExprManager()));
-  d_subSolver->setIsInternalSubsolver();
+  initializeSubsolver(d_subSolver);
   // get the logic
-  LogicInfo l = d_logic.getUnlockedCopy();
+  LogicInfo l = d_subSolver->getLogicInfo().getUnlockedCopy();
   // enable everything needed for sygus
   l.enableSygus();
   d_subSolver->setLogic(l);
diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index 0fe66694f..4abe94f15 100644
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -46,8 +46,6 @@ class SygusInterpol
  public:
   SygusInterpol();
 
-  SygusInterpol(LogicInfo logic);
-
   /**
    * Returns the sygus conjecture in interpol corresponding to the interpolation
    * problem for input problem (F above) given by axioms (Fa above), and conj
@@ -65,7 +63,7 @@ class SygusInterpol
                           const std::vector<Node>& axioms,
                           const Node& conj,
                           const TypeNode& itpGType,
-                          Expr& interpol);
+                          Node& interpol);
 
  private:
   /**
@@ -158,7 +156,7 @@ class SygusInterpol
    * @param interpol the solution to the sygus conjecture.
    * @param itp the interpolation predicate.
    */
-  bool findInterpol(Expr& interpol, Node itp);
+  bool findInterpol(Node& interpol, Node itp);
 
   /** The SMT engine subSolver
    *
@@ -179,10 +177,6 @@ class SygusInterpol
   std::unique_ptr<SmtEngine> d_subSolver;
 
   /**
-   * The logic for the local copy of SMT engine (d_subSolver).
-   */
-  LogicInfo d_logic;
-  /**
    * symbols from axioms and conjecture.
    */
   std::vector<Node> d_syms;
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index c9b6a9d89..573449287 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -1646,9 +1646,9 @@ void TheorySep::computeLabelModel( Node lbl ) {
     Trace("sep-process") << "Model value (from valuation) for " << lbl << " : " << v_val << std::endl;
     if( v_val.getKind()!=kind::EMPTYSET ){
       while( v_val.getKind()==kind::UNION ){
-        Assert(v_val[1].getKind() == kind::SINGLETON);
-        d_label_model[lbl].d_heap_locs_model.push_back( v_val[1] );
-        v_val = v_val[0];
+        Assert(v_val[0].getKind() == kind::SINGLETON);
+        d_label_model[lbl].d_heap_locs_model.push_back(v_val[0]);
+        v_val = v_val[1];
       }
       if( v_val.getKind()==kind::SINGLETON ){
         d_label_model[lbl].d_heap_locs_model.push_back( v_val );
@@ -1916,15 +1916,13 @@ Node TheorySep::HeapInfo::getValue( TypeNode tn ) {
   Assert(d_heap_locs.size() == d_heap_locs_model.size());
   if( d_heap_locs.empty() ){
     return NodeManager::currentNM()->mkConst(EmptySet(tn));
-  }else if( d_heap_locs.size()==1 ){
-    return d_heap_locs[0];
-  }else{
-    Node curr = NodeManager::currentNM()->mkNode( kind::UNION, d_heap_locs[0], d_heap_locs[1] );
-    for( unsigned j=2; j<d_heap_locs.size(); j++ ){
-      curr = NodeManager::currentNM()->mkNode( kind::UNION, curr, d_heap_locs[j] );
-    }
-    return curr;
   }
+  Node curr = d_heap_locs[0];
+  for (unsigned j = 1; j < d_heap_locs.size(); j++)
+  {
+    curr = NodeManager::currentNM()->mkNode(kind::UNION, d_heap_locs[j], curr);
+  }
+  return curr;
 }
 
 }/* CVC4::theory::sep namespace */
diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h
index 0607a0e6c..b53a1c03d 100644
--- a/src/theory/sets/normal_form.h
+++ b/src/theory/sets/normal_form.h
@@ -25,6 +25,12 @@ namespace sets {
 
 class NormalForm {
  public:
+  /**
+   * Constructs a set of the form:
+   *   (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
+   * from the set { c1 ... cn }, also handles empty set case, which is why
+   * setType is passed to this method.
+   */
   template <bool ref_count>
   static Node elementsToSet(const std::set<NodeTemplate<ref_count> >& elements,
                             TypeNode setType)
@@ -42,12 +48,21 @@ class NormalForm {
       Node cur = nm->mkNode(kind::SINGLETON, *it);
       while (++it != elements.end())
       {
-        cur = nm->mkNode(kind::UNION, cur, nm->mkNode(kind::SINGLETON, *it));
+        cur = nm->mkNode(kind::UNION, nm->mkNode(kind::SINGLETON, *it), cur);
       }
       return cur;
     }
   }
 
+  /**
+   * Returns true if n is considered a to be a (canonical) constant set value.
+   * A canonical set value is one whose AST is:
+   *   (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
+   * where c1 ... cn are constants and the node identifier of these constants
+   * are such that:
+   *   c1 > ... > cn.
+   * Also handles the corner cases of empty set and singleton set.
+   */
   static bool checkNormalConstant(TNode n) {
     Debug("sets-checknormal") << "[sets-checknormal] checkNormal " << n << " :"
                               << std::endl;
@@ -56,46 +71,62 @@ class NormalForm {
     } else if (n.getKind() == kind::SINGLETON) {
       return n[0].isConst();
     } else if (n.getKind() == kind::UNION) {
-      // assuming (union ... (union {SmallestNodeID} {BiggerNodeId}) ...
-      // {BiggestNodeId})
-
-      // store BiggestNodeId in prvs
-      if (n[1].getKind() != kind::SINGLETON) return false;
-      if (!n[1][0].isConst()) return false;
-      Debug("sets-checknormal")
-          << "[sets-checknormal]              frst element = " << n[1][0] << " "
-          << n[1][0].getId() << std::endl;
-      TNode prvs = n[1][0];
-      n = n[0];
+      // assuming (union {SmallestNodeID} ... (union {BiggerNodeId} ...
 
+      Node orig = n;
+      TNode prvs;
       // check intermediate nodes
-      while (n.getKind() == kind::UNION) {
-        if (n[1].getKind() != kind::SINGLETON) return false;
-        if (!n[1].isConst()) return false;
+      while (n.getKind() == kind::UNION)
+      {
+        if (n[0].getKind() != kind::SINGLETON || !n[0][0].isConst())
+        {
+          // not a constant
+          Trace("sets-isconst") << "sets::isConst: " << orig << " not due to "
+                                << n[0] << std::endl;
+          return false;
+        }
         Debug("sets-checknormal")
-            << "[sets-checknormal]              element = " << n[1][0] << " "
-            << n[1][0].getId() << std::endl;
-        if (n[1][0] >= prvs) return false;
-        prvs = n[1][0];
-        n = n[0];
+            << "[sets-checknormal]              element = " << n[0][0] << " "
+            << n[0][0].getId() << std::endl;
+        if (!prvs.isNull() && n[0][0] >= prvs)
+        {
+          Trace("sets-isconst")
+              << "sets::isConst: " << orig << " not due to compare " << n[0][0]
+              << std::endl;
+          return false;
+        }
+        prvs = n[0][0];
+        n = n[1];
       }
 
       // check SmallestNodeID is smallest
-      if (n.getKind() != kind::SINGLETON) return false;
-      if (!n[0].isConst()) return false;
+      if (n.getKind() != kind::SINGLETON || !n[0].isConst())
+      {
+        Trace("sets-isconst") << "sets::isConst: " << orig
+                              << " not due to final " << n << std::endl;
+        return false;
+      }
       Debug("sets-checknormal")
           << "[sets-checknormal]              lst element = " << n[0] << " "
           << n[0].getId() << std::endl;
-      if (n[0] >= prvs) return false;
-
-      // we made it
-      return true;
-
-    } else {
-      return false;
+      // compare last ID
+      if (n[0] < prvs)
+      {
+        return true;
+      }
+      Trace("sets-isconst")
+          << "sets::isConst: " << orig << " not due to compare final " << n[0]
+          << std::endl;
     }
+    return false;
   }
 
+  /**
+   * Converts a set term to a std::set of its elements. This expects a set of
+   * the form:
+   *   (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
+   * Also handles the corner cases of empty set and singleton set.
+   */
   static std::set<Node> getElementsFromNormalConstant(TNode n) {
     Assert(n.isConst());
     std::set<Node> ret;
@@ -103,29 +134,15 @@ class NormalForm {
       return ret;
     }
     while (n.getKind() == kind::UNION) {
-      Assert(n[1].getKind() == kind::SINGLETON);
-      ret.insert(ret.begin(), n[1][0]);
-      n = n[0];
+      Assert(n[0].getKind() == kind::SINGLETON);
+      ret.insert(ret.begin(), n[0][0]);
+      n = n[1];
     }
     Assert(n.getKind() == kind::SINGLETON);
     ret.insert(n[0]);
     return ret;
   }
   
-  
-  //AJR
-  
-  static void getElementsFromBop( Kind k, Node n, std::vector< Node >& els ){
-    if( n.getKind()==k ){
-      for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        getElementsFromBop( k, n[i], els );
-      }
-    }else{
-      if( std::find( els.begin(), els.end(), n )==els.end() ){
-        els.push_back( n );
-      }
-    }
-  }
   static Node mkBop( Kind k, std::vector< Node >& els, TypeNode tn, unsigned index = 0 ){
     if( index>=els.size() ){
       return NodeManager::currentNM()->mkConst(EmptySet(tn));
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 741f45dd8..b1831f261 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -320,7 +320,7 @@ void TheorySetsPrivate::fullEffortCheck()
         Node n = (*eqc_i);
         if (n != eqc)
         {
-          Trace("sets-eqc") << n << " ";
+          Trace("sets-eqc") << n << " (" << n.isConst() << ") ";
         }
         TypeNode tnn = n.getType();
         if (isSet)
diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index eb168c6ed..50aa89cc8 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -27,7 +27,7 @@ namespace CVC4 {
 namespace theory {
 namespace sets {
 
-bool checkConstantMembership(TNode elementTerm, TNode setTerm)
+bool TheorySetsRewriter::checkConstantMembership(TNode elementTerm, TNode setTerm)
 {
   if(setTerm.getKind() == kind::EMPTYSET) {
     return false;
@@ -38,12 +38,11 @@ bool checkConstantMembership(TNode elementTerm, TNode setTerm)
   }
 
   Assert(setTerm.getKind() == kind::UNION
-         && setTerm[1].getKind() == kind::SINGLETON)
+         && setTerm[0].getKind() == kind::SINGLETON)
       << "kind was " << setTerm.getKind() << ", term: " << setTerm;
 
-  return
-    elementTerm == setTerm[1][0] ||
-    checkConstantMembership(elementTerm, setTerm[0]);
+  return elementTerm == setTerm[0][0]
+         || checkConstantMembership(elementTerm, setTerm[1]);
 }
 
 // static
@@ -53,6 +52,8 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
   Trace("sets-postrewrite") << "Process: " << node << std::endl;
 
   if(node.isConst()) {
+    Trace("sets-rewrite-nf")
+        << "Sets::rewrite: no rewrite (constant) " << node << std::endl;
     // Dare you touch the const and mangle it to something else.
     return RewriteResponse(REWRITE_DONE, node);
   }
@@ -163,23 +164,13 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
       Assert(newNode.isConst());
       Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
       return RewriteResponse(REWRITE_DONE, newNode);
-    } else {
-      std::vector< Node > els;
-      NormalForm::getElementsFromBop( kind::INTERSECTION, node, els );
-      std::sort( els.begin(), els.end() );
-      Node rew = NormalForm::mkBop( kind::INTERSECTION, els, node.getType() );
-      if( rew!=node ){
-        Trace("sets-rewrite") << "Sets::rewrite " << node << " -> " << rew << std::endl;
-      }
-      return RewriteResponse(REWRITE_DONE, rew);
     }
-    /*
-    } else if (node[0] > node[1]) {
+    else if (node[0] > node[1])
+    {
       Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
-      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
       return RewriteResponse(REWRITE_DONE, newNode);
     }
-    */
+    // we don't merge non-constant intersections
     break;
   }//kind::INTERSECION
 
@@ -200,19 +191,16 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
                           std::inserter(newSet, newSet.begin()));
       Node newNode = NormalForm::elementsToSet(newSet, node.getType());
       Assert(newNode.isConst());
-      Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
+      Trace("sets-rewrite")
+          << "Sets::rewrite: UNION_CONSTANT_MERGE: " << newNode << std::endl;
       return RewriteResponse(REWRITE_DONE, newNode);
-    } else {
-      std::vector< Node > els;
-      NormalForm::getElementsFromBop( kind::UNION, node, els );
-      std::sort( els.begin(), els.end() );
-      Node rew = NormalForm::mkBop( kind::UNION, els, node.getType() );
-      if( rew!=node ){
-        Trace("sets-rewrite") << "Sets::rewrite " << node << " -> " << rew << std::endl;
-      }
-      Trace("sets-rewrite") << "...no rewrite." << std::endl;
-      return RewriteResponse(REWRITE_DONE, rew);
     }
+    else if (node[0] > node[1])
+    {
+      Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
+      return RewriteResponse(REWRITE_DONE, newNode);
+    }
+    // we don't merge non-constant unions
     break;
   }//kind::UNION
   case kind::COMPLEMENT: {
@@ -491,16 +479,15 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
 // static
 RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
   NodeManager* nm = NodeManager::currentNM();
-
-  if(node.getKind() == kind::EQUAL) {
-
+  Kind k = node.getKind();
+  if (k == kind::EQUAL)
+  {
     if(node[0] == node[1]) {
       return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
     }
-
-  }//kind::EQUAL
-  else if(node.getKind() == kind::INSERT) {
-
+  }
+  else if (k == kind::INSERT)
+  {
     Node insertedElements = nm->mkNode(kind::SINGLETON, node[0]);
     size_t setNodeIndex =  node.getNumChildren()-1;
     for(size_t i = 1; i < setNodeIndex; ++i) {
@@ -512,17 +499,16 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
                            nm->mkNode(kind::UNION,
                                       insertedElements,
                                       node[setNodeIndex]));
-
-  }//kind::INSERT
-  else if(node.getKind() == kind::SUBSET) {
-
+  }
+  else if (k == kind::SUBSET)
+  {
     // rewrite (A subset-or-equal B) as (A union B = B)
     return RewriteResponse(REWRITE_AGAIN,
                            nm->mkNode(kind::EQUAL,
                                       nm->mkNode(kind::UNION, node[0], node[1]),
                                       node[1]) );
-
-  }//kind::SUBSET
+  }
+  // could have an efficient normalizer for union here
 
   return RewriteResponse(REWRITE_DONE, node);
 }
diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
index 7d1a6c188..fdc9caefb 100644
--- a/src/theory/sets/theory_sets_rewriter.h
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -70,7 +70,11 @@ class TheorySetsRewriter : public TheoryRewriter
     // often this will suffice
     return postRewrite(equality).d_node;
   }
-
+private:
+  /**
+   * Returns true if elementTerm is in setTerm, where both terms are constants.
+   */
+  bool checkConstantMembership(TNode elementTerm, TNode setTerm);
 }; /* class TheorySetsRewriter */
 
 }/* CVC4::theory::sets namespace */
diff --git a/src/theory/theory_inference_manager.cpp b/src/theory/theory_inference_manager.cpp
index 81f5c45e6..980763040 100644
--- a/src/theory/theory_inference_manager.cpp
+++ b/src/theory/theory_inference_manager.cpp
@@ -141,6 +141,7 @@ TrustNode TheoryInferenceManager::mkConflictExp(const std::vector<Node>& exp,
 {
   if (d_pfee != nullptr)
   {
+    Assert(pg != nullptr);
     // use proof equality engine to construct the trust node
     return d_pfee->assertConflict(exp, pg);
   }
diff --git a/src/theory/uf/proof_equality_engine.cpp b/src/theory/uf/proof_equality_engine.cpp
index 00e4662f9..fa9482094 100644
--- a/src/theory/uf/proof_equality_engine.cpp
+++ b/src/theory/uf/proof_equality_engine.cpp
@@ -221,6 +221,7 @@ TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
 TrustNode ProofEqEngine::assertConflict(const std::vector<Node>& exp,
                                         ProofGenerator* pg)
 {
+  Assert(pg != nullptr);
   Trace("pfee") << "pfee::assertConflict " << exp << " via generator"
                 << std::endl;
   return assertLemma(d_false, exp, {}, pg);
@@ -306,6 +307,7 @@ TrustNode ProofEqEngine::assertLemma(Node conc,
                                      const std::vector<Node>& noExplain,
                                      ProofGenerator* pg)
 {
+  Assert(pg != nullptr);
   Trace("pfee") << "pfee::assertLemma " << conc << ", exp = " << exp
                 << ", noExplain = " << noExplain << " via buffer with generator"
                 << std::endl;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index ed07c7474..ef0981372 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -858,6 +858,7 @@ set(regress_0_tests
   regress0/sep/sep-01.smt2
   regress0/sep/sep-plus1.smt2
   regress0/sep/sep-simp-unsat-emp.smt2
+  regress0/sep/simple-080420-const-sets.smt2
   regress0/sep/skolem_emp.smt2
   regress0/sep/trees-1.smt2
   regress0/sep/wand-crash.smt2
@@ -1942,6 +1943,14 @@ set(regress_1_tests
   regress1/sygus/inv-example.sy
   regress1/sygus/inv-missed-sol-true.sy
   regress1/sygus/inv-unused.sy
+  regress1/sygus/interpol1.smt2
+  regress1/sygus/interpol2.smt2
+  regress1/sygus/interpol3.smt2
+  regress1/sygus/interpol_arr1.smt2
+  regress1/sygus/interpol_arr2.smt2
+  regress1/sygus/interpol_cosa_1.smt2
+  regress1/sygus/interpol_from_pono_1.smt2
+  regress1/sygus/interpol_from_pono_2.smt2
   regress1/sygus/issue2914.sy
   regress1/sygus/issue2935.sy
   regress1/sygus/issue3199.smt2
diff --git a/test/regress/regress0/sep/simple-080420-const-sets.smt2 b/test/regress/regress0/sep/simple-080420-const-sets.smt2
new file mode 100644
index 000000000..1d85fb133
--- /dev/null
+++ b/test/regress/regress0/sep/simple-080420-const-sets.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_ALL_SUPPORTED)
+(set-option :produce-models true)
+(set-info :status sat)
+(declare-fun x () Int)
+
+; works
+;(assert (sep (pto 1 2) (pto 5 6) (pto x 8)))
+
+; didn't work due to sets rewriter
+(assert (sep (pto 1 2) (pto 5 6) (pto 7 8)))
+
+(check-sat)
diff --git a/test/regress/regress1/sygus/interpol1.smt2 b/test/regress/regress1/sygus/interpol1.smt2
new file mode 100644
index 000000000..58ef5420f
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol1.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic NIA)
+(declare-fun x ( ) Int)
+(declare-fun y ( ) Int)
+(declare-fun z ( ) Int)
+(assert (= (* 2 x) y))
+(get-interpol A (distinct (+ (* 2 z) 1) y)
+
+; the grammar for the interpol-to-synthesize
+((Start Bool) (StartInt Int))
+(
+(Start Bool ((< StartInt StartInt)))
+(StartInt Int 
+(y (+ StartInt StartInt) (div StartInt StartInt) (mod StartInt StartInt) 0 1 2))
+)
+
+)
diff --git a/test/regress/regress1/sygus/interpol2.smt2 b/test/regress/regress1/sygus/interpol2.smt2
new file mode 100644
index 000000000..c6876ee15
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol2.smt2
@@ -0,0 +1,31 @@
+; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+(set-logic QF_UFLIA)
+
+; Let A1,...,An be formulas (called assumptions)
+; Let C be a formula (called a conjecture)
+; An interpolant of {A1,...,An} and G is any formula B such that:
+; - A1,...,An |- B
+; - B |- C
+; - B has only variables that occur both in {A_1,...,A_n} and B.
+
+;The variables used are n,m,x,y, all integers.
+(declare-fun n () Int)
+(declare-fun m () Int)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+;The assumptions are:
+; (*) 1 <= n <= x <= n+5
+; (*) 1 <= y <= m
+(define-fun A1 () Bool (<= 1 n))
+(define-fun A2 () Bool (<= n x))
+(define-fun A3 () Bool (<= x (+ n 5)))
+(define-fun A4 () Bool (<= 1 y))
+(define-fun A5 () Bool (<= y m))
+(assert (and A1 A2 A3 A4 A5))
+
+;The conjuecture is: 2 <= x+y
+(get-interpol A (<= 2 (+ x y)))
diff --git a/test/regress/regress1/sygus/interpol3.smt2 b/test/regress/regress1/sygus/interpol3.smt2
new file mode 100644
index 000000000..8681acf3a
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol3.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --produce-interpols=default --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic LIA)
+(declare-fun a () Int)
+(assert (> a 1))
+(get-interpol A (> a 0))
diff --git a/test/regress/regress1/sygus/interpol_arr1.smt2 b/test/regress/regress1/sygus/interpol_arr1.smt2
new file mode 100644
index 000000000..16190f877
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol_arr1.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-fun a () (Array (_ BitVec 4) (_ BitVec 4)))
+(declare-fun y () (_ BitVec 4))
+(assert (= (select a y) (_ bv0 4)))
+(get-interpol A (distinct (select a y) (_ bv1 4)))
diff --git a/test/regress/regress1/sygus/interpol_arr2.smt2 b/test/regress/regress1/sygus/interpol_arr2.smt2
new file mode 100644
index 000000000..18ce2b35f
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol_arr2.smt2
@@ -0,0 +1,15 @@
+; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-fun arr () (Array Int Int))
+
+(define-fun A1 () Bool (<= 1 (select arr 0)))
+(define-fun A2 () Bool (<= (select arr 0) (select arr 2)))
+(define-fun A3 () Bool (<= (select arr 2) (+ (select arr 0) 5)))
+(define-fun A4 () Bool (<= 1 (select arr 3)))
+(define-fun A5 () Bool (<= (select arr 3) (select arr 1)))
+(assert (and A1 A2 A3 A4 A5))
+
+;The conjuecture is: 2 <= x+y
+(get-interpol A (<= 2 (+ (select arr 2) (select arr 3))))
diff --git a/test/regress/regress1/sygus/interpol_cosa_1.smt2 b/test/regress/regress1/sygus/interpol_cosa_1.smt2
new file mode 100644
index 000000000..583f94ed4
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol_cosa_1.smt2
@@ -0,0 +1,30 @@
+; COMMAND-LINE: --produce-interpols=conjecture --sygus-active-gen=enum --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(set-option :produce-interpols conjecture)
+(set-option :sygus-active-gen enum)
+(declare-fun cfg@1 () (_ BitVec 1))
+(declare-fun witness_0@1 () Bool)
+(declare-fun op@1 () (_ BitVec 4))
+(declare-fun counter@1 () (_ BitVec 16))
+(declare-fun input14@1 () (_ BitVec 1))
+(declare-fun clk@1 () (_ BitVec 1))
+(declare-fun a@1 () (_ BitVec 16))
+(declare-fun b@1 () (_ BitVec 16))
+(reset-assertions)
+(declare-fun cfg@0 () (_ BitVec 1))
+(declare-fun witness_0@0 () Bool)
+(declare-fun counter@0 () (_ BitVec 16))
+(declare-fun op@0 () (_ BitVec 4))
+(declare-fun input14@0 () (_ BitVec 1))
+(declare-fun b@0 () (_ BitVec 16))
+(declare-fun a@0 () (_ BitVec 16))
+(assert (and (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1)))))
+(assert (and (or (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) witness_0@0) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1)))))
+(declare-fun cfg@2 () (_ BitVec 1))
+(declare-fun counter@2 () (_ BitVec 16))
+(declare-fun op@2 () (_ BitVec 4))
+(declare-fun witness_0@2 () Bool)
+(assert (and (and (and (and true (= counter@0 (_ bv0 16))) witness_0@0) (= cfg@0 (_ bv1 1))) (and (and (and (and true (= witness_0@1 (not (= (bvand (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@0 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@0 (_ bv0 4))) (bvadd a@0 b@0) (bvsub a@0 b@0)) (bvadd a@0 b@0)) input14@0))) (_ bv1 1))))) (= op@1 (ite (= cfg@0 (_ bv1 1)) (_ bv0 4) op@0))) (= counter@1 (bvadd counter@0 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@1 (_ bv0 1)))))
+(get-interpol I (not (and (and true (and (and (and (and true (= witness_0@2 (not (= (bvand (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (_ bv1 1) (_ bv0 1)) (bvnot (ite (bvugt counter@1 ((_ zero_extend 15) (_ bv0 1))) (bvcomp (ite (not (distinct op@1 (_ bv0 4))) (bvadd a@1 b@1) (bvsub a@1 b@1)) (bvadd a@1 b@1)) input14@1))) (_ bv1 1))))) (= op@2 (ite (= cfg@1 (_ bv1 1)) (_ bv0 4) op@1))) (= counter@2 (bvadd counter@1 ((_ zero_extend 15) (_ bv1 1))))) (= cfg@2 (_ bv0 1)))) (not witness_0@2))))
diff --git a/test/regress/regress1/sygus/interpol_dt.smt2 b/test/regress/regress1/sygus/interpol_dt.smt2
new file mode 100644
index 000000000..f64ce4a0e
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol_dt.smt2
@@ -0,0 +1,12 @@
+; COMMAND-LINE: --produce-interpols=default
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-datatypes ((List 0)) (((nil) (cons (head Int) (tail List)))))
+(declare-fun x () List)
+(declare-fun y () List)
+(assert ((_ is cons) x))
+(assert ((_ is nil) (tail x)))
+(assert (= (head x) 0))
+(assert (= x y))
+(get-interpol A (distinct y nil))
diff --git a/test/regress/regress1/sygus/interpol_from_pono_1.smt2 b/test/regress/regress1/sygus/interpol_from_pono_1.smt2
new file mode 100644
index 000000000..eff00e066
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol_from_pono_1.smt2
@@ -0,0 +1,39 @@
+; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-fun a_S_a2@1 () (_ BitVec 1))
+(declare-fun a_R_a2@1 () (_ BitVec 1))
+(declare-fun a_Q_a2@1 () (_ BitVec 1))
+(declare-fun dve_invalid@1 () (_ BitVec 1))
+(declare-fun v_x1@1 () (_ BitVec 16))
+(declare-fun a_S_a1@1 () (_ BitVec 1))
+(declare-fun v_c@1 () (_ BitVec 16))
+(declare-fun v_x2@1 () (_ BitVec 16))
+(declare-fun a_Q_a1@1 () (_ BitVec 1))
+(declare-fun a_R_a1@1 () (_ BitVec 1))
+(declare-fun f3@1 () (_ BitVec 1))
+(declare-fun f0@1 () (_ BitVec 1))
+(declare-fun f5@1 () (_ BitVec 1))
+(declare-fun f1@1 () (_ BitVec 1))
+(declare-fun f2@1 () (_ BitVec 1))
+(declare-fun f4@1 () (_ BitVec 1))
+(declare-fun dve_invalid@0 () (_ BitVec 1))
+(declare-fun a_S_a2@0 () (_ BitVec 1))
+(declare-fun a_R_a2@0 () (_ BitVec 1))
+(declare-fun a_Q_a2@0 () (_ BitVec 1))
+(declare-fun a_S_a1@0 () (_ BitVec 1))
+(declare-fun a_R_a1@0 () (_ BitVec 1))
+(declare-fun a_Q_a1@0 () (_ BitVec 1))
+(declare-fun v_x2@0 () (_ BitVec 16))
+(declare-fun v_x1@0 () (_ BitVec 16))
+(declare-fun v_c@0 () (_ BitVec 16))
+(declare-fun f5@0 () (_ BitVec 1))
+(declare-fun f3@0 () (_ BitVec 1))
+(declare-fun f4@0 () (_ BitVec 1))
+(declare-fun f2@0 () (_ BitVec 1))
+(declare-fun f0@0 () (_ BitVec 1))
+(declare-fun f1@0 () (_ BitVec 1))
+(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0)))))))
+
+(get-interpol I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1)))))))
diff --git a/test/regress/regress1/sygus/interpol_from_pono_2.smt2 b/test/regress/regress1/sygus/interpol_from_pono_2.smt2
new file mode 100644
index 000000000..894e8e781
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol_from_pono_2.smt2
@@ -0,0 +1,41 @@
+; COMMAND-LINE: --produce-interpols=default --sygus-active-gen=enum --check-interpols
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-fun a_S_a2@1 () (_ BitVec 1))
+(declare-fun a_R_a2@1 () (_ BitVec 1))
+(declare-fun a_Q_a2@1 () (_ BitVec 1))
+(declare-fun dve_invalid@1 () (_ BitVec 1))
+(declare-fun v_x1@1 () (_ BitVec 16))
+(declare-fun a_S_a1@1 () (_ BitVec 1))
+(declare-fun v_c@1 () (_ BitVec 16))
+(declare-fun v_x2@1 () (_ BitVec 16))
+(declare-fun a_Q_a1@1 () (_ BitVec 1))
+(declare-fun a_R_a1@1 () (_ BitVec 1))
+(declare-fun f3@1 () (_ BitVec 1))
+(declare-fun f0@1 () (_ BitVec 1))
+(declare-fun f5@1 () (_ BitVec 1))
+(declare-fun f1@1 () (_ BitVec 1))
+(declare-fun f2@1 () (_ BitVec 1))
+(declare-fun f4@1 () (_ BitVec 1))
+(declare-fun dve_invalid@0 () (_ BitVec 1))
+(declare-fun a_S_a2@0 () (_ BitVec 1))
+(declare-fun a_R_a2@0 () (_ BitVec 1))
+(declare-fun a_Q_a2@0 () (_ BitVec 1))
+(declare-fun a_S_a1@0 () (_ BitVec 1))
+(declare-fun a_R_a1@0 () (_ BitVec 1))
+(declare-fun a_Q_a1@0 () (_ BitVec 1))
+(declare-fun v_x2@0 () (_ BitVec 16))
+(declare-fun v_x1@0 () (_ BitVec 16))
+(declare-fun v_c@0 () (_ BitVec 16))
+(declare-fun f5@0 () (_ BitVec 1))
+(declare-fun f3@0 () (_ BitVec 1))
+(declare-fun f4@0 () (_ BitVec 1))
+(declare-fun f2@0 () (_ BitVec 1))
+(declare-fun f0@0 () (_ BitVec 1))
+(declare-fun f1@0 () (_ BitVec 1))
+(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0)))))))
+(assert (and (or (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (bvult v_c@0 (_ bv2 16))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0)))))))
+
+(get-interpol I (not (and true (not (not (= (bvand (bvnot dve_invalid@1) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1)))))))
+
diff --git a/test/regress/regress1/sygus/interpol_from_pono_3.smt2 b/test/regress/regress1/sygus/interpol_from_pono_3.smt2
new file mode 100644
index 000000000..5de1d4ebd
--- /dev/null
+++ b/test/regress/regress1/sygus/interpol_from_pono_3.smt2
@@ -0,0 +1,54 @@
+; COMMAND-LINE: --produce-interpols=default
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic ALL)
+(declare-fun a_S_a2@1 () (_ BitVec 1))
+(declare-fun a_R_a2@1 () (_ BitVec 1))
+(declare-fun a_Q_a2@1 () (_ BitVec 1))
+(declare-fun dve_invalid@1 () (_ BitVec 1))
+(declare-fun v_x1@1 () (_ BitVec 16))
+(declare-fun a_S_a1@1 () (_ BitVec 1))
+(declare-fun v_c@1 () (_ BitVec 16))
+(declare-fun v_x2@1 () (_ BitVec 16))
+(declare-fun a_Q_a1@1 () (_ BitVec 1))
+(declare-fun a_R_a1@1 () (_ BitVec 1))
+(declare-fun f3@1 () (_ BitVec 1))
+(declare-fun f0@1 () (_ BitVec 1))
+(declare-fun f5@1 () (_ BitVec 1))
+(declare-fun f1@1 () (_ BitVec 1))
+(declare-fun f2@1 () (_ BitVec 1))
+(declare-fun f4@1 () (_ BitVec 1))
+(declare-fun dve_invalid@0 () (_ BitVec 1))
+(declare-fun a_S_a2@0 () (_ BitVec 1))
+(declare-fun a_R_a2@0 () (_ BitVec 1))
+(declare-fun a_Q_a2@0 () (_ BitVec 1))
+(declare-fun a_S_a1@0 () (_ BitVec 1))
+(declare-fun a_R_a1@0 () (_ BitVec 1))
+(declare-fun a_Q_a1@0 () (_ BitVec 1))
+(declare-fun v_x2@0 () (_ BitVec 16))
+(declare-fun v_x1@0 () (_ BitVec 16))
+(declare-fun v_c@0 () (_ BitVec 16))
+(declare-fun f5@0 () (_ BitVec 1))
+(declare-fun f3@0 () (_ BitVec 1))
+(declare-fun f4@0 () (_ BitVec 1))
+(declare-fun f2@0 () (_ BitVec 1))
+(declare-fun f0@0 () (_ BitVec 1))
+(declare-fun f1@0 () (_ BitVec 1))
+(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0)))))))
+(assert (and (or (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (bvult v_c@0 (_ bv2 16))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0)))))))
+
+(declare-fun dve_invalid@2 () (_ BitVec 1))
+(declare-fun a_S_a2@2 () (_ BitVec 1))
+(declare-fun a_R_a2@2 () (_ BitVec 1))
+(declare-fun a_Q_a2@2 () (_ BitVec 1))
+(declare-fun a_S_a1@2 () (_ BitVec 1))
+(declare-fun a_R_a1@2 () (_ BitVec 1))
+(declare-fun a_Q_a1@2 () (_ BitVec 1))
+(declare-fun v_x2@2 () (_ BitVec 16))
+(declare-fun v_x1@2 () (_ BitVec 16))
+(declare-fun v_c@2 () (_ BitVec 16))
+(assert (and (and (and (and (and (and (and (and (and (and (and true (= v_c@0 (_ bv0 16))) (= v_x1@0 (_ bv0 16))) (= v_x2@0 (_ bv0 16))) (= a_Q_a1@0 (_ bv0 1))) (= a_R_a1@0 (_ bv0 1))) (= a_S_a1@0 (_ bv0 1))) (= a_Q_a2@0 (_ bv0 1))) (= a_R_a2@0 (_ bv0 1))) (= a_S_a2@0 (_ bv0 1))) (= dve_invalid@0 (_ bv0 1))) (and (and (and (and (and (and (and (and (and (and true (= v_c@1 (bvxor (_ bv1 16) (ite (= f5@0 (_ bv1 1)) v_x2@0 (ite (= f2@0 (_ bv1 1)) v_x1@0 (bvxor (_ bv1 16) v_c@0)))))) (= v_x1@1 (ite (= f1@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x1@0)))) (= v_x2@1 (ite (= f4@0 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@0 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@0 (_ bv1 1)) (bvxor (_ bv1 16) v_c@0) v_x2@0)))) (= a_Q_a1@1 (bvnot (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (= a_R_a1@1 (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)))) (= a_S_a1@1 (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)))) (= a_Q_a2@1 (bvnot (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))) (= a_R_a2@1 (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)))) (= a_S_a2@1 (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)))) (= dve_invalid@1 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@0) (bvand (bvnot a_Q_a1@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@0 (bvnot f1@0))) (bvor a_S_a1@0 (bvnot f2@0))) (bvor (bvnot f3@0) (bvand (bvnot a_Q_a2@0) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@0) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@0 (bvnot f4@0))) (bvor a_S_a2@0 (bvnot f5@0))) (bvor f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@0 f1@0) (bvand f2@0 (bvor f0@0 f1@0))) (bvand f3@0 (bvor f2@0 (bvor f0@0 f1@0)))) (bvand f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0))))) (bvand f5@0 (bvor f4@0 (bvor f3@0 (bvor f2@0 (bvor f0@0 f1@0)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@0) a_R_a1@0) (bvand a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0)))) (bvor a_S_a1@0 (bvor (bvnot a_Q_a1@0) a_R_a1@0))) (bvnot (bvor (bvand (bvnot a_Q_a2@0) a_R_a2@0) (bvand a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0))))) (bvor a_S_a2@0 (bvor (bvnot a_Q_a2@0) a_R_a2@0)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)) (bvand (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0))))) (bvor (bvand (bvor a_S_a1@0 f1@0) (bvnot f2@0)) (bvor (bvand (bvor a_R_a1@0 f0@0) (bvnot f1@0)) (bvor (bvand (bvnot a_Q_a1@0) (bvnot f0@0)) f2@0)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)) (bvand (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0)))))) (bvor (bvand (bvor a_S_a2@0 f4@0) (bvnot f5@0)) (bvor (bvand (bvor a_R_a2@0 f3@0) (bvnot f4@0)) (bvor (bvand (bvnot a_Q_a2@0) (bvnot f3@0)) f5@0))))) (bvnot dve_invalid@0)))))))
+
+(get-interpol I (not (and (and true (and (and (and (and (and (and (and (and (and (and true (= v_c@2 (bvxor (_ bv1 16) (ite (= f5@1 (_ bv1 1)) v_x2@1 (ite (= f2@1 (_ bv1 1)) v_x1@1 (bvxor (_ bv1 16) v_c@1)))))) (= v_x1@2 (ite (= f1@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x1@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f0@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x1@1)))) (= v_x2@2 (ite (= f4@1 (_ bv1 1)) ((_ extract 15 0) (bvadd (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)) (bvashr (concat v_x2@1 (_ bv0 16)) (_ bv16 32)))) (ite (= f3@1 (_ bv1 1)) (bvxor (_ bv1 16) v_c@1) v_x2@1)))) (= a_Q_a1@2 (bvnot (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (= a_R_a1@2 (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)))) (= a_S_a1@2 (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)))) (= a_Q_a2@2 (bvnot (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))) (= a_R_a2@2 (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)))) (= a_S_a2@2 (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)))) (= dve_invalid@2 (bvnot (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvand (bvor (bvnot f0@1) (bvand (bvnot a_Q_a1@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1)))) (bvor a_R_a1@1 (bvnot f1@1))) (bvor a_S_a1@1 (bvnot f2@1))) (bvor (bvnot f3@1) (bvand (bvnot a_Q_a2@1) (ite (not (bvule (_ bv200 32) (bvashr (concat (bvxor (_ bv1 16) v_c@1) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1) (_ bv0 1))))) (bvor a_R_a2@1 (bvnot f4@1))) (bvor a_S_a2@1 (bvnot f5@1))) (bvor f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))) (bvnot (bvor (bvor (bvor (bvor (bvand f0@1 f1@1) (bvand f2@1 (bvor f0@1 f1@1))) (bvand f3@1 (bvor f2@1 (bvor f0@1 f1@1)))) (bvand f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1))))) (bvand f5@1 (bvor f4@1 (bvor f3@1 (bvor f2@1 (bvor f0@1 f1@1)))))))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvnot a_Q_a1@1) a_R_a1@1) (bvand a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1)))) (bvor a_S_a1@1 (bvor (bvnot a_Q_a1@1) a_R_a1@1))) (bvnot (bvor (bvand (bvnot a_Q_a2@1) a_R_a2@1) (bvand a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1))))) (bvor a_S_a2@1 (bvor (bvnot a_Q_a2@1) a_R_a2@1)))) (bvand (bvand (bvand (bvnot (bvor (bvand (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)) (bvand (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1))))) (bvor (bvand (bvor a_S_a1@1 f1@1) (bvnot f2@1)) (bvor (bvand (bvor a_R_a1@1 f0@1) (bvnot f1@1)) (bvor (bvand (bvnot a_Q_a1@1) (bvnot f0@1)) f2@1)))) (bvnot (bvor (bvand (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)) (bvand (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1)))))) (bvor (bvand (bvor a_S_a2@1 f4@1) (bvnot f5@1)) (bvor (bvand (bvor a_R_a2@1 f3@1) (bvnot f4@1)) (bvor (bvand (bvnot a_Q_a2@1) (bvnot f3@1)) f5@1))))) (bvnot dve_invalid@1)))))) (not (not (= (bvand (bvnot dve_invalid@2) (bvcomp (_ bv500 32) (bvashr (concat (bvxor (_ bv1 16) v_c@2) (_ bv0 16)) (_ bv16 32)))) (_ bv1 1)))))))
+
+
diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h
index dff4b2e98..ec0293876 100644
--- a/test/unit/theory/theory_sets_type_enumerator_white.h
+++ b/test/unit/theory/theory_sets_type_enumerator_white.h
@@ -49,32 +49,35 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
     delete d_em;
   }
 
+  void addAndCheckUnique(Node n, std::vector<Node>& elems)
+  {
+    TS_ASSERT(n.isConst());
+    TS_ASSERT(std::find(elems.begin(), elems.end(), n) == elems.end());
+    elems.push_back(n);
+  }
+
   void testSetOfBooleans()
   {
     TypeNode boolType = d_nm->booleanType();
     SetEnumerator setEnumerator(d_nm->mkSetType(boolType));
     TS_ASSERT(!setEnumerator.isFinished());
 
+    std::vector<Node> elems;
+
     Node actual0 = *setEnumerator;
-    Node expected0 =
-        d_nm->mkConst(EmptySet(d_nm->mkSetType(boolType)));
-    TS_ASSERT_EQUALS(expected0, actual0);
+    addAndCheckUnique(actual0, elems);
     TS_ASSERT(!setEnumerator.isFinished());
 
     Node actual1 = *++setEnumerator;
-    Node expected1 = d_nm->mkNode(Kind::SINGLETON, d_nm->mkConst(false));
-    TS_ASSERT_EQUALS(expected1, actual1);
+    addAndCheckUnique(actual1, elems);
     TS_ASSERT(!setEnumerator.isFinished());
 
     Node actual2 = *++setEnumerator;
-    Node expected2 = d_nm->mkNode(Kind::SINGLETON, d_nm->mkConst(true));
-    TS_ASSERT_EQUALS(expected2, actual2);
+    addAndCheckUnique(actual2, elems);
     TS_ASSERT(!setEnumerator.isFinished());
 
     Node actual3 = Rewriter::rewrite(*++setEnumerator);
-    Node expected3 =
-        Rewriter::rewrite(d_nm->mkNode(Kind::UNION, expected1, expected2));
-    TS_ASSERT_EQUALS(expected3, actual3);
+    addAndCheckUnique(actual3, elems);
     TS_ASSERT(!setEnumerator.isFinished());
 
     TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&);
@@ -95,43 +98,14 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
     TS_ASSERT_EQUALS(expected0, actual0);
     TS_ASSERT(!setEnumerator.isFinished());
 
-    Node actual1 = *++setEnumerator;
-    Node expected1 = d_nm->mkNode(
-        Kind::SINGLETON, d_nm->mkConst(UninterpretedConstant(sort, 0)));
-    TS_ASSERT_EQUALS(expected1, actual1);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual2 = *++setEnumerator;
-    Node expected2 = d_nm->mkNode(
-        Kind::SINGLETON, d_nm->mkConst(UninterpretedConstant(sort, 1)));
-    TS_ASSERT_EQUALS(expected2, actual2);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual3 = *++setEnumerator;
-    Node expected3 = d_nm->mkNode(Kind::UNION, expected1, expected2);
-    TS_ASSERT_EQUALS(expected3, actual3);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual4 = *++setEnumerator;
-    Node expected4 = d_nm->mkNode(
-        Kind::SINGLETON, d_nm->mkConst(UninterpretedConstant(sort, 2)));
-    TS_ASSERT_EQUALS(expected4, actual4);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual5 = *++setEnumerator;
-    Node expected5 = d_nm->mkNode(Kind::UNION, expected1, expected4);
-    TS_ASSERT_EQUALS(expected5, actual5);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual6 = *++setEnumerator;
-    Node expected6 = d_nm->mkNode(Kind::UNION, expected2, expected4);
-    TS_ASSERT_EQUALS(expected6, actual6);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual7 = *++setEnumerator;
-    Node expected7 = d_nm->mkNode(Kind::UNION, expected3, expected4);
-    TS_ASSERT_EQUALS(expected7, actual7);
-    TS_ASSERT(!setEnumerator.isFinished());
+    std::vector<Node> elems;
+    for (unsigned i = 0; i < 7; i++)
+    {
+      Node actual = *setEnumerator;
+      addAndCheckUnique(actual, elems);
+      TS_ASSERT(!setEnumerator.isFinished());
+      ++setEnumerator;
+    }
   }
 
   void testSetOfFiniteDatatype()
@@ -151,46 +125,14 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
 
     Node blue = d_nm->mkNode(APPLY_CONSTRUCTOR, dtcons[2]->getConstructor());
 
-    Node actual0 = *setEnumerator;
-    Node expected0 =
-        d_nm->mkConst(EmptySet(d_nm->mkSetType(datatype)));
-    TS_ASSERT_EQUALS(expected0, actual0);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual1 = *++setEnumerator;
-    Node expected1 = d_nm->mkNode(Kind::SINGLETON, red);
-    TS_ASSERT_EQUALS(expected1, actual1);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual2 = *++setEnumerator;
-    Node expected2 = d_nm->mkNode(Kind::SINGLETON, green);
-    TS_ASSERT_EQUALS(expected2, actual2);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual3 = *++setEnumerator;
-    Node expected3 = d_nm->mkNode(Kind::UNION, expected1, expected2);
-    TS_ASSERT_EQUALS(expected3, actual3);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual4 = *++setEnumerator;
-    Node expected4 = d_nm->mkNode(Kind::SINGLETON, blue);
-    TS_ASSERT_EQUALS(expected4, actual4);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual5 = *++setEnumerator;
-    Node expected5 = d_nm->mkNode(Kind::UNION, expected1, expected4);
-    TS_ASSERT_EQUALS(expected5, actual5);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual6 = *++setEnumerator;
-    Node expected6 = d_nm->mkNode(Kind::UNION, expected2, expected4);
-    TS_ASSERT_EQUALS(expected6, actual6);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual7 = *++setEnumerator;
-    Node expected7 = d_nm->mkNode(Kind::UNION, expected3, expected4);
-    TS_ASSERT_EQUALS(expected7, actual7);
-    TS_ASSERT(!setEnumerator.isFinished());
+    std::vector<Node> elems;
+    for (unsigned i = 0; i < 8; i++)
+    {
+      Node actual = *setEnumerator;
+      addAndCheckUnique(actual, elems);
+      TS_ASSERT(!setEnumerator.isFinished());
+      ++setEnumerator;
+    }
 
     TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&);
     TS_ASSERT(setEnumerator.isFinished());
@@ -204,92 +146,15 @@ class SetEnumeratorWhite : public CxxTest::TestSuite
   {
     TypeNode bitVector2 = d_nm->mkBitVectorType(2);
     SetEnumerator setEnumerator(d_nm->mkSetType(bitVector2));
-    Node zero = d_nm->mkConst(BitVector(2u, 0u));
-    Node one = d_nm->mkConst(BitVector(2u, 1u));
-    Node two = d_nm->mkConst(BitVector(2u, 2u));
-    Node three = d_nm->mkConst(BitVector(2u, 3u));
-    Node four = d_nm->mkConst(BitVector(2u, 4u));
-
-    Node actual0 = *setEnumerator;
-    Node expected0 =
-        d_nm->mkConst(EmptySet(d_nm->mkSetType(bitVector2)));
-    TS_ASSERT_EQUALS(expected0, actual0);
-    TS_ASSERT(!setEnumerator.isFinished());
 
-    Node actual1 = *++setEnumerator;
-    Node expected1 = d_nm->mkNode(Kind::SINGLETON, zero);
-    TS_ASSERT_EQUALS(expected1, actual1);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual2 = *++setEnumerator;
-    Node expected2 = d_nm->mkNode(Kind::SINGLETON, one);
-    TS_ASSERT_EQUALS(expected2, actual2);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual3 = *++setEnumerator;
-    Node expected3 = d_nm->mkNode(Kind::UNION, expected1, expected2);
-    TS_ASSERT_EQUALS(expected3, actual3);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual4 = *++setEnumerator;
-    Node expected4 = d_nm->mkNode(Kind::SINGLETON, two);
-    TS_ASSERT_EQUALS(expected4, actual4);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual5 = *++setEnumerator;
-    Node expected5 = d_nm->mkNode(Kind::UNION, expected1, expected4);
-    TS_ASSERT_EQUALS(expected5, actual5);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual6 = *++setEnumerator;
-    Node expected6 = d_nm->mkNode(Kind::UNION, expected2, expected4);
-    TS_ASSERT_EQUALS(expected6, actual6);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual7 = *++setEnumerator;
-    Node expected7 = d_nm->mkNode(Kind::UNION, expected3, expected4);
-    TS_ASSERT_EQUALS(expected7, actual7);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual8 = *++setEnumerator;
-    Node expected8 = d_nm->mkNode(Kind::SINGLETON, three);
-    TS_ASSERT_EQUALS(expected8, actual8);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual9 = *++setEnumerator;
-    Node expected9 = d_nm->mkNode(Kind::UNION, expected1, expected8);
-    TS_ASSERT_EQUALS(expected9, actual9);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual10 = *++setEnumerator;
-    Node expected10 = d_nm->mkNode(Kind::UNION, expected2, expected8);
-    TS_ASSERT_EQUALS(expected10, actual10);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual11 = *++setEnumerator;
-    Node expected11 = d_nm->mkNode(Kind::UNION, expected3, expected8);
-    TS_ASSERT_EQUALS(expected11, actual11);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual12 = *++setEnumerator;
-    Node expected12 = d_nm->mkNode(Kind::UNION, expected4, expected8);
-    TS_ASSERT_EQUALS(expected12, actual12);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual13 = *++setEnumerator;
-    Node expected13 = d_nm->mkNode(Kind::UNION, expected5, expected8);
-    TS_ASSERT_EQUALS(expected13, actual13);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual14 = *++setEnumerator;
-    Node expected14 = d_nm->mkNode(Kind::UNION, expected6, expected8);
-    TS_ASSERT_EQUALS(expected14, actual14);
-    TS_ASSERT(!setEnumerator.isFinished());
-
-    Node actual15 = *++setEnumerator;
-    Node expected15 = d_nm->mkNode(Kind::UNION, expected7, expected8);
-    TS_ASSERT_EQUALS(expected15, actual15);
-    TS_ASSERT(!setEnumerator.isFinished());
+    std::vector<Node> elems;
+    for (unsigned i = 0; i < 16; i++)
+    {
+      Node actual = *setEnumerator;
+      addAndCheckUnique(actual, elems);
+      TS_ASSERT(!setEnumerator.isFinished());
+      ++setEnumerator;
+    }
 
     TS_ASSERT_THROWS(*++setEnumerator, NoMoreValuesException&);
     TS_ASSERT(setEnumerator.isFinished());