diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-14 07:04:17 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-14 14:04:17 +0100 |
| commit | d16b689f85e4962dfc77e8e9a1b7de23ab11ac7d (patch) | |
| tree | 3268a45a2316217b108deb3d1700ce54b9a29233 /src/theory/strings/term_registry.cpp | |
| parent | a49efc8c32020b7c2285fa744ae61a576801c51d (diff) | |
Fix SAT-context dependent issue in strings preregistration (#5564)
This makes preregistration of terms SAT-context dependent in strings instead of user-context dependent.
Fixes #5547.
This is required to avoid model unsoundness on sequence benchmarks, as demonstrated in that issue.
It furthermore impacts how we have been handling theory combination with arithmetic for str.len and impacts how propagation is setup for the strings equality engine.
I will do performance testing on this PR.
Diffstat (limited to 'src/theory/strings/term_registry.cpp')
| -rw-r--r-- | src/theory/strings/term_registry.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 8274b7dc0..cce2b117f 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -46,7 +46,7 @@ TermRegistry::TermRegistry(SolverState& s, d_hasStrCode(false), d_functionsTerms(s.getSatContext()), d_inputVars(s.getUserContext()), - d_preregisteredTerms(s.getUserContext()), + d_preregisteredTerms(s.getSatContext()), d_registeredTerms(s.getUserContext()), d_registeredTypes(s.getUserContext()), d_lengthLemmaTermsCache(s.getUserContext()), |