From 3845f112ff053c6485fd5c00c5b0c87522157ca9 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 7 Feb 2022 18:48:12 -0600
Subject: [PATCH] Make witness form visited ref counted (#8081)

Fixes #8079.
---
 src/smt/witness_form.cpp | 2 +-
 src/smt/witness_form.h   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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 */
-- 
2.30.2