Store Node instead of TNode (#5993)

The justification heuristic stores a "copy" of assertions as TNode. As witnessed by #5938, these TNodes may invalid.
This PR changes this to store Nodes instead.
Fixes #5938.

diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index f4e30417cacc1abb9704e50399001f8cd15e81dc..0a16759e1ee6cc7a70e872a39d64237fc939d9b1 100644 (file)
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -65,7 +65,7 @@ class JustificationHeuristic : public ITEDecisionStrategy {
    * A copy of the assertions that need to be justified
    * directly. Doesn't have ones introduced during during term removal.
    */
-  context::CDList<TNode> d_assertions;
+  context::CDList<Node> d_assertions;
   //TNode is fine since decisionEngine has them too
 
   /** map from skolems introduced in term removal to the corresponding assertion