2 files changed, 23 insertions, 15 deletions

diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp
index 8ce2a3e81..0f4af2458 100644
--- a/src/theory/strings/extf_solver.cpp
+++ b/src/theory/strings/extf_solver.cpp
@@ -47,7 +47,8 @@ ExtfSolver::ExtfSolver(context::Context* c,
       d_statistics(statistics),
       d_preproc(&skc, u, statistics),
       d_hasExtf(c, false),
-      d_extfInferCache(c)
+      d_extfInferCache(c),
+      d_reduced(u)
 {
   d_extt->addFunctionKind(kind::STRING_SUBSTR);
   d_extt->addFunctionKind(kind::STRING_STRIDOF);
@@ -69,7 +70,7 @@ ExtfSolver::ExtfSolver(context::Context* c,
 
 ExtfSolver::~ExtfSolver() {}
 
-bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
+bool ExtfSolver::doReduction(int effort, Node n)
 {
   Assert(d_extfInfoTmp.find(n) != d_extfInfoTmp.end());
   if (!d_extfInfoTmp[n].d_modelActive)
@@ -77,6 +78,11 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
     // n is not active in the model, no need to reduce
     return false;
   }
+  if (d_reduced.find(n)!=d_reduced.end())
+  {
+    // already sent a reduction lemma
+    return false;
+  }
   // determine the effort level to process the extf at
   // 0 - at assertion time, 1+ - after no other reduction is applicable
   int r_effort = -1;
@@ -118,9 +124,9 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
             Node xneqs = x.eqNode(s).negate();
             d_im.sendInference(lexp, xneqs, Inference::CTN_NEG_EQUAL, true);
           }
-          // this depends on the current assertions, so we set that this
-          // inference is context-dependent.
-          isCd = true;
+          // this depends on the current assertions, so this
+          // inference is context-dependent
+          d_extt->markReduced(n, true);
           return true;
         }
         else
@@ -168,7 +174,7 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
     Trace("strings-red-lemma") << "Reduction (positive contains) lemma : " << n
                                << " => " << eq << std::endl;
     // context-dependent because it depends on the polarity of n itself
-    isCd = true;
+    d_extt->markReduced(n, true);
   }
   else if (k != kind::STRING_TO_CODE)
   {
@@ -190,7 +196,8 @@ bool ExtfSolver::doReduction(int effort, Node n, bool& isCd)
     d_im.sendInference(d_emptyVec, nnlem, Inference::REDUCTION, true);
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on reduction." << std::endl;
-    isCd = false;
+    // add as reduction lemma
+    d_reduced.insert(n);
   }
   return true;
 }
@@ -209,12 +216,10 @@ void ExtfSolver::checkExtfReductions(int effort)
     Trace("strings-process")
         << "  check " << n
         << ", active in model=" << d_extfInfoTmp[n].d_modelActive << std::endl;
-    // whether the reduction was context-dependent
-    bool isCd = false;
-    bool ret = doReduction(effort, n, isCd);
+    bool ret = doReduction(effort, n);
     if (ret)
     {
-      d_extt->markReduced(n, isCd);
+      // we do not mark as reduced, since we may want to evaluate
       if (d_im.hasProcessed())
       {
         return;
diff --git a/src/theory/strings/extf_solver.h b/src/theory/strings/extf_solver.h
index e7e2512bd..f0f0d790b 100644
--- a/src/theory/strings/extf_solver.h
+++ b/src/theory/strings/extf_solver.h
@@ -161,11 +161,12 @@ class ExtfSolver
    * This is called when an extended function application n is not able to be
    * simplified by context-depdendent simplification, and we are resorting to
    * expanding n to its full semantics via a reduction. This method returns
-   * true if it successfully reduced n by some reduction and sets isCd to
-   * true if the reduction was (SAT)-context-dependent, and false otherwise.
-   * The argument effort has the same meaning as in checkExtfReductions.
+   * true if it successfully reduced n by some reduction. If so, it either
+   * caches that the reduction lemma was sent, or marks n as reduced in this
+   * SAT-context. The argument effort has the same meaning as in
+   * checkExtfReductions.
    */
-  bool doReduction(int effort, Node n, bool& isCd);
+  bool doReduction(int effort, Node n);
   /** check extended function inferences
    *
    * This function makes additional inferences for n that do not contribute
@@ -205,6 +206,8 @@ class ExtfSolver
   context::CDO<bool> d_hasExtf;
   /** extended functions inferences cache */
   NodeSet d_extfInferCache;
+  /** The set of extended functions we have sent reduction lemmas for */
+  NodeSet d_reduced;
 };
 
 }  // namespace strings