From ee7442e1c79e94be8e3e23777679980b8c505d1c Mon Sep 17 00:00:00 2001
From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Tue, 13 Apr 2021 05:45:43 -0700
Subject: [PATCH] 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.
---
 src/theory/quantifiers/sygus/sygus_reconstruct.cpp | 9 +++++++--
 1 file 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())
-- 
2.30.2