diff options
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 463a4f83b..319315d09 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1829,17 +1829,13 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef Node lit = pol ? conc : conc[0]; if (lit.getKind() == EQUAL) { - do_infer = pol ? areEqual(lit[0], lit[1]) - : areDisequal(lit[0], lit[1]); + do_infer = pol ? !areEqual(lit[0], lit[1]) + : !areDisequal(lit[0], lit[1]); } else { do_infer = !areEqual(lit, pol ? d_true : d_false); } - if (hasTerm(lit)) - { - getExtTheory()->markReduced(lit); - } if (do_infer) { std::vector<Node> exp_c; |