diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-14 23:38:23 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-02-14 23:38:23 -0800 |
| commit | 9c7bc79d3a0cd4d320ce400a752cb530209a1f0f (patch) | |
| tree | f49ffa5b41b8e34dd93f513d2e90d83949099e07 | |
| parent | b6e6f76371b2da8e45e2666d3e6d3d0dd78beb84 (diff) | |
test
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 319315d09..b797953ff 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1834,7 +1834,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef } else { - do_infer = !areEqual(lit, pol ? d_true : d_false); + do_infer = areEqual(lit, !pol ? d_true : d_false); } if (do_infer) { @@ -1849,6 +1849,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef } } + /* for (const auto& kv : d_extf_info_tmp) { if (kv.second.d_ctn.find(opol) != kv.second.d_ctn.end()) @@ -1893,6 +1894,7 @@ void TheoryStrings::checkExtfInference( Node n, Node nr, ExtfInfoTmp& in, int ef } } } + */ } else { |