diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-02-04 00:16:00 -0800 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2020-02-04 00:16:00 -0800 |
| commit | 2a71a63f0d13a8aca5208334ecd329e68209e056 (patch) | |
| tree | b34841cd92a99dbf32e2eda3e79fff67b2a39d74 | |
| parent | d3e45c1fd1ef3f56f15ad08c783a3d5c54ea10c1 (diff) | |
Revert semantic change from refactoringfixInConflict
In PR #3398, a minor change was introduced: One of the checks for
whether there is a conflict or not was flipped
(https://github.com/CVC4/CVC4/pull/3398/files#diff-62fffb0d9df0385909621e424bdcef72R1652). This commit reverts that change.
| -rw-r--r-- | src/theory/strings/theory_strings.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 152160cde..c3a67aec9 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1629,7 +1629,7 @@ void TheoryStrings::checkExtfEval( int effort ) { Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << std::endl; d_im.sendInference( einfo.d_exp, conc, effort == 0 ? "EXTF" : "EXTF-N", true); - if (!d_state.isInConflict()) + if (d_state.isInConflict()) { Trace("strings-extf-debug") << " conflict, return." << std::endl; return; |