projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c725b56) | patch
Store Node instead of TNode (#5993)
authorGereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Fri, 26 Feb 2021 05:02:43 +0000 (06:02 +0100)
committerGitHub <noreply@github.com>
Fri, 26 Feb 2021 05:02:43 +0000 (23:02 -0600)
commit55fd45841d2f51c5194b710d8d99ad43c2315c08
tree347a250c3bd52fac9244d36a52a92301ab69705etree
parentc725b56d1a5a1f896ee76178c718093859aedccbcommit | 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.
src/decision/justification_heuristic.h diff | blob | history