diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-15 16:07:40 -0800 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-15 16:07:40 -0800 |
commit | a94907e166ee4e43cfe8ac9ecb1cd2547b5946fc (patch) | |
tree | 31114cd911907143c65e3b64dcdb7e48f74d3039 | |
parent | c24214305022cb580a3a2d11943949dc6689a6c8 (diff) |
updatenewCtnInf
-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; |