diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-08-05 10:21:48 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-08-05 10:21:48 -0500 |
| commit | 48a1854491c99d61d21482115e18399195d4d365 (patch) | |
| tree | 47b933d38ac7577dba75dee11d19925bec6a50f8 /src/theory/strings/extf_solver.cpp | |
| parent | 183808b608071890b4d8a05d51233fe37a133873 (diff) | |
Fix policy for rewriting string equalities (#6916)
This PR simplifies our rewriter for string equalities. We do not try to rewrite equalities to true/false by default.
This prevents cases where lemmas may contain vacuous premises that rewrite to false, hence making a lemma rewrite to true.
This PR reorganizes the interplay between the rewrite and the post-processing of rewrites via extended equality rewriting.
Fixes #6913. Also adds benchmarks from #6101 which appear related but were fixed in previous commits, thus fixes #6101 as well.
Diffstat (limited to 'src/theory/strings/extf_solver.cpp')
| -rw-r--r-- | src/theory/strings/extf_solver.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/extf_solver.cpp b/src/theory/strings/extf_solver.cpp index 98f7d7d7c..32726f4ae 100644 --- a/src/theory/strings/extf_solver.cpp +++ b/src/theory/strings/extf_solver.cpp @@ -228,7 +228,7 @@ void ExtfSolver::checkExtfReductions(int effort) for (const Node& n : extf) { Assert(!d_state.isInConflict()); - Trace("strings-process") + Trace("strings-extf-debug") << " check " << n << ", active in model=" << d_extfInfoTmp[n].d_modelActive << std::endl; bool ret = doReduction(effort, n); |