summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/CMakeLists.txt2
-rw-r--r--src/expr/array_store_all.cpp2
-rw-r--r--src/expr/array_store_all.h2
-rw-r--r--src/expr/ascription_type.cpp2
-rw-r--r--src/expr/ascription_type.h2
-rw-r--r--src/expr/attribute.cpp2
-rw-r--r--src/expr/attribute.h2
-rw-r--r--src/expr/attribute_internals.h2
-rw-r--r--src/expr/attribute_unique_id.h2
-rw-r--r--src/expr/bound_var_manager.cpp2
-rw-r--r--src/expr/bound_var_manager.h2
-rw-r--r--src/expr/buffered_proof_generator.cpp2
-rw-r--r--src/expr/buffered_proof_generator.h4
-rw-r--r--src/expr/datatype_index.cpp2
-rw-r--r--src/expr/datatype_index.h2
-rw-r--r--src/expr/dtype.cpp2
-rw-r--r--src/expr/dtype.h2
-rw-r--r--src/expr/dtype_cons.cpp2
-rw-r--r--src/expr/dtype_cons.h2
-rw-r--r--src/expr/dtype_selector.cpp2
-rw-r--r--src/expr/dtype_selector.h2
-rw-r--r--src/expr/emptybag.cpp2
-rw-r--r--src/expr/emptybag.h2
-rw-r--r--src/expr/emptyset.cpp2
-rw-r--r--src/expr/emptyset.h2
-rw-r--r--src/expr/expr_iomanip.cpp2
-rw-r--r--src/expr/expr_iomanip.h2
-rw-r--r--src/expr/expr_manager_scope.h2
-rw-r--r--src/expr/expr_manager_template.cpp2
-rw-r--r--src/expr/expr_manager_template.h2
-rw-r--r--src/expr/expr_template.cpp2
-rw-r--r--src/expr/expr_template.h2
-rw-r--r--src/expr/kind_map.h4
-rw-r--r--src/expr/kind_template.cpp2
-rw-r--r--src/expr/kind_template.h2
-rw-r--r--src/expr/lazy_proof.cpp2
-rw-r--r--src/expr/lazy_proof.h4
-rw-r--r--src/expr/lazy_proof_chain.cpp4
-rw-r--r--src/expr/lazy_proof_chain.h4
-rw-r--r--src/expr/match_trie.cpp2
-rw-r--r--src/expr/match_trie.h2
-rw-r--r--src/expr/metakind_template.cpp2
-rw-r--r--src/expr/metakind_template.h2
-rw-r--r--src/expr/node.cpp2
-rw-r--r--src/expr/node.h2
-rw-r--r--src/expr/node_algorithm.cpp2
-rw-r--r--src/expr/node_algorithm.h2
-rw-r--r--src/expr/node_builder.h2
-rw-r--r--src/expr/node_manager.cpp2
-rw-r--r--src/expr/node_manager.h2
-rw-r--r--src/expr/node_manager_attributes.h4
-rw-r--r--src/expr/node_self_iterator.h2
-rw-r--r--src/expr/node_traversal.cpp2
-rw-r--r--src/expr/node_traversal.h2
-rw-r--r--src/expr/node_trie.cpp4
-rw-r--r--src/expr/node_trie.h2
-rw-r--r--src/expr/node_value.cpp2
-rw-r--r--src/expr/node_value.h2
-rw-r--r--src/expr/node_visitor.h2
-rw-r--r--src/expr/proof.cpp2
-rw-r--r--src/expr/proof.h4
-rw-r--r--src/expr/proof_checker.cpp2
-rw-r--r--src/expr/proof_checker.h4
-rw-r--r--src/expr/proof_ensure_closed.cpp2
-rw-r--r--src/expr/proof_ensure_closed.h4
-rw-r--r--src/expr/proof_generator.cpp2
-rw-r--r--src/expr/proof_generator.h4
-rw-r--r--src/expr/proof_node.cpp2
-rw-r--r--src/expr/proof_node.h4
-rw-r--r--src/expr/proof_node_algorithm.cpp2
-rw-r--r--src/expr/proof_node_algorithm.h4
-rw-r--r--src/expr/proof_node_manager.cpp2
-rw-r--r--src/expr/proof_node_manager.h4
-rw-r--r--src/expr/proof_node_to_sexpr.cpp4
-rw-r--r--src/expr/proof_node_to_sexpr.h4
-rw-r--r--src/expr/proof_node_updater.cpp2
-rw-r--r--src/expr/proof_node_updater.h4
-rw-r--r--src/expr/proof_rule.cpp4
-rw-r--r--src/expr/proof_rule.h4
-rw-r--r--src/expr/proof_set.h2
-rw-r--r--src/expr/proof_step_buffer.cpp2
-rw-r--r--src/expr/proof_step_buffer.h4
-rw-r--r--src/expr/record.cpp2
-rw-r--r--src/expr/record.h2
-rw-r--r--src/expr/sequence.cpp2
-rw-r--r--src/expr/sequence.h2
-rw-r--r--src/expr/skolem_manager.cpp2
-rw-r--r--src/expr/skolem_manager.h2
-rw-r--r--src/expr/subs.cpp2
-rw-r--r--src/expr/subs.h2
-rw-r--r--src/expr/sygus_datatype.cpp2
-rw-r--r--src/expr/sygus_datatype.h2
-rw-r--r--src/expr/symbol_manager.cpp2
-rw-r--r--src/expr/symbol_manager.h2
-rw-r--r--src/expr/symbol_table.cpp2
-rw-r--r--src/expr/symbol_table.h2
-rw-r--r--src/expr/tconv_seq_proof_generator.cpp2
-rw-r--r--src/expr/tconv_seq_proof_generator.h4
-rw-r--r--src/expr/term_canonize.cpp2
-rw-r--r--src/expr/term_canonize.h2
-rw-r--r--src/expr/term_context.cpp2
-rw-r--r--src/expr/term_context.h2
-rw-r--r--src/expr/term_context_node.cpp2
-rw-r--r--src/expr/term_context_node.h4
-rw-r--r--src/expr/term_context_stack.cpp2
-rw-r--r--src/expr/term_context_stack.h2
-rw-r--r--src/expr/term_conversion_proof_generator.cpp2
-rw-r--r--src/expr/term_conversion_proof_generator.h4
-rw-r--r--src/expr/type.cpp2
-rw-r--r--src/expr/type.h2
-rw-r--r--src/expr/type_checker.h2
-rw-r--r--src/expr/type_checker_template.cpp2
-rw-r--r--src/expr/type_checker_util.h2
-rw-r--r--src/expr/type_matcher.cpp2
-rw-r--r--src/expr/type_matcher.h2
-rw-r--r--src/expr/type_node.cpp2
-rw-r--r--src/expr/type_node.h2
-rw-r--r--src/expr/type_properties_template.h2
-rw-r--r--src/expr/uninterpreted_constant.cpp2
-rw-r--r--src/expr/uninterpreted_constant.h2
-rw-r--r--src/expr/variable_type_map.h2
121 files changed, 144 insertions, 144 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 65cf36c34..343d55800 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -3,7 +3,7 @@
## Top contributors (to current version):
## Mathias Preiner, Andrew Reynolds, Aina Niemetz
## This file is part of the CVC4 project.
-## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## Copyright (c) 2009-2021 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.
diff --git a/src/expr/array_store_all.cpp b/src/expr/array_store_all.cpp
index ed21f8f9c..6d14ac40d 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tim King, Andres Noetzli, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/array_store_all.h b/src/expr/array_store_all.h
index 5bb796961..b47b19d5f 100644
--- a/src/expr/array_store_all.h
+++ b/src/expr/array_store_all.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tim King, Andres Noetzli, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/ascription_type.cpp b/src/expr/ascription_type.cpp
index cc5fc8557..6f50568f1 100644
--- a/src/expr/ascription_type.cpp
+++ b/src/expr/ascription_type.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h
index 13715a6d7..9bf9b131a 100644
--- a/src/expr/ascription_type.h
+++ b/src/expr/ascription_type.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 34c05976c..5973aab17 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tim King, Dejan Jovanovic, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 1b5b6974d..9a1f4682e 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Tim King, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index e93656708..271c34d3c 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Tim King, Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h
index bf7c8926b..247e0b1f1 100644
--- a/src/expr/attribute_unique_id.h
+++ b/src/expr/attribute_unique_id.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/bound_var_manager.cpp b/src/expr/bound_var_manager.cpp
index 9aa3834e6..36b824c31 100644
--- a/src/expr/bound_var_manager.cpp
+++ b/src/expr/bound_var_manager.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/bound_var_manager.h b/src/expr/bound_var_manager.h
index 59ce2bac9..16ff97cce 100644
--- a/src/expr/bound_var_manager.h
+++ b/src/expr/bound_var_manager.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp
index 266cfb18a..b1abee0d0 100644
--- a/src/expr/buffered_proof_generator.cpp
+++ b/src/expr/buffered_proof_generator.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Haniel Barbosa
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
index 15ae6ea83..4b46aa56a 100644
--- a/src/expr/buffered_proof_generator.h
+++ b/src/expr/buffered_proof_generator.h
@@ -2,9 +2,9 @@
/*! \file buffered_proof_generator.h
** \verbatim
** Top contributors (to current version):
- ** Haniel Barbosa, Andrew Reynolds
+ ** Haniel Barbosa, Andrew Reynolds, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/datatype_index.cpp b/src/expr/datatype_index.cpp
index 23d6b3ca1..5a41ca08a 100644
--- a/src/expr/datatype_index.cpp
+++ b/src/expr/datatype_index.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/datatype_index.h b/src/expr/datatype_index.h
index 08640e1d5..32656b08c 100644
--- a/src/expr/datatype_index.h
+++ b/src/expr/datatype_index.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King, Ken Matsui
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 5451edc02..162afd84a 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index c68a7d44a..18694bf64 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index b378985be..d02435465 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/dtype_cons.h b/src/expr/dtype_cons.h
index 2dba895e9..dd9fc6a0b 100644
--- a/src/expr/dtype_cons.h
+++ b/src/expr/dtype_cons.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp
index d6b907cc1..522e6b4c1 100644
--- a/src/expr/dtype_selector.cpp
+++ b/src/expr/dtype_selector.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/dtype_selector.h b/src/expr/dtype_selector.h
index 4ba88c8aa..b134c7f7d 100644
--- a/src/expr/dtype_selector.h
+++ b/src/expr/dtype_selector.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/emptybag.cpp b/src/expr/emptybag.cpp
index 8e59a8eb1..d23ccef09 100644
--- a/src/expr/emptybag.cpp
+++ b/src/expr/emptybag.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Mudathir Mohamed
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/emptybag.h b/src/expr/emptybag.h
index 8a9776f42..b7d348335 100644
--- a/src/expr/emptybag.h
+++ b/src/expr/emptybag.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Mudathir Mohamed
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/emptyset.cpp b/src/expr/emptyset.cpp
index 059670f6a..97a986054 100644
--- a/src/expr/emptyset.cpp
+++ b/src/expr/emptyset.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tim King, Kshitij Bansal, Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/emptyset.h b/src/expr/emptyset.h
index 511b21c66..8bc0929e5 100644
--- a/src/expr/emptyset.h
+++ b/src/expr/emptyset.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tim King, Andres Noetzli, Kshitij Bansal
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp
index 0395a9b07..82ac83d33 100644
--- a/src/expr/expr_iomanip.cpp
+++ b/src/expr/expr_iomanip.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Tim King, Kshitij Bansal
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/expr_iomanip.h b/src/expr/expr_iomanip.h
index e90366a81..5e29ce303 100644
--- a/src/expr/expr_iomanip.h
+++ b/src/expr/expr_iomanip.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Tim King, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h
index 8749bb8d6..a737c669b 100644
--- a/src/expr/expr_manager_scope.h
+++ b/src/expr/expr_manager_scope.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Christopher L. Conway, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 5dd7a4dfd..c4a8871fe 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Christopher L. Conway, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index f1386b84d..37c3a7255 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 67ceaf89c..745588a9a 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Mathias Preiner, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index e62dee7f6..2676c12b0 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Aina Niemetz
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h
index ef46c2093..d118b7077 100644
--- a/src/expr/kind_map.h
+++ b/src/expr/kind_map.h
@@ -2,9 +2,9 @@
/*! \file kind_map.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Mathias Preiner
+ ** Gereon Kremer, Mathias Preiner, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp
index e82e614b3..0aff7a79b 100644
--- a/src/expr/kind_template.cpp
+++ b/src/expr/kind_template.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andres Noetzli, Christopher L. Conway, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 359e7234a..6d08279cc 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andres Noetzli, Morgan Deters, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/lazy_proof.cpp b/src/expr/lazy_proof.cpp
index 9c6d0e290..3f333eeab 100644
--- a/src/expr/lazy_proof.cpp
+++ b/src/expr/lazy_proof.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/lazy_proof.h b/src/expr/lazy_proof.h
index 7c39164fe..989fd55dc 100644
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -2,9 +2,9 @@
/*! \file lazy_proof.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index 0e5e8c376..e6fba747e 100644
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -2,9 +2,9 @@
/*! \file lazy_proof_chain.cpp
** \verbatim
** Top contributors (to current version):
- ** Haniel Barbosa, Andrew Reynolds
+ ** Haniel Barbosa, Andrew Reynolds, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
index e1b0f3cd0..4c21eea99 100644
--- a/src/expr/lazy_proof_chain.h
+++ b/src/expr/lazy_proof_chain.h
@@ -2,9 +2,9 @@
/*! \file lazy_proof_chain.h
** \verbatim
** Top contributors (to current version):
- ** Haniel Barbosa, Andrew Reynolds
+ ** Haniel Barbosa, Andrew Reynolds, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/match_trie.cpp b/src/expr/match_trie.cpp
index a76779b6e..f2465e030 100644
--- a/src/expr/match_trie.cpp
+++ b/src/expr/match_trie.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/match_trie.h b/src/expr/match_trie.h
index 37f2a0f71..976b70fba 100644
--- a/src/expr/match_trie.h
+++ b/src/expr/match_trie.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Mathias Preiner, Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp
index a4b9d17c8..96e06156d 100644
--- a/src/expr/metakind_template.cpp
+++ b/src/expr/metakind_template.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andres Noetzli, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 3a453f9ac..4e47d4230 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andres Noetzli, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index eee8d0136..59d002631 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Tim King, Yoni Zohar
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node.h b/src/expr/node.h
index 06c327018..c73850e59 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Aina Niemetz
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node_algorithm.cpp b/src/expr/node_algorithm.cpp
index 34ebfcd59..1ec6c7f3a 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Andres Noetzli, Haniel Barbosa
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node_algorithm.h b/src/expr/node_algorithm.h
index f5d9f6516..e7d71ce3a 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Andres Noetzli, Yoni Zohar
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index eaa9a46d5..2f4640668 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Mathias Preiner, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 4404e3445..5eb01ecbb 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 319ab4461..99e0bd969 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Christopher L. Conway
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node_manager_attributes.h b/src/expr/node_manager_attributes.h
index ba19a3bbb..2add5a314 100644
--- a/src/expr/node_manager_attributes.h
+++ b/src/expr/node_manager_attributes.h
@@ -2,9 +2,9 @@
/*! \file node_manager_attributes.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Kshitij Bansal
+ ** Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node_self_iterator.h b/src/expr/node_self_iterator.h
index 118449b80..475e0a122 100644
--- a/src/expr/node_self_iterator.h
+++ b/src/expr/node_self_iterator.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Mathias Preiner, Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node_traversal.cpp b/src/expr/node_traversal.cpp
index 0b778ebef..f3b4c2ede 100644
--- a/src/expr/node_traversal.cpp
+++ b/src/expr/node_traversal.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Alex Ozdemir, Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node_traversal.h b/src/expr/node_traversal.h
index 124372f79..1f3b1f563 100644
--- a/src/expr/node_traversal.h
+++ b/src/expr/node_traversal.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Alex Ozdemir, Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node_trie.cpp b/src/expr/node_trie.cpp
index d2da99509..f02035c43 100644
--- a/src/expr/node_trie.cpp
+++ b/src/expr/node_trie.cpp
@@ -2,9 +2,9 @@
/*! \file node_trie.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node_trie.h b/src/expr/node_trie.h
index d783000ee..81529f38e 100644
--- a/src/expr/node_trie.h
+++ b/src/expr/node_trie.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 9964d7aec..dc682a9fb 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Aina Niemetz, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 1ad498ecd..d6b6d3c45 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Aina Niemetz, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/node_visitor.h b/src/expr/node_visitor.h
index 1ffd39406..dcf8e38e0 100644
--- a/src/expr/node_visitor.h
+++ b/src/expr/node_visitor.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Dejan Jovanovic, Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp
index 6596f6c5f..e3c70590c 100644
--- a/src/expr/proof.cpp
+++ b/src/expr/proof.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof.h b/src/expr/proof.h
index abb0b9b37..e676731ea 100644
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -2,9 +2,9 @@
/*! \file proof.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp
index a5655c9db..bcff07c30 100644
--- a/src/expr/proof_checker.cpp
+++ b/src/expr/proof_checker.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h
index 200a1839d..fff7def4f 100644
--- a/src/expr/proof_checker.h
+++ b/src/expr/proof_checker.h
@@ -2,9 +2,9 @@
/*! \file proof_checker.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_ensure_closed.cpp b/src/expr/proof_ensure_closed.cpp
index 183ff0d5b..451a6a530 100644
--- a/src/expr/proof_ensure_closed.cpp
+++ b/src/expr/proof_ensure_closed.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_ensure_closed.h b/src/expr/proof_ensure_closed.h
index c54a5dfd5..dd137343a 100644
--- a/src/expr/proof_ensure_closed.h
+++ b/src/expr/proof_ensure_closed.h
@@ -2,9 +2,9 @@
/*! \file proof_ensure_closed.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_generator.cpp b/src/expr/proof_generator.cpp
index 31af09b7f..53bc54d7a 100644
--- a/src/expr/proof_generator.cpp
+++ b/src/expr/proof_generator.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_generator.h b/src/expr/proof_generator.h
index 3b376d77c..497e89d7a 100644
--- a/src/expr/proof_generator.h
+++ b/src/expr/proof_generator.h
@@ -2,9 +2,9 @@
/*! \file proof_generator.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp
index 3bef451ee..755a37643 100644
--- a/src/expr/proof_node.cpp
+++ b/src/expr/proof_node.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
index a505b1bc0..f7b323018 100644
--- a/src/expr/proof_node.h
+++ b/src/expr/proof_node.h
@@ -2,9 +2,9 @@
/*! \file proof_node.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Haniel Barbosa
+ ** Andrew Reynolds, Haniel Barbosa, Alex Ozdemir
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp
index 751dcc39e..90b1e9030 100644
--- a/src/expr/proof_node_algorithm.cpp
+++ b/src/expr/proof_node_algorithm.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Haniel Barbosa
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h
index af8de066d..9106bb36f 100644
--- a/src/expr/proof_node_algorithm.h
+++ b/src/expr/proof_node_algorithm.h
@@ -2,9 +2,9 @@
/*! \file proof_node_algorithm.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Haniel Barbosa
+ ** Andrew Reynolds, Haniel Barbosa, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index 91858f239..6d8b05c0a 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Haniel Barbosa
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index e7be50065..434cffe28 100644
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -2,9 +2,9 @@
/*! \file proof_node_manager.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Haniel Barbosa
+ ** Andrew Reynolds, Haniel Barbosa, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp
index 6830326ba..34868b67f 100644
--- a/src/expr/proof_node_to_sexpr.cpp
+++ b/src/expr/proof_node_to_sexpr.cpp
@@ -2,9 +2,9 @@
/*! \file proof_node_to_sexpr.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Haniel Barbosa
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_node_to_sexpr.h b/src/expr/proof_node_to_sexpr.h
index e6c003d10..cf2e86263 100644
--- a/src/expr/proof_node_to_sexpr.h
+++ b/src/expr/proof_node_to_sexpr.h
@@ -2,9 +2,9 @@
/*! \file proof_node_to_sexpr.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Haniel Barbosa, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
index f421ff4f3..cacadc815 100644
--- a/src/expr/proof_node_updater.cpp
+++ b/src/expr/proof_node_updater.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Haniel Barbosa
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h
index 2df668384..693168a25 100644
--- a/src/expr/proof_node_updater.h
+++ b/src/expr/proof_node_updater.h
@@ -2,9 +2,9 @@
/*! \file proof_node_updater.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Haniel Barbosa
+ ** Andrew Reynolds, Haniel Barbosa, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp
index d29aca6ea..0b7c8cc69 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -2,9 +2,9 @@
/*! \file proof_rule.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Haniel Barbosa, Alex Ozdemir
+ ** Andrew Reynolds, Haniel Barbosa, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 76c2d0958..b25866b5e 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -2,9 +2,9 @@
/*! \file proof_rule.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Haniel Barbosa, Alex Ozdemir
+ ** Andrew Reynolds, Haniel Barbosa, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_set.h b/src/expr/proof_set.h
index 9c6c21ec4..a45a0f1f8 100644
--- a/src/expr/proof_set.h
+++ b/src/expr/proof_set.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Gereon Kremer, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_step_buffer.cpp b/src/expr/proof_step_buffer.cpp
index 4c99855df..51aa9f098 100644
--- a/src/expr/proof_step_buffer.cpp
+++ b/src/expr/proof_step_buffer.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/proof_step_buffer.h b/src/expr/proof_step_buffer.h
index 1b09a8f96..0b4b8552b 100644
--- a/src/expr/proof_step_buffer.h
+++ b/src/expr/proof_step_buffer.h
@@ -2,9 +2,9 @@
/*! \file proof_step_buffer.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/record.cpp b/src/expr/record.cpp
index cddfd7a22..ed4e05567 100644
--- a/src/expr/record.cpp
+++ b/src/expr/record.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/record.h b/src/expr/record.h
index 1ab84c30c..cccbf625a 100644
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Tim King, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/sequence.cpp b/src/expr/sequence.cpp
index 68c4985bb..b02b68815 100644
--- a/src/expr/sequence.cpp
+++ b/src/expr/sequence.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/sequence.h b/src/expr/sequence.h
index 27e5cf6f4..1c0b1fbb9 100644
--- a/src/expr/sequence.h
+++ b/src/expr/sequence.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp
index 53cbf76de..3f77a170a 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h
index 59e48528d..6e44db263 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/subs.cpp b/src/expr/subs.cpp
index 3ca75050a..0434cacf3 100644
--- a/src/expr/subs.cpp
+++ b/src/expr/subs.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/subs.h b/src/expr/subs.h
index ac678d2ee..86c7d1758 100644
--- a/src/expr/subs.h
+++ b/src/expr/subs.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/sygus_datatype.cpp b/src/expr/sygus_datatype.cpp
index e67a1befe..d2e845452 100644
--- a/src/expr/sygus_datatype.cpp
+++ b/src/expr/sygus_datatype.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Haniel Barbosa
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/sygus_datatype.h b/src/expr/sygus_datatype.h
index 2be3d9d49..1350e9e57 100644
--- a/src/expr/sygus_datatype.h
+++ b/src/expr/sygus_datatype.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Haniel Barbosa
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/symbol_manager.cpp b/src/expr/symbol_manager.cpp
index 5fb46a5d0..0fa2db1d4 100644
--- a/src/expr/symbol_manager.cpp
+++ b/src/expr/symbol_manager.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/symbol_manager.h b/src/expr/symbol_manager.h
index 73018d7ca..36f3b46bd 100644
--- a/src/expr/symbol_manager.h
+++ b/src/expr/symbol_manager.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index 8d5e36554..3942f3775 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index ff8906b2c..cdfe3a6a3 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Christopher L. Conway
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/expr/tconv_seq_proof_generator.cpp
index 105c811d4..e7fba5088 100644
--- a/src/expr/tconv_seq_proof_generator.cpp
+++ b/src/expr/tconv_seq_proof_generator.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/tconv_seq_proof_generator.h b/src/expr/tconv_seq_proof_generator.h
index 9197028d6..e907ef09c 100644
--- a/src/expr/tconv_seq_proof_generator.h
+++ b/src/expr/tconv_seq_proof_generator.h
@@ -2,9 +2,9 @@
/*! \file tconv_seq_proof_generator.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/term_canonize.cpp b/src/expr/term_canonize.cpp
index 91f7f3190..72c59136b 100644
--- a/src/expr/term_canonize.cpp
+++ b/src/expr/term_canonize.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/term_canonize.h b/src/expr/term_canonize.h
index cd15fba41..3eefb0c4a 100644
--- a/src/expr/term_canonize.h
+++ b/src/expr/term_canonize.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/term_context.cpp b/src/expr/term_context.cpp
index 67da6d842..2ade0943d 100644
--- a/src/expr/term_context.cpp
+++ b/src/expr/term_context.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/term_context.h b/src/expr/term_context.h
index b0ce03e48..7b4dbe928 100644
--- a/src/expr/term_context.h
+++ b/src/expr/term_context.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/term_context_node.cpp b/src/expr/term_context_node.cpp
index e5610ef46..871193442 100644
--- a/src/expr/term_context_node.cpp
+++ b/src/expr/term_context_node.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/term_context_node.h b/src/expr/term_context_node.h
index 061cf1ed2..15e7f9f1b 100644
--- a/src/expr/term_context_node.h
+++ b/src/expr/term_context_node.h
@@ -2,9 +2,9 @@
/*! \file term_context_node.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/term_context_stack.cpp b/src/expr/term_context_stack.cpp
index f35514fa6..07d7746ed 100644
--- a/src/expr/term_context_stack.cpp
+++ b/src/expr/term_context_stack.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/term_context_stack.h b/src/expr/term_context_stack.h
index ca72a6acd..f40f5f6b2 100644
--- a/src/expr/term_context_stack.h
+++ b/src/expr/term_context_stack.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/term_conversion_proof_generator.cpp b/src/expr/term_conversion_proof_generator.cpp
index a47214ae1..d15776c3f 100644
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/term_conversion_proof_generator.h b/src/expr/term_conversion_proof_generator.h
index 4d6a169cb..5996cd747 100644
--- a/src/expr/term_conversion_proof_generator.h
+++ b/src/expr/term_conversion_proof_generator.h
@@ -2,9 +2,9 @@
/*! \file term_conversion_proof_generator.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Gereon Kremer
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index cbc15e153..baf3ddf8c 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/type.h b/src/expr/type.h
index 0c70b1667..8f8ccc1bf 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/type_checker.h b/src/expr/type_checker.h
index f385856e0..0ca2fb806 100644
--- a/src/expr/type_checker.h
+++ b/src/expr/type_checker.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tim King, Morgan Deters, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp
index 3436cc138..527f98384 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Mathias Preiner, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/type_checker_util.h b/src/expr/type_checker_util.h
index 32c1254de..5f227423b 100644
--- a/src/expr/type_checker_util.h
+++ b/src/expr/type_checker_util.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/type_matcher.cpp b/src/expr/type_matcher.cpp
index b41004880..b71a4b515 100644
--- a/src/expr/type_matcher.cpp
+++ b/src/expr/type_matcher.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Mathias Preiner, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/type_matcher.h b/src/expr/type_matcher.h
index 126175582..98c3ce865 100644
--- a/src/expr/type_matcher.h
+++ b/src/expr/type_matcher.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 3c038546a..8b0d6d7f7 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 01e096c72..63c26f5e9 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h
index 723f805b7..c0f9fb844 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp
index ee490c7c7..b2d5a2b12 100644
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andres Noetzli, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h
index b36bd6b1a..93a9fc1c6 100644
--- a/src/expr/uninterpreted_constant.h
+++ b/src/expr/uninterpreted_constant.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andres Noetzli, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
diff --git a/src/expr/variable_type_map.h b/src/expr/variable_type_map.h
index fd51e0243..afccac13f 100644
--- a/src/expr/variable_type_map.h
+++ b/src/expr/variable_type_map.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Tim King, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2021 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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback