diff options
| author | Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com> | 2021-04-13 05:45:43 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-13 12:45:43 +0000 |
| commit | ee7442e1c79e94be8e3e23777679980b8c505d1c (patch) | |
| tree | 403225dbe01d4c2a5612d037ebb73a50cb841590 /src | |
| parent | ec0daa929c59dbed12ea119f3a5503e37f13d887 (diff) | |
Avoid using substitute's input cache after the method call. (#6328)
As it traverses a node, Node::substitute populates its input cache with TNodes that are not preserved by the SygusReconstruct module and maybe destroyed after the method call. This PR fixes a bug where those unsafe TNodes are referenced throughout the module by passing the method a temporary copy of the cache instead.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_reconstruct.cpp | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp index 7b8d897c4..0fe3032ff 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp @@ -284,7 +284,11 @@ TypeObligationSetMap SygusReconstruct::matchNewObs(Node k, Node sz) if (isSolved) { - Node s = sz.substitute(d_sol); + // As it traverses sz, substitute populates its input cache with TNodes + // that are not preserved by this module and maybe destroyed after the + // method call. To avoid referencing those unsafe TNodes throughout this + // module, we pass a iterators of d_sol instead. + Node s = sz.substitute(d_sol.cbegin(), d_sol.cend()); markSolved(k, s); } else @@ -340,7 +344,8 @@ void SygusReconstruct::markSolved(Node k, Node s) { // then it is completely solved and can be used as a solution of its // corresponding obligation - Node parentSol = parent.substitute(d_sol); + // pass iterators of d_sol to avoid populating it with unsafe TNodes + Node parentSol = parent.substitute(d_sol.cbegin(), d_sol.cend()); Node parentOb = d_parentOb[parent]; // proceed only if parent obligation is not already solved if (d_sol[parentOb].isNull()) |