summaryrefslogtreecommitdiff
path: root/src/proof/uf_proof.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/uf_proof.cpp')
-rw-r--r--src/proof/uf_proof.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 5d4a1ce11..10823693d 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Guy Katz, Yoni Zohar
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
@@ -141,7 +141,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
return Node();
}
-
+ // TODO (#2965): improve this code, which is highly complicated.
switch(pf.d_id) {
case theory::eq::MERGED_THROUGH_CONGRUENCE: {
Debug("pf::uf") << "\nok, looking at congruence:\n";
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback