diff options
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 39 |
1 files changed, 19 insertions, 20 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 3db8f39bb..d643fac70 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2847,28 +2847,27 @@ void TheoryStrings::processNEqc( std::vector< std::vector< Node > > &normal_form EQUAL, TheoryStringsRewriter::mkConcat(STRING_CONCAT, normal_forms[i]), TheoryStringsRewriter::mkConcat(STRING_CONCAT, normal_forms[j])); - Node eqr = TheoryStringsRewriter::rewriteEqualityExt(eq); - if (eq != eqr) + eq = Rewriter::rewrite(eq); + if (eq.getKind() == EQUAL) { - eqr = Rewriter::rewrite(eqr); - std::vector<Node> antec; - getExplanationVectorForPrefixEq(normal_forms, - normal_form_src, - normal_forms_exp, - normal_forms_exp_depend, - i, - j, - -1, - -1, - false, - antec); - //antec.push_back(eq); - - if (getExtTheory()->isActive(eq)) { - getExtTheory()->markReduced(eq); + Node eqr = TheoryStringsRewriter::rewriteEqualityExt(eq); + if (eq != eqr) + { + eqr = Rewriter::rewrite(eqr); + std::vector<Node> antec; + getExplanationVectorForPrefixEq(normal_forms, + normal_form_src, + normal_forms_exp, + normal_forms_exp_depend, + i, + j, + -1, + -1, + false, + antec); + + sendInternalInference(antec, eqr, "__equality_rew"); } - sendInference(antec, eqr, "__equality_rew"); - return; } //process the reverse direction first (check for easy conflicts and inferences) |