Merge branch 'master' into fixBetterSkolemsfixBetterSkolems

15 files changed, 597 insertions, 260 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 9ba7f4b2e..b224032e8 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1004,7 +1004,7 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
       }else if( PARSER_STATE->isDeclared(name,SYM_VARIABLE) ){
         Debug("parser-sygus") << "Sygus grammar " << fun << " : symbol "
                               << name << std::endl;
-        sgt.d_expr = PARSER_STATE->getVariable(name);
+        sgt.d_expr = PARSER_STATE->getExpressionForName(name);
         sgt.d_name = name;
         sgt.d_gterm_type = SygusGTerm::gterm_op;
       }else{
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 303295112..2b81b3835 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4201,7 +4201,10 @@ Expr SmtEngine::getValue(const Expr& ex) const
   Trace("smt") << "--- model-post expected " << expectedType << endl;
 
   // type-check the result we got
-  Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(expectedType),
+  // Notice that lambdas have function type, which does not respect the subtype
+  // relation, so we ignore them here.
+  Assert(resultNode.isNull() || resultNode.getKind() == kind::LAMBDA
+             || resultNode.getType().isSubtypeOf(expectedType),
          "Run with -t smt for details.");
 
   // ensure it's a constant
diff --git a/src/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 29b1cf2fc..1f6e1388a 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -3282,6 +3282,7 @@ std::vector<Node> NonlinearExtension::checkMonomialMagnitude( unsigned c ) {
 std::vector<Node> NonlinearExtension::checkTangentPlanes() {
   std::vector< Node > lemmas;
   Trace("nl-ext") << "Get monomial tangent plane lemmas..." << std::endl;
+  NodeManager* nm = NodeManager::currentNM();
   unsigned kstart = d_ms_vars.size();
   for (unsigned k = kstart; k < d_mterms.size(); k++) {
     Node t = d_mterms[k];
@@ -3321,7 +3322,8 @@ std::vector<Node> NonlinearExtension::checkTangentPlanes() {
                   Node pt_v = d_tangent_val_bound[p][a][b];
                   Assert( !pt_v.isNull() );
                   if( curr_v!=pt_v ){
-                    Node do_extend = NodeManager::currentNM()->mkNode( ( p==1 || p==3 ) ? GT : LT, curr_v, pt_v );
+                    Node do_extend =
+                        nm->mkNode((p == 1 || p == 3) ? GT : LT, curr_v, pt_v);
                     do_extend = Rewriter::rewrite( do_extend );
                     if( do_extend==d_true ){
                       for( unsigned q=0; q<2; q++ ){
@@ -3340,26 +3342,69 @@ std::vector<Node> NonlinearExtension::checkTangentPlanes() {
                 Node b_v = pts[1][p];
               
                 // tangent plane
-                Node tplane = NodeManager::currentNM()->mkNode(
-                    MINUS,
-                    NodeManager::currentNM()->mkNode(
-                        PLUS,
-                        NodeManager::currentNM()->mkNode(MULT, b_v, a),
-                        NodeManager::currentNM()->mkNode(MULT, a_v, b)),
-                    NodeManager::currentNM()->mkNode(MULT, a_v, b_v));
+                Node tplane = nm->mkNode(MINUS,
+                                         nm->mkNode(PLUS,
+                                                    nm->mkNode(MULT, b_v, a),
+                                                    nm->mkNode(MULT, a_v, b)),
+                                         nm->mkNode(MULT, a_v, b_v));
                 for (unsigned d = 0; d < 4; d++) {
-                  Node aa = NodeManager::currentNM()->mkNode(
-                      d == 0 || d == 3 ? GEQ : LEQ, a, a_v);
-                  Node ab = NodeManager::currentNM()->mkNode(
-                      d == 1 || d == 3 ? GEQ : LEQ, b, b_v);
-                  Node conc = NodeManager::currentNM()->mkNode(
-                      d <= 1 ? LEQ : GEQ, t, tplane);
-                  Node tlem = NodeManager::currentNM()->mkNode(
-                      OR, aa.negate(), ab.negate(), conc);
+                  Node aa = nm->mkNode(d == 0 || d == 3 ? GEQ : LEQ, a, a_v);
+                  Node ab = nm->mkNode(d == 1 || d == 3 ? GEQ : LEQ, b, b_v);
+                  Node conc = nm->mkNode(d <= 1 ? LEQ : GEQ, t, tplane);
+                  Node tlem = nm->mkNode(OR, aa.negate(), ab.negate(), conc);
                   Trace("nl-ext-tplanes")
                       << "Tangent plane lemma : " << tlem << std::endl;
                   lemmas.push_back(tlem);
                 }
+
+                // tangent plane reverse implication
+
+                // t <= tplane -> ( (a <= a_v ^ b >= b_v) v
+                // (a >= a_v ^ b <= b_v) ).
+                // in clause form, the above becomes
+                // t <= tplane -> a <= a_v v b <= b_v.
+                // t <= tplane -> b >= b_v v a >= a_v.
+                Node a_leq_av = nm->mkNode(LEQ, a, a_v);
+                Node b_leq_bv = nm->mkNode(LEQ, b, b_v);
+                Node a_geq_av = nm->mkNode(GEQ, a, a_v);
+                Node b_geq_bv = nm->mkNode(GEQ, b, b_v);
+
+                Node t_leq_tplane = nm->mkNode(LEQ, t, tplane);
+                Node a_leq_av_or_b_leq_bv = nm->mkNode(OR, a_leq_av, b_leq_bv);
+                Node b_geq_bv_or_a_geq_av = nm->mkNode(OR, b_geq_bv, a_geq_av);
+                Node ub_reverse1 =
+                    nm->mkNode(OR, t_leq_tplane.negate(), a_leq_av_or_b_leq_bv);
+                Trace("nl-ext-tplanes")
+                    << "Tangent plane lemma (reverse) : " << ub_reverse1
+                    << std::endl;
+                lemmas.push_back(ub_reverse1);
+                Node ub_reverse2 =
+                    nm->mkNode(OR, t_leq_tplane.negate(), b_geq_bv_or_a_geq_av);
+                Trace("nl-ext-tplanes")
+                    << "Tangent plane lemma (reverse) : " << ub_reverse2
+                    << std::endl;
+                lemmas.push_back(ub_reverse2);
+
+                // t >= tplane -> ( (a <= a_v ^ b <= b_v) v
+                // (a >= a_v ^ b >= b_v) ).
+                // in clause form, the above becomes
+                // t >= tplane -> a <= a_v v b >= b_v.
+                // t >= tplane -> b >= b_v v a <= a_v
+                Node t_geq_tplane = nm->mkNode(GEQ, t, tplane);
+                Node a_leq_av_or_b_geq_bv = nm->mkNode(OR, a_leq_av, b_geq_bv);
+                Node a_geq_av_or_b_leq_bv = nm->mkNode(OR, a_geq_av, b_leq_bv);
+                Node lb_reverse1 =
+                    nm->mkNode(OR, t_geq_tplane.negate(), a_leq_av_or_b_geq_bv);
+                Trace("nl-ext-tplanes")
+                    << "Tangent plane lemma (reverse) : " << lb_reverse1
+                    << std::endl;
+                lemmas.push_back(lb_reverse1);
+                Node lb_reverse2 =
+                    nm->mkNode(OR, t_geq_tplane.negate(), a_geq_av_or_b_leq_bv);
+                Trace("nl-ext-tplanes")
+                    << "Tangent plane lemma (reverse) : " << lb_reverse2
+                    << std::endl;
+                lemmas.push_back(lb_reverse2);
               }
             }
           }
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index be87b7e8d..ac3bff21b 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -16,6 +16,8 @@
 
 #include "theory/datatypes/datatypes_rewriter.h"
 
+#include "expr/node_algorithm.h"
+
 using namespace CVC4;
 using namespace CVC4::kind;
 
@@ -115,8 +117,7 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
     if (ev.getKind() == APPLY_CONSTRUCTOR)
     {
       Trace("dt-sygus-util") << "Rewrite " << in << " by unfolding...\n";
-      const Datatype& dt =
-          static_cast<DatatypeType>(ev.getType().toType()).getDatatype();
+      const Datatype& dt = ev.getType().getDatatype();
       unsigned i = indexOf(ev.getOperator());
       Node op = Node::fromExpr(dt[i].getSygusOp());
       // if it is the "any constant" constructor, return its argument
@@ -141,14 +142,8 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
         children.push_back(nm->mkNode(DT_SYGUS_EVAL, cc));
       }
       Node ret = mkSygusTerm(dt, i, children);
-      // if it is a variable, apply the substitution
-      if (ret.getKind() == BOUND_VARIABLE)
-      {
-        Assert(ret.hasAttribute(SygusVarNumAttribute()));
-        int vn = ret.getAttribute(SygusVarNumAttribute());
-        Assert(Node::fromExpr(dt.getSygusVarList())[vn] == ret);
-        ret = args[vn];
-      }
+      // apply the appropriate substitution
+      ret = applySygusArgs(dt, op, ret, args);
       Trace("dt-sygus-util") << "...got " << ret << "\n";
       return RewriteResponse(REWRITE_AGAIN_FULL, ret);
     }
@@ -186,6 +181,67 @@ RewriteResponse DatatypesRewriter::postRewrite(TNode in)
   return RewriteResponse(REWRITE_DONE, in);
 }
 
+Node DatatypesRewriter::applySygusArgs(const Datatype& dt,
+                                       Node op,
+                                       Node n,
+                                       const std::vector<Node>& args)
+{
+  if (n.getKind() == BOUND_VARIABLE)
+  {
+    Assert(n.hasAttribute(SygusVarNumAttribute()));
+    int vn = n.getAttribute(SygusVarNumAttribute());
+    Assert(Node::fromExpr(dt.getSygusVarList())[vn] == n);
+    return args[vn];
+  }
+  // n is an application of operator op.
+  // We must compute the free variables in op to determine if there are
+  // any substitutions we need to make to n.
+  TNode val;
+  if (!op.hasAttribute(SygusVarFreeAttribute()))
+  {
+    std::unordered_set<Node, NodeHashFunction> fvs;
+    if (expr::getFreeVariables(op, fvs))
+    {
+      if (fvs.size() == 1)
+      {
+        for (const Node& v : fvs)
+        {
+          val = v;
+        }
+      }
+      else
+      {
+        val = op;
+      }
+    }
+    Trace("dt-sygus-fv") << "Free var in " << op << " : " << val << std::endl;
+    op.setAttribute(SygusVarFreeAttribute(), val);
+  }
+  else
+  {
+    val = op.getAttribute(SygusVarFreeAttribute());
+  }
+  if (val.isNull())
+  {
+    return n;
+  }
+  if (val.getKind() == BOUND_VARIABLE)
+  {
+    // single substitution case
+    int vn = val.getAttribute(SygusVarNumAttribute());
+    TNode sub = args[vn];
+    return n.substitute(val, sub);
+  }
+  // do the full substitution
+  std::vector<Node> vars;
+  Node bvl = Node::fromExpr(dt.getSygusVarList());
+  for (unsigned i = 0, nvars = bvl.getNumChildren(); i < nvars; i++)
+  {
+    vars.push_back(bvl[i]);
+  }
+  return n.substitute(vars.begin(), vars.end(), args.begin(), args.end());
+}
+
 Kind DatatypesRewriter::getOperatorKindForSygusBuiltin(Node op)
 {
   Assert(op.getKind() != BUILTIN);
@@ -224,6 +280,13 @@ Node DatatypesRewriter::mkSygusTerm(const Datatype& dt,
   Assert(!dt[i].getSygusOp().isNull());
   std::vector<Node> schildren;
   Node op = Node::fromExpr(dt[i].getSygusOp());
+  Trace("dt-sygus-util") << "Operator is " << op << std::endl;
+  if (children.empty())
+  {
+    // no children, return immediately
+    Trace("dt-sygus-util") << "...return direct op" << std::endl;
+    return op;
+  }
   // if it is the any constant, we simply return the child
   if (op.getAttribute(SygusAnyConstAttribute()))
   {
@@ -243,18 +306,13 @@ Node DatatypesRewriter::mkSygusTerm(const Datatype& dt,
     return ret;
   }
   Kind ok = NodeManager::operatorToKind(op);
+  Trace("dt-sygus-util") << "operator kind is " << ok << std::endl;
   if (ok != UNDEFINED_KIND)
   {
-    if (ok == APPLY_UF && schildren.size() == 1)
-    {
-      // This case is triggered for defined constant symbols. In this case,
-      // we return the operator itself instead of an APPLY_UF node.
-      ret = schildren[0];
-    }
-    else
-    {
-      ret = NodeManager::currentNM()->mkNode(ok, schildren);
-    }
+    // If it is an APPLY_UF operator, we should have at least an operator and
+    // a child.
+    Assert(ok != APPLY_UF || schildren.size() != 1);
+    ret = NodeManager::currentNM()->mkNode(ok, schildren);
     Trace("dt-sygus-util") << "...return (op) " << ret << std::endl;
     return ret;
   }
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 6c1d64e5b..1a1735402 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -51,6 +51,28 @@ struct SygusSymBreakOkAttributeId
 typedef expr::Attribute<SygusSymBreakOkAttributeId, bool>
     SygusSymBreakOkAttribute;
 
+/** sygus var free
+ *
+ * This attribute is used to mark whether sygus operators have free occurrences
+ * of variables from the formal argument list of the function-to-synthesize.
+ *
+ * We store three possible cases for sygus operators op:
+ * (1) op.getAttribute(SygusVarFreeAttribute())==Node::null()
+ * In this case, op has no free variables from the formal argument list of the
+ * function-to-synthesize.
+ * (2) op.getAttribute(SygusVarFreeAttribute())==v, where v is a bound variable.
+ * In this case, op has exactly one free variable, v.
+ * (3) op.getAttribute(SygusVarFreeAttribute())==op
+ * In this case, op has an arbitrary set (cardinality >1) of free variables from
+ * the formal argument list of the function to synthesize.
+ *
+ * This attribute is used to compute applySygusArgs below.
+ */
+struct SygusVarFreeAttributeId
+{
+};
+typedef expr::Attribute<SygusVarFreeAttributeId, Node> SygusVarFreeAttribute;
+
 namespace datatypes {
 
 class DatatypesRewriter {
@@ -150,6 +172,37 @@ public:
                          unsigned i,
                          const std::vector<Node>& children);
  /**
+  * n is a builtin term that is an application of operator op.
+  *
+  * This returns an n' such that (eval n args) is n', where n' is a instance of
+  * n for the appropriate substitution.
+  *
+  * For example, given a function-to-synthesize with formal argument list (x,y),
+  * say we have grammar:
+  *   A -> A+A | A+x | A+(x+y) | y
+  * These lead to constructors with sygus ops:
+  *   C1 / (lambda w1 w2. w1+w2)
+  *   C2 / (lambda w1. w1+x)
+  *   C3 / (lambda w1. w1+(x+y))
+  *   C4 / y
+  * Examples of calling this function:
+  *   applySygusArgs( dt, C1, (APPLY_UF (lambda w1 w2. w1+w2) t1 t2), { 3, 5 } )
+  *     ... returns (APPLY_UF (lambda w1 w2. w1+w2) t1 t2).
+  *   applySygusArgs( dt, C2, (APPLY_UF (lambda w1. w1+x) t1), { 3, 5 } )
+  *     ... returns (APPLY_UF (lambda w1. w1+3) t1).
+  *   applySygusArgs( dt, C3, (APPLY_UF (lambda w1. w1+(x+y)) t1), { 3, 5 } )
+  *     ... returns (APPLY_UF (lambda w1. w1+(3+5)) t1).
+  *   applySygusArgs( dt, C4, y, { 3, 5 } )
+  *     ... returns 5.
+  * Notice the attribute SygusVarFreeAttribute is applied to C1, C2, C3, C4,
+  * to cache the results of whether the evaluation of this constructor needs
+  * a substitution over the formal argument list of the function-to-synthesize.
+  */
+ static Node applySygusArgs(const Datatype& dt,
+                            Node op,
+                            Node n,
+                            const std::vector<Node>& args);
+ /**
   * Get the builtin sygus operator for constructor term n of sygus datatype
   * type. For example, if n is the term C_+( d1, d2 ) where C_+ is a sygus
   * constructor whose sygus op is the builtin operator +, this method returns +.
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index dc18a2005..07f754810 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -561,7 +561,9 @@ bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) {
   return false;
 }
 
-bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ) {
+bool QuantInfo::isTConstraintSpurious(QuantConflictFind* p,
+                                      std::vector<Node>& terms)
+{
   if( options::qcfEagerTest() ){
     //check whether the instantiation evaluates as expected
     if (p->atConflictEffort()) {
@@ -571,12 +573,14 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node
         Trace("qcf-instance-check") << "  " << terms[i] << std::endl;
         subs[d_q[0][i]] = terms[i];
       }
+      TermDb* tdb = p->getTermDatabase();
       for( unsigned i=0; i<d_extra_var.size(); i++ ){
         Node n = getCurrentExpValue( d_extra_var[i] );
         Trace("qcf-instance-check") << "  " << d_extra_var[i] << " -> " << n << std::endl;
         subs[d_extra_var[i]] = n;
       }
-      if( !p->getTermDatabase()->isEntailed( d_q[1], subs, false, false ) ){
+      if (!tdb->isEntailed(d_q[1], subs, false, false))
+      {
         Trace("qcf-instance-check") << "...not entailed to be false." << std::endl;
         return true;
       }
@@ -1822,8 +1826,9 @@ QuantConflictFind::QuantConflictFind(QuantifiersEngine* qe, context::Context* c)
       d_conflict(c, false),
       d_true(NodeManager::currentNM()->mkConst<bool>(true)),
       d_false(NodeManager::currentNM()->mkConst<bool>(false)),
-      d_effort(EFFORT_INVALID),
-      d_needs_computeRelEqr() {}
+      d_effort(EFFORT_INVALID)
+{
+}
 
 //-------------------------------------------------- registration
 
@@ -1892,7 +1897,25 @@ bool QuantConflictFind::needsCheck( Theory::Effort level ) {
 }
 
 void QuantConflictFind::reset_round( Theory::Effort level ) {
-  d_needs_computeRelEqr = true;
+  Trace("qcf-check") << "QuantConflictFind::reset_round" << std::endl;
+  Trace("qcf-check") << "Compute relevant equivalence classes..." << std::endl;
+  d_eqcs.clear();
+
+  eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(getEqualityEngine());
+  TermDb* tdb = getTermDatabase();
+  while (!eqcs_i.isFinished())
+  {
+    Node r = (*eqcs_i);
+    if (tdb->hasTermCurrent(r))
+    {
+      TypeNode rtn = r.getType();
+      if (!options::cbqi() || !TermUtil::hasInstConstAttr(r))
+      {
+        d_eqcs[rtn].push_back(r);
+      }
+    }
+    ++eqcs_i;
+  }
 }
 
 void QuantConflictFind::setIrrelevantFunction( TNode f ) {
@@ -1928,182 +1951,240 @@ inline QuantConflictFind::Effort QcfEffortEnd() {
 void QuantConflictFind::check(Theory::Effort level, QEffort quant_e)
 {
   CodeTimer codeTimer(d_quantEngine->d_statistics.d_qcf_time);
-  if (quant_e == QEFFORT_CONFLICT)
+  if (quant_e != QEFFORT_CONFLICT)
   {
-    Trace("qcf-check") << "QCF : check : " << level << std::endl;
-    if( d_conflict ){
-      Trace("qcf-check2") << "QCF : finished check : already in conflict." << std::endl;
-      if( level>=Theory::EFFORT_FULL ){
-        Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;
-        //Assert( false );
-      }
-    }else{
-      int addedLemmas = 0;
-      ++(d_statistics.d_inst_rounds);
-      double clSet = 0;
-      int prevEt = 0;
-      if( Trace.isOn("qcf-engine") ){
-        prevEt = d_statistics.d_entailment_checks.getData();
-        clSet = double(clock())/double(CLOCKS_PER_SEC);
-        Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;
-      }
-      computeRelevantEqr();
-
-      d_irr_func.clear();
-      d_irr_quant.clear();
-
-      if( Trace.isOn("qcf-debug") ){
-        Trace("qcf-debug") << std::endl;
-        debugPrint("qcf-debug");
-        Trace("qcf-debug") << std::endl;
-      }
-      bool isConflict = false;
-      for (unsigned e = QcfEffortStart(), end = QcfEffortEnd(); e <= end; ++e) {
-        d_effort = static_cast<Effort>(e);
-        Trace("qcf-check") << "Checking quantified formulas at effort " << e << "..." << std::endl;
-        for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
-          Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
-          if( d_quantEngine->hasOwnership( q, this ) && d_irr_quant.find( q )==d_irr_quant.end() ){
-            QuantInfo * qi = &d_qinfo[q];
-
-            Assert( d_qinfo.find( q )!=d_qinfo.end() );
-            if( qi->matchGeneratorIsValid() ){
-              Trace("qcf-check") << "Check quantified formula ";
-              debugPrintQuant("qcf-check", q);
-              Trace("qcf-check") << " : " << q << "..." << std::endl;
-
-              Trace("qcf-check-debug") << "Reset round..." << std::endl;
-              if( qi->reset_round( this ) ){
-                //try to make a matches making the body false
-                Trace("qcf-check-debug") << "Get next match..." << std::endl;
-                while( qi->getNextMatch( this ) ){
-                  if( d_quantEngine->inConflict() ){
-                    Trace("qcf-check") << "   ... Quantifiers engine discovered conflict, ";
-                    Trace("qcf-check") << "probably related to disequal congruent terms in master equality engine" << std::endl;
-                    break;
-                  }else{
-                    Trace("qcf-inst") << "*** Produced match at effort " << e << " : " << std::endl;
-                    qi->debugPrintMatch("qcf-inst");
-                    Trace("qcf-inst") << std::endl;
-                    if( !qi->isMatchSpurious( this ) ){
-                      std::vector< int > assigned;
-                      if( qi->completeMatch( this, assigned ) ){
-                        std::vector< Node > terms;
-                        qi->getMatch( terms );
-                        bool tcs = qi->isTConstraintSpurious( this, terms );
-                        if( !tcs ){
-                          //for debugging
-                          if( Debug.isOn("qcf-check-inst") ){
-                            Node inst = d_quantEngine->getInstantiate()
-                                            ->getInstantiation(q, terms);
-                            Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;
-                            Assert( !getTermDatabase()->isEntailed( inst, true ) );
-                            Assert(getTermDatabase()->isEntailed(inst, false) ||
-                                   e > EFFORT_CONFLICT);
-                          }
-                          if (d_quantEngine->getInstantiate()->addInstantiation(
-                                  q, terms))
-                          {
-                            Trace("qcf-check") << "   ... Added instantiation" << std::endl;
-                            Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;
-                            qi->debugPrintMatch("qcf-inst");
-                            Trace("qcf-inst") << std::endl;
-                            ++addedLemmas;
-                            if (e == EFFORT_CONFLICT) {
-                              d_quantEngine->markRelevant( q );
-                              ++(d_quantEngine->d_statistics.d_instantiations_qcf);
-                              if( options::qcfAllConflict() ){
-                                isConflict = true;
-                              }else{
-                                d_conflict.set( true );
-                              }
-                              break;
-                            } else if (e == EFFORT_PROP_EQ) {
-                              d_quantEngine->markRelevant( q );
-                              ++(d_quantEngine->d_statistics.d_instantiations_qcf);
-                            }
-                          }else{
-                            Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;
-                            //this should only happen if the algorithm generates the same propagating instance twice this round
-                            //in this case, break to avoid exponential behavior
-                            break;
-                          }
-                        }else{
-                          Trace("qcf-inst") << "   ... Spurious instantiation (match is T-inconsistent)" << std::endl;
-                        }
-                        //clean up assigned
-                        qi->revertMatch( this, assigned );
-                        d_tempCache.clear();
-                      }else{
-                        Trace("qcf-inst") << "   ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;
-                      }
-                    }else{
-                      Trace("qcf-inst") << "   ... Spurious instantiation (match is inconsistent)" << std::endl;
-                    }
-                  }
-                }
-                Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl;
-              }
-              if (d_conflict || d_quantEngine->inConflict())
-              {
-                break;
-              }
-            }
-          }
-        }
-        if( addedLemmas>0 || d_quantEngine->inConflict() ){
+    return;
+  }
+  Trace("qcf-check") << "QCF : check : " << level << std::endl;
+  if (d_conflict)
+  {
+    Trace("qcf-check2") << "QCF : finished check : already in conflict."
+                        << std::endl;
+    if (level >= Theory::EFFORT_FULL)
+    {
+      Trace("qcf-warn") << "ALREADY IN CONFLICT? " << level << std::endl;
+    }
+    return;
+  }
+  unsigned addedLemmas = 0;
+  ++(d_statistics.d_inst_rounds);
+  double clSet = 0;
+  int prevEt = 0;
+  if (Trace.isOn("qcf-engine"))
+  {
+    prevEt = d_statistics.d_entailment_checks.getData();
+    clSet = double(clock()) / double(CLOCKS_PER_SEC);
+    Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level
+                        << "---" << std::endl;
+  }
+
+  // reset the round-specific information
+  d_irr_func.clear();
+  d_irr_quant.clear();
+
+  if (Trace.isOn("qcf-debug"))
+  {
+    Trace("qcf-debug") << std::endl;
+    debugPrint("qcf-debug");
+    Trace("qcf-debug") << std::endl;
+  }
+  bool isConflict = false;
+  FirstOrderModel* fm = d_quantEngine->getModel();
+  unsigned nquant = fm->getNumAssertedQuantifiers();
+  // for each effort level (find conflict, find propagating)
+  for (unsigned e = QcfEffortStart(), end = QcfEffortEnd(); e <= end; ++e)
+  {
+    // set the effort (data member for convienence of access)
+    d_effort = static_cast<Effort>(e);
+    Trace("qcf-check") << "Checking quantified formulas at effort " << e
+                       << "..." << std::endl;
+    // for each quantified formula
+    for (unsigned i = 0; i < nquant; i++)
+    {
+      Node q = fm->getAssertedQuantifier(i, true);
+      if (d_quantEngine->hasOwnership(q, this)
+          && d_irr_quant.find(q) == d_irr_quant.end()
+          && fm->isQuantifierActive(q))
+      {
+        // check this quantified formula
+        checkQuantifiedFormula(q, isConflict, addedLemmas);
+        if (d_conflict || d_quantEngine->inConflict())
+        {
           break;
         }
       }
-      if( isConflict ){
-        d_conflict.set( true );
-      }
-      if( Trace.isOn("qcf-engine") ){
-        double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
-        Trace("qcf-engine") << "Finished conflict find engine, time = " << (clSet2-clSet);
-        if( addedLemmas>0 ){
-          Trace("qcf-engine")
-              << ", effort = "
-              << (d_effort == EFFORT_CONFLICT
-                      ? "conflict"
-                      : (d_effort == EFFORT_PROP_EQ ? "prop_eq" : "mc"));
-          Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
-        }
-        Trace("qcf-engine") << std::endl;
-        int currEt = d_statistics.d_entailment_checks.getData();
-        if( currEt!=prevEt ){
-          Trace("qcf-engine") << "  Entailment checks = " << ( currEt - prevEt ) << std::endl;
-        }
-      }
-      Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
     }
+    // We are done if we added a lemma, or discovered a conflict in another
+    // way. An example of the latter case is when two disequal congruent terms
+    // are discovered during term indexing.
+    if (addedLemmas > 0 || d_quantEngine->inConflict())
+    {
+      break;
+    }
+  }
+  if (isConflict)
+  {
+    d_conflict.set(true);
   }
+  if (Trace.isOn("qcf-engine"))
+  {
+    double clSet2 = double(clock()) / double(CLOCKS_PER_SEC);
+    Trace("qcf-engine") << "Finished conflict find engine, time = "
+                        << (clSet2 - clSet);
+    if (addedLemmas > 0)
+    {
+      Trace("qcf-engine") << ", effort = "
+                          << (d_effort == EFFORT_CONFLICT
+                                  ? "conflict"
+                                  : (d_effort == EFFORT_PROP_EQ ? "prop_eq"
+                                                                : "mc"));
+      Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;
+    }
+    Trace("qcf-engine") << std::endl;
+    int currEt = d_statistics.d_entailment_checks.getData();
+    if (currEt != prevEt)
+    {
+      Trace("qcf-engine") << "  Entailment checks = " << (currEt - prevEt)
+                          << std::endl;
+    }
+  }
+  Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;
 }
 
-void QuantConflictFind::computeRelevantEqr() {
-  if( d_needs_computeRelEqr ){
-    d_needs_computeRelEqr = false;
-    Trace("qcf-check") << "Compute relevant equivalence classes..." << std::endl;
-    d_eqcs.clear();
-
-    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( getEqualityEngine() );
-    while( !eqcs_i.isFinished() ){
-      Node r = (*eqcs_i);
-      if( getTermDatabase()->hasTermCurrent( r ) ){
-        TypeNode rtn = r.getType();
-        if( !options::cbqi() || !TermUtil::hasInstConstAttr( r ) ){
-          d_eqcs[rtn].push_back( r );
+void QuantConflictFind::checkQuantifiedFormula(Node q,
+                                               bool& isConflict,
+                                               unsigned& addedLemmas)
+{
+  QuantInfo* qi = &d_qinfo[q];
+  Assert(d_qinfo.find(q) != d_qinfo.end());
+  if (!qi->matchGeneratorIsValid())
+  {
+    // quantified formula is not properly set up for matching
+    return;
+  }
+  if (Trace.isOn("qcf-check"))
+  {
+    Trace("qcf-check") << "Check quantified formula ";
+    debugPrintQuant("qcf-check", q);
+    Trace("qcf-check") << " : " << q << "..." << std::endl;
+  }
+
+  Trace("qcf-check-debug") << "Reset round..." << std::endl;
+  if (!qi->reset_round(this))
+  {
+    // it is typically the case that another conflict (e.g. in the term
+    // database) was discovered if we fail here.
+    return;
+  }
+  // try to make a matches making the body false or propagating
+  Trace("qcf-check-debug") << "Get next match..." << std::endl;
+  Instantiate* qinst = d_quantEngine->getInstantiate();
+  while (qi->getNextMatch(this))
+  {
+    if (d_quantEngine->inConflict())
+    {
+      Trace("qcf-check") << "   ... Quantifiers engine discovered conflict, ";
+      Trace("qcf-check") << "probably related to disequal congruent terms in "
+                            "master equality engine"
+                         << std::endl;
+      return;
+    }
+    if (Trace.isOn("qcf-inst"))
+    {
+      Trace("qcf-inst") << "*** Produced match at effort " << d_effort << " : "
+                        << std::endl;
+      qi->debugPrintMatch("qcf-inst");
+      Trace("qcf-inst") << std::endl;
+    }
+    // check whether internal match constraints are satisfied
+    if (qi->isMatchSpurious(this))
+    {
+      Trace("qcf-inst") << "   ... Spurious (match is inconsistent)"
+                        << std::endl;
+      continue;
+    }
+    // check whether match can be completed
+    std::vector<int> assigned;
+    if (!qi->completeMatch(this, assigned))
+    {
+      Trace("qcf-inst") << "   ... Spurious (cannot assign unassigned vars)"
+                        << std::endl;
+      continue;
+    }
+    // check whether the match is spurious according to (T-)entailment checks
+    std::vector<Node> terms;
+    qi->getMatch(terms);
+    bool tcs = qi->isTConstraintSpurious(this, terms);
+    if (tcs)
+    {
+      Trace("qcf-inst") << "   ... Spurious (match is T-inconsistent)"
+                        << std::endl;
+    }
+    else
+    {
+      // otherwise, we have a conflict/propagating instance
+      // for debugging
+      if (Debug.isOn("qcf-check-inst"))
+      {
+        Node inst = qinst->getInstantiation(q, terms);
+        Debug("qcf-check-inst")
+            << "Check instantiation " << inst << "..." << std::endl;
+        Assert(!getTermDatabase()->isEntailed(inst, true));
+        Assert(getTermDatabase()->isEntailed(inst, false)
+               || d_effort > EFFORT_CONFLICT);
+      }
+      // Process the lemma: either add an instantiation or specific lemmas
+      // constructed during the isTConstraintSpurious call, or both.
+      if (!qinst->addInstantiation(q, terms))
+      {
+        Trace("qcf-inst") << "   ... Failed to add instantiation" << std::endl;
+        // This should only happen if the algorithm generates the same
+        // propagating instance twice this round. In this case, return
+        // to avoid exponential behavior.
+        return;
+      }
+      Trace("qcf-check") << "   ... Added instantiation" << std::endl;
+      if (Trace.isOn("qcf-inst"))
+      {
+        Trace("qcf-inst") << "*** Was from effort " << d_effort << " : "
+                          << std::endl;
+        qi->debugPrintMatch("qcf-inst");
+        Trace("qcf-inst") << std::endl;
+      }
+      ++addedLemmas;
+      if (d_effort == EFFORT_CONFLICT)
+      {
+        // mark relevant: this ensures that quantified formula q is
+        // checked first on the next round. This is an optimization to
+        // ensure that quantified formulas that are more likely to have
+        // conflicting instances are checked earlier.
+        d_quantEngine->markRelevant(q);
+        ++(d_quantEngine->d_statistics.d_instantiations_qcf);
+        if (options::qcfAllConflict())
+        {
+          isConflict = true;
+        }
+        else
+        {
+          d_conflict.set(true);
         }
+        return;
+      }
+      else if (d_effort == EFFORT_PROP_EQ)
+      {
+        d_quantEngine->markRelevant(q);
+        ++(d_quantEngine->d_statistics.d_instantiations_qcf);
       }
-      ++eqcs_i;
     }
+    // clean up assigned
+    qi->revertMatch(this, assigned);
+    d_tempCache.clear();
   }
+  Trace("qcf-check") << "Done, conflict = " << d_conflict << std::endl;
 }
 
-
 //-------------------------------------------------- debugging
 
-
 void QuantConflictFind::debugPrint( const char * c ) {
   //print the equivalance classes
   Trace(c) << "----------EQ classes" << std::endl;
diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index f22910191..7e4eb517d 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -242,14 +242,30 @@ public:
   bool needsCheck(Theory::Effort level) override;
   /** reset round */
   void reset_round(Theory::Effort level) override;
-  /** check */
+  /** check
+   *
+   * This method attempts to construct a conflicting or propagating instance.
+   * If such an instance exists, then it makes a call to
+   * Instantiation::addInstantiation or QuantifiersEngine::addLemma.
+   */
   void check(Theory::Effort level, QEffort quant_e) override;
 
  private:
-  bool d_needs_computeRelEqr;
-public:
-  void computeRelevantEqr();
-private:
+  /** check quantified formula
+   *
+   * This method is called by the above check method for each quantified
+   * formula q. It attempts to find a conflicting or propagating instance for
+   * q, depending on the effort level (d_effort).
+   *
+   * isConflict: this is set to true if we discovered a conflicting instance.
+   * This flag may be set instead of d_conflict if --qcf-all-conflict is true,
+   * in which we continuing adding all conflicts.
+   * addedLemmas: tracks the total number of lemmas added, and is incremented by
+   * this method when applicable.
+   */
+  void checkQuantifiedFormula(Node q, bool& isConflict, unsigned& addedLemmas);
+
+ private:
   void debugPrint( const char * c );
   //for debugging
   std::vector< Node > d_quants;
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index ff42a9c89..d92f36afb 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -119,7 +119,6 @@ int RewriteEngine::checkRewriteRule( Node f, Theory::Effort e ) {
   QuantConflictFind * qcf = d_quantEngine->getConflictFind();
   if( qcf ){
     //reset QCF module
-    qcf->computeRelevantEqr();
     qcf->setEffort(QuantConflictFind::EFFORT_CONFLICT);
     //get the proper quantifiers info
     std::map< Node, QuantInfo >::iterator it = d_qinfo.find( f );
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index e44b604d0..7324add50 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -133,7 +133,18 @@ void SygusEvalUnfold::registerModelValue(Node a,
         bool do_unfold = false;
         if (options::sygusEvalUnfoldBool())
         {
-          if (bTerm.getKind() == ITE || bTerm.getType().isBoolean())
+          Node bTermUse = bTerm;
+          if (bTerm.getKind() == APPLY_UF)
+          {
+            // if the builtin term is non-beta-reduced application of lambda,
+            // we look at the body of the lambda.
+            Node bTermOp = bTerm.getOperator();
+            if (bTermOp.getKind() == LAMBDA)
+            {
+              bTermUse = bTermOp[0];
+            }
+          }
+          if (bTermUse.getKind() == ITE || bTermUse.getType().isBoolean())
           {
             do_unfold = true;
           }
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 48da8e8e8..263c88d15 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -712,7 +712,14 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       for (unsigned k = 0, size_k = dt.getNumConstructors(); k < size_k; ++k)
       {
         Trace("sygus-grammar-def") << "...for " << dt[k].getName() << std::endl;
-        ops[i].push_back( dt[k].getConstructor() );
+        Expr cop = dt[k].getConstructor();
+        if (dt[k].getNumArgs() == 0)
+        {
+          // Nullary constructors are interpreted as terms, not operators.
+          // Thus, we apply them to no arguments here.
+          cop = nm->mkNode(APPLY_CONSTRUCTOR, Node::fromExpr(cop)).toExpr();
+        }
+        ops[i].push_back(cop);
         cnames[i].push_back(dt[k].getName());
         cargs[i].push_back(std::vector<Type>());
         Trace("sygus-grammar-def") << "...add for selectors" << std::endl;
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
index 6ad590f28..2b2c87f38 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_red.cpp
@@ -43,7 +43,6 @@ void SygusRedundantCons::initialize(QuantifiersEngine* qe, TypeNode tn)
     std::map<int, Node> pre;
     Node g = tds->mkGeneric(dt, i, pre);
     Trace("sygus-red-debug") << "  ...pre-rewrite : " << g << std::endl;
-    Assert(g.getNumChildren() == dt[i].getNumArgs());
     d_gen_terms[i] = g;
     for (unsigned j = 0, nargs = dt[i].getNumArgs(); j < nargs; j++)
     {
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index af820b0fc..01d08dad8 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -411,6 +411,11 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
             Trace("sygus-db") << ", kind = " << sk;
             d_kinds[tn][sk] = i;
             d_arg_kind[tn][i] = sk;
+            if (sk == ITE)
+            {
+              // mark that this type has an ITE
+              d_hasIte[tn] = true;
+            }
           }
           else if (sop.isConst() && dt[i].getNumArgs() == 0)
           {
@@ -432,6 +437,11 @@ void TermDbSygus::registerSygusType( TypeNode tn ) {
                   << ", argument to a lambda constructor is not " << lat
                   << std::endl;
             }
+            if (sop[0].getKind() == ITE)
+            {
+              // mark that this type has an ITE
+              d_hasIte[tn] = true;
+            }
           }
           // symbolic constructors
           if (n.getAttribute(SygusAnyConstAttribute()))
@@ -602,7 +612,7 @@ void TermDbSygus::registerEnumerator(Node e,
         // solution" clauses.
         const Datatype& dt = et.getDatatype();
         if (options::sygusStream()
-            || (!hasKind(et, ITE) && !dt.getSygusType().isBoolean()))
+            || (!hasIte(et) && !dt.getSygusType().isBoolean()))
         {
           isActiveGen = true;
         }
@@ -1003,6 +1013,10 @@ int TermDbSygus::getOpConsNum( TypeNode tn, Node n ) {
 bool TermDbSygus::hasKind( TypeNode tn, Kind k ) {
   return getKindConsNum( tn, k )!=-1;
 }
+bool TermDbSygus::hasIte(TypeNode tn) const
+{
+  return d_hasIte.find(tn) != d_hasIte.end();
+}
 bool TermDbSygus::hasConst( TypeNode tn, Node n ) {
   return getConstConsNum( tn, n )!=-1;
 }
@@ -1502,14 +1516,9 @@ Node TermDbSygus::unfold( Node en, std::map< Node, Node >& vtm, std::vector< Nod
     pre[j] = nm->mkNode(DT_SYGUS_EVAL, cc);
   }
   Node ret = mkGeneric(dt, i, pre);
-  // if it is a variable, apply the substitution
-  if (ret.getKind() == kind::BOUND_VARIABLE)
-  {
-    Assert(ret.hasAttribute(SygusVarNumAttribute()));
-    int i = ret.getAttribute(SygusVarNumAttribute());
-    Assert(Node::fromExpr(dt.getSygusVarList())[i] == ret);
-    return args[i];
-  }
+  // apply the appropriate substitution to ret
+  ret = datatypes::DatatypesRewriter::applySygusArgs(dt, sop, ret, args);
+  // rewrite
   ret = Rewriter::rewrite(ret);
   return ret;
 }
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 0f3d650d3..2854ecab6 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -393,6 +393,11 @@ class TermDbSygus {
   std::map<TypeNode, std::vector<Node> > d_var_list;
   std::map<TypeNode, std::map<int, Kind> > d_arg_kind;
   std::map<TypeNode, std::map<Kind, int> > d_kinds;
+  /**
+   * Whether this sygus type has a constructors whose sygus operator is ITE,
+   * or is a lambda whose body is ITE.
+   */
+  std::map<TypeNode, bool> d_hasIte;
   std::map<TypeNode, std::map<int, Node> > d_arg_const;
   std::map<TypeNode, std::map<Node, int> > d_consts;
   std::map<TypeNode, std::map<Node, int> > d_ops;
@@ -462,6 +467,11 @@ class TermDbSygus {
   int getConstConsNum( TypeNode tn, Node n );
   int getOpConsNum( TypeNode tn, Node n );
   bool hasKind( TypeNode tn, Kind k );
+  /**
+   * Returns true if this sygus type has a constructors whose sygus operator is
+   * ITE, or is a lambda whose body is ITE.
+   */
+  bool hasIte(TypeNode tn) const;
   bool hasConst( TypeNode tn, Node n );
   bool hasOp( TypeNode tn, Node n );
   Node getConsNumConst( TypeNode tn, int i );
diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index 91beb1ab5..0360228c6 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -20,6 +20,9 @@
 #include "options/strings_options.h"
 #include "theory/strings/theory_strings_rewriter.h"
 
+using namespace CVC4;
+using namespace CVC4::kind;
+
 namespace CVC4 {
 namespace theory {
 namespace strings {
@@ -808,39 +811,72 @@ void RegExpOpr::simplifyNRegExp( Node s, Node r, std::vector< Node > &new_nodes
         break;
       }
       case kind::REGEXP_CONCAT: {
-        //TODO: rewrite empty
-        Node lens = NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s);
-        Node b1 = NodeManager::currentNM()->mkBoundVar(NodeManager::currentNM()->integerType());
-        Node b1v = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, b1);
-        Node g1 = NodeManager::currentNM()->mkNode( kind::AND, NodeManager::currentNM()->mkNode(kind::GEQ, b1, d_zero),
-              NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode(kind::STRING_LENGTH, s), b1 ) );
-        Node s1 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, d_zero, b1));
-        Node s2 = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::STRING_SUBSTR, s, b1, NodeManager::currentNM()->mkNode(kind::MINUS, lens, b1)));
-        Node s1r1 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s1, r[0]).negate();
-        if(r[0].getKind() == kind::STRING_TO_REGEXP) {
-          s1r1 = s1.eqNode(r[0][0]).negate();
-        } else if(r[0].getKind() == kind::REGEXP_EMPTY) {
-          s1r1 = d_true;
+        // The following simplification states that
+        //    ~( s in R1 ++ R2 )
+        // is equivalent to
+        //    forall x.
+        //      0 <= x <= len(s) =>
+        //        ~( substr(s,0,x) in R1 ) OR ~( substr(s,x,len(s)-x) in R2)
+        Node lens = nm->mkNode(STRING_LENGTH, s);
+        // the index we are removing from the RE concatenation
+        unsigned indexRm = 0;
+        Node b1;
+        Node b1v;
+        // As an optimization to the above reduction, if we can determine that
+        // all strings in the language of R1 have the same length, say n,
+        // then the conclusion of the reduction is quantifier-free:
+        //    ~( substr(s,0,n) in R1 ) OR ~( substr(s,n,len(s)-n) in R2)
+        Node reLength = TheoryStringsRewriter::getFixedLengthForRegexp(r[0]);
+        if (reLength.isNull())
+        {
+          // try from the opposite end
+          unsigned indexE = r.getNumChildren() - 1;
+          reLength = TheoryStringsRewriter::getFixedLengthForRegexp(r[indexE]);
+          if (!reLength.isNull())
+          {
+            indexRm = indexE;
+          }
+        }
+        Node guard;
+        if (reLength.isNull())
+        {
+          b1 = nm->mkBoundVar(nm->integerType());
+          b1v = nm->mkNode(BOUND_VAR_LIST, b1);
+          guard = nm->mkNode(AND,
+                             nm->mkNode(GEQ, b1, d_zero),
+                             nm->mkNode(GEQ, nm->mkNode(STRING_LENGTH, s), b1));
+        }
+        else
+        {
+          b1 = reLength;
+        }
+        Node s1 = nm->mkNode(STRING_SUBSTR, s, d_zero, b1);
+        Node s2 = nm->mkNode(STRING_SUBSTR, s, b1, nm->mkNode(MINUS, lens, b1));
+        if (indexRm != 0)
+        {
+          // swap if we are removing from the end
+          Node sswap = s1;
+          s1 = s2;
+          s2 = sswap;
         }
-        Node r2 = r[1];
-        if(r.getNumChildren() > 2) {
-          std::vector< Node > nvec;
-          for(unsigned i=1; i<r.getNumChildren(); i++) {
+        Node s1r1 = nm->mkNode(STRING_IN_REGEXP, s1, r[indexRm]).negate();
+        std::vector<Node> nvec;
+        for (unsigned i = 0, nchild = r.getNumChildren(); i < nchild; i++)
+        {
+          if (i != indexRm)
+          {
             nvec.push_back( r[i] );
           }
-          r2 = NodeManager::currentNM()->mkNode(kind::REGEXP_CONCAT, nvec);
         }
+        Node r2 = nvec.size() == 1 ? nvec[0] : nm->mkNode(REGEXP_CONCAT, nvec);
         r2 = Rewriter::rewrite(r2);
-        Node s2r2 = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, s2, r2).negate();
-        if(r2.getKind() == kind::STRING_TO_REGEXP) {
-          s2r2 = s2.eqNode(r2[0]).negate();
-        } else if(r2.getKind() == kind::REGEXP_EMPTY) {
-          s2r2 = d_true;
+        Node s2r2 = nm->mkNode(STRING_IN_REGEXP, s2, r2).negate();
+        conc = nm->mkNode(OR, s1r1, s2r2);
+        if (!b1v.isNull())
+        {
+          conc = nm->mkNode(OR, guard.negate(), conc);
+          conc = nm->mkNode(FORALL, b1v, conc);
         }
-
-        conc = NodeManager::currentNM()->mkNode(kind::OR, s1r1, s2r2);
-        conc = NodeManager::currentNM()->mkNode(kind::IMPLIES, g1, conc);
-        conc = NodeManager::currentNM()->mkNode(kind::FORALL, b1v, conc);
         break;
       }
       case kind::REGEXP_UNION: {
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index c7f7c5c99..0883eebfa 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -4475,19 +4475,29 @@ void TheoryStrings::checkNormalFormsDeq()
         for( unsigned j=0; j<cols[i].size(); j++ ){
           for( unsigned k=(j+1); k<cols[i].size(); k++ ){
             //for strings that are disequal, but have the same length
-            if( areDisequal( cols[i][j], cols[i][k] ) ){
-              Assert( !d_conflict );
-              if (Trace.isOn("strings-solve"))
+            if (cols[i][j].isConst() && cols[i][k].isConst())
+            {
+              // if both are constants, they should be distinct, and its trivial
+              Assert(cols[i][j] != cols[i][k]);
+            }
+            else
+            {
+              if (areDisequal(cols[i][j], cols[i][k]))
               {
-                Trace("strings-solve") << "- Compare " << cols[i][j] << " ";
-                printConcat(getNormalForm(cols[i][j]).d_nf, "strings-solve");
-                Trace("strings-solve") << " against " << cols[i][k] << " ";
-                printConcat(getNormalForm(cols[i][k]).d_nf, "strings-solve");
-                Trace("strings-solve") << "..." << std::endl;
-              }
-              processDeq( cols[i][j], cols[i][k] );
-              if( hasProcessed() ){
-                return;
+                Assert(!d_conflict);
+                if (Trace.isOn("strings-solve"))
+                {
+                  Trace("strings-solve") << "- Compare " << cols[i][j] << " ";
+                  printConcat(getNormalForm(cols[i][j]).d_nf, "strings-solve");
+                  Trace("strings-solve") << " against " << cols[i][k] << " ";
+                  printConcat(getNormalForm(cols[i][k]).d_nf, "strings-solve");
+                  Trace("strings-solve") << "..." << std::endl;
+                }
+                processDeq(cols[i][j], cols[i][k]);
+                if (hasProcessed())
+                {
+                  return;
+                }
               }
             }
           }