From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 8 Mar 2022 22:38:20 +0000 (-0600)
Subject: Do not expand APPLY_SELECTOR (#8174)
X-Git-Tag: cvc5-1.0.0~299
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4da209c2260060501104568bde0d7539d80e9027;p=cvc5.git

Do not expand APPLY_SELECTOR (#8174)

Currently we expand (sel_C_n x) to (ite (is-C x) (sel_C_n_total x) (uf x)) during ppRewrite. This introduces ITEs very eagerly and moreover is not necessary since we do congruence over selectors.

This makes it so that we don't do this expansion. The code changes to use APPLY_SELECTOR everywhere instead of APPLY_SELECTOR_TOTAL, which can be deleted in a followup PR. It makes some of the datatype utilities more robust and independent of options.

This required changing one detail of the sygus solver to not do evaluation unfolding in cases where a selector chain was wrongly applied, as this now will not rewrite to a constant.
---

diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index a054dffb8..269f3ebca 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -260,26 +260,25 @@ Node DTypeConstructor::getSelectorInternal(TypeNode domainType,
 int DTypeConstructor::getSelectorIndexInternal(Node sel) const
 {
   Assert(isResolved());
-  if (options::dtSharedSelectors())
+  Assert(sel.getType().isSelector());
+  // might be a builtin selector
+  if (sel.hasAttribute(DTypeIndexAttr()))
   {
-    Assert(sel.getType().isSelector());
-    TypeNode domainType = sel.getType().getSelectorDomainType();
-    computeSharedSelectors(domainType);
-    std::map<Node, unsigned>::iterator its =
-        d_sharedSelectorIndex[domainType].find(sel);
-    if (its != d_sharedSelectorIndex[domainType].end())
-    {
-      return (int)its->second;
-    }
-  }
-  else
-  {
-    unsigned sindex = DType::indexOf(sel);
+    size_t sindex = DType::indexOf(sel);
     if (getNumArgs() > sindex && d_args[sindex]->getSelector() == sel)
     {
       return static_cast<int>(sindex);
     }
   }
+  // otherwise, check shared selector
+  TypeNode domainType = sel.getType().getSelectorDomainType();
+  computeSharedSelectors(domainType);
+  std::map<Node, unsigned>::iterator its =
+      d_sharedSelectorIndex[domainType].find(sel);
+  if (its != d_sharedSelectorIndex[domainType].end())
+  {
+    return (int)its->second;
+  }
   return -1;
 }
 
diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 12acc1402..a88421c7a 100644
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -395,29 +395,9 @@ RewriteResponse DatatypesRewriter::rewriteSelector(TNode in)
                                      << std::endl;
     // The argument that the selector extracts, or -1 if the selector is
     // is wrongly applied.
-    int selectorIndex = -1;
-    if (k == kind::APPLY_SELECTOR_TOTAL)
-    {
-      // The argument index of internal selectors is obtained by
-      // getSelectorIndexInternal.
-      selectorIndex = c.getSelectorIndexInternal(selector);
-    }
-    else
-    {
-      // The argument index of external selectors (applications of
-      // APPLY_SELECTOR) is given by an attribute and obtained via indexOf below
-      // The argument is only valid if it is the proper constructor.
-      selectorIndex = utils::indexOf(selector);
-      if (selectorIndex < 0
-          || selectorIndex >= static_cast<int>(c.getNumArgs()))
-      {
-        selectorIndex = -1;
-      }
-      else if (c[selectorIndex].getSelector() != selector)
-      {
-        selectorIndex = -1;
-      }
-    }
+    // The argument index of internal selectors is obtained by
+    // getSelectorIndexInternal.
+    int selectorIndex = c.getSelectorIndexInternal(selector);
     Trace("datatypes-rewrite-debug") << "Internal selector index is "
                                      << selectorIndex << std::endl;
     if (selectorIndex >= 0)
@@ -840,39 +820,24 @@ Node DatatypesRewriter::expandApplySelector(Node n)
 {
   Assert(n.getKind() == APPLY_SELECTOR);
   Node selector = n.getOperator();
+  if (!options::dtSharedSelectors()
+      || !selector.hasAttribute(DTypeConsIndexAttr()))
+  {
+    return n;
+  }
   // APPLY_SELECTOR always applies to an external selector, cindexOf is
   // legal here
   size_t cindex = utils::cindexOf(selector);
   const DType& dt = utils::datatypeOf(selector);
   const DTypeConstructor& c = dt[cindex];
-  Node selector_use;
   TypeNode ndt = n[0].getType();
-  if (options::dtSharedSelectors())
-  {
-    size_t selectorIndex = utils::indexOf(selector);
-    Trace("dt-expand") << "...selector index = " << selectorIndex << std::endl;
-    Assert(selectorIndex < c.getNumArgs());
-    selector_use = c.getSelectorInternal(ndt, selectorIndex);
-  }
-  else
-  {
-    selector_use = selector;
-  }
+  size_t selectorIndex = utils::indexOf(selector);
+  Trace("dt-expand") << "...selector index = " << selectorIndex << std::endl;
+  Assert(selectorIndex < c.getNumArgs());
+  Node selector_use = c.getSelectorInternal(ndt, selectorIndex);
   NodeManager* nm = NodeManager::currentNM();
-  Node sel = nm->mkNode(kind::APPLY_SELECTOR_TOTAL, selector_use, n[0]);
-  if (options::dtRewriteErrorSel())
-  {
-    return sel;
-  }
-  Node tester = c.getTester();
-  Node tst = nm->mkNode(APPLY_TESTER, tester, n[0]);
-  SkolemManager* sm = nm->getSkolemManager();
-  TypeNode tnw = nm->mkFunctionType(ndt, n.getType());
-  Node f = sm->mkSkolemFunction(SkolemFunId::SELECTOR_WRONG, tnw, selector);
-  Node sk = nm->mkNode(kind::APPLY_UF, f, n[0]);
-  Node ret = nm->mkNode(kind::ITE, tst, sel, sk);
-  Trace("dt-expand") << "Expand def : " << n << " to " << ret << std::endl;
-  return ret;
+  Node sel = nm->mkNode(kind::APPLY_SELECTOR, selector_use, n[0]);
+  return sel;
 }
 
 TrustNode DatatypesRewriter::expandDefinition(Node n)
@@ -916,8 +881,7 @@ TrustNode DatatypesRewriter::expandDefinition(Node n)
         }
         else
         {
-          b << nm->mkNode(
-              APPLY_SELECTOR_TOTAL, dc.getSelectorInternal(tn, i), n[0]);
+          b << nm->mkNode(APPLY_SELECTOR, dc.getSelectorInternal(tn, i), n[0]);
         }
       }
       ret = b;
diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 86ff493ea..5139d81b8 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -64,11 +64,12 @@ class DatatypesRewriter : public TheoryRewriter
    * Expand an APPLY_SELECTOR term n, return its expanded form. If n is
    *   (APPLY_SELECTOR selC x)
    * its expanded form is
-   *   (ITE (APPLY_TESTER is-C x)
-   *     (APPLY_SELECTOR_TOTAL selC' x)
-   *     (f x))
+   *   (APPLY_SELECTOR selC' x)
    * where f is a skolem function with id SELECTOR_WRONG, and selC' is the
    * internal selector function for selC (possibly a shared selector).
+   * Note that we do not introduce an uninterpreted function here, e.g. to
+   * handle when the selector is misapplied. This is because it suffices to
+   * reason about the original selector term e.g. via congruence.
    */
   static Node expandApplySelector(Node n);
   /**
diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index e49d58f91..86386ab78 100644
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -169,7 +169,7 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
         Node concAtom = concPol ? conc : conc[0];
         concEq = concAtom.eqNode(nm->mkConst(concPol));
       }
-      if (concEq[0].getKind() != APPLY_SELECTOR_TOTAL)
+      if (concEq[0].getKind() != APPLY_SELECTOR)
       {
         // can happen for Boolean term variables, which are not currently
         // supported.
@@ -179,14 +179,14 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
       {
         Assert(exp[0].getType().isDatatype());
         Node sop = concEq[0].getOperator();
-        Node sl = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[0]);
-        Node sr = nm->mkNode(APPLY_SELECTOR_TOTAL, sop, exp[1]);
+        Node sl = nm->mkNode(APPLY_SELECTOR, sop, exp[0]);
+        Node sr = nm->mkNode(APPLY_SELECTOR, sop, exp[1]);
         // exp[0] = exp[1]
         // --------------------- CONG        ----------------- DT_COLLAPSE
         // s(exp[0]) = s(exp[1])             s(exp[1]) = r
         // --------------------------------------------------- TRANS
         // s(exp[0]) = r
-        Node asn = ProofRuleChecker::mkKindNode(APPLY_SELECTOR_TOTAL);
+        Node asn = ProofRuleChecker::mkKindNode(APPLY_SELECTOR);
         Node seq = sl.eqNode(sr);
         cdp->addStep(seq, PfRule::CONG, {exp}, {asn, sop});
         Node sceq = sr.eqNode(concEq[1]);
diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp
index 69153ef00..938441151 100644
--- a/src/theory/datatypes/proof_checker.cpp
+++ b/src/theory/datatypes/proof_checker.cpp
@@ -82,7 +82,7 @@ Node DatatypesProofRuleChecker::checkInternal(PfRule id,
     Assert(children.empty());
     Assert(args.size() == 1);
     Node t = args[0];
-    if (t.getKind() != kind::APPLY_SELECTOR_TOTAL
+    if (t.getKind() != kind::APPLY_SELECTOR
         || t[0].getKind() != kind::APPLY_CONSTRUCTOR)
     {
       return Node::null();
diff --git a/src/theory/datatypes/sygus_extension.cpp b/src/theory/datatypes/sygus_extension.cpp
index 03c1fe9e0..d46e6e28d 100644
--- a/src/theory/datatypes/sygus_extension.cpp
+++ b/src/theory/datatypes/sygus_extension.cpp
@@ -81,7 +81,8 @@ void SygusExtension::assertTester(int tindex, TNode n, Node exp)
       bool do_add = true;
       if (options().datatypes.sygusSymBreakLazy)
       {
-        if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){
+        if (n.getKind() == kind::APPLY_SELECTOR)
+        {
           NodeSet::const_iterator it = d_active_terms.find( n[0] );
           if( it==d_active_terms.end() ){
             do_add = false;
@@ -158,7 +159,8 @@ void SygusExtension::registerTerm(Node n)
     unsigned d = 0;
     bool is_top_level = false;
     bool success = false;
-    if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){
+    if (n.getKind() == kind::APPLY_SELECTOR)
+    {
       registerTerm(n[0]);
       std::unordered_map<Node, Node>::iterator it = d_term_to_anchor.find(n[0]);
       if( it!=d_term_to_anchor.end() ) {
@@ -169,7 +171,9 @@ void SygusExtension::registerTerm(Node n)
         is_top_level = computeTopLevel( tn, n[0] );
         success = true;
       }
-    }else if( n.isVar() ){
+    }
+    else if (n.isVar())
+    {
       registerSizeTerm(n);
       if( d_register_st[n] ){
         d_term_to_anchor[n] = n;
@@ -197,9 +201,13 @@ void SygusExtension::registerTerm(Node n)
 bool SygusExtension::computeTopLevel( TypeNode tn, Node n ){
   if( n.getType()==tn ){
     return false;
-  }else if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){
+  }
+  else if (n.getKind() == kind::APPLY_SELECTOR)
+  {
     return computeTopLevel( tn, n[0] );
-  }else{
+  }
+  else
+  {
     return true;
   }
 }
@@ -367,8 +375,8 @@ void SygusExtension::assertTesterInternal(int tindex, TNode n, Node exp)
   {
     Trace("sygus-sb-debug") << "Do lazy symmetry breaking...\n";
     for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
-      Node sel = nm->mkNode(
-          APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(ntn, j), n);
+      Node sel =
+          nm->mkNode(APPLY_SELECTOR, dt[tindex].getSelectorInternal(ntn, j), n);
       Trace("sygus-sb-debug2") << "  activate child sel : " << sel << std::endl;
       Assert(d_active_terms.find(sel) == d_active_terms.end());
       IntMap::const_iterator itt = d_testers.find( sel );
@@ -389,7 +397,7 @@ Node SygusExtension::getRelevancyCondition( Node n ) {
   std::map< Node, Node >::iterator itr = d_rlv_cond.find( n );
   if( itr==d_rlv_cond.end() ){
     Node cond;
-    if (n.getKind() == APPLY_SELECTOR_TOTAL)
+    if (n.getKind() == APPLY_SELECTOR)
     {
       TypeNode ntn = n[0].getType();
       const DType& dt = ntn.getDType();
@@ -476,7 +484,7 @@ Node SygusExtension::eliminateTraversalPredicates(Node n)
       {
         Assert(cur.getType().isBoolean());
         Assert(cur.getNumChildren() == 1
-               && (cur[0].isVar() || cur[0].getKind() == APPLY_SELECTOR_TOTAL));
+               && (cur[0].isVar() || cur[0].getKind() == APPLY_SELECTOR));
         ittb = d_traversal_bool.find(cur);
         Node ret;
         if (ittb == d_traversal_bool.end())
@@ -593,8 +601,8 @@ Node SygusExtension::getSimpleSymBreakPred(Node e,
   std::vector<Node> children;
   for (unsigned j = 0; j < dt_index_nargs; j++)
   {
-    Node sel = nm->mkNode(
-        APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(tn, j), n);
+    Node sel =
+        nm->mkNode(APPLY_SELECTOR, dt[tindex].getSelectorInternal(tn, j), n);
     Assert(sel.getType().isDatatype());
     children.push_back(sel);
   }
@@ -919,9 +927,8 @@ Node SygusExtension::getSimpleSymBreakPred(Node e,
           && children[0].getType() == tn && children[1].getType() == tn)
       {
         // chainable
-        Node child11 = nm->mkNode(APPLY_SELECTOR_TOTAL,
-                                  dt[tindex].getSelectorInternal(tn, 1),
-                                  children[0]);
+        Node child11 = nm->mkNode(
+            APPLY_SELECTOR, dt[tindex].getSelectorInternal(tn, 1), children[0]);
         Assert(child11.getType() == children[1].getType());
         Node order_pred_trans =
             nm->mkNode(OR,
@@ -1007,8 +1014,8 @@ Node SygusExtension::registerSearchValue(Node a,
     bool childrenChanged = false;
     for (unsigned i = 0, nchild = nv.getNumChildren(); i < nchild; i++)
     {
-      Node sel = nm->mkNode(
-          APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), n);
+      Node sel =
+          nm->mkNode(APPLY_SELECTOR, dt[cindex].getSelectorInternal(tn, i), n);
       Node nvc = registerSearchValue(a,
                                      sel,
                                      nv[i],
@@ -1726,8 +1733,8 @@ bool SygusExtension::checkValue(Node n, TNode vn, int ind)
     }
   }
   for( unsigned i=0; i<vn.getNumChildren(); i++ ){
-    Node sel = nm->mkNode(
-        APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), n);
+    Node sel =
+        nm->mkNode(APPLY_SELECTOR, dt[cindex].getSelectorInternal(tn, i), n);
     if (!checkValue(sel, vn[i], ind + 1))
     {
       return false;
@@ -1749,7 +1756,7 @@ Node SygusExtension::getCurrentTemplate( Node n, std::map< TypeNode, int >& var_
     children.push_back(dt[tindex].getConstructor());
     for( unsigned i=0; i<dt[tindex].getNumArgs(); i++ ){
       Node sel = NodeManager::currentNM()->mkNode(
-          APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(tn, i), n);
+          APPLY_SELECTOR, dt[tindex].getSelectorInternal(tn, i), n);
       Node cc = getCurrentTemplate( sel, var_count );
       children.push_back( cc );
     }
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 555b35a36..74228167a 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -104,7 +104,7 @@ void TheoryDatatypes::finishInit()
   Assert(d_equalityEngine != nullptr);
   // The kinds we are treating as function application in congruence
   d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
-  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
+  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR);
   d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
   // We could but don't do congruence for DT_SIZE and DT_HEIGHT_BOUND here.
   // It also could make sense in practice to do congruence for APPLY_UF, but
@@ -445,8 +445,8 @@ void TheoryDatatypes::preRegisterTerm(TNode n)
 {
   Trace("datatypes-prereg")
       << "TheoryDatatypes::preRegisterTerm() " << n << endl;
-  // external selectors should be preprocessed away by now
-  Assert(n.getKind() != APPLY_SELECTOR);
+  // should not use APPLY_SELECTOR_TOTAL
+  Assert(n.getKind() != APPLY_SELECTOR_TOTAL);
   // must ensure the type is well founded and has no nested recursion if
   // the option dtNestedRec is not set to true.
   TypeNode tn = n.getType();
@@ -992,30 +992,26 @@ void TheoryDatatypes::collapseSelector( Node s, Node c ) {
   Node r;
   bool wrong = false;
   Node eq_exp = s[0].eqNode(c);
-  if( s.getKind()==kind::APPLY_SELECTOR_TOTAL ){
+  if (s.getKind() == kind::APPLY_SELECTOR)
+  {
     Node selector = s.getOperator();
     size_t constructorIndex = utils::indexOf(c.getOperator());
     const DType& dt = utils::datatypeOf(selector);
     const DTypeConstructor& dtc = dt[constructorIndex];
     int selectorIndex = dtc.getSelectorIndexInternal(selector);
+    Trace("dt-collapse-sel")
+        << "selector index is " << selectorIndex << std::endl;
     wrong = selectorIndex<0;
-    r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
+    r = NodeManager::currentNM()->mkNode(
+        kind::APPLY_SELECTOR, s.getOperator(), c);
   }
   if( !r.isNull() ){
     Node rrs;
     if (wrong)
     {
-      // Must use make ground term here instead of the rewriter, since we
-      // do not want to introduce arbitrary values. This is important so that
-      // we avoid constants for types that are not "closed enumerable", e.g.
-      // uninterpreted sorts and arrays, where the solver does not fully
-      // handle values of the sort. The call to mkGroundTerm does not introduce
-      // values for these sorts.
-      NodeManager* nm = NodeManager::currentNM();
-      rrs = nm->mkGroundTerm(r.getType());
-      Trace("datatypes-wrong-sel")
-          << "Bad apply " << r << " term = " << rrs
-          << ", value = " << nm->mkGroundValue(r.getType()) << std::endl;
+      // If the selector application was wrong, we do nothing. The selector
+      // term in this context will be unevaluated, and treated via congruence.
+      return;
     }
     else
     {
@@ -1387,7 +1383,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
     }
     return;
   }
-  if (nk == APPLY_SELECTOR_TOTAL || nk == DT_SIZE || nk == DT_HEIGHT_BOUND)
+  if (nk == APPLY_SELECTOR || nk == DT_SIZE || nk == DT_HEIGHT_BOUND)
   {
     d_functionTerms.push_back(n);
     // we must also record which selectors exist
diff --git a/src/theory/datatypes/theory_datatypes_utils.cpp b/src/theory/datatypes/theory_datatypes_utils.cpp
index a429f8333..d69ec9cd5 100644
--- a/src/theory/datatypes/theory_datatypes_utils.cpp
+++ b/src/theory/datatypes/theory_datatypes_utils.cpp
@@ -36,8 +36,8 @@ Node getInstCons(Node n, const DType& dt, size_t index)
   TypeNode tn = n.getType();
   for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++)
   {
-    Node nc = nm->mkNode(
-        APPLY_SELECTOR_TOTAL, dt[index].getSelectorInternal(tn, i), n);
+    Node nc =
+        nm->mkNode(APPLY_SELECTOR, dt[index].getSelectorInternal(tn, i), n);
     children.push_back(nc);
   }
   Node n_ic = mkApplyCons(tn, dt, index, children);
@@ -77,7 +77,7 @@ int isInstCons(Node t, Node n, const DType& dt)
     TypeNode tn = n.getType();
     for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
     {
-      if (n[i].getKind() != APPLY_SELECTOR_TOTAL
+      if (n[i].getKind() != APPLY_SELECTOR
           || n[i].getOperator() != c.getSelectorInternal(tn, i) || n[i][0] != t)
       {
         return -1;
diff --git a/src/theory/datatypes/tuple_utils.cpp b/src/theory/datatypes/tuple_utils.cpp
index d691b3831..0a852c01e 100644
--- a/src/theory/datatypes/tuple_utils.cpp
+++ b/src/theory/datatypes/tuple_utils.cpp
@@ -33,7 +33,7 @@ Node TupleUtils::nthElementOfTuple(Node tuple, int n_th)
   TypeNode tn = tuple.getType();
   const DType& dt = tn.getDType();
   return NodeManager::currentNM()->mkNode(
-      APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(tn, n_th), tuple);
+      APPLY_SELECTOR, dt[0].getSelectorInternal(tn, n_th), tuple);
 }
 
 std::vector<Node> TupleUtils::getTupleElements(Node tuple)
diff --git a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
index b5ce012b7..0d8da809e 100644
--- a/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp
@@ -66,9 +66,8 @@ bool DtInstantiator::processEqualTerms(CegInstantiator* ci,
       // now must solve for selectors applied to pv
       for (unsigned j = 0, nargs = dt[cindex].getNumArgs(); j < nargs; j++)
       {
-        Node c = nm->mkNode(APPLY_SELECTOR_TOTAL,
-                            dt[cindex].getSelectorInternal(d_type, j),
-                            pv);
+        Node c = nm->mkNode(
+            APPLY_SELECTOR, dt[cindex].getSelectorInternal(d_type, j), pv);
         ci->pushStackVariable(c);
         children.push_back(c);
       }
@@ -154,7 +153,7 @@ Node DtInstantiator::solve_dt(Node v, Node a, Node b, Node sa, Node sb)
       for (unsigned i = 0, nchild = a.getNumChildren(); i < nchild; i++)
       {
         Node nn = nm->mkNode(
-            APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), sb);
+            APPLY_SELECTOR, dt[cindex].getSelectorInternal(tn, i), sb);
         Node s = solve_dt(v, a[i], Node::null(), sa[i], nn);
         if (!s.isNull())
         {
diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 414ff2e3b..8d1f9f007 100644
--- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
@@ -232,7 +232,7 @@ void CegInstantiator::computeProgVars( Node n ){
       d_prog_var[n].insert(d_prog_var[n[i]].begin(), d_prog_var[n[i]].end());
     }
     // selectors applied to program variables are also variables
-    if (n.getKind() == APPLY_SELECTOR_TOTAL
+    if (n.getKind() == APPLY_SELECTOR
         && d_prog_var[n].find(n[0]) != d_prog_var[n].end())
     {
       d_prog_var[n].insert(n);
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index db62da53b..7f2ddd35d 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -1844,7 +1844,9 @@ void TermGenEnv::collectSignatureInformation() {
     {
       Node nn = dbl->d_list[0];
       Trace("sg-rel-sig-debug") << "Check in signature : " << nn << std::endl;
-      if( d_cg->isHandledTerm( nn ) && nn.getKind()!=APPLY_SELECTOR_TOTAL && !nn.getType().isBoolean() ){
+      if (d_cg->isHandledTerm(nn) && nn.getKind() != APPLY_SELECTOR
+          && !nn.getType().isBoolean())
+      {
         bool do_enum = true;
         //check if we have enumerated ground terms
         if( nn.getKind()==APPLY_UF ){
diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp
index 57752d375..f32655eb2 100644
--- a/src/theory/quantifiers/ematching/candidate_generator.cpp
+++ b/src/theory/quantifiers/ematching/candidate_generator.cpp
@@ -291,7 +291,7 @@ Node CandidateGeneratorConsExpand::getNextCandidate()
   for (unsigned i = 0, nargs = dt[0].getNumArgs(); i < nargs; i++)
   {
     Node sel = nm->mkNode(
-        APPLY_SELECTOR_TOTAL, dt[0].getSelectorInternal(d_mpat_type, i), curr);
+        APPLY_SELECTOR, dt[0].getSelectorInternal(d_mpat_type, i), curr);
     children.push_back(sel);
   }
   return nm->mkNode(APPLY_CONSTRUCTOR, children);
@@ -316,12 +316,12 @@ CandidateGeneratorSelector::CandidateGeneratorSelector(QuantifiersState& qs,
   Trace("sel-trigger") << "Expands to: " << mpatExp << std::endl;
   if (mpatExp.getKind() == ITE)
   {
-    Assert(mpatExp[1].getKind() == APPLY_SELECTOR_TOTAL);
+    Assert(mpatExp[1].getKind() == APPLY_SELECTOR);
     Assert(mpatExp[2].getKind() == APPLY_UF);
     d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[1]);
     d_ufOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp[2]);
   }
-  else if (mpatExp.getKind() == APPLY_SELECTOR_TOTAL)
+  else if (mpatExp.getKind() == APPLY_SELECTOR)
   {
     // corner case of datatype with one constructor
     d_selOp = d_treg.getTermDatabase()->getMatchOperator(mpatExp);
diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp
index 8392cd493..516c9803c 100644
--- a/src/theory/quantifiers/ematching/inst_match_generator.cpp
+++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp
@@ -245,7 +245,7 @@ void InstMatchGenerator::initialize(Node q,
   }
   else if (mpk == INST_CONSTANT)
   {
-    if (d_pattern.getKind() == APPLY_SELECTOR_TOTAL)
+    if (d_pattern.getKind() == APPLY_SELECTOR)
     {
       Node selectorExpr = tdb->getMatchOperator(d_pattern);
       size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr);
diff --git a/src/theory/quantifiers/ematching/trigger_term_info.cpp b/src/theory/quantifiers/ematching/trigger_term_info.cpp
index 611f30ef0..0ba980d59 100644
--- a/src/theory/quantifiers/ematching/trigger_term_info.cpp
+++ b/src/theory/quantifiers/ematching/trigger_term_info.cpp
@@ -49,16 +49,12 @@ bool TriggerTermInfo::isAtomicTrigger(Node n)
 
 bool TriggerTermInfo::isAtomicTriggerKind(Kind k)
 {
-  // we use both APPLY_SELECTOR and APPLY_SELECTOR_TOTAL since this
-  // method is used both for trigger selection and for ground term registration,
-  // where these two things require those kinds respectively.
   return k == APPLY_UF || k == SELECT || k == STORE || k == APPLY_CONSTRUCTOR
-         || k == APPLY_SELECTOR || k == APPLY_SELECTOR_TOTAL
-         || k == APPLY_TESTER || k == SET_UNION || k == SET_INTER
-         || k == SET_SUBSET || k == SET_MINUS || k == SET_MEMBER
-         || k == SET_SINGLETON || k == SEP_PTO || k == BITVECTOR_TO_NAT
-         || k == INT_TO_BITVECTOR || k == HO_APPLY || k == STRING_LENGTH
-         || k == SEQ_NTH;
+         || k == APPLY_SELECTOR || k == APPLY_TESTER || k == SET_UNION
+         || k == SET_INTER || k == SET_SUBSET || k == SET_MINUS
+         || k == SET_MEMBER || k == SET_SINGLETON || k == SEP_PTO
+         || k == BITVECTOR_TO_NAT || k == INT_TO_BITVECTOR || k == HO_APPLY
+         || k == STRING_LENGTH || k == SEQ_NTH;
 }
 
 bool TriggerTermInfo::isRelationalTrigger(Node n)
diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index 2b44d2404..330308946 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -787,9 +787,8 @@ Node BoundedIntegers::matchBoundVar( Node v, Node t, Node e ){
       if( e.getKind()==kind::APPLY_CONSTRUCTOR ){
         u = matchBoundVar( v, t[i], e[i] );
       }else{
-        Node se = nm->mkNode(APPLY_SELECTOR_TOTAL,
-                             dt[index].getSelectorInternal(e.getType(), i),
-                             e);
+        Node se = nm->mkNode(
+            APPLY_SELECTOR, dt[index].getSelectorInternal(e.getType(), i), e);
         u = matchBoundVar( v, t[i], se );
       }
       if( !u.isNull() ){
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index fc2928343..f24a1d646 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2078,10 +2078,6 @@ bool MatchGen::isHandledBoolConnective( TNode n ) {
 }
 
 bool MatchGen::isHandledUfTerm( TNode n ) {
-  //return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||
-  //       n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
-  //TODO : treat APPLY_TESTER as a T-constraint instead of matching (currently leads to overabundance of instantiations)
-  //return inst::Trigger::isAtomicTriggerKind( n.getKind() ) && ( !options::qcfTConstraint() || n.getKind()!=APPLY_TESTER );
   return inst::TriggerTermInfo::isAtomicTriggerKind(n.getKind());
 }
 
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index fdd5fa0ac..6d37fd75a 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -168,8 +168,8 @@ void Skolemize::getSelfSel(const DType& dt,
     }
     for (unsigned k = 0; k < ssc.size(); k++)
     {
-      Node ss = nm->mkNode(
-          APPLY_SELECTOR_TOTAL, dc.getSelectorInternal(n.getType(), j), n);
+      Node ss =
+          nm->mkNode(APPLY_SELECTOR, dc.getSelectorInternal(n.getType(), j), n);
       if (std::find(selfSel.begin(), selfSel.end(), ss) == selfSel.end())
       {
         selfSel.push_back(ss);
diff --git a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
index b3c0522f9..2e52f67d3 100644
--- a/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
+++ b/src/theory/quantifiers/sygus/sygus_eval_unfold.cpp
@@ -100,6 +100,11 @@ void SygusEvalUnfold::registerModelValue(Node a,
       TNode vt = v;
       Node vn = n.substitute(at, vt);
       vn = rewrite(vn);
+      // it might be incorrectly applied
+      if (!vn.isConst())
+      {
+        continue;
+      }
       unsigned start = d_node_mv_args_proc[n][vn];
       // get explanation in terms of testers
       std::vector<Node> antec_exp;
@@ -275,7 +280,7 @@ Node SygusEvalUnfold::unfold(Node en,
     else
     {
       Node ret = nm->mkNode(
-          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, 0), en[0]);
+          APPLY_SELECTOR, dt[i].getSelectorInternal(headType, 0), en[0]);
       Trace("sygus-eval-unfold-debug")
           << "...return (from constructor) " << ret << std::endl;
       return ret;
@@ -298,7 +303,7 @@ Node SygusEvalUnfold::unfold(Node en,
     else
     {
       s = nm->mkNode(
-          APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(headType, j), en[0]);
+          APPLY_SELECTOR, dt[i].getSelectorInternal(headType, j), en[0]);
     }
     cc.push_back(s);
     if (track_exp)
diff --git a/src/theory/quantifiers/sygus/sygus_explain.cpp b/src/theory/quantifiers/sygus/sygus_explain.cpp
index 23c315f42..dfbbc64b2 100644
--- a/src/theory/quantifiers/sygus/sygus_explain.cpp
+++ b/src/theory/quantifiers/sygus/sygus_explain.cpp
@@ -153,7 +153,7 @@ void SygusExplain::getExplanationForEquality(Node n,
     if (cexc.find(j) == cexc.end())
     {
       Node sel = NodeManager::currentNM()->mkNode(
-          kind::APPLY_SELECTOR_TOTAL, dt[i].getSelectorInternal(tn, j), n);
+          kind::APPLY_SELECTOR, dt[i].getSelectorInternal(tn, j), n);
       getExplanationForEquality(sel, vn[j], exp);
     }
   }
@@ -249,7 +249,7 @@ void SygusExplain::getExplanationFor(TermRecBuild& trb,
   for (unsigned i = 0; i < vn.getNumChildren(); i++)
   {
     Node sel = NodeManager::currentNM()->mkNode(
-        kind::APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(ntn, i), n);
+        kind::APPLY_SELECTOR, dt[cindex].getSelectorInternal(ntn, i), n);
     Node vnr_c = vnr.isNull() ? vnr : (vn[i] == vnr[i] ? Node::null() : vnr[i]);
     if (cexc.find(i) == cexc.end())
     {
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 622aa2a6a..4bea7b26b 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -258,7 +258,7 @@ Node TermDbSygus::canonizeBuiltin(Node n, std::map<TypeNode, int>& var_count)
   Trace("sygus-db-canon") << "  CanonizeBuiltin : compute for " << n << "\n";
   Node ret = n;
   // it is symbolic if it represents "any constant"
-  if (n.getKind() == APPLY_SELECTOR_TOTAL)
+  if (n.getKind() == APPLY_SELECTOR)
   {
     ret = getFreeVarInc(n[0].getType(), var_count, true);
   }
@@ -960,17 +960,23 @@ bool TermDbSygus::involvesDivByZero( Node n ) {
 }
 
 Node TermDbSygus::getAnchor( Node n ) {
-  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+  if (n.getKind() == APPLY_SELECTOR)
+  {
     return getAnchor( n[0] );
-  }else{
+  }
+  else
+  {
     return n;
   }
 }
 
 unsigned TermDbSygus::getAnchorDepth( Node n ) {
-  if( n.getKind()==APPLY_SELECTOR_TOTAL ){
+  if (n.getKind() == APPLY_SELECTOR)
+  {
     return 1+getAnchorDepth( n[0] );
-  }else{
+  }
+  else
+  {
     return 0;
   }
 }
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 9ff181b9b..b12acf942 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -188,9 +188,8 @@ Node TermDb::getMatchOperator( Node n ) {
   //datatype operators may be parametric, always assume they are
   if (k == SELECT || k == STORE || k == SET_UNION || k == SET_INTER
       || k == SET_SUBSET || k == SET_MINUS || k == SET_MEMBER
-      || k == SET_SINGLETON || k == APPLY_SELECTOR_TOTAL || k == APPLY_SELECTOR
-      || k == APPLY_TESTER || k == SEP_PTO || k == HO_APPLY || k == SEQ_NTH
-      || k == STRING_LENGTH)
+      || k == SET_SINGLETON || k == APPLY_SELECTOR || k == APPLY_TESTER
+      || k == SEP_PTO || k == HO_APPLY || k == SEQ_NTH || k == STRING_LENGTH)
   {
     //since it is parametric, use a particular one as op
     TypeNode tn = n[0].getType();
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 69e205da1..54dbcdd3c 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -59,7 +59,7 @@ void TheoryModel::finishInit(eq::EqualityEngine* ee)
   d_equalityEngine->addFunctionKind(kind::SELECT);
   // d_equalityEngine->addFunctionKind(kind::STORE);
   d_equalityEngine->addFunctionKind(kind::APPLY_CONSTRUCTOR);
-  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
+  d_equalityEngine->addFunctionKind(kind::APPLY_SELECTOR);
   d_equalityEngine->addFunctionKind(kind::APPLY_TESTER);
   d_equalityEngine->addFunctionKind(kind::SEQ_NTH);
   d_equalityEngine->addFunctionKind(kind::SEQ_NTH_TOTAL);
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 367bf557a..6b61ea110 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -127,7 +127,7 @@ bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a)
 
 bool TheoryEngineModelBuilder::isAssignable(TNode n)
 {
-  if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL
+  if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR
       || n.getKind() == kind::SEQ_NTH_TOTAL || n.getKind() == kind::SEQ_NTH)
   {
     // selectors are always assignable (where we guarantee that they are not
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 604bb91de..6e8f5a774 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -2856,7 +2856,6 @@ set(regress_2_tests
   regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
   regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2
   regress2/quantifiers/cee-event-wrong-sat.smt2
-  regress2/quantifiers/exp-trivially-dd3.smt2
   regress2/quantifiers/gn-wrong-091018.smt2
   regress2/quantifiers/issue3481-unsat1.smt2
   regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2
@@ -3113,6 +3112,8 @@ set(regression_disabled_tests
   regress2/nl/nt-lemmas-bad.smt2
   # timeout after refactoring justification heuristic
   regress2/ho/SYO362^5.p
+  # timeout after refactoring selectors
+  regress2/quantifiers/exp-trivially-dd3.smt2
   # time out
   regress3/unifpi-solve-car_1.lus.sy
   # unknown (is sat)
diff --git a/test/regress/regress0/datatypes/data-nested-codata.smt2 b/test/regress/regress0/datatypes/data-nested-codata.smt2
index 6a5716123..d49f47427 100644
--- a/test/regress/regress0/datatypes/data-nested-codata.smt2
+++ b/test/regress/regress0/datatypes/data-nested-codata.smt2
@@ -1,4 +1,5 @@
-
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic QF_DTLIA)
 (set-info :status sat)
 
diff --git a/test/regress/regress0/datatypes/parametric-alt-list.cvc.smt2 b/test/regress/regress0/datatypes/parametric-alt-list.cvc.smt2
index 2ea829b6c..a9694c623 100644
--- a/test/regress/regress0/datatypes/parametric-alt-list.cvc.smt2
+++ b/test/regress/regress0/datatypes/parametric-alt-list.cvc.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-option :incremental false)
diff --git a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2 b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
index 764c2dbed..ece9532b4 100644
--- a/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
+++ b/test/regress/regress0/quantifiers/pure_dt_cbqi.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi
+; COMMAND-LINE: --cegqi -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
diff --git a/test/regress/regress1/cee-bug0909-dd-scope.smt2 b/test/regress/regress1/cee-bug0909-dd-scope.smt2
index 6ce621a98..5000dcb94 100644
--- a/test/regress/regress1/cee-bug0909-dd-scope.smt2
+++ b/test/regress/regress1/cee-bug0909-dd-scope.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --ee-mode=distributed
-; COMMAND-LINE: --ee-mode=central
+; COMMAND-LINE: --ee-mode=distributed -q
+; COMMAND-LINE: --ee-mode=central -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
diff --git a/test/regress/regress1/datatypes/non-simple-rec-param.smt2 b/test/regress/regress1/datatypes/non-simple-rec-param.smt2
index 8db92b0fd..345a67d73 100644
--- a/test/regress/regress1/datatypes/non-simple-rec-param.smt2
+++ b/test/regress/regress1/datatypes/non-simple-rec-param.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --dt-nested-rec
+; COMMAND-LINE: --dt-nested-rec -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/cons-sets-bounds.smt2 b/test/regress/regress1/fmf/cons-sets-bounds.smt2
index f0ff20de9..c917d74d9 100644
--- a/test/regress/regress1/fmf/cons-sets-bounds.smt2
+++ b/test/regress/regress1/fmf/cons-sets-bounds.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fmf-bound
+; COMMAND-LINE: --fmf-bound -q
 ; EXPECT: sat
 (set-logic ALL)
 (declare-datatypes ((list 0)) (((cons (head Int) (tail list)) (nil))))
diff --git a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2 b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2
index 7241dab4b..9cafbfc6b 100644
--- a/test/regress/regress1/fmf/jasmin-cdt-crash.smt2
+++ b/test/regress/regress1/fmf/jasmin-cdt-crash.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/loopy_coda.smt2 b/test/regress/regress1/fmf/loopy_coda.smt2
index 2b91b8c7a..273235261 100644
--- a/test/regress/regress1/fmf/loopy_coda.smt2
+++ b/test/regress/regress1/fmf/loopy_coda.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone
+; COMMAND-LINE: --finite-model-find --fmf-inst-engine --uf-ss-fair-monotone -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
diff --git a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
index 2ed01adc6..432a3fdf6 100644
--- a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
+++ b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel
+; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel -q
 ; EXPECT: sat
 (set-logic ALL)
 (declare-datatypes ((Nat 0) (Lst 0)) (((succ (pred Nat)) (zero)) ((cons (hd Nat) (tl Lst)) (nil))))
diff --git a/test/regress/regress1/fmf/nun-0208-to.smt2 b/test/regress/regress1/fmf/nun-0208-to.smt2
index 32974ef41..f74b4b243 100644
--- a/test/regress/regress1/fmf/nun-0208-to.smt2
+++ b/test/regress/regress1/fmf/nun-0208-to.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find
+; COMMAND-LINE: --finite-model-find -q
 ; EXPECT: sat
 (set-logic ALL)
 (declare-sort b__ 0)
diff --git a/test/regress/regress1/strings/issue1105.smt2 b/test/regress/regress1/strings/issue1105.smt2
index 59f618403..0a5513fec 100644
--- a/test/regress/regress1/strings/issue1105.smt2
+++ b/test/regress/regress1/strings/issue1105.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
 (set-logic ALL)
 (set-option :strings-exp true)
 (set-info :status sat)
diff --git a/test/regress/regress2/quantifiers/net-policy-no-time.smt2 b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
index 162ea0ad1..b688d3fcf 100644
--- a/test/regress/regress2/quantifiers/net-policy-no-time.smt2
+++ b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE:
+; COMMAND-LINE: -q
 ; EXPECT: sat
 (set-logic UFDTLIRA)
 (set-option :fmf-bound true)
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index 70ea31883..d057154fc 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -3226,5 +3226,32 @@ TEST_F(TestApiBlackSolver, proj_issue422)
   slv.push(4);
 }
 
+TEST_F(TestApiBlackSolver, projIssue431)
+{
+  Solver slv;
+  slv.setOption("produce-abducts", "true");
+  Sort s2 = slv.mkBitVectorSort(22);
+  Sort s4 = slv.mkSetSort(s2);
+  Sort s5 = slv.getBooleanSort();
+  Sort s6 = slv.getRealSort();
+  Sort s7 = slv.mkFunctionSort({s6}, s5);
+  DatatypeDecl _dt46 = slv.mkDatatypeDecl("_dt46", {});
+  DatatypeConstructorDecl _cons64 = slv.mkDatatypeConstructorDecl("_cons64");
+  _cons64.addSelector("_sel62", s6);
+  _cons64.addSelector("_sel63", s4);
+  _dt46.addConstructor(_cons64);
+  Sort s14 = slv.mkDatatypeSorts({_dt46})[0];
+  Term t31 = slv.mkConst(s7, "_x100");
+  Term t47 = slv.mkConst(s14, "_x112");
+  Term sel =
+      t47.getSort().getDatatype().getConstructor("_cons64").getSelectorTerm(
+          "_sel62");
+  Term t274 = slv.mkTerm(APPLY_SELECTOR, sel, t47);
+  Term t488 = slv.mkTerm(Kind::APPLY_UF, {t31, t274});
+  slv.assertFormula({t488});
+  Term abduct;
+  slv.getAbduct(t488, abduct);
+}
+
 }  // namespace test
 }  // namespace cvc5