From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Fri, 26 Feb 2021 05:02:43 +0000 (+0100)
Subject: Store Node instead of TNode (#5993)
X-Git-Tag: cvc5-1.0.0~2206
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=55fd45841d2f51c5194b710d8d99ad43c2315c08;p=cvc5.git

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 f4e30417c..0a16759e1 100644
--- 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