From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 8 Feb 2022 00:48:12 +0000 (-0600)
Subject: Make witness form visited ref counted (#8081)
X-Git-Tag: cvc5-1.0.0~440
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3845f112ff053c6485fd5c00c5b0c87522157ca9;p=cvc5.git

Make witness form visited ref counted (#8081)

Fixes #8079.
---

diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp
index 16d297495..07700a9e7 100644
--- a/src/smt/witness_form.cpp
+++ b/src/smt/witness_form.cpp
@@ -72,7 +72,7 @@ Node WitnessFormGenerator::convertToWitnessForm(Node t)
     // trivial case
     return tw;
   }
-  std::unordered_set<TNode>::iterator it;
+  std::unordered_set<Node>::iterator it;
   std::vector<TNode> visit;
   TNode cur;
   TNode curw;
diff --git a/src/smt/witness_form.h b/src/smt/witness_form.h
index 06d60c1ed..b2ee28c48 100644
--- a/src/smt/witness_form.h
+++ b/src/smt/witness_form.h
@@ -97,7 +97,7 @@ class WitnessFormGenerator : public ProofGenerator
   /** The term conversion proof generator */
   TConvProofGenerator d_tcpg;
   /** The nodes we have already added rewrite steps for in d_tcpg */
-  std::unordered_set<TNode> d_visited;
+  std::unordered_set<Node> d_visited;
   /** The set of equalities added as proof steps */
   std::unordered_set<Node> d_eqs;
   /** Lazy proof storing witness intro steps */