diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-11-02 13:46:05 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-11-02 13:46:05 -0600 |
| commit | 457b0fe003c8192e35df48cfb3528b9aefe2fd1b (patch) | |
| tree | d301b0a6111d5fec5514158a7e1134ede96a99d4 /src/theory/strings/term_registry.cpp | |
| parent | 17f261ab726e8cd010156234df2808d9b7af3ae0 (diff) | |
Update strings proxy variable map to be context independent (#5377)
This makes strings proxy variables map to be context-independent. They should be context independent since we are using attributes to mark proxy variables, which are context-independent. This led to the crash reported on #5374 since proxy variables would persist across multiple user contexts, but would be missing in the user-context dependent map.
This fixes #5374.
Diffstat (limited to 'src/theory/strings/term_registry.cpp')
| -rw-r--r-- | src/theory/strings/term_registry.cpp | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/theory/strings/term_registry.cpp b/src/theory/strings/term_registry.cpp index 2b5daa476..76230bcff 100644 --- a/src/theory/strings/term_registry.cpp +++ b/src/theory/strings/term_registry.cpp @@ -49,8 +49,6 @@ TermRegistry::TermRegistry(SolverState& s, d_preregisteredTerms(s.getUserContext()), d_registeredTerms(s.getUserContext()), d_registeredTypes(s.getUserContext()), - d_proxyVar(s.getUserContext()), - d_proxyVarToLength(s.getUserContext()), d_lengthLemmaTermsCache(s.getUserContext()), d_epg(pnm ? new EagerProofGenerator( pnm, @@ -567,7 +565,7 @@ Node TermRegistry::getSymbolicDefinition(Node n, std::vector<Node>& exp) const Node TermRegistry::getProxyVariableFor(Node n) const { - NodeNodeMap::const_iterator it = d_proxyVar.find(n); + std::map<Node, Node>::const_iterator it = d_proxyVar.find(n); if (it != d_proxyVar.end()) { return (*it).second; |