Make witness form visited ref counted (#8081)

Fixes #8079.

diff --git a/src/smt/witness_form.cpp b/src/smt/witness_form.cpp
index 16d297495bd1afb451790a1dfe0b5245323f6fd1..07700a9e7bc876504614d25454e32b7aca7db619 100644 (file)
--- 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 06d60c1edfdc6b59d609ca9ecf190c6f002be6c5..b2ee28c48780a8e4c29ea8ec6c1452f356bdd640 100644 (file)
--- 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 */