Merge branch 'master' into replreplRewreplreplRew

22 files changed, 717 insertions, 463 deletions

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 6616f470f..b54290612 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -165,6 +165,62 @@ bool TypeNode::isInterpretedFinite()
   return getAttribute(IsInterpretedFiniteAttr());
 }
 
+/** Attribute true for types that are closed enumerable */
+struct IsClosedEnumerableTag
+{
+};
+struct IsClosedEnumerableComputedTag
+{
+};
+typedef expr::Attribute<IsClosedEnumerableTag, bool> IsClosedEnumerableAttr;
+typedef expr::Attribute<IsClosedEnumerableComputedTag, bool>
+    IsClosedEnumerableComputedAttr;
+
+bool TypeNode::isClosedEnumerable()
+{
+  // check it is already cached
+  if (!getAttribute(IsClosedEnumerableComputedAttr()))
+  {
+    bool ret = true;
+    if (isArray() || isSort() || isCodatatype() || isFunction())
+    {
+      ret = false;
+    }
+    else if (isSet())
+    {
+      ret = getSetElementType().isClosedEnumerable();
+    }
+    else if (isDatatype())
+    {
+      // avoid infinite loops: initially set to true
+      setAttribute(IsClosedEnumerableAttr(), ret);
+      setAttribute(IsClosedEnumerableComputedAttr(), true);
+      TypeNode tn = *this;
+      const Datatype& dt = getDatatype();
+      for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+      {
+        for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
+        {
+          TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
+          if (tn != ctn && !ctn.isClosedEnumerable())
+          {
+            ret = false;
+            break;
+          }
+        }
+        if (!ret)
+        {
+          break;
+        }
+      }
+    }
+    setAttribute(IsClosedEnumerableAttr(), ret);
+    setAttribute(IsClosedEnumerableComputedAttr(), true);
+    return ret;
+  }
+  return getAttribute(IsClosedEnumerableAttr());
+}
+
 bool TypeNode::isFirstClass() const {
   return ( getKind() != kind::FUNCTION_TYPE || options::ufHo() ) && 
          getKind() != kind::CONSTRUCTOR_TYPE &&
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 9cb6efc29..5b0caf659 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -429,6 +429,19 @@ public:
    */
   bool isInterpretedFinite();
 
+  /** is closed enumerable type
+   *
+   * This returns true if this type has an enumerator that produces constants
+   * that are fully handled by CVC4's quantifier-free theory solvers. Examples
+   * of types that are not closed enumerable are:
+   * (1) uninterpreted sorts,
+   * (2) arrays,
+   * (3) codatatypes,
+   * (4) functions,
+   * (5) parametric sorts involving any of the above.
+   */
+  bool isClosedEnumerable();
+
   /**
    * Is this a first-class type?
    * First-class types are types for which:
diff --git a/src/lib/clock_gettime.c b/src/lib/clock_gettime.c
index b440b8d28..71b2bf569 100644
--- a/src/lib/clock_gettime.c
+++ b/src/lib/clock_gettime.c
@@ -9,11 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Replacement for clock_gettime() for systems without it (like
- ** Mac OS X)
+ ** \brief Replacement for clock_gettime() for systems without it (Windows)
  **
- ** Replacement for clock_gettime() for systems without it (like Mac
- ** OS X).
+ ** Replacement for clock_gettime() for systems without it (Windows).
  **/
 
 // #warning "TODO(taking): Make lib/clock_gettime.h cvc4_private.h again."
@@ -26,43 +24,6 @@
 extern "C" {
 #endif /* __cplusplus */
 
-#ifdef __APPLE__
-
-#include <stdio.h>
-#include <errno.h>
-#include <mach/mach_time.h>
-
-static double s_clockconv = 0.0;
-
-long clock_gettime(clockid_t which_clock, struct timespec* tp) {
-  if( s_clockconv == 0.0 ) {
-    mach_timebase_info_data_t tb;
-    kern_return_t err = mach_timebase_info(&tb);
-    if(err == 0) {
-      s_clockconv = ((double) tb.numer) / tb.denom;
-    } else {
-      return -EINVAL;
-    }
-  }
-
-  switch(which_clock) {
-  case CLOCK_REALTIME:
-  case CLOCK_REALTIME_HR:
-  case CLOCK_MONOTONIC:
-  case CLOCK_MONOTONIC_HR: {
-      uint64_t t = mach_absolute_time() * s_clockconv;
-      tp->tv_sec = t / 1000000000ul;
-      tp->tv_nsec = t % 1000000000ul;
-    }
-    break;
-  default:
-    return -EINVAL;
-  }
-
-  return 0;
-}
-
-#else /* not defined __APPLE__ */
 #ifdef __WIN32__
 
 #include <time.h>
@@ -80,7 +41,6 @@ long clock_gettime(clockid_t which_clock, struct timespec* tp) {
 }
 
 #endif /* closing #ifdef __WIN32__ */
-#endif /* closing #else for #ifdef __APPLE__ / __WIN32__ */
 
 #ifdef __cplusplus
 }/* extern "C" */
diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h
index 2ad9442dd..db83da853 100644
--- a/src/lib/clock_gettime.h
+++ b/src/lib/clock_gettime.h
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Replacement for clock_gettime() for systems without it (like Mac OS X)
+ ** \brief Replacement for clock_gettime() for systems without it (Windows)
  **
- ** Replacement for clock_gettime() for systems without it (like Mac OS X).
+ ** Replacement for clock_gettime() for systems without it (Windows).
  **/
 
 #include "cvc4_private_library.h"
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 8abe8d541..22d944e4c 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -29,7 +29,6 @@
 #include "base/modal_exception.h"
 #include "base/output.h"
 #include "lib/strtok_r.h"
-#include "gmp.h"
 #include "options/arith_heuristic_pivot_rule.h"
 #include "options/arith_propagation_mode.h"
 #include "options/arith_unate_lemma_mode.h"
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index b90d98ca6..46649154e 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -29,7 +29,6 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/term_database.h"
-#include "theory/quantifiers/term_enumeration.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/theory_engine.h"
 
@@ -1645,7 +1644,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st
 
 
 Instantiator::Instantiator( QuantifiersEngine * qe, TypeNode tn ) : d_type( tn ){
-  d_closed_enum_type = qe->getTermEnumeration()->isClosedEnumerableType(tn);
+  d_closed_enum_type = tn.isClosedEnumerable();
 }
 
 bool Instantiator::processEqualTerm(CegInstantiator* ci,
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index 69f89021b..0dc704219 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1088,7 +1088,7 @@ void ConjectureGenerator::getEnumerateUfTerm( Node n, unsigned num, std::vector<
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       vec.push_back( 0 );
       TypeNode tn = n[i].getType();
-      if (te->isClosedEnumerableType(tn))
+      if (tn.isClosedEnumerable())
       {
         types.push_back( tn );
       }else{
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 1e3116f43..0eec40de2 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -317,7 +317,7 @@ Node FirstOrderModel::getModelBasisTerm(TypeNode tn)
   if (d_model_basis_term.find(tn) == d_model_basis_term.end())
   {
     Node mbt;
-    if (d_qe->getTermEnumeration()->isClosedEnumerableType(tn))
+    if (tn.isClosedEnumerable())
     {
       mbt = d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
     }
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index eab05f454..24f418b0c 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -491,7 +491,7 @@ bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms)
 
 Node Instantiate::getTermForType(TypeNode tn)
 {
-  if (d_qe->getTermEnumeration()->isClosedEnumerableType(tn))
+  if (tn.isClosedEnumerable())
   {
     return d_qe->getTermEnumeration()->getEnumerateTerm(tn, 0);
   }
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 1f6660f2f..1f94dd3df 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -735,36 +735,15 @@ Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol
   }
 }
 
-
-bool QuantifiersRewriter::isConditionalVariableElim( Node n, int pol ){
-  if( n.getKind()==NOT ){
-    return isConditionalVariableElim( n[0], -pol );
-  }else if( ( n.getKind()==AND && pol>=0 ) || ( n.getKind()==OR && pol<=0 ) ){
-    pol = n.getKind()==AND ? 1 : -1;
-    for( unsigned i=0; i<n.getNumChildren(); i++ ){
-      if( isConditionalVariableElim( n[i], pol ) ){
-        return true;
-      }
-    }
-  }else if( n.getKind()==EQUAL ){
-    for (unsigned i = 0; i < 2; i++)
-    {
-      if (n[i].getKind() == BOUND_VARIABLE)
-      {
-        if (!expr::hasSubterm(n[1 - i], n[i]))
-        {
-          return true;
-        }
-      }
-    }
-  }else if( n.getKind()==BOUND_VARIABLE ){
-    return true;
-  }
-  return false;
-}
-
-Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){
-  if( options::iteDtTesterSplitQuant() && body.getKind()==ITE ){
+Node QuantifiersRewriter::computeCondSplit(Node body,
+                                           const std::vector<Node>& args,
+                                           QAttributes& qa)
+{
+  NodeManager* nm = NodeManager::currentNM();
+  Kind bk = body.getKind();
+  if (options::iteDtTesterSplitQuant() && bk == ITE
+      && body[0].getKind() == APPLY_TESTER)
+  {
     Trace("quantifiers-rewrite-ite-debug") << "DTT split : " << body << std::endl;
     std::map< Node, Node > pcons;
     std::map< Node, std::map< int, Node > > ncons;
@@ -776,119 +755,131 @@ Node QuantifiersRewriter::computeCondSplit( Node body, QAttributes& qa ){
       for( unsigned i=0; i<conj.size(); i++ ){
         Trace("quantifiers-rewrite-ite") << "   " << conj[i] << std::endl;
       }
-      return NodeManager::currentNM()->mkNode( AND, conj );
+      return nm->mkNode(AND, conj);
     }
   }
-  if( options::condVarSplitQuant() ){
-    if( body.getKind()==ITE || ( body.getKind()==EQUAL && body[0].getType().isBoolean() && options::condVarSplitQuantAgg() ) ){
-      Assert( !qa.isFunDef() );
-      Trace("quantifiers-rewrite-debug") << "Conditional var elim split " << body << "?" << std::endl;
-      bool do_split = false;
-      unsigned index_max = body.getKind()==ITE ? 0 : 1;
-      for( unsigned index=0; index<=index_max; index++ ){
-        if( isConditionalVariableElim( body[index] ) ){
-          do_split = true;
-          break;
-        }
+  if (!options::condVarSplitQuant())
+  {
+    return body;
+  }
+  Trace("cond-var-split-debug")
+      << "Conditional var elim split " << body << "?" << std::endl;
+
+  if (bk == ITE
+      || (bk == EQUAL && body[0].getType().isBoolean()
+          && options::condVarSplitQuantAgg()))
+  {
+    Assert(!qa.isFunDef());
+    bool do_split = false;
+    unsigned index_max = bk == ITE ? 0 : 1;
+    std::vector<Node> tmpArgs = args;
+    for (unsigned index = 0; index <= index_max; index++)
+    {
+      if (hasVarElim(body[index], true, tmpArgs)
+          || hasVarElim(body[index], false, tmpArgs))
+      {
+        do_split = true;
+        break;
       }
-      if( do_split ){
-        Node pos;
-        Node neg;
-        if( body.getKind()==ITE ){
-          pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
-          neg = NodeManager::currentNM()->mkNode( OR, body[0], body[2] );
-        }else{
-          pos = NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] );
-          neg = NodeManager::currentNM()->mkNode( OR, body[0], body[1].negate() );
-        }
-        Trace("quantifiers-rewrite-debug") << "*** Split (conditional variable eq) " << body << " into : " << std::endl;
-        Trace("quantifiers-rewrite-debug") << "   " << pos << std::endl;
-        Trace("quantifiers-rewrite-debug") << "   " << neg << std::endl;
-        return NodeManager::currentNM()->mkNode( AND, pos, neg );
-      }
-    }else if( body.getKind()==OR && options::condVarSplitQuantAgg() ){
-      std::vector< Node > bchildren;
-      std::vector< Node > nchildren;
-      for( unsigned i=0; i<body.getNumChildren(); i++ ){
-        bool split = false;
-        if( nchildren.empty() ){
-          if( body[i].getKind()==AND ){
-            std::vector< Node > children;
-            for( unsigned j=0; j<body[i].getNumChildren(); j++ ){
-              if( ( body[i][j].getKind()==NOT && body[i][j][0].getKind()==EQUAL && isConditionalVariableElim( body[i][j][0] ) ) ||
-                  body[i][j].getKind()==BOUND_VARIABLE ){
-                nchildren.push_back( body[i][j] );
-              }else{
-                children.push_back( body[i][j] );
-              }
+    }
+    if (do_split)
+    {
+      Node pos;
+      Node neg;
+      if (bk == ITE)
+      {
+        pos = nm->mkNode(OR, body[0].negate(), body[1]);
+        neg = nm->mkNode(OR, body[0], body[2]);
+      }
+      else
+      {
+        pos = nm->mkNode(OR, body[0].negate(), body[1]);
+        neg = nm->mkNode(OR, body[0], body[1].negate());
+      }
+      Trace("cond-var-split-debug") << "*** Split (conditional variable eq) "
+                                    << body << " into : " << std::endl;
+      Trace("cond-var-split-debug") << "   " << pos << std::endl;
+      Trace("cond-var-split-debug") << "   " << neg << std::endl;
+      return nm->mkNode(AND, pos, neg);
+    }
+  }
+
+  if (bk == OR)
+  {
+    unsigned size = body.getNumChildren();
+    bool do_split = false;
+    unsigned split_index = 0;
+    for (unsigned i = 0; i < size; i++)
+    {
+      // check if this child is a (conditional) variable elimination
+      Node b = body[i];
+      if (b.getKind() == AND)
+      {
+        std::vector<Node> vars;
+        std::vector<Node> subs;
+        std::vector<Node> tmpArgs = args;
+        for (unsigned j = 0, bsize = b.getNumChildren(); j < bsize; j++)
+        {
+          if (getVarElimLit(b[j], false, tmpArgs, vars, subs))
+          {
+            Trace("cond-var-split-debug") << "Variable elimination in child #"
+                                          << j << " under " << i << std::endl;
+            // Figure out if we should split
+            // Currently we split if the aggressive option is set, or
+            // if the top-level OR is binary.
+            if (options::condVarSplitQuantAgg() || size == 2)
+            {
+              do_split = true;
             }
-            if( !nchildren.empty() ){
-              if( !children.empty() ){
-                nchildren.push_back( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children ) );
-              }
-              split = true;
+            // other splitting criteria go here
+
+            if (do_split)
+            {
+              split_index = i;
+              break;
             }
+            vars.clear();
+            subs.clear();
+            tmpArgs = args;
           }
         }
-        if( !split ){
-          bchildren.push_back( body[i] );
-        }
       }
-      if( !nchildren.empty() ){
-        Trace("quantifiers-rewrite-debug") << "*** Split (conditional variable eq) " << body << " into : " << std::endl;
-        for( unsigned i=0; i<nchildren.size(); i++ ){
-          bchildren.push_back( nchildren[i] );
-          nchildren[i] = NodeManager::currentNM()->mkNode( OR, bchildren );
-          Trace("quantifiers-rewrite-debug") << "   " << nchildren[i] << std::endl;
-          bchildren.pop_back();
-        }
-        return NodeManager::currentNM()->mkNode( AND, nchildren );
+      if (do_split)
+      {
+        break;
+      }
+    }
+    if (do_split)
+    {
+      std::vector<Node> children;
+      for (TNode bc : body)
+      {
+        children.push_back(bc);
       }
+      std::vector<Node> split_children;
+      for (TNode bci : body[split_index])
+      {
+        children[split_index] = bci;
+        split_children.push_back(nm->mkNode(OR, children));
+      }
+      // split the AND child, for example:
+      //  ( x!=a ^ P(x) ) V Q(x) ---> ( x!=a V Q(x) ) ^ ( P(x) V Q(x) )
+      return nm->mkNode(AND, split_children);
     }
   }
+
   return body;
 }
 
-bool QuantifiersRewriter::isVariableElim(Node v, Node s)
+bool QuantifiersRewriter::isVarElim(Node v, Node s)
 {
+  Assert(v.getKind() == BOUND_VARIABLE);
   return !expr::hasSubterm(s, v) && s.getType().isSubtypeOf(v.getType());
 }
 
-void QuantifiersRewriter::isVariableBoundElig( Node n, std::map< Node, int >& exclude, std::map< Node, std::map< int, bool > >& visited, bool hasPol, bool pol, 
-                                               std::map< Node, bool >& elig_vars  ) {
-  int vindex = hasPol ? ( pol ? 1 : -1 ) : 0;
-  if( visited[n].find( vindex )==visited[n].end() ){
-    visited[n][vindex] = true;
-    if( elig_vars.find( n )!=elig_vars.end() ){
-      //variable contained in a place apart from bounds, no longer eligible for elimination
-      elig_vars.erase( n );
-      Trace("var-elim-ineq-debug") << "...found occurrence of " << n << ", mark ineligible" << std::endl;
-    }else{
-      if( hasPol ){
-        std::map< Node, int >::iterator itx = exclude.find( n );
-        if( itx!=exclude.end() && itx->second==vindex ){
-          //already processed this literal
-          return;
-        }
-      }
-      for( unsigned j=0; j<n.getNumChildren(); j++ ){
-        bool newHasPol;
-        bool newPol;
-        QuantPhaseReq::getPolarity( n, j, hasPol, pol, newHasPol, newPol );
-        isVariableBoundElig( n[j], exclude, visited, newHasPol, newPol, elig_vars );
-        if( elig_vars.empty() ){
-          break;
-        }
-      }
-    }
-  }else{
-    //already visited
-  }
-}
-
-Node QuantifiersRewriter::computeVariableElimLitBv(Node lit,
-                                                   std::vector<Node>& args,
-                                                   Node& var)
+Node QuantifiersRewriter::getVarElimLitBv(Node lit,
+                                          std::vector<Node>& args,
+                                          Node& var)
 {
   if (Trace.isOn("quant-velim-bv"))
   {
@@ -922,7 +913,7 @@ Node QuantifiersRewriter::computeVariableElimLitBv(Node lit,
         // if this is a proper variable elimination, that is, var = slv where
         // var is not in the free variables of slv, then we can return this
         // as the variable elimination for lit.
-        if (isVariableElim(var, slv))
+        if (isVarElim(var, slv))
         {
           return slv;
         }
@@ -937,17 +928,58 @@ Node QuantifiersRewriter::computeVariableElimLitBv(Node lit,
   return Node::null();
 }
 
-bool QuantifiersRewriter::computeVariableElimLit(
-    Node lit,
-    bool pol,
-    std::vector<Node>& args,
-    std::vector<Node>& vars,
-    std::vector<Node>& subs,
-    std::map<Node, std::map<bool, std::map<Node, bool> > >& num_bounds)
+bool QuantifiersRewriter::getVarElimLit(Node lit,
+                                        bool pol,
+                                        std::vector<Node>& args,
+                                        std::vector<Node>& vars,
+                                        std::vector<Node>& subs)
 {
+  if (lit.getKind() == NOT)
+  {
+    return getVarElimLit(lit[0], !pol, args, vars, subs);
+  }
+  NodeManager* nm = NodeManager::currentNM();
   Trace("var-elim-quant-debug")
       << "Eliminate : " << lit << ", pol = " << pol << "?" << std::endl;
-  if (lit.getKind() == EQUAL && options::varElimQuant())
+  if (lit.getKind() == APPLY_TESTER && pol && lit[0].getKind() == BOUND_VARIABLE
+      && options::dtVarExpandQuant())
+  {
+    Trace("var-elim-dt") << "Expand datatype variable based on : " << lit
+                         << std::endl;
+    std::vector<Node>::iterator ita =
+        std::find(args.begin(), args.end(), lit[0]);
+    if (ita != args.end())
+    {
+      vars.push_back(lit[0]);
+      Expr testerExpr = lit.getOperator().toExpr();
+      int index = Datatype::indexOf(testerExpr);
+      const Datatype& dt = Datatype::datatypeOf(testerExpr);
+      const DatatypeConstructor& c = dt[index];
+      std::vector<Node> newChildren;
+      newChildren.push_back(Node::fromExpr(c.getConstructor()));
+      std::vector<Node> newVars;
+      for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
+      {
+        TypeNode tn = TypeNode::fromType(c[j].getRangeType());
+        Node v = nm->mkBoundVar(tn);
+        newChildren.push_back(v);
+        newVars.push_back(v);
+      }
+      subs.push_back(nm->mkNode(APPLY_CONSTRUCTOR, newChildren));
+      Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/"
+                           << vars[0] << std::endl;
+      args.erase(ita);
+      args.insert(args.end(), newVars.begin(), newVars.end());
+      return true;
+    }
+  }
+  // all eliminations below guarded by varElimQuant()
+  if (!options::varElimQuant())
+  {
+    return false;
+  }
+
+  if (lit.getKind() == EQUAL)
   {
     if (pol || lit[0].getType().isBoolean())
     {
@@ -964,7 +996,7 @@ bool QuantifiersRewriter::computeVariableElimLit(
             std::find(args.begin(), args.end(), v_slv);
         if (ita != args.end())
         {
-          if (isVariableElim(v_slv, lit[1 - i]))
+          if (isVarElim(v_slv, lit[1 - i]))
           {
             Node slv = lit[1 - i];
             if (!tpol)
@@ -983,31 +1015,9 @@ bool QuantifiersRewriter::computeVariableElimLit(
         }
       }
     }
-  }else if( lit.getKind()==APPLY_TESTER && pol && lit[0].getKind()==BOUND_VARIABLE && options::dtVarExpandQuant() ){
-    Trace("var-elim-dt") << "Expand datatype variable based on : " << lit << std::endl;
-    std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit[0] );
-    if( ita!=args.end() ){
-      vars.push_back( lit[0] );
-      Expr testerExpr = lit.getOperator().toExpr();
-      int index = Datatype::indexOf( testerExpr );
-      const Datatype& dt = Datatype::datatypeOf(testerExpr);
-      const DatatypeConstructor& c = dt[index];
-      std::vector< Node > newChildren;
-      newChildren.push_back( Node::fromExpr( c.getConstructor() ) );
-      std::vector< Node > newVars;
-      for( unsigned j=0; j<c.getNumArgs(); j++ ){
-        TypeNode tn = TypeNode::fromType( c[j].getRangeType() );
-        Node v = NodeManager::currentNM()->mkBoundVar( tn );
-        newChildren.push_back( v );
-        newVars.push_back( v );
-      }
-      subs.push_back( NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, newChildren ) );
-      Trace("var-elim-dt") << "...apply substitution " << subs[0] << "/" << vars[0] << std::endl;
-      args.erase( ita );
-      args.insert( args.end(), newVars.begin(), newVars.end() );
-      return true;
-    }
-  }else if( lit.getKind()==BOUND_VARIABLE && options::varElimQuant() ){
+  }
+  if (lit.getKind() == BOUND_VARIABLE)
+  {
     std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), lit );
     if( ita!=args.end() ){
       Trace("var-elim-bool") << "Variable eliminate : " << lit << std::endl;
@@ -1017,9 +1027,9 @@ bool QuantifiersRewriter::computeVariableElimLit(
       return true;
     }
   }
-  if( ( lit.getKind()==EQUAL && lit[0].getType().isReal() && pol && options::varElimQuant() ) || 
-      ( ( lit.getKind()==GEQ || lit.getKind()==GT ) && options::varIneqElimQuant() ) ){
-    //for arithmetic, solve the (in)equality
+  if (lit.getKind() == EQUAL && lit[0].getType().isReal() && pol)
+  {
+    // for arithmetic, solve the equality
     std::map< Node, Node > msum;
     if (ArithMSum::getMonomialSumLit(lit, msum))
     {
@@ -1027,58 +1037,29 @@ bool QuantifiersRewriter::computeVariableElimLit(
         if( !itm->first.isNull() ){
           std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), itm->first );
           if( ita!=args.end() ){
-            if( lit.getKind()==EQUAL ){
-              Assert( pol );
-              Node veq_c;
-              Node val;
-              int ires =
-                  ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL);
-              if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val ) ){
-                Trace("var-elim-quant") << "Variable eliminate based on solved equality : " << itm->first << " -> " << val << std::endl;
-                vars.push_back( itm->first );
-                subs.push_back( val );
-                args.erase( ita );
-                return true;
-              }
-            }else{
-              Assert( lit.getKind()==GEQ || lit.getKind()==GT );
-              //store that this literal is upper/lower bound for itm->first
-              Node veq_c;
-              Node val;
-              int ires = ArithMSum::isolate(
-                  itm->first, msum, veq_c, val, lit.getKind());
-              if( ires!=0 && veq_c.isNull() ){
-                bool is_upper = pol!=( ires==1 );
-                Trace("var-elim-ineq-debug") << lit << " is a " << ( is_upper ? "upper" : "lower" ) << " bound for " << itm->first << std::endl;
-                Trace("var-elim-ineq-debug") << "  pol/ires = " << pol << " " << ires << std::endl;
-                num_bounds[itm->first][is_upper][lit] = pol;
-              }else{
-                Trace("var-elim-ineq-debug") << "...ineligible " << itm->first << " since it cannot be solved for (" << ires << ", " << veq_c << ")." << std::endl;
-                num_bounds[itm->first][true].clear();
-                num_bounds[itm->first][false].clear();
-              }
-            }
-          }else{
-            if( lit.getKind()==GEQ || lit.getKind()==GT ){
-              //compute variables in itm->first, these are not eligible for elimination
-              std::vector< Node > bvs;
-              TermUtil::getBoundVars( itm->first, bvs );
-              for( unsigned j=0; j<bvs.size(); j++ ){
-                Trace("var-elim-ineq-debug") << "...ineligible " << bvs[j] << " since it is contained in monomial." << std::endl;
-                num_bounds[bvs[j]][true].clear();
-                num_bounds[bvs[j]][false].clear();
-              }
+            Assert(pol);
+            Node veq_c;
+            Node val;
+            int ires = ArithMSum::isolate(itm->first, msum, veq_c, val, EQUAL);
+            if (ires != 0 && veq_c.isNull() && isVarElim(itm->first, val))
+            {
+              Trace("var-elim-quant")
+                  << "Variable eliminate based on solved equality : "
+                  << itm->first << " -> " << val << std::endl;
+              vars.push_back(itm->first);
+              subs.push_back(val);
+              args.erase(ita);
+              return true;
             }
           }
         }
       }
     }
   }
-  else if (lit.getKind() == EQUAL && lit[0].getType().isBitVector() && pol
-           && options::varElimQuant())
+  if (lit.getKind() == EQUAL && lit[0].getType().isBitVector() && pol)
   {
     Node var;
-    Node slv = computeVariableElimLitBv(lit, args, var);
+    Node slv = getVarElimLitBv(lit, args, var);
     if (!slv.isNull())
     {
       Assert(!var.isNull());
@@ -1096,92 +1077,282 @@ bool QuantifiersRewriter::computeVariableElimLit(
       return true;
     }
   }
-
   return false;
 }
 
-Node QuantifiersRewriter::computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa ){
-  Trace("var-elim-quant-debug") << "Compute var elimination for " << body << std::endl;
-  std::map< Node, std::map< bool, std::map< Node, bool > > > num_bounds;
-  QuantPhaseReq qpr( body );
+bool QuantifiersRewriter::getVarElim(Node n,
+                                     bool pol,
+                                     std::vector<Node>& args,
+                                     std::vector<Node>& vars,
+                                     std::vector<Node>& subs)
+{
+  Kind nk = n.getKind();
+  if (nk == NOT)
+  {
+    return getVarElim(n[0], !pol, args, vars, subs);
+  }
+  else if ((nk == AND && pol) || (nk == OR && !pol))
+  {
+    for (const Node& cn : n)
+    {
+      if (getVarElim(cn, pol, args, vars, subs))
+      {
+        return true;
+      }
+    }
+    return false;
+  }
+  return getVarElimLit(n, pol, args, vars, subs);
+}
+
+bool QuantifiersRewriter::hasVarElim(Node n, bool pol, std::vector<Node>& args)
+{
   std::vector< Node > vars;
   std::vector< Node > subs;
-  for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
-    Trace("var-elim-quant-debug") << "   phase req : " << it->first << " -> " << ( it->second ? "true" : "false" ) << std::endl;
-    if( computeVariableElimLit( it->first, it->second, args, vars, subs, num_bounds ) ){
-      break;
+  return getVarElim(n, pol, args, vars, subs);
+}
+
+bool QuantifiersRewriter::getVarElimIneq(Node body,
+                                         std::vector<Node>& args,
+                                         std::vector<Node>& bounds,
+                                         std::vector<Node>& subs,
+                                         QAttributes& qa)
+{
+  // elimination based on inequalities
+  std::map<Node, std::map<bool, std::map<Node, bool> > > num_bounds;
+  QuantPhaseReq qpr(body);
+  for (const std::pair<const Node, bool>& pr : qpr.d_phase_reqs)
+  {
+    // an inequality that is entailed with a given polarity
+    Node lit = pr.first;
+    if (lit.getKind() != GEQ)
+    {
+      continue;
+    }
+    bool pol = pr.second;
+    Trace("var-elim-quant-debug") << "Process inequality bounds : " << lit
+                                  << ", pol = " << pol << "..." << std::endl;
+    // solve the inequality
+    std::map<Node, Node> msum;
+    if (!ArithMSum::getMonomialSumLit(lit, msum))
+    {
+      // not an inequality, cannot use
+      continue;
+    }
+    for (const std::pair<const Node, Node>& m : msum)
+    {
+      if (!m.first.isNull())
+      {
+        std::vector<Node>::iterator ita =
+            std::find(args.begin(), args.end(), m.first);
+        if (ita != args.end())
+        {
+          // store that this literal is upper/lower bound for itm->first
+          Node veq_c;
+          Node val;
+          int ires =
+              ArithMSum::isolate(m.first, msum, veq_c, val, lit.getKind());
+          if (ires != 0 && veq_c.isNull())
+          {
+            bool is_upper = pol != (ires == 1);
+            Trace("var-elim-ineq-debug")
+                << lit << " is a " << (is_upper ? "upper" : "lower")
+                << " bound for " << m.first << std::endl;
+            Trace("var-elim-ineq-debug")
+                << "  pol/ires = " << pol << " " << ires << std::endl;
+            num_bounds[m.first][is_upper][lit] = pol;
+          }
+          else
+          {
+            Trace("var-elim-ineq-debug")
+                << "...ineligible " << m.first
+                << " since it cannot be solved for (" << ires << ", " << veq_c
+                << ")." << std::endl;
+            num_bounds[m.first][true].clear();
+            num_bounds[m.first][false].clear();
+          }
+        }
+        else
+        {
+          // compute variables in itm->first, these are not eligible for
+          // elimination
+          std::vector<Node> bvs;
+          TermUtil::getBoundVars(m.first, bvs);
+          for (TNode v : bvs)
+          {
+            Trace("var-elim-ineq-debug")
+                << "...ineligible " << v
+                << " since it is contained in monomial." << std::endl;
+            num_bounds[v][true].clear();
+            num_bounds[v][false].clear();
+          }
+        }
+      }
     }
   }
-  
-  if( !vars.empty() ){
-    Trace("var-elim-quant-debug") << "VE " << vars.size() << "/" << args.size() << std::endl;
-    //remake with eliminated nodes
-    body = body.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
-    body = Rewriter::rewrite( body );
-    if( !qa.d_ipl.isNull() ){
-      qa.d_ipl = qa.d_ipl.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+
+  // collect all variables that have only upper/lower bounds
+  std::map<Node, bool> elig_vars;
+  for (const std::pair<const Node, std::map<bool, std::map<Node, bool> > >& nb :
+       num_bounds)
+  {
+    if (nb.second.find(true) == nb.second.end())
+    {
+      Trace("var-elim-ineq-debug")
+          << "Variable " << nb.first << " has only lower bounds." << std::endl;
+      elig_vars[nb.first] = false;
     }
-    Trace("var-elim-quant") << "Return " << body << std::endl;
-  }else{
-    //collect all variables that have only upper/lower bounds
-    std::map< Node, bool > elig_vars;
-    for( std::map< Node, std::map< bool, std::map< Node, bool > > >::iterator it = num_bounds.begin(); it != num_bounds.end(); ++it ){
-      if( it->second.find( true )==it->second.end() ){
-        Trace("var-elim-ineq-debug") << "Variable " << it->first << " has only lower bounds." << std::endl;
-        elig_vars[it->first] = false;
-      }else if( it->second.find( false )==it->second.end() ){
-        Trace("var-elim-ineq-debug") << "Variable " << it->first << " has only upper bounds." << std::endl;
-        elig_vars[it->first] = true;
-      }
-    }
-    if( !elig_vars.empty() ){
-      std::vector< Node > inactive_vars;
-      std::map< Node, std::map< int, bool > > visited;
-      std::map< Node, int > exclude;
-      for( std::map< Node, bool >::iterator it = qpr.d_phase_reqs.begin(); it != qpr.d_phase_reqs.end(); ++it ){
-        if( it->first.getKind()==GEQ || it->first.getKind()==GT ){
-          exclude[ it->first ] = it->second ? -1 : 1;
-          Trace("var-elim-ineq-debug") << "...exclude " << it->first << " at polarity " << exclude[ it->first ] << std::endl;
-        }
+    else if (nb.second.find(false) == nb.second.end())
+    {
+      Trace("var-elim-ineq-debug")
+          << "Variable " << nb.first << " has only upper bounds." << std::endl;
+      elig_vars[nb.first] = true;
+    }
+  }
+  if (elig_vars.empty())
+  {
+    return false;
+  }
+  std::vector<Node> inactive_vars;
+  std::map<Node, std::map<int, bool> > visited;
+  std::map<Node, int> exclude;
+  for (const std::pair<Node, bool>& pr : qpr.d_phase_reqs)
+  {
+    if (pr.first.getKind() == GEQ)
+    {
+      exclude[pr.first] = pr.second ? -1 : 1;
+      Trace("var-elim-ineq-debug")
+          << "...exclude " << pr.first << " at polarity " << exclude[pr.first]
+          << std::endl;
+    }
+  }
+  // traverse the body, invalidate variables if they occur in places other than
+  // the bounds they occur in
+  std::unordered_map<TNode, std::unordered_set<int>, TNodeHashFunction>
+      evisited;
+  std::vector<TNode> evisit;
+  std::vector<int> evisit_pol;
+  TNode ecur;
+  int ecur_pol;
+  evisit.push_back(body);
+  evisit_pol.push_back(1);
+  if (!qa.d_ipl.isNull())
+  {
+    // do not eliminate variables that occur in the annotation
+    evisit.push_back(qa.d_ipl);
+    evisit_pol.push_back(0);
+  }
+  do
+  {
+    ecur = evisit.back();
+    evisit.pop_back();
+    ecur_pol = evisit_pol.back();
+    evisit_pol.pop_back();
+    std::unordered_set<int>& epp = evisited[ecur];
+    if (epp.find(ecur_pol) == epp.end())
+    {
+      epp.insert(ecur_pol);
+      if (elig_vars.find(ecur) != elig_vars.end())
+      {
+        // variable contained in a place apart from bounds, no longer eligible
+        // for elimination
+        elig_vars.erase(ecur);
+        Trace("var-elim-ineq-debug") << "...found occurrence of " << ecur
+                                     << ", mark ineligible" << std::endl;
       }
-      //traverse the body, invalidate variables if they occur in places other than the bounds they occur in
-      isVariableBoundElig( body, exclude, visited, true, true, elig_vars );
-      
-      if( !elig_vars.empty() ){
-        if( !qa.d_ipl.isNull() ){
-          isVariableBoundElig( qa.d_ipl, exclude, visited, false, true, elig_vars );
+      else
+      {
+        bool rec = true;
+        bool pol = ecur_pol >= 0;
+        bool hasPol = ecur_pol != 0;
+        if (hasPol)
+        {
+          std::map<Node, int>::iterator itx = exclude.find(ecur);
+          if (itx != exclude.end() && itx->second == ecur_pol)
+          {
+            // already processed this literal as a bound
+            rec = false;
+          }
         }
-        for( std::map< Node, bool >::iterator itev = elig_vars.begin(); itev != elig_vars.end(); ++itev ){
-          Node v = itev->first;
-          Trace("var-elim-ineq-debug") << v << " is eligible for elimination." << std::endl;
-          //do substitution corresponding to infinite projection, all literals involving unbounded variable go to true/false
-          std::vector< Node > terms;
-          std::vector< Node > subs;
-          for( std::map< Node, bool >::iterator itb = num_bounds[v][elig_vars[v]].begin(); itb != num_bounds[v][elig_vars[v]].end(); ++itb ){
-            Trace("var-elim-ineq-debug") << "  subs : " << itb->first << " -> " << itb->second << std::endl;
-            terms.push_back( itb->first );
-            subs.push_back( NodeManager::currentNM()->mkConst( itb->second ) );
+        if (rec)
+        {
+          for (unsigned j = 0, size = ecur.getNumChildren(); j < size; j++)
+          {
+            bool newHasPol;
+            bool newPol;
+            QuantPhaseReq::getPolarity(ecur, j, hasPol, pol, newHasPol, newPol);
+            evisit.push_back(ecur[j]);
+            evisit_pol.push_back(newHasPol ? (newPol ? 1 : -1) : 0);
           }
-          body = body.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
-          Trace("var-elim-ineq-debug") << "Return " << body << std::endl;
-          //eliminate from args
-          std::vector< Node >::iterator ita = std::find( args.begin(), args.end(), v );
-          Assert( ita!=args.end() );
-          args.erase( ita );
         }
-      } 
+      }
     }
-  }
-  return body;
+  } while (!evisit.empty() && !elig_vars.empty());
+
+  bool ret = false;
+  for (const std::pair<Node, bool>& ev : elig_vars)
+  {
+    Node v = ev.first;
+    Trace("var-elim-ineq-debug")
+        << v << " is eligible for elimination." << std::endl;
+    // do substitution corresponding to infinite projection, all literals
+    // involving unbounded variable go to true/false
+    for (const std::pair<const Node, bool>& nb : num_bounds[v][elig_vars[v]])
+    {
+      Trace("var-elim-ineq-debug")
+          << "  subs : " << nb.first << " -> " << nb.second << std::endl;
+      bounds.push_back(nb.first);
+      subs.push_back(NodeManager::currentNM()->mkConst(nb.second));
+    }
+    // eliminate from args
+    std::vector<Node>::iterator ita = std::find(args.begin(), args.end(), v);
+    Assert(ita != args.end());
+    args.erase(ita);
+    ret = true;
+  }
+  return ret;
 }
 
 Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ){
-  if( options::varElimQuant() || options::dtVarExpandQuant() ){
-    Node prev;
-    do{
-      prev = body;
-      body = computeVarElimination2( body, args, qa );
-    }while( prev!=body && !args.empty() );
+  if (!options::varElimQuant() && !options::dtVarExpandQuant()
+      && !options::varIneqElimQuant())
+  {
+    return body;
+  }
+  Node prev;
+  while (prev != body && !args.empty())
+  {
+    prev = body;
+
+    std::vector<Node> vars;
+    std::vector<Node> subs;
+    // standard variable elimination
+    if (options::varElimQuant())
+    {
+      getVarElim(body, false, args, vars, subs);
+    }
+    // variable elimination based on one-direction inequalities
+    if (vars.empty() && options::varIneqElimQuant())
+    {
+      getVarElimIneq(body, args, vars, subs, qa);
+    }
+    // if we eliminated a variable, update body and reprocess
+    if (!vars.empty())
+    {
+      Trace("var-elim-quant-debug")
+          << "VE " << vars.size() << "/" << args.size() << std::endl;
+      Assert(vars.size() == subs.size());
+      // remake with eliminated nodes
+      body =
+          body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
+      body = Rewriter::rewrite(body);
+      if (!qa.d_ipl.isNull())
+      {
+        qa.d_ipl = qa.d_ipl.substitute(
+            vars.begin(), vars.end(), subs.begin(), subs.end());
+      }
+      Trace("var-elim-quant") << "Return " << body << std::endl;
+    }
   }
   return body;
 }
@@ -1725,7 +1896,7 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
       n = NodeManager::currentNM()->mkNode( OR, new_conds );
     }
   }else if( computeOption==COMPUTE_COND_SPLIT ){
-    n = computeCondSplit( n, qa );
+    n = computeCondSplit(n, args, qa);
   }else if( computeOption==COMPUTE_PRENEX ){
     if( options::prenexQuant()==PRENEX_QUANT_DISJ_NORMAL || options::prenexQuant()==PRENEX_QUANT_NORMAL ){
       //will rewrite at preprocess time
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 963e73701..a1d6d25c3 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -43,33 +43,103 @@ private:
                                     std::map< Node, Node >& cache, std::map< Node, Node >& icache,
                                     std::vector< Node >& new_vars, std::vector< Node >& new_conds, bool elimExtArith );
   static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
-  static bool isConditionalVariableElim( Node n, int pol=0 );
-  static bool isVariableElim( Node v, Node s );
-  static void isVariableBoundElig( Node n, std::map< Node, int >& exclude, std::map< Node, std::map< int, bool > >& visited, bool hasPol, bool pol, 
-                                   std::map< Node, bool >& elig_vars );
-  static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs,
-                                      std::map< Node, std::map< bool, std::map< Node, bool > > >& num_bounds );
-  static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa );
+  //-------------------------------------variable elimination
+  /** is variable elimination
+   *
+   * Returns true if v is not a subterm of s, and the type of s is a subtype of
+   * the type of v.
+   */
+  static bool isVarElim(Node v, Node s);
+  /** get variable elimination literal
+   *
+   * If n asserted with polarity pol is equivalent to an equality of the form
+   * v = s for some v in args, where isVariableElim( v, s ) holds, then this
+   * method removes v from args, adds v to vars, adds s to subs, and returns
+   * true. Otherwise, it returns false.
+   */
+  static bool getVarElimLit(Node n,
+                            bool pol,
+                            std::vector<Node>& args,
+                            std::vector<Node>& vars,
+                            std::vector<Node>& subs);
   /** variable eliminate for bit-vector literals
    *
    * If this returns a non-null value ret, then var is updated to a member of
-   * args, and lit is equivalent to ( var = ret ).
+   * args, lit is equivalent to ( var = ret ), and var is removed from args.
    */
-  static Node computeVariableElimLitBv(Node lit,
-                                       std::vector<Node>& args,
-                                       Node& var);
-
+  static Node getVarElimLitBv(Node lit, std::vector<Node>& args, Node& var);
+  /** get variable elimination
+   *
+   * If n asserted with polarity pol entails a literal lit that corresponds
+   * to a variable elimination for some v via the above method, we return true.
+   * In this case, we update args/vars/subs based on eliminating v.
+   */
+  static bool getVarElim(Node n,
+                         bool pol,
+                         std::vector<Node>& args,
+                         std::vector<Node>& vars,
+                         std::vector<Node>& subs);
+  /** has variable elimination
+   *
+   * Returns true if n asserted with polarity pol entails a literal for
+   * which variable elimination is possible.
+   */
+  static bool hasVarElim(Node n, bool pol, std::vector<Node>& args);
+  /** compute variable elimination inequality
+   *
+   * This method eliminates variables from the body of quantified formula
+   * "body" using (global) reasoning about inequalities. In particular, if there
+   * exists a variable x that only occurs in body or annotation qa in literals
+   * of the form x>=t with a fixed polarity P, then we may replace all such
+   * literals with P. For example, note that:
+   *   forall xy. x>y OR P(y) is equivalent to forall y. P(y).
+   *
+   * In the case that a variable x from args can be eliminated in this way,
+   * we remove x from args, add x >= t1, ..., x >= tn to bounds, add false, ...,
+   * false to subs, and return true.
+   */
+  static bool getVarElimIneq(Node body,
+                             std::vector<Node>& args,
+                             std::vector<Node>& bounds,
+                             std::vector<Node>& subs,
+                             QAttributes& qa);
+  /** compute variable elimination
+   *
+   * This computes variable elimination rewrites for a body of a quantified
+   * formula with bound variables args. This method updates args to args' and
+   * returns a node body' such that (forall args. body) is equivalent to
+   * (forall args'. body'). An example of a variable elimination rewrite is:
+   *   forall xy. x != a V P( x,y ) ---> forall y. P( a, y )
+   */
+  static Node computeVarElimination(Node body,
+                                    std::vector<Node>& args,
+                                    QAttributes& qa);
+  //-------------------------------------end variable elimination
+  //-------------------------------------conditional splitting
+  /** compute conditional splitting
+   *
+   * This computes conditional splitting rewrites for a body of a quantified
+   * formula with bound variables args. It returns a body' that is equivalent
+   * to body. We split body into a conjunction if variable elimination can
+   * occur in one of the conjuncts. Examples of this are:
+   *   ite( x=a, P(x), Q(x) ) ----> ( x!=a V P(x) ) ^ ( x=a V Q(x) )
+   *   (x=a) = P(x) ----> ( x!=a V P(x) ) ^ ( x=a V ~P(x) )
+   *   ( x!=a ^ P(x) ) V Q(x) ---> ( x!=a V Q(x) ) ^ ( P(x) V Q(x) )
+   * where in each case, x can be eliminated in the first conjunct.
+   */
+  static Node computeCondSplit(Node body,
+                               const std::vector<Node>& args,
+                               QAttributes& qa);
+  //-------------------------------------end conditional splitting
  public:
   static Node computeElimSymbols( Node body );
   static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
   //cache is dependent upon currCond, icache is not, new_conds are negated conditions
   static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa );
-  static Node computeCondSplit( Node body, QAttributes& qa );
   static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg );
   static Node computePrenexAgg( Node n, bool topLevel, std::map< unsigned, std::map< Node, Node > >& visited );
   static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
-  static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa );
 private:
   enum{
     COMPUTE_ELIM_SYMBOLS = 0,
@@ -79,8 +149,6 @@ private:
     COMPUTE_PRENEX,
     COMPUTE_VAR_ELIMINATION,
     COMPUTE_COND_SPLIT,
-    //COMPUTE_FLATTEN_ARGS_UF,
-    //COMPUTE_CNF,
     COMPUTE_LAST
   };
   static Node computeOperation( Node f, int computeOption, QAttributes& qa );
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
index 1d070417e..0a212598b 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.cpp
@@ -202,7 +202,8 @@ bool CegConjecture::isSingleInvocation() const {
   return d_ceg_si->isSingleInvocation();
 }
 
-bool CegConjecture::needsCheck( std::vector< Node >& lem ) {
+bool CegConjecture::needsCheck()
+{
   if( isSingleInvocation() && !d_ceg_si->needsCheck() ){
     return false;
   }
diff --git a/src/theory/quantifiers/sygus/ce_guided_conjecture.h b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
index 48d307f1e..612a2b4ce 100644
--- a/src/theory/quantifiers/sygus/ce_guided_conjecture.h
+++ b/src/theory/quantifiers/sygus/ce_guided_conjecture.h
@@ -58,7 +58,7 @@ public:
    * refinement */
   void incrementRefineCount() { d_refine_count++; }
   /** whether the conjecture is waiting for a call to doCheck below */
-  bool needsCheck( std::vector< Node >& lem );
+  bool needsCheck();
   /** whether the conjecture is waiting for a call to doRefine below */
   bool needsRefinement() const;
   /** do single invocation check 
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
index 83a576d37..c59195746 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.cpp
@@ -52,10 +52,20 @@ QuantifiersModule::QEffort CegInstantiation::needsModel(Theory::Effort e)
 
 void CegInstantiation::check(Theory::Effort e, QEffort quant_e)
 {
+  // are we at the proper effort level?
+  unsigned echeck =
+      d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL;
+  if (quant_e != echeck)
+  {
+    return;
+  }
+
   // if we are waiting to assign the conjecture, do it now
   if (!d_waiting_conj.isNull())
   {
     Node q = d_waiting_conj;
+    Trace("cegqi-engine") << "--- Conjecture waiting to assign: " << q
+                          << std::endl;
     d_waiting_conj = Node::null();
     if (!d_conj->isAssigned())
     {
@@ -65,31 +75,29 @@ void CegInstantiation::check(Theory::Effort e, QEffort quant_e)
       return;
     }
   }
-  unsigned echeck =
-      d_conj->isSingleInvocation() ? QEFFORT_STANDARD : QEFFORT_MODEL;
-  if( quant_e==echeck ){
-    Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---" << std::endl;
-    Trace("cegqi-engine-debug") << std::endl;
-    bool active = false;
-    bool value;
-    if( d_quantEngine->getValuation().hasSatValue( d_conj->getConjecture(), value ) ) {
-      active = value;
-    }else{
-      Trace("cegqi-engine-debug") << "...no value for quantified formula." << std::endl;
-    }
-    Trace("cegqi-engine-debug") << "Current conjecture status : active : " << active << std::endl;
-    std::vector< Node > lem;
-    if( active && d_conj->needsCheck( lem ) ){
-      checkCegConjecture( d_conj );
-    }else{
-      Trace("cegqi-engine-debug") << "...does not need check." << std::endl;
-      for( unsigned i=0; i<lem.size(); i++ ){
-        Trace("cegqi-lemma") << "Cegqi::Lemma : check lemma : " << lem[i] << std::endl;
-        d_quantEngine->addLemma( lem[i] );
-      }
-    }
-    Trace("cegqi-engine") << "Finished Counterexample Guided Instantiation engine." << std::endl;
+
+  Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---"
+                        << std::endl;
+  Trace("cegqi-engine-debug") << std::endl;
+  bool active = false;
+  bool value;
+  if (d_quantEngine->getValuation().hasSatValue(d_conj->getConjecture(), value))
+  {
+    active = value;
+  }
+  else
+  {
+    Trace("cegqi-engine-debug")
+        << "...no value for quantified formula." << std::endl;
   }
+  Trace("cegqi-engine-debug")
+      << "Current conjecture status : active : " << active << std::endl;
+  if (active && d_conj->needsCheck())
+  {
+    checkConjecture(d_conj);
+  }
+  Trace("cegqi-engine")
+      << "Finished Counterexample Guided Instantiation engine." << std::endl;
 }
 
 bool CegInstantiation::assignConjecture(Node q)
@@ -98,6 +106,7 @@ bool CegInstantiation::assignConjecture(Node q)
   {
     return false;
   }
+  Trace("cegqi-engine") << "--- Assign conjecture " << q << std::endl;
   if (options::sygusQePreproc())
   {
     // the following does quantifier elimination as a preprocess step
@@ -236,7 +245,7 @@ void CegInstantiation::registerQuantifier(Node q)
       else
       {
         // assign it now
-        d_conj->assign(q);
+        assignConjecture(q);
       }
     }else{
       Assert( d_conj->getEmbeddedConjecture()==q );
@@ -257,7 +266,8 @@ Node CegInstantiation::getNextDecisionRequest( unsigned& priority ) {
   return Node::null();
 }
 
-void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
+void CegInstantiation::checkConjecture(CegConjecture* conj)
+{
   Node q = conj->getEmbeddedConjecture();
   Node aq = conj->getConjecture();
   if( Trace.isOn("cegqi-engine-debug") ){
@@ -322,7 +332,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
       if (conj->needsRefinement())
       {
         // immediately go to refine candidate
-        checkCegConjecture(conj);
+        checkConjecture(conj);
         return;
       }
     }
diff --git a/src/theory/quantifiers/sygus/ce_guided_instantiation.h b/src/theory/quantifiers/sygus/ce_guided_instantiation.h
index 03b4c4cc1..9c81b6978 100644
--- a/src/theory/quantifiers/sygus/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/sygus/ce_guided_instantiation.h
@@ -48,8 +48,9 @@ private:
    */
   bool assignConjecture(Node q);
   /** check conjecture */
-  void checkCegConjecture( CegConjecture * conj );
-public:
+  void checkConjecture(CegConjecture* conj);
+
+ public:
   CegInstantiation( QuantifiersEngine * qe, context::Context* c );
   ~CegInstantiation();
 public:
diff --git a/src/theory/quantifiers/term_enumeration.cpp b/src/theory/quantifiers/term_enumeration.cpp
index 34b9d7e81..8e3219768 100644
--- a/src/theory/quantifiers/term_enumeration.cpp
+++ b/src/theory/quantifiers/term_enumeration.cpp
@@ -53,84 +53,38 @@ Node TermEnumeration::getEnumerateTerm(TypeNode tn, unsigned index)
   return d_enum_terms[tn][index];
 }
 
-bool TermEnumeration::isClosedEnumerableType(TypeNode tn)
-{
-  std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
-      d_typ_closed_enum.find(tn);
-  if (it == d_typ_closed_enum.end())
-  {
-    d_typ_closed_enum[tn] = true;
-    bool ret = true;
-    if (tn.isArray() || tn.isSort() || tn.isCodatatype() || tn.isFunction())
-    {
-      ret = false;
-    }
-    else if (tn.isSet())
-    {
-      ret = isClosedEnumerableType(tn.getSetElementType());
-    }
-    else if (tn.isDatatype())
-    {
-      const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
-      for (unsigned i = 0; i < dt.getNumConstructors(); i++)
-      {
-        for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
-        {
-          TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
-          if (tn != ctn && !isClosedEnumerableType(ctn))
-          {
-            ret = false;
-            break;
-          }
-        }
-        if (!ret)
-        {
-          break;
-        }
-      }
-    }
-    
-    // other parametric sorts go here
-    
-    d_typ_closed_enum[tn] = ret;
-    return ret;
-  }
-  else
-  {
-    return it->second;
-  }
-}
-
-// checks whether a type is closed enumerable and is reasonably small enough (<1000)
-// such that all of its domain elements can be enumerated
 bool TermEnumeration::mayComplete(TypeNode tn)
 {
   std::unordered_map<TypeNode, bool, TypeNodeHashFunction>::iterator it =
       d_may_complete.find(tn);
   if (it == d_may_complete.end())
   {
-    bool mc = false;
-    if (isClosedEnumerableType(tn) && tn.isInterpretedFinite())
-    {
-      Cardinality c = tn.getCardinality();
-      if (!c.isLargeFinite())
-      {
-        NodeManager* nm = NodeManager::currentNM();
-        Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
-        // check if less than fixed upper bound, default 1000
-        Node oth = nm->mkConst(Rational(options::fmfTypeCompletionThresh()));
-        Node eq = nm->mkNode(LEQ, card, oth);
-        eq = Rewriter::rewrite(eq);
-        mc = eq.isConst() && eq.getConst<bool>();
-      }
-    }
+    // cache
+    bool mc = mayComplete(tn, options::fmfTypeCompletionThresh());
     d_may_complete[tn] = mc;
     return mc;
   }
-  else
+  return it->second;
+}
+
+bool TermEnumeration::mayComplete(TypeNode tn, unsigned maxCard)
+{
+  bool mc = false;
+  if (tn.isClosedEnumerable() && tn.isInterpretedFinite())
   {
-    return it->second;
+    Cardinality c = tn.getCardinality();
+    if (!c.isLargeFinite())
+    {
+      NodeManager* nm = NodeManager::currentNM();
+      Node card = nm->mkConst(Rational(c.getFiniteCardinality()));
+      // check if less than fixed upper bound
+      Node oth = nm->mkConst(Rational(maxCard));
+      Node eq = nm->mkNode(LEQ, card, oth);
+      eq = Rewriter::rewrite(eq);
+      mc = eq.isConst() && eq.getConst<bool>();
+    }
   }
+  return mc;
 }
 
 } /* CVC4::theory::quantifiers namespace */
diff --git a/src/theory/quantifiers/term_enumeration.h b/src/theory/quantifiers/term_enumeration.h
index cede77dbe..cf25335f4 100644
--- a/src/theory/quantifiers/term_enumeration.h
+++ b/src/theory/quantifiers/term_enumeration.h
@@ -42,25 +42,19 @@ class TermEnumeration
   ~TermEnumeration() {}
   /** get i^th term for type tn */
   Node getEnumerateTerm(TypeNode tn, unsigned i);
-  /** is closed enumerable type
-   *
-   * This returns true if this type has an enumerator that produces
-   * constants that are handled by ground theory solvers.
-   * Examples of types that are not closed enumerable are:
-   * (1) uninterpreted sorts,
-   * (2) arrays,
-   * (3) codatatypes,
-   * (4) parametric sorts involving any of the above.
-   */
-  bool isClosedEnumerableType(TypeNode tn);
   /** may complete type
    *
-   * Returns true if the type tn is closed 
-   * enumerable, and is small enough
-   * for finite model finding to enumerate it,
-   * by some heuristic (current cardinality < 1000).
+   * Returns true if the type tn is closed enumerable, is interpreted as a
+   * finite type, and has cardinality less than some reasonable value
+   * (currently < 1000). This method caches the results of whether each type
+   * may be completed.
    */
   bool mayComplete(TypeNode tn);
+  /**
+   * Static version of the above method where maximum cardinality is
+   * configurable.
+   */
+  static bool mayComplete(TypeNode tn, unsigned cardMax);
 
  private:
   /** ground terms enumerated for types */
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 7fa22e418..dcd90c236 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -403,7 +403,7 @@ int RepSetIterator::increment(){
 
 bool RepSetIterator::isFinished() const { return d_index.empty(); }
 
-Node RepSetIterator::getCurrentTerm(unsigned v, bool valTerm)
+Node RepSetIterator::getCurrentTerm(unsigned v, bool valTerm) const
 {
   unsigned ii = d_index_order[v];
   unsigned curr = d_index[ii];
@@ -422,6 +422,14 @@ Node RepSetIterator::getCurrentTerm(unsigned v, bool valTerm)
   return t;
 }
 
+void RepSetIterator::getCurrentTerms(std::vector<Node>& terms) const
+{
+  for (unsigned i = 0, size = d_index_order.size(); i < size; i++)
+  {
+    terms.push_back(getCurrentTerm(i));
+  }
+}
+
 void RepSetIterator::debugPrint( const char* c ){
   for( unsigned v=0; v<d_index.size(); v++ ){
     Debug( c ) << v << " : " << getCurrentTerm( v ) << std::endl;
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index 29cca462a..d5de1e520 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -148,7 +148,7 @@ public:
  };
 
 public:
- RepSetIterator(const RepSet* rs, RepBoundExt* rext);
+ RepSetIterator(const RepSet* rs, RepBoundExt* rext = nullptr);
  ~RepSetIterator() {}
  /** set that this iterator will be iterating over instantiations for a
   * quantifier */
@@ -168,9 +168,11 @@ public:
  /** get domain size of the i^th field of this iterator */
  unsigned domainSize(unsigned i);
  /** get the i^th term in the tuple we are considering */
- Node getCurrentTerm(unsigned v, bool valTerm = false);
+ Node getCurrentTerm(unsigned v, bool valTerm = false) const;
  /** get the number of terms in the tuple we are considering */
- unsigned getNumTerms() { return d_index_order.size(); }
+ unsigned getNumTerms() const { return d_index_order.size(); }
+ /** get current terms */
+ void getCurrentTerms(std::vector<Node>& terms) const;
  /** get index order, returns var # */
  unsigned getIndexOrder(unsigned v) { return d_index_order[v]; }
  /** get variable order, returns index # */
diff --git a/src/util/dense_map.h b/src/util/dense_map.h
index a3a1573c0..410fcc8fa 100644
--- a/src/util/dense_map.h
+++ b/src/util/dense_map.h
@@ -26,7 +26,7 @@
 
 #pragma once
 
-#include <boost/integer_traits.hpp>
+#include <limits>
 #include <vector>
 
 #include "base/cvc4_assert.h"
@@ -48,7 +48,8 @@ private:
 
   typedef Index Position;
   typedef std::vector<Position> PositionMap;
-  static const Position POSITION_SENTINEL = boost::integer_traits<Position>::const_max;
+  static const Position POSITION_SENTINEL =
+      std::numeric_limits<Position>::max();
 
   //Each Key in the set is mapped to its position in d_list.
   //Each Key not in the set is mapped to KEY_SENTINEL
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index ae99caedd..59a5b5f64 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -610,6 +610,7 @@ REG0_TESTS = \
 	regress0/quantifiers/cegqi-nl-sq.smt2 \
 	regress0/quantifiers/clock-10.smt2 \
 	regress0/quantifiers/clock-3.smt2 \
+	regress0/quantifiers/cond-var-elim-binary.smt2 \
 	regress0/quantifiers/delta-simp.smt2 \
 	regress0/quantifiers/double-pattern.smt2 \
 	regress0/quantifiers/ex3.smt2 \
diff --git a/test/regress/regress0/quantifiers/cond-var-elim-binary.smt2 b/test/regress/regress0/quantifiers/cond-var-elim-binary.smt2
new file mode 100644
index 000000000..edf780b4e
--- /dev/null
+++ b/test/regress/regress0/quantifiers/cond-var-elim-binary.smt2
@@ -0,0 +1,16 @@
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun k_42 () (_ BitVec 32))
+(declare-fun k_332 () (_ BitVec 32))
+(declare-fun k_28 () (_ BitVec 32))
+
+(assert (and 
+(bvult k_332 k_42)
+
+(forall ((x (_ BitVec 32)) (y (_ BitVec 32))) (or 
+  (and (not (bvult y (_ bv65539 32))) (not (= (_ bv1 32) x))) 
+  (not (bvult k_332 (bvmul x k_42)))) )
+)
+)
+
+(check-sat)