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.

diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.cpp b/src/theory/quantifiers/sygus/sygus_reconstruct.cpp
index 7b8d897c400e5f4c904d5febe9dd034d07157d35..0fe3032ffcd15d9de7ffdb5647c656592a6d16c4 100644 (file)
--- 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())