summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/CMakeLists.txt10
-rw-r--r--src/expr/array.h2
-rw-r--r--src/expr/array_store_all.cpp4
-rw-r--r--src/expr/array_store_all.h4
-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/datatype_index.cpp4
-rw-r--r--src/expr/datatype_index.h4
-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.cpp4
-rw-r--r--src/expr/dtype_selector.h2
-rw-r--r--src/expr/emptyset.cpp4
-rw-r--r--src/expr/emptyset.h4
-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.h4
-rw-r--r--src/expr/expr_template.cpp2
-rw-r--r--src/expr/expr_template.h2
-rw-r--r--src/expr/kind_map.h2
-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.h2
-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.h4
-rw-r--r--src/expr/node_manager_attributes.h2
-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.cpp2
-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.h2
-rw-r--r--src/expr/proof_checker.cpp2
-rw-r--r--src/expr/proof_checker.h2
-rw-r--r--src/expr/proof_generator.cpp2
-rw-r--r--src/expr/proof_generator.h2
-rw-r--r--src/expr/proof_node.cpp2
-rw-r--r--src/expr/proof_node.h2
-rw-r--r--src/expr/proof_node_algorithm.cpp2
-rw-r--r--src/expr/proof_node_algorithm.h2
-rw-r--r--src/expr/proof_node_manager.cpp2
-rw-r--r--src/expr/proof_node_manager.h2
-rw-r--r--src/expr/proof_node_to_sexpr.cpp2
-rw-r--r--src/expr/proof_node_to_sexpr.h2
-rw-r--r--src/expr/proof_node_updater.cpp4
-rw-r--r--src/expr/proof_node_updater.h2
-rw-r--r--src/expr/proof_rule.cpp4
-rw-r--r--src/expr/proof_rule.h4
-rw-r--r--src/expr/proof_step_buffer.cpp2
-rw-r--r--src/expr/proof_step_buffer.h2
-rw-r--r--src/expr/record.cpp2
-rw-r--r--src/expr/record.h2
-rw-r--r--src/expr/sequence.cpp4
-rw-r--r--src/expr/sequence.h4
-rw-r--r--src/expr/skolem_manager.cpp2
-rw-r--r--src/expr/skolem_manager.h2
-rw-r--r--src/expr/sygus_datatype.cpp2
-rw-r--r--src/expr/sygus_datatype.h2
-rw-r--r--src/expr/symbol_table.cpp2
-rw-r--r--src/expr/symbol_table.h2
-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.h2
-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.cpp4
-rw-r--r--src/expr/uninterpreted_constant.h4
-rw-r--r--src/expr/variable_type_map.h2
104 files changed, 130 insertions, 120 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 7fa8b12e7..14d84e320 100644
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -1,3 +1,13 @@
+#####################
+## CMakeLists.txt
+## Top contributors (to current version):
+## Mathias Preiner, Aina Niemetz, Andrew Reynolds
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 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.
+##
libcvc4_add_sources(
array.h
array_store_all.cpp
diff --git a/src/expr/array.h b/src/expr/array.h
index 5bfd39844..620e61ea0 100644
--- a/src/expr/array.h
+++ b/src/expr/array.h
@@ -5,7 +5,7 @@
** Mathias Preiner, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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.cpp b/src/expr/array_store_all.cpp
index 0777bc1cf..92383dcd1 100644
--- a/src/expr/array_store_all.cpp
+++ b/src/expr/array_store_all.cpp
@@ -2,10 +2,10 @@
/*! \file array_store_all.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 7fa25516c..5bb796961 100644
--- a/src/expr/array_store_all.h
+++ b/src/expr/array_store_all.h
@@ -2,10 +2,10 @@
/*! \file array_store_all.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters, Mathias Preiner
+ ** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 743d779ef..0ce3df88d 100644
--- a/src/expr/ascription_type.h
+++ b/src/expr/ascription_type.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 db05dc7e9..34c05976c 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 9fa4b8a84..fcaa47f15 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 c2441d539..37846cf45 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 7cd93c1f3..2862e0d44 100644
--- a/src/expr/attribute_unique_id.h
+++ b/src/expr/attribute_unique_id.h
@@ -5,7 +5,7 @@
** Tim King, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 988965b74..694d75db6 100644
--- a/src/expr/datatype_index.cpp
+++ b/src/expr/datatype_index.cpp
@@ -2,10 +2,10 @@
/*! \file datatype_index.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Tim King
+ ** Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 f871129fe..c7f170ff6 100644
--- a/src/expr/datatype_index.h
+++ b/src/expr/datatype_index.h
@@ -2,10 +2,10 @@
/*! \file datatype_index.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Tim King
+ ** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 fa9bb9793..657298491 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 44482c6cf..e4bae29b8 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 05daae1b8..7eec52b19 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 ee85d5f25..fc414c756 100644
--- a/src/expr/dtype_cons.h
+++ b/src/expr/dtype_cons.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 e29d229af..d6b907cc1 100644
--- a/src/expr/dtype_selector.cpp
+++ b/src/expr/dtype_selector.cpp
@@ -2,10 +2,10 @@
/*! \file dtype_selector.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 6a3a7b268..4ba88c8aa 100644
--- a/src/expr/dtype_selector.h
+++ b/src/expr/dtype_selector.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 6260e4373..059670f6a 100644
--- a/src/expr/emptyset.cpp
+++ b/src/expr/emptyset.cpp
@@ -2,10 +2,10 @@
/*! \file emptyset.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King, Kshitij Bansal
+ ** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 1b5bc6897..511b21c66 100644
--- a/src/expr/emptyset.h
+++ b/src/expr/emptyset.h
@@ -2,10 +2,10 @@
/*! \file emptyset.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Kshitij Bansal, Morgan Deters
+ ** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 1ea1ca6aa..c4353cb00 100644
--- a/src/expr/expr_iomanip.cpp
+++ b/src/expr/expr_iomanip.cpp
@@ -5,7 +5,7 @@
** Tim King, Morgan Deters, Kshitij Bansal
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 f8464392a..82358bb68 100644
--- a/src/expr/expr_iomanip.h
+++ b/src/expr/expr_iomanip.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 12d47c89b..8749bb8d6 100644
--- a/src/expr/expr_manager_scope.h
+++ b/src/expr/expr_manager_scope.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 bac9e3b43..37f0e2527 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 145f64bd3..1458101ca 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -2,10 +2,10 @@
/*! \file expr_manager_template.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds, Dejan Jovanovic
+ ** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 a92081fe8..4fcbe8597 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 0acce2cb0..88c43c9a2 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 10f475911..e440fbc3d 100644
--- a/src/expr/kind_map.h
+++ b/src/expr/kind_map.h
@@ -5,7 +5,7 @@
** Dejan Jovanovic, Mathias Preiner
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 b2e165558..0bda68b7b 100644
--- a/src/expr/kind_template.cpp
+++ b/src/expr/kind_template.cpp
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 8ae7018b3..359e7234a 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 dc984438c..d66a8984b 100644
--- a/src/expr/lazy_proof.cpp
+++ b/src/expr/lazy_proof.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 4368cbb85..691902945 100644
--- a/src/expr/lazy_proof.h
+++ b/src/expr/lazy_proof.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 a7a1a1839..a76779b6e 100644
--- a/src/expr/match_trie.cpp
+++ b/src/expr/match_trie.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 7d330ee0d..37f2a0f71 100644
--- a/src/expr/match_trie.h
+++ b/src/expr/match_trie.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 5f72d5670..a4b9d17c8 100644
--- a/src/expr/metakind_template.cpp
+++ b/src/expr/metakind_template.cpp
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 e1668836b..3a453f9ac 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 90fb1f004..c45295622 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 e431727f4..7ae56d313 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 be436bf8b..9b7b2b036 100644
--- a/src/expr/node_algorithm.cpp
+++ b/src/expr/node_algorithm.cpp
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 4fb40c739..97a0cb6e2 100644
--- a/src/expr/node_algorithm.h
+++ b/src/expr/node_algorithm.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 899961d73..d8e15a60a 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 0f2db7869..6ac26fbee 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -5,7 +5,7 @@
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 abbe998b5..0d62e686d 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -2,10 +2,10 @@
/*! \file node_manager.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Christopher L. Conway, Dejan Jovanovic
+ ** Morgan Deters, Christopher L. Conway, Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 be1fe5a6b..ba8df6fd0 100644
--- a/src/expr/node_manager_attributes.h
+++ b/src/expr/node_manager_attributes.h
@@ -5,7 +5,7 @@
** Morgan Deters, Kshitij Bansal
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 ae76434af..118449b80 100644
--- a/src/expr/node_self_iterator.h
+++ b/src/expr/node_self_iterator.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 5968c4348..75a11eac7 100644
--- a/src/expr/node_traversal.cpp
+++ b/src/expr/node_traversal.cpp
@@ -5,7 +5,7 @@
** Alex Ozdemir, Andres Noetzli
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 586cbb64d..1bc907019 100644
--- a/src/expr/node_traversal.h
+++ b/src/expr/node_traversal.h
@@ -5,7 +5,7 @@
** Alex Ozdemir, Andres Noetzli
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 da1e6a001..58ad36da9 100644
--- a/src/expr/node_trie.cpp
+++ b/src/expr/node_trie.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 c1c7fdfc0..d783000ee 100644
--- a/src/expr/node_trie.h
+++ b/src/expr/node_trie.h
@@ -5,7 +5,7 @@
** Andrew Reynolds, Mathias Preiner
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 908f93104..58e5cebd9 100644
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -5,7 +5,7 @@
** Morgan Deters, Aina Niemetz, Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 fdc07b1ef..03fcaaa3c 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 c960dde09..1ffd39406 100644
--- a/src/expr/node_visitor.h
+++ b/src/expr/node_visitor.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 a9e6d6940..4aac1cac7 100644
--- a/src/expr/proof.cpp
+++ b/src/expr/proof.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 5fbcc4ec8..b5bcc7d50 100644
--- a/src/expr/proof.h
+++ b/src/expr/proof.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 5e942b7a3..7accd08dc 100644
--- a/src/expr/proof_checker.cpp
+++ b/src/expr/proof_checker.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 245bd351a..b12b10ad8 100644
--- a/src/expr/proof_checker.h
+++ b/src/expr/proof_checker.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 93f291e9a..68a819122 100644
--- a/src/expr/proof_generator.cpp
+++ b/src/expr/proof_generator.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 f2ce6c74b..6e6316356 100644
--- a/src/expr/proof_generator.h
+++ b/src/expr/proof_generator.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 5f34127df..3bef451ee 100644
--- a/src/expr/proof_node.cpp
+++ b/src/expr/proof_node.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 930badbb1..d6ead49f2 100644
--- a/src/expr/proof_node.h
+++ b/src/expr/proof_node.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 984379d54..8f8813f41 100644
--- a/src/expr/proof_node_algorithm.cpp
+++ b/src/expr/proof_node_algorithm.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 aec098e17..71d29532f 100644
--- a/src/expr/proof_node_algorithm.h
+++ b/src/expr/proof_node_algorithm.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 66a8197d8..eb298cc83 100644
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 799a50f2e..47fdf3ebd 100644
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 c6bde49fd..db7fb1a6f 100644
--- a/src/expr/proof_node_to_sexpr.cpp
+++ b/src/expr/proof_node_to_sexpr.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 1f38f4cad..16a60e252 100644
--- a/src/expr/proof_node_to_sexpr.h
+++ b/src/expr/proof_node_to_sexpr.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 3368cb856..b97d27c05 100644
--- a/src/expr/proof_node_updater.cpp
+++ b/src/expr/proof_node_updater.cpp
@@ -2,10 +2,10 @@
/*! \file proof_node_updater.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds, Tim King
+ ** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 d5c0a884f..63e764d20 100644
--- a/src/expr/proof_node_updater.h
+++ b/src/expr/proof_node_updater.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 400567b5d..0fea387b5 100644
--- a/src/expr/proof_rule.cpp
+++ b/src/expr/proof_rule.cpp
@@ -2,10 +2,10 @@
/*! \file proof_rule.cpp
** \verbatim
** Top contributors (to current version):
- ** Haniel Barbosa, Andrew Reynolds
+ ** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 a51cb92f0..c621bffdc 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -2,10 +2,10 @@
/*! \file proof_rule.h
** \verbatim
** Top contributors (to current version):
- ** Haniel Barbosa, Andrew Reynolds
+ ** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 7108e4dae..bb02aeb20 100644
--- a/src/expr/proof_step_buffer.cpp
+++ b/src/expr/proof_step_buffer.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 5a9d82e42..4e463a7b3 100644
--- a/src/expr/proof_step_buffer.h
+++ b/src/expr/proof_step_buffer.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 075ca4de4..f4004d2e7 100644
--- a/src/expr/record.cpp
+++ b/src/expr/record.cpp
@@ -5,7 +5,7 @@
** Tim King, Morgan Deters, Piotr Trojanek
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 0a2dcc515..62ccd42db 100644
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 394c1a407..f65558184 100644
--- a/src/expr/sequence.cpp
+++ b/src/expr/sequence.cpp
@@ -2,10 +2,10 @@
/*! \file sequence.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Andres Noetzli
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 5a037752f..27e5cf6f4 100644
--- a/src/expr/sequence.h
+++ b/src/expr/sequence.h
@@ -2,10 +2,10 @@
/*! \file sequence.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Andrew Reynolds, Andres Noetzli
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 e22bd26cf..e34813dcd 100644
--- a/src/expr/skolem_manager.cpp
+++ b/src/expr/skolem_manager.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 1e02d94f4..ec5189d6d 100644
--- a/src/expr/skolem_manager.h
+++ b/src/expr/skolem_manager.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 d6004e7cb..3401e55f7 100644
--- a/src/expr/sygus_datatype.cpp
+++ b/src/expr/sygus_datatype.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds, Haniel Barbosa
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 6fe0531fb..2be3d9d49 100644
--- a/src/expr/sygus_datatype.h
+++ b/src/expr/sygus_datatype.h
@@ -5,7 +5,7 @@
** Andrew Reynolds, Haniel Barbosa
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 1da60eb05..42c9e10d3 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 2824d9f7a..fb6457f2e 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -5,7 +5,7 @@
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 4f92edd31..e5ebd0209 100644
--- a/src/expr/term_canonize.cpp
+++ b/src/expr/term_canonize.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 32ac2fd72..cd15fba41 100644
--- a/src/expr/term_canonize.h
+++ b/src/expr/term_canonize.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 fcb8edfdc..6974e2114 100644
--- a/src/expr/term_context.cpp
+++ b/src/expr/term_context.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 0c51dd493..ec7b488f9 100644
--- a/src/expr/term_context.h
+++ b/src/expr/term_context.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 519012ae8..e5610ef46 100644
--- a/src/expr/term_context_node.cpp
+++ b/src/expr/term_context_node.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 028a590b1..ff8187bbc 100644
--- a/src/expr/term_context_node.h
+++ b/src/expr/term_context_node.h
@@ -1,11 +1,11 @@
/********************* */
-/*! \file term_context.h
+/*! \file term_context_node.h
** \verbatim
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 4deb0627c..64cab7035 100644
--- a/src/expr/term_context_stack.cpp
+++ b/src/expr/term_context_stack.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 6f5dece81..ca72a6acd 100644
--- a/src/expr/term_context_stack.h
+++ b/src/expr/term_context_stack.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 215793318..11e8eb054 100644
--- a/src/expr/term_conversion_proof_generator.cpp
+++ b/src/expr/term_conversion_proof_generator.cpp
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 1153995ad..184f24e13 100644
--- a/src/expr/term_conversion_proof_generator.h
+++ b/src/expr/term_conversion_proof_generator.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 5dd15dd37..dadbdc91d 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 d58643811..5fd68e89e 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 4b8bff946..f385856e0 100644
--- a/src/expr/type_checker.h
+++ b/src/expr/type_checker.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 8e4dd9236..e7685dba8 100644
--- a/src/expr/type_checker_template.cpp
+++ b/src/expr/type_checker_template.cpp
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 411733dcb..312ffe53a 100644
--- a/src/expr/type_checker_util.h
+++ b/src/expr/type_checker_util.h
@@ -5,7 +5,7 @@
** Andres Noetzli
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 c09f98ee1..b41004880 100644
--- a/src/expr/type_matcher.cpp
+++ b/src/expr/type_matcher.cpp
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 17a3917c8..47fc36eee 100644
--- a/src/expr/type_matcher.h
+++ b/src/expr/type_matcher.h
@@ -5,7 +5,7 @@
** Andrew Reynolds
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 7e38fac3d..ba3a26058 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 2c5be80aa..0f134353a 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 9bccd5892..264d065d6 100644
--- a/src/expr/type_properties_template.h
+++ b/src/expr/type_properties_template.h
@@ -5,7 +5,7 @@
** Morgan Deters, Mathias Preiner
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 c9cbcba20..ee490c7c7 100644
--- a/src/expr/uninterpreted_constant.cpp
+++ b/src/expr/uninterpreted_constant.cpp
@@ -2,10 +2,10 @@
/*! \file uninterpreted_constant.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King, Morgan Deters
+ ** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 eb6cc203a..b36bd6b1a 100644
--- a/src/expr/uninterpreted_constant.h
+++ b/src/expr/uninterpreted_constant.h
@@ -2,10 +2,10 @@
/*! \file uninterpreted_constant.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King
+ ** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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 38f6e520d..fd51e0243 100644
--- a/src/expr/variable_type_map.h
+++ b/src/expr/variable_type_map.h
@@ -5,7 +5,7 @@
** 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
- ** in the top-level source directory) and their institutional affiliations.
+ ** 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