Fix context-dependent for positive contains reduction (#2644)

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 984b47e72abb5966d5b71ac9db4c40f083b68ffe..883683f52f734fd7f3d0efe06e7a9190c787db4d 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -493,6 +493,10 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on positive contain reduction."
         << std::endl;
+    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;
   }
   else if (k != kind::STRING_CODE)
   {
@@ -513,8 +517,8 @@ bool TheoryStrings::doReduction(int effort, Node n, bool& isCd)
     sendInference(d_empty_vec, nnlem, "Reduction", true);
     Trace("strings-extf-debug")
         << "  resolve extf : " << n << " based on reduction." << std::endl;
+    isCd = false;
   }
-  isCd = false;
   return true;
 }
 
@@ -1001,6 +1005,7 @@ void TheoryStrings::checkExtfReductions( int effort ) {
   Trace("strings-process") << "  checking " << extf.size() << " active extf"
                            << std::endl;
   for( unsigned i=0; i<extf.size(); i++ ){
+    Assert(!d_conflict);
     Node n = extf[i];
     Trace("strings-process") << "  check " << n << ", active in model="
                              << d_extf_info_tmp[n].d_model_active << std::endl;