From: Abdalrhman Mohamed <32971963+abdoo8080@users.noreply.github.com>
Date: Tue, 13 Apr 2021 12:45:43 +0000 (-0700)
Subject: Avoid using substitute's input cache after the method call. (#6328)
X-Git-Tag: cvc5-1.0.0~1918
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ee7442e1c79e94be8e3e23777679980b8c505d1c;p=cvc5.git

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 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())