Update copyright headers.

78 files changed, 120 insertions, 120 deletions

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 6b277a10a..a006d43b3 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -2,9 +2,9 @@
 /*! \file approx_simplex.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Andres Noetzli
+ **   Tim King, Mathias Preiner, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index 2914c2da8..e72b25274 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.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-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 3930d7359..4892389f2 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -2,9 +2,9 @@
 /*! \file arith_ite_utils.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Aina Niemetz, Kshitij Bansal
+ **   Tim King, Aina Niemetz, Piotr Trojanek
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h
index a9e7aa92c..f86328d5d 100644
--- a/src/theory/arith/arith_ite_utils.h
+++ b/src/theory/arith/arith_ite_utils.h
@@ -2,9 +2,9 @@
 /*! \file arith_ite_utils.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Aina Niemetz
+ **   Tim King, Mathias Preiner, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp
index 7f13ce07d..5c654a90b 100644
--- a/src/theory/arith/arith_msum.cpp
+++ b/src/theory/arith/arith_msum.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/arith_msum.h b/src/theory/arith/arith_msum.h
index 8a9dbf791..4458bdecd 100644
--- a/src/theory/arith/arith_msum.h
+++ b/src/theory/arith/arith_msum.h
@@ -2,9 +2,9 @@
 /*! \file arith_msum.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 222b63db5..e50b79bbc 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 600f38d4f..0563aa1de 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -2,9 +2,9 @@
 /*! \file arith_rewriter.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Morgan Deters
+ **   Dejan Jovanovic, Tim King, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 810eded82..9bd5ad774 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.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-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index bc77f8ec0..5abada539 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -2,9 +2,9 @@
 /*! \file arith_static_learner.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Dejan Jovanovic, Morgan Deters
+ **   Tim King, Dejan Jovanovic, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp
index cb8524a58..3d708c94e 100644
--- a/src/theory/arith/arith_utilities.cpp
+++ b/src/theory/arith/arith_utilities.cpp
@@ -2,9 +2,9 @@
 /*! \file arith_utilities.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 2d466f52f..bfc1fbf88 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -2,9 +2,9 @@
 /*! \file arith_utilities.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andrew Reynolds, Morgan Deters
+ **   Tim King, Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/arithvar.cpp b/src/theory/arith/arithvar.cpp
index 2eb349984..7f2535004 100644
--- a/src/theory/arith/arithvar.cpp
+++ b/src/theory/arith/arithvar.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/arithvar.h b/src/theory/arith/arithvar.h
index 9ab452947..7e0894afa 100644
--- a/src/theory/arith/arithvar.h
+++ b/src/theory/arith/arithvar.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h
index 03b061504..a6569bded 100644
--- a/src/theory/arith/arithvar_node_map.h
+++ b/src/theory/arith/arithvar_node_map.h
@@ -2,9 +2,9 @@
 /*! \file arithvar_node_map.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King
+ **   Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index 983fa2b30..91e922fa1 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -2,9 +2,9 @@
 /*! \file attempt_solution_simplex.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King
+ **   Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h
index 1fd8ee146..4c05372ad 100644
--- a/src/theory/arith/attempt_solution_simplex.h
+++ b/src/theory/arith/attempt_solution_simplex.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-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h
index 43fa4e437..a9466ef45 100644
--- a/src/theory/arith/bound_counts.h
+++ b/src/theory/arith/bound_counts.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Clark Barrett
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index 158a81e8d..758a337ba 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -2,9 +2,9 @@
 /*! \file callbacks.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King
+ **   Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index ee39c76f9..f947ca03b 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Mathias Preiner, Clark Barrett
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 6bfa2c705..4c35e5d19 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -2,9 +2,9 @@
 /*! \file congruence_manager.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Paul Meng, Dejan Jovanovic
+ **   Tim King, Dejan Jovanovic, Paul Meng
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 837b7c07f..96f82b059 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -2,9 +2,9 @@
 /*! \file congruence_manager.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Mathias Preiner, Paul Meng
+ **   Tim King, Mathias Preiner, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 11c6c15a7..abfaca954 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -2,9 +2,9 @@
 /*! \file constraint.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Alex Ozdemir, Aina Niemetz
+ **   Tim King, Alex Ozdemir, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 17b4fa4e3..873b33ced 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Alex Ozdemir, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/constraint_forward.h b/src/theory/arith/constraint_forward.h
index 5f3f2251d..986104539 100644
--- a/src/theory/arith/constraint_forward.h
+++ b/src/theory/arith/constraint_forward.h
@@ -2,9 +2,9 @@
 /*! \file constraint_forward.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King
+ **   Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/cut_log.cpp b/src/theory/arith/cut_log.cpp
index 43ef97123..7eb173f4f 100644
--- a/src/theory/arith/cut_log.cpp
+++ b/src/theory/arith/cut_log.cpp
@@ -2,9 +2,9 @@
 /*! \file cut_log.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King
+ **   Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index a5a729f58..691b4d7fd 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Morgan Deters, Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp
index 35640ac1a..c983b5e76 100644
--- a/src/theory/arith/delta_rational.cpp
+++ b/src/theory/arith/delta_rational.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index 7fd4e2031..1394bef8a 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -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-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 438e11511..7b33d24f7 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -2,9 +2,9 @@
 /*! \file dio_solver.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Dejan Jovanovic
+ **   Tim King, Mathias Preiner, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index fa6c08696..1e5f4a97f 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -2,9 +2,9 @@
 /*! \file dio_solver.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters
+ **   Tim King, Morgan Deters, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index bcb90f8ae..643161758 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -2,9 +2,9 @@
 /*! \file dual_simplex.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Andres Noetzli
+ **   Tim King, Morgan Deters, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h
index ab04bc616..5abce830b 100644
--- a/src/theory/arith/dual_simplex.h
+++ b/src/theory/arith/dual_simplex.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Mathias Preiner, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp
index 12e352e4d..236c09fde 100644
--- a/src/theory/arith/error_set.cpp
+++ b/src/theory/arith/error_set.cpp
@@ -2,9 +2,9 @@
 /*! \file error_set.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King
+ **   Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index 5599cd268..795c86f3b 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -2,9 +2,9 @@
 /*! \file error_set.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters
+ **   Tim King, Mathias Preiner, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 125a24f5e..2135944ab 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -2,9 +2,9 @@
 /*! \file fc_simplex.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Andres Noetzli
+ **   Tim King, Mathias Preiner, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index cfeef1d26..7451d5c48 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.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-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp
index 5ce617061..3714f3eb6 100644
--- a/src/theory/arith/infer_bounds.cpp
+++ b/src/theory/arith/infer_bounds.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h
index bce9a07db..e9ea01071 100644
--- a/src/theory/arith/infer_bounds.h
+++ b/src/theory/arith/infer_bounds.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 8c7d22088..7eb2f3f9e 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -2,9 +2,9 @@
 /*! \file linear_equality.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters
+ **   Tim King, Mathias Preiner, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 1f5bb9ea4..f19b3d6ef 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Mathias Preiner, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp
index c6332fd23..14593f550 100644
--- a/src/theory/arith/matrix.cpp
+++ b/src/theory/arith/matrix.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h
index c845ccb05..22a669f9b 100644
--- a/src/theory/arith/matrix.h
+++ b/src/theory/arith/matrix.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Mathias Preiner, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/nl/nl_constraint.cpp b/src/theory/arith/nl/nl_constraint.cpp
index c4c4dfbe7..ae678ccdf 100644
--- a/src/theory/arith/nl/nl_constraint.cpp
+++ b/src/theory/arith/nl/nl_constraint.cpp
@@ -2,9 +2,9 @@
 /*! \file nl_constraint.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/nl/nl_constraint.h b/src/theory/arith/nl/nl_constraint.h
index e86ac4b66..113c573d8 100644
--- a/src/theory/arith/nl/nl_constraint.h
+++ b/src/theory/arith/nl/nl_constraint.h
@@ -2,9 +2,9 @@
 /*! \file nl_constraint.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
+ **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/nl/nl_lemma_utils.cpp b/src/theory/arith/nl/nl_lemma_utils.cpp
index c1ec42497..0497b5822 100644
--- a/src/theory/arith/nl/nl_lemma_utils.cpp
+++ b/src/theory/arith/nl/nl_lemma_utils.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/nl/nl_lemma_utils.h b/src/theory/arith/nl/nl_lemma_utils.h
index a0fce378f..eaa9adcc3 100644
--- a/src/theory/arith/nl/nl_lemma_utils.h
+++ b/src/theory/arith/nl/nl_lemma_utils.h
@@ -2,9 +2,9 @@
 /*! \file nl_lemma_utils.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/nl/nl_model.cpp b/src/theory/arith/nl/nl_model.cpp
index 2ed901f1f..bf27ecbb3 100644
--- a/src/theory/arith/nl/nl_model.cpp
+++ b/src/theory/arith/nl/nl_model.cpp
@@ -2,9 +2,9 @@
 /*! \file nl_model.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/nl/nl_model.h b/src/theory/arith/nl/nl_model.h
index 7a40e3926..86bac88a9 100644
--- a/src/theory/arith/nl/nl_model.h
+++ b/src/theory/arith/nl/nl_model.h
@@ -2,9 +2,9 @@
 /*! \file nl_model.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/nl/nl_monomial.cpp b/src/theory/arith/nl/nl_monomial.cpp
index 678a94819..1cd0a848d 100644
--- a/src/theory/arith/nl/nl_monomial.cpp
+++ b/src/theory/arith/nl/nl_monomial.cpp
@@ -2,9 +2,9 @@
 /*! \file nl_monomial.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Tim King, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/nl/nl_monomial.h b/src/theory/arith/nl/nl_monomial.h
index b226730ac..e84233e8e 100644
--- a/src/theory/arith/nl/nl_monomial.h
+++ b/src/theory/arith/nl/nl_monomial.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/nl/nl_solver.cpp b/src/theory/arith/nl/nl_solver.cpp
index c24ea41c8..fee89caf6 100644
--- a/src/theory/arith/nl/nl_solver.cpp
+++ b/src/theory/arith/nl/nl_solver.cpp
@@ -2,9 +2,9 @@
 /*! \file nl_solver.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Tim King, Ahmed Irfan
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/nl/nl_solver.h b/src/theory/arith/nl/nl_solver.h
index a2f514b9d..b5176a4dd 100644
--- a/src/theory/arith/nl/nl_solver.h
+++ b/src/theory/arith/nl/nl_solver.h
@@ -2,9 +2,9 @@
 /*! \file nl_solver.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
+ **   Andrew Reynolds, Tim King, Tianyi Liang
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/nl/nonlinear_extension.cpp b/src/theory/arith/nl/nonlinear_extension.cpp
index bf3e7fdda..087d7681a 100644
--- a/src/theory/arith/nl/nonlinear_extension.cpp
+++ b/src/theory/arith/nl/nonlinear_extension.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index 5cf2eb84b..7310233f1 100644
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -2,9 +2,9 @@
 /*! \file nonlinear_extension.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
+ **   Andrew Reynolds, Tim King, Tianyi Liang
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/nl/transcendental_solver.cpp b/src/theory/arith/nl/transcendental_solver.cpp
index 3b5bdb17f..1377aa54a 100644
--- a/src/theory/arith/nl/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental_solver.cpp
@@ -2,9 +2,9 @@
 /*! \file transcendental_solver.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/nl/transcendental_solver.h b/src/theory/arith/nl/transcendental_solver.h
index 0285b49e3..c80fa99e6 100644
--- a/src/theory/arith/nl/transcendental_solver.h
+++ b/src/theory/arith/nl/transcendental_solver.h
@@ -2,9 +2,9 @@
 /*! \file transcendental_solver.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index c0658b9af..c7b4b3625 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 8099339ae..3ab5d907a 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -2,9 +2,9 @@
 /*! \file normal_form.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Andrew Reynolds
+ **   Tim King, Morgan Deters, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 855b673c5..9b2c38d81 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 5006c6a9c..43c265278 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -2,9 +2,9 @@
 /*! \file partial_model.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters
+ **   Tim King, Morgan Deters, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index bf27af36a..50248167e 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 5bd6034d2..6a297113e 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -2,9 +2,9 @@
 /*! \file simplex.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Clark Barrett
+ **   Tim King, Mathias Preiner, Clark Barrett
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/simplex_update.cpp b/src/theory/arith/simplex_update.cpp
index 011e07143..613a30a07 100644
--- a/src/theory/arith/simplex_update.cpp
+++ b/src/theory/arith/simplex_update.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h
index b1153d36f..7668bb2f0 100644
--- a/src/theory/arith/simplex_update.h
+++ b/src/theory/arith/simplex_update.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-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 1876f4b88..71d5fda8b 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -2,9 +2,9 @@
 /*! \file soi_simplex.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Andres Noetzli
+ **   Tim King, Morgan Deters, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index 6fd8cf7c1..95c19a50a 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.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-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 82b46bf30..4c119ba36 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 3f3bf883a..1affc61d4 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.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-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/tableau_sizes.cpp b/src/theory/arith/tableau_sizes.cpp
index aec7b0384..f54c3dfef 100644
--- a/src/theory/arith/tableau_sizes.cpp
+++ b/src/theory/arith/tableau_sizes.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/tableau_sizes.h b/src/theory/arith/tableau_sizes.h
index 95820dc93..085ff9640 100644
--- a/src/theory/arith/tableau_sizes.h
+++ b/src/theory/arith/tableau_sizes.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index e65369f96..b63566c29 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -2,9 +2,9 @@
 /*! \file theory_arith.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Dejan Jovanovic, Andrew Reynolds
+ **   Tim King, Andrew Reynolds, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 8672f7145..5b68e3e7a 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Alex Ozdemir, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 443aaa9b7..ed0adc59e 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2,9 +2,9 @@
 /*! \file theory_arith_private.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andrew Reynolds, Morgan Deters
+ **   Tim King, Andrew Reynolds, Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 822b38f69..8252326bf 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/theory_arith_private_forward.h b/src/theory/arith/theory_arith_private_forward.h
index 84dea1b4e..363debf30 100644
--- a/src/theory/arith/theory_arith_private_forward.h
+++ b/src/theory/arith/theory_arith_private_forward.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 8b587c0fb..2d3d8a28b 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -2,9 +2,9 @@
 /*! \file theory_arith_type_rules.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Morgan Deters, Christopher L. Conway
+ **   Dejan Jovanovic, Christopher L. Conway, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim
diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index bb1612928..ff6308122 100644
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.h
@@ -2,9 +2,9 @@
 /*! \file type_enumerator.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King
+ **   Morgan Deters, Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** 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.\endverbatim