diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-26 06:02:43 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-25 23:02:43 -0600 |
| commit | 55fd45841d2f51c5194b710d8d99ad43c2315c08 (patch) | |
| tree | 347a250c3bd52fac9244d36a52a92301ab69705e /src | |
| parent | c725b56d1a5a1f896ee76178c718093859aedccb (diff) | |
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.
Diffstat (limited to 'src')
| -rw-r--r-- | src/decision/justification_heuristic.h | 2 |
1 files changed, 1 insertions, 1 deletions
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 |