diff options
Diffstat (limited to 'src/theory/strings/theory_strings.cpp')
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 984b47e72..883683f52 100644 --- 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; |