summaryrefslogtreecommitdiff
path: root/src/theory
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory')
-rw-r--r--src/theory/arith/approx_simplex.cpp4
-rw-r--r--src/theory/arith/approx_simplex.h4
-rw-r--r--src/theory/arith/arith_ite_utils.cpp4
-rw-r--r--src/theory/arith/arith_ite_utils.h4
-rw-r--r--src/theory/arith/arith_rewriter.cpp2
-rw-r--r--src/theory/arith/arith_rewriter.h2
-rw-r--r--src/theory/arith/arith_static_learner.cpp2
-rw-r--r--src/theory/arith/arith_static_learner.h4
-rw-r--r--src/theory/arith/arith_utilities.h4
-rw-r--r--src/theory/arith/arithvar.cpp4
-rw-r--r--src/theory/arith/arithvar.h4
-rw-r--r--src/theory/arith/arithvar_node_map.h4
-rw-r--r--src/theory/arith/attempt_solution_simplex.cpp4
-rw-r--r--src/theory/arith/attempt_solution_simplex.h4
-rw-r--r--src/theory/arith/bound_counts.h4
-rw-r--r--src/theory/arith/callbacks.cpp4
-rw-r--r--src/theory/arith/callbacks.h4
-rw-r--r--src/theory/arith/congruence_manager.cpp4
-rw-r--r--src/theory/arith/congruence_manager.h4
-rw-r--r--src/theory/arith/constraint.cpp4
-rw-r--r--src/theory/arith/constraint.h4
-rw-r--r--src/theory/arith/constraint_forward.h4
-rw-r--r--src/theory/arith/cut_log.cpp4
-rw-r--r--src/theory/arith/cut_log.h2
-rw-r--r--src/theory/arith/delta_rational.cpp4
-rw-r--r--src/theory/arith/delta_rational.h2
-rw-r--r--src/theory/arith/dio_solver.cpp4
-rw-r--r--src/theory/arith/dio_solver.h4
-rw-r--r--src/theory/arith/dual_simplex.cpp4
-rw-r--r--src/theory/arith/dual_simplex.h4
-rw-r--r--src/theory/arith/error_set.cpp4
-rw-r--r--src/theory/arith/error_set.h4
-rw-r--r--src/theory/arith/fc_simplex.cpp4
-rw-r--r--src/theory/arith/fc_simplex.h4
-rw-r--r--src/theory/arith/infer_bounds.cpp4
-rw-r--r--src/theory/arith/infer_bounds.h4
-rw-r--r--src/theory/arith/linear_equality.cpp4
-rw-r--r--src/theory/arith/linear_equality.h4
-rw-r--r--src/theory/arith/matrix.cpp4
-rw-r--r--src/theory/arith/matrix.h4
-rw-r--r--src/theory/arith/nonlinear_extension.cpp6
-rw-r--r--src/theory/arith/nonlinear_extension.h2
-rw-r--r--src/theory/arith/normal_form.cpp4
-rw-r--r--src/theory/arith/normal_form.h4
-rw-r--r--src/theory/arith/partial_model.cpp4
-rw-r--r--src/theory/arith/partial_model.h4
-rw-r--r--src/theory/arith/pseudoboolean_proc.cpp4
-rw-r--r--src/theory/arith/pseudoboolean_proc.h4
-rw-r--r--src/theory/arith/simplex.cpp4
-rw-r--r--src/theory/arith/simplex.h4
-rw-r--r--src/theory/arith/simplex_update.cpp4
-rw-r--r--src/theory/arith/simplex_update.h4
-rw-r--r--src/theory/arith/soi_simplex.cpp4
-rw-r--r--src/theory/arith/soi_simplex.h4
-rw-r--r--src/theory/arith/tableau.cpp4
-rw-r--r--src/theory/arith/tableau.h4
-rw-r--r--src/theory/arith/tableau_sizes.cpp4
-rw-r--r--src/theory/arith/tableau_sizes.h4
-rw-r--r--src/theory/arith/theory_arith.cpp2
-rw-r--r--src/theory/arith/theory_arith.h2
-rw-r--r--src/theory/arith/theory_arith_private.cpp4
-rw-r--r--src/theory/arith/theory_arith_private.h4
-rw-r--r--src/theory/arith/theory_arith_private_forward.h4
-rw-r--r--src/theory/arith/theory_arith_type_rules.h2
-rw-r--r--src/theory/arith/type_enumerator.h4
-rw-r--r--src/theory/arrays/array_info.cpp2
-rw-r--r--src/theory/arrays/array_info.h2
-rw-r--r--src/theory/arrays/array_proof_reconstruction.cpp2
-rw-r--r--src/theory/arrays/array_proof_reconstruction.h4
-rw-r--r--src/theory/arrays/static_fact_manager.cpp4
-rw-r--r--src/theory/arrays/static_fact_manager.h4
-rw-r--r--src/theory/arrays/theory_arrays.cpp2
-rw-r--r--src/theory/arrays/theory_arrays.h2
-rw-r--r--src/theory/arrays/theory_arrays_rewriter.cpp4
-rw-r--r--src/theory/arrays/theory_arrays_rewriter.h2
-rw-r--r--src/theory/arrays/theory_arrays_type_rules.h4
-rw-r--r--src/theory/arrays/type_enumerator.h2
-rw-r--r--src/theory/arrays/union_find.cpp4
-rw-r--r--src/theory/arrays/union_find.h4
-rw-r--r--src/theory/assertion.cpp2
-rw-r--r--src/theory/atom_requests.cpp4
-rw-r--r--src/theory/atom_requests.h4
-rw-r--r--src/theory/booleans/circuit_propagator.cpp4
-rw-r--r--src/theory/booleans/circuit_propagator.h2
-rw-r--r--src/theory/booleans/theory_bool.cpp4
-rw-r--r--src/theory/booleans/theory_bool.h4
-rw-r--r--src/theory/booleans/theory_bool_rewriter.cpp2
-rw-r--r--src/theory/booleans/theory_bool_rewriter.h4
-rw-r--r--src/theory/booleans/theory_bool_type_rules.h2
-rw-r--r--src/theory/booleans/type_enumerator.h4
-rw-r--r--src/theory/builtin/theory_builtin.cpp4
-rw-r--r--src/theory/builtin/theory_builtin.h4
-rw-r--r--src/theory/builtin/theory_builtin_rewriter.cpp4
-rw-r--r--src/theory/builtin/theory_builtin_rewriter.h4
-rw-r--r--src/theory/builtin/theory_builtin_type_rules.h2
-rw-r--r--src/theory/builtin/type_enumerator.h4
-rw-r--r--src/theory/bv/abstraction.cpp4
-rw-r--r--src/theory/bv/abstraction.h4
-rw-r--r--src/theory/bv/aig_bitblaster.cpp4
-rw-r--r--src/theory/bv/bitblast_strategies_template.h4
-rw-r--r--src/theory/bv/bitblast_utils.h4
-rw-r--r--src/theory/bv/bitblaster_template.h4
-rw-r--r--src/theory/bv/bv_eager_solver.cpp4
-rw-r--r--src/theory/bv/bv_eager_solver.h4
-rw-r--r--src/theory/bv/bv_inequality_graph.cpp4
-rw-r--r--src/theory/bv/bv_inequality_graph.h4
-rw-r--r--src/theory/bv/bv_quick_check.cpp2
-rw-r--r--src/theory/bv/bv_quick_check.h4
-rw-r--r--src/theory/bv/bv_subtheory.h2
-rw-r--r--src/theory/bv/bv_subtheory_algebraic.cpp2
-rw-r--r--src/theory/bv/bv_subtheory_algebraic.h4
-rw-r--r--src/theory/bv/bv_subtheory_bitblast.cpp2
-rw-r--r--src/theory/bv/bv_subtheory_bitblast.h2
-rw-r--r--src/theory/bv/bv_subtheory_core.cpp2
-rw-r--r--src/theory/bv/bv_subtheory_core.h2
-rw-r--r--src/theory/bv/bv_subtheory_inequality.cpp4
-rw-r--r--src/theory/bv/bv_subtheory_inequality.h2
-rw-r--r--src/theory/bv/bv_to_bool.cpp4
-rw-r--r--src/theory/bv/bv_to_bool.h4
-rw-r--r--src/theory/bv/bvintropow2.cpp4
-rw-r--r--src/theory/bv/bvintropow2.h4
-rw-r--r--src/theory/bv/cd_set_collection.h4
-rw-r--r--src/theory/bv/eager_bitblaster.cpp2
-rw-r--r--src/theory/bv/lazy_bitblaster.cpp2
-rw-r--r--src/theory/bv/slicer.cpp4
-rw-r--r--src/theory/bv/slicer.h4
-rw-r--r--src/theory/bv/theory_bv.cpp4
-rw-r--r--src/theory/bv/theory_bv.h2
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules.h2
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h2
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_core.h2
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_normalization.h2
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h2
-rw-r--r--src/theory/bv/theory_bv_rewrite_rules_simplification.h2
-rw-r--r--src/theory/bv/theory_bv_rewriter.cpp4
-rw-r--r--src/theory/bv/theory_bv_rewriter.h2
-rw-r--r--src/theory/bv/theory_bv_type_rules.h4
-rw-r--r--src/theory/bv/theory_bv_utils.cpp4
-rw-r--r--src/theory/bv/theory_bv_utils.h2
-rw-r--r--src/theory/bv/type_enumerator.h4
-rw-r--r--src/theory/datatypes/datatypes_rewriter.h4
-rw-r--r--src/theory/datatypes/datatypes_sygus.cpp2
-rw-r--r--src/theory/datatypes/datatypes_sygus.h4
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp2
-rw-r--r--src/theory/datatypes/theory_datatypes.h2
-rw-r--r--src/theory/datatypes/theory_datatypes_type_rules.h4
-rw-r--r--src/theory/datatypes/type_enumerator.cpp2
-rw-r--r--src/theory/datatypes/type_enumerator.h4
-rw-r--r--src/theory/example/ecdata.cpp4
-rw-r--r--src/theory/example/ecdata.h4
-rw-r--r--src/theory/example/theory_uf_tim.cpp4
-rw-r--r--src/theory/example/theory_uf_tim.h4
-rw-r--r--src/theory/fp/theory_fp.cpp4
-rw-r--r--src/theory/fp/theory_fp.h4
-rw-r--r--src/theory/fp/theory_fp_rewriter.cpp4
-rw-r--r--src/theory/fp/theory_fp_rewriter.h4
-rw-r--r--src/theory/fp/theory_fp_type_rules.h4
-rw-r--r--src/theory/idl/idl_assertion.cpp4
-rw-r--r--src/theory/idl/idl_assertion.h4
-rw-r--r--src/theory/idl/idl_assertion_db.cpp4
-rw-r--r--src/theory/idl/idl_assertion_db.h4
-rw-r--r--src/theory/idl/idl_model.cpp4
-rw-r--r--src/theory/idl/idl_model.h4
-rw-r--r--src/theory/idl/theory_idl.cpp2
-rw-r--r--src/theory/idl/theory_idl.h4
-rw-r--r--src/theory/interrupted.h4
-rw-r--r--src/theory/ite_utilities.cpp2
-rw-r--r--src/theory/ite_utilities.h4
-rw-r--r--src/theory/logic_info.cpp2
-rw-r--r--src/theory/logic_info.h4
-rw-r--r--src/theory/output_channel.h2
-rw-r--r--src/theory/quantifiers/alpha_equivalence.cpp2
-rw-r--r--src/theory/quantifiers/alpha_equivalence.h4
-rw-r--r--src/theory/quantifiers/ambqi_builder.cpp4
-rw-r--r--src/theory/quantifiers/ambqi_builder.h4
-rw-r--r--src/theory/quantifiers/anti_skolem.cpp2
-rw-r--r--src/theory/quantifiers/anti_skolem.h2
-rw-r--r--src/theory/quantifiers/bounded_integers.cpp4
-rw-r--r--src/theory/quantifiers/bounded_integers.h2
-rw-r--r--src/theory/quantifiers/candidate_generator.cpp2
-rw-r--r--src/theory/quantifiers/candidate_generator.h2
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.cpp2
-rw-r--r--src/theory/quantifiers/ce_guided_instantiation.h2
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.cpp2
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv.h4
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv_ei.cpp4
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv_ei.h4
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv_sol.cpp4
-rw-r--r--src/theory/quantifiers/ce_guided_single_inv_sol.h4
-rw-r--r--src/theory/quantifiers/ceg_instantiator.cpp2
-rw-r--r--src/theory/quantifiers/ceg_instantiator.h2
-rw-r--r--src/theory/quantifiers/ceg_t_instantiator.cpp2
-rw-r--r--src/theory/quantifiers/ceg_t_instantiator.h2
-rw-r--r--src/theory/quantifiers/conjecture_generator.cpp2
-rw-r--r--src/theory/quantifiers/conjecture_generator.h4
-rw-r--r--src/theory/quantifiers/equality_infer.cpp2
-rw-r--r--src/theory/quantifiers/equality_infer.h2
-rw-r--r--src/theory/quantifiers/first_order_model.cpp2
-rw-r--r--src/theory/quantifiers/first_order_model.h4
-rw-r--r--src/theory/quantifiers/full_model_check.cpp2
-rw-r--r--src/theory/quantifiers/full_model_check.h2
-rw-r--r--src/theory/quantifiers/fun_def_engine.cpp4
-rw-r--r--src/theory/quantifiers/fun_def_engine.h4
-rw-r--r--src/theory/quantifiers/fun_def_process.cpp4
-rw-r--r--src/theory/quantifiers/fun_def_process.h4
-rw-r--r--src/theory/quantifiers/inst_match.cpp2
-rw-r--r--src/theory/quantifiers/inst_match.h4
-rw-r--r--src/theory/quantifiers/inst_match_generator.cpp2
-rw-r--r--src/theory/quantifiers/inst_match_generator.h4
-rw-r--r--src/theory/quantifiers/inst_propagator.cpp2
-rw-r--r--src/theory/quantifiers/inst_propagator.h2
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.cpp4
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.h2
-rw-r--r--src/theory/quantifiers/inst_strategy_e_matching.cpp2
-rw-r--r--src/theory/quantifiers/inst_strategy_e_matching.h2
-rw-r--r--src/theory/quantifiers/instantiation_engine.cpp2
-rw-r--r--src/theory/quantifiers/instantiation_engine.h2
-rw-r--r--src/theory/quantifiers/local_theory_ext.cpp4
-rw-r--r--src/theory/quantifiers/local_theory_ext.h2
-rw-r--r--src/theory/quantifiers/macros.cpp2
-rw-r--r--src/theory/quantifiers/macros.h2
-rw-r--r--src/theory/quantifiers/model_builder.cpp2
-rw-r--r--src/theory/quantifiers/model_builder.h2
-rw-r--r--src/theory/quantifiers/model_engine.cpp2
-rw-r--r--src/theory/quantifiers/model_engine.h2
-rw-r--r--src/theory/quantifiers/quant_conflict_find.cpp4
-rw-r--r--src/theory/quantifiers/quant_conflict_find.h4
-rw-r--r--src/theory/quantifiers/quant_equality_engine.cpp4
-rw-r--r--src/theory/quantifiers/quant_equality_engine.h4
-rw-r--r--src/theory/quantifiers/quant_split.cpp2
-rw-r--r--src/theory/quantifiers/quant_split.h2
-rw-r--r--src/theory/quantifiers/quant_util.cpp2
-rw-r--r--src/theory/quantifiers/quant_util.h4
-rw-r--r--src/theory/quantifiers/quantifiers_attributes.cpp4
-rw-r--r--src/theory/quantifiers/quantifiers_attributes.h4
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.cpp2
-rw-r--r--src/theory/quantifiers/quantifiers_rewriter.h2
-rw-r--r--src/theory/quantifiers/relevant_domain.cpp2
-rw-r--r--src/theory/quantifiers/relevant_domain.h2
-rw-r--r--src/theory/quantifiers/rewrite_engine.cpp2
-rw-r--r--src/theory/quantifiers/rewrite_engine.h2
-rw-r--r--src/theory/quantifiers/symmetry_breaking.cpp4
-rw-r--r--src/theory/quantifiers/symmetry_breaking.h2
-rw-r--r--src/theory/quantifiers/term_database.cpp2
-rw-r--r--src/theory/quantifiers/term_database.h2
-rw-r--r--src/theory/quantifiers/theory_quantifiers.cpp2
-rw-r--r--src/theory/quantifiers/theory_quantifiers.h2
-rw-r--r--src/theory/quantifiers/theory_quantifiers_type_rules.h4
-rw-r--r--src/theory/quantifiers/trigger.cpp2
-rw-r--r--src/theory/quantifiers/trigger.h4
-rw-r--r--src/theory/quantifiers_engine.cpp2
-rw-r--r--src/theory/quantifiers_engine.h2
-rw-r--r--src/theory/rep_set.cpp2
-rw-r--r--src/theory/rep_set.h2
-rw-r--r--src/theory/rewriter.cpp2
-rw-r--r--src/theory/rewriter.h4
-rw-r--r--src/theory/rewriter_attributes.h4
-rw-r--r--src/theory/rewriter_tables_template.h2
-rw-r--r--src/theory/sep/theory_sep.cpp4
-rw-r--r--src/theory/sep/theory_sep.h4
-rw-r--r--src/theory/sep/theory_sep_rewriter.cpp4
-rw-r--r--src/theory/sep/theory_sep_rewriter.h4
-rw-r--r--src/theory/sep/theory_sep_type_rules.h4
-rw-r--r--src/theory/sets/normal_form.h4
-rw-r--r--src/theory/sets/rels_utils.h4
-rw-r--r--src/theory/sets/theory_sets.cpp4
-rw-r--r--src/theory/sets/theory_sets.h4
-rw-r--r--src/theory/sets/theory_sets_private.cpp4
-rw-r--r--src/theory/sets/theory_sets_private.h4
-rw-r--r--src/theory/sets/theory_sets_rels.cpp4
-rw-r--r--src/theory/sets/theory_sets_rels.h4
-rw-r--r--src/theory/sets/theory_sets_rewriter.cpp4
-rw-r--r--src/theory/sets/theory_sets_rewriter.h4
-rw-r--r--src/theory/sets/theory_sets_type_enumerator.h4
-rw-r--r--src/theory/sets/theory_sets_type_rules.h4
-rw-r--r--src/theory/shared_terms_database.cpp2
-rw-r--r--src/theory/shared_terms_database.h2
-rw-r--r--src/theory/sort_inference.cpp4
-rw-r--r--src/theory/sort_inference.h4
-rw-r--r--src/theory/strings/regexp_operation.cpp4
-rw-r--r--src/theory/strings/regexp_operation.h2
-rw-r--r--src/theory/strings/theory_strings.cpp2
-rw-r--r--src/theory/strings/theory_strings.h2
-rw-r--r--src/theory/strings/theory_strings_preprocess.cpp2
-rw-r--r--src/theory/strings/theory_strings_preprocess.h2
-rw-r--r--src/theory/strings/theory_strings_rewriter.cpp2
-rw-r--r--src/theory/strings/theory_strings_rewriter.h2
-rw-r--r--src/theory/strings/theory_strings_type_rules.h4
-rw-r--r--src/theory/strings/type_enumerator.h4
-rw-r--r--src/theory/substitutions.cpp2
-rw-r--r--src/theory/substitutions.h2
-rw-r--r--src/theory/term_registration_visitor.cpp2
-rw-r--r--src/theory/term_registration_visitor.h4
-rw-r--r--src/theory/theory.cpp4
-rw-r--r--src/theory/theory.h4
-rw-r--r--src/theory/theory_engine.cpp4
-rw-r--r--src/theory/theory_engine.h2
-rw-r--r--src/theory/theory_model.cpp2
-rw-r--r--src/theory/theory_model.h2
-rw-r--r--src/theory/theory_registrar.h4
-rw-r--r--src/theory/theory_test_utils.h2
-rw-r--r--src/theory/theory_traits_template.h4
-rw-r--r--src/theory/type_enumerator.h2
-rw-r--r--src/theory/type_enumerator_template.cpp4
-rw-r--r--src/theory/uf/equality_engine.cpp2
-rw-r--r--src/theory/uf/equality_engine.h2
-rw-r--r--src/theory/uf/equality_engine_types.h4
-rw-r--r--src/theory/uf/symmetry_breaker.cpp4
-rw-r--r--src/theory/uf/symmetry_breaker.h4
-rw-r--r--src/theory/uf/theory_uf.cpp4
-rw-r--r--src/theory/uf/theory_uf.h2
-rw-r--r--src/theory/uf/theory_uf_model.cpp2
-rw-r--r--src/theory/uf/theory_uf_model.h4
-rw-r--r--src/theory/uf/theory_uf_rewriter.h4
-rw-r--r--src/theory/uf/theory_uf_strong_solver.cpp2
-rw-r--r--src/theory/uf/theory_uf_strong_solver.h4
-rw-r--r--src/theory/uf/theory_uf_type_rules.h4
-rw-r--r--src/theory/unconstrained_simplifier.cpp4
-rw-r--r--src/theory/unconstrained_simplifier.h4
-rw-r--r--src/theory/valuation.cpp4
-rw-r--r--src/theory/valuation.h2
321 files changed, 516 insertions, 516 deletions
diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 9b8efb783..a500ec55d 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
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 8832fce71..234fd10c0 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -2,9 +2,9 @@
/*! \file approx_simplex.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 6695e641f..3e767b6db 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, Morgan Deters, Kshitij Bansal
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 44c3c080b..47f1caf9e 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, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 4d7e9deef..4684ec4a3 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, Morgan Deters, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 3cb502249..38b6c9451 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.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-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 7c648c941..bd13bd874 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-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 4951d34d7..cca4b2285 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, Morgan Deters, Dejan Jovanovic
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 ba1a9b037..68d4d8f1a 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, Morgan Deters, Dejan Jovanovic
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 1ab125a47..d63dc6fca 100644
--- a/src/theory/arith/arithvar.cpp
+++ b/src/theory/arith/arithvar.cpp
@@ -2,9 +2,9 @@
/*! \file arithvar.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 f9ff6da26..d1f71803f 100644
--- a/src/theory/arith/arithvar.h
+++ b/src/theory/arith/arithvar.h
@@ -2,9 +2,9 @@
/*! \file arithvar.h
** \verbatim
** Top contributors (to current version):
- ** Tim King
+ ** Tim King, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 da0b03ef2..62a8301e7 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, Morgan Deters, Dejan Jovanovic
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 333b0bfae..fe6755951 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, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 00df8c075..73798f94c 100644
--- a/src/theory/arith/attempt_solution_simplex.h
+++ b/src/theory/arith/attempt_solution_simplex.h
@@ -2,9 +2,9 @@
/*! \file attempt_solution_simplex.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 b6417ed63..70ddc2bfa 100644
--- a/src/theory/arith/bound_counts.h
+++ b/src/theory/arith/bound_counts.h
@@ -2,9 +2,9 @@
/*! \file bound_counts.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters, Clark Barrett
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 766c7424a..73aa5c34e 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, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 606f4111b..3710ac5c0 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -2,9 +2,9 @@
/*! \file callbacks.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters, Clark Barrett
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 25822afdf..04d8d50ea 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, Dejan Jovanovic, Morgan Deters, Andrew Reynolds
+ ** Tim King, Paul Meng, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 8d92a4153..228f29838 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, Morgan Deters, Dejan Jovanovic, Andrew Reynolds
+ ** Tim King, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 a82ec4c95..9ba4074c1 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, Morgan Deters, Dejan Jovanovic
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 3ae2d0b29..662327301 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -2,9 +2,9 @@
/*! \file constraint.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 1ebffc1b0..80a0fa0a4 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, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 3af2a7178..ad04cfe22 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, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 e6475b58e..77273f609 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-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 207fd79a4..467f868a3 100644
--- a/src/theory/arith/delta_rational.cpp
+++ b/src/theory/arith/delta_rational.cpp
@@ -2,9 +2,9 @@
/*! \file delta_rational.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 afe4c0eb0..b0ea8a9c1 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, Morgan Deters, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 f34bbc67a..d862dabbd 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, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 6c53d6ad0..2b8b64e75 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, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 72d7a8602..a40db89a7 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
+ ** Tim King, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 25461972c..2911592c7 100644
--- a/src/theory/arith/dual_simplex.h
+++ b/src/theory/arith/dual_simplex.h
@@ -2,9 +2,9 @@
/*! \file dual_simplex.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 7c8efc4e8..0bd283252 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, Morgan Deters
+ ** Tim King, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 4b88e3f50..e09a85aaf 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, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 ef5ff93c7..59bb35293 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
+ ** Tim King, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 ca1e666fc..c4f996f9f 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -2,9 +2,9 @@
/*! \file fc_simplex.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 96b2a6189..e9a85d7d7 100644
--- a/src/theory/arith/infer_bounds.cpp
+++ b/src/theory/arith/infer_bounds.cpp
@@ -2,9 +2,9 @@
/*! \file infer_bounds.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King
+ ** Tim King, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 f65952f7c..720b5704d 100644
--- a/src/theory/arith/infer_bounds.h
+++ b/src/theory/arith/infer_bounds.h
@@ -2,9 +2,9 @@
/*! \file infer_bounds.h
** \verbatim
** Top contributors (to current version):
- ** Tim King
+ ** Tim King, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 7e1d84ebb..9d414fcd7 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
+ ** Tim King, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 aa6b10c5e..c2fa99e31 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -2,9 +2,9 @@
/*! \file linear_equality.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Clark Barrett, Morgan Deters
+ ** Tim King, Paul Meng, Clark Barrett
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 25ed96b0c..2817a1dca 100644
--- a/src/theory/arith/matrix.cpp
+++ b/src/theory/arith/matrix.cpp
@@ -2,9 +2,9 @@
/*! \file matrix.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King
+ ** Tim King, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 f0d4ec42c..2e0a1ebb2 100644
--- a/src/theory/arith/matrix.h
+++ b/src/theory/arith/matrix.h
@@ -2,9 +2,9 @@
/*! \file matrix.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters, Clark Barrett
+ ** Tim King, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 26f232142..02266f331 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -1,10 +1,10 @@
/********************* */
-/*! \file nl_alg.cpp
+/*! \file nonlinear_extension.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Tim King, Andrew Reynolds, Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index 7c7bfbce9..dc93046c0 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -2,7 +2,7 @@
/*! \file nonlinear_extension.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds
+ ** Tim King
** This file is part of the CVC4 project.
** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 14607f4e4..605dfe495 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -2,9 +2,9 @@
/*! \file normal_form.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters, Dejan Jovanovic
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 d0c9df1a6..4a2b6114f 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, Dejan Jovanovic
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 632be2a81..2c50a1b1d 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -2,9 +2,9 @@
/*! \file partial_model.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 b5eafb2c4..50fb2cb48 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, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/pseudoboolean_proc.cpp b/src/theory/arith/pseudoboolean_proc.cpp
index 0c1496a89..230cfb7ca 100644
--- a/src/theory/arith/pseudoboolean_proc.cpp
+++ b/src/theory/arith/pseudoboolean_proc.cpp
@@ -2,9 +2,9 @@
/*! \file pseudoboolean_proc.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King
+ ** Tim King, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/pseudoboolean_proc.h b/src/theory/arith/pseudoboolean_proc.h
index 23065ca48..471e37fa1 100644
--- a/src/theory/arith/pseudoboolean_proc.h
+++ b/src/theory/arith/pseudoboolean_proc.h
@@ -2,9 +2,9 @@
/*! \file pseudoboolean_proc.h
** \verbatim
** Top contributors (to current version):
- ** Tim King
+ ** Tim King, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 9dd13711c..a7c5a1ac1 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -2,9 +2,9 @@
/*! \file simplex.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 b4cd54a78..13fba2c77 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, Morgan Deters, Clark Barrett
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 adf0dc039..e5bcfa612 100644
--- a/src/theory/arith/simplex_update.cpp
+++ b/src/theory/arith/simplex_update.cpp
@@ -2,9 +2,9 @@
/*! \file simplex_update.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King
+ ** Tim King, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 2c02e3f77..7b487c8a3 100644
--- a/src/theory/arith/simplex_update.h
+++ b/src/theory/arith/simplex_update.h
@@ -2,9 +2,9 @@
/*! \file simplex_update.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 0a437cde0..b2f7b08b5 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
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 c2afe062a..5f2233b3f 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -2,9 +2,9 @@
/*! \file soi_simplex.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 0bd130985..080104118 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -2,9 +2,9 @@
/*! \file tableau.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 c4c8cfba3..caf360153 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -2,9 +2,9 @@
/*! \file tableau.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 08f7a69d8..6d7b2e7da 100644
--- a/src/theory/arith/tableau_sizes.cpp
+++ b/src/theory/arith/tableau_sizes.cpp
@@ -2,9 +2,9 @@
/*! \file tableau_sizes.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 635330798..da6f0f828 100644
--- a/src/theory/arith/tableau_sizes.h
+++ b/src/theory/arith/tableau_sizes.h
@@ -2,9 +2,9 @@
/*! \file tableau_sizes.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 f390503a3..c0af3827e 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tim King, Morgan Deters, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 5dcea4be0..e1226279a 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, Morgan Deters, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 250317b78..c5e8de96a 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, Morgan Deters, Martin Brain
+ ** Tim King, Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 a56028f32..b2471c5e8 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -2,9 +2,9 @@
/*! \file theory_arith_private.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Martin Brain, Morgan Deters
+ ** Tim King, Martin Brain, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 ffab816f1..f52a80e68 100644
--- a/src/theory/arith/theory_arith_private_forward.h
+++ b/src/theory/arith/theory_arith_private_forward.h
@@ -2,9 +2,9 @@
/*! \file theory_arith_private_forward.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 071ec9391..e13dee0fe 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Christopher L. Conway
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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 36b7b543a..5d6b936a7 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, Andrew Reynolds
+ ** Morgan Deters, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index c63d528a7..fc86e00de 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Clark Barrett, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/arrays/array_info.h b/src/theory/arrays/array_info.h
index 11455a97d..cc5fddf25 100644
--- a/src/theory/arrays/array_info.h
+++ b/src/theory/arrays/array_info.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Clark Barrett, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/arrays/array_proof_reconstruction.cpp b/src/theory/arrays/array_proof_reconstruction.cpp
index 5ecccdd53..471084d6f 100644
--- a/src/theory/arrays/array_proof_reconstruction.cpp
+++ b/src/theory/arrays/array_proof_reconstruction.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Guy Katz
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/arrays/array_proof_reconstruction.h b/src/theory/arrays/array_proof_reconstruction.h
index ef3e09aed..c5ba21569 100644
--- a/src/theory/arrays/array_proof_reconstruction.h
+++ b/src/theory/arrays/array_proof_reconstruction.h
@@ -2,9 +2,9 @@
/*! \file array_proof_reconstruction.h
** \verbatim
** Top contributors (to current version):
- ** Guy Katz
+ ** Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/arrays/static_fact_manager.cpp b/src/theory/arrays/static_fact_manager.cpp
index da1d7bba9..a3f1ae929 100644
--- a/src/theory/arrays/static_fact_manager.cpp
+++ b/src/theory/arrays/static_fact_manager.cpp
@@ -2,9 +2,9 @@
/*! \file static_fact_manager.cpp
** \verbatim
** Top contributors (to current version):
- ** Clark Barrett, Tim King
+ ** Clark Barrett, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/arrays/static_fact_manager.h b/src/theory/arrays/static_fact_manager.h
index d40f56e61..53d935813 100644
--- a/src/theory/arrays/static_fact_manager.h
+++ b/src/theory/arrays/static_fact_manager.h
@@ -2,9 +2,9 @@
/*! \file static_fact_manager.h
** \verbatim
** Top contributors (to current version):
- ** Clark Barrett, Tim King, Morgan Deters
+ ** Clark Barrett, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index e712a51b6..bde88abab 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Clark Barrett, Morgan Deters, Guy Katz
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 48da4c681..7e8831733 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Clark Barrett, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp
index f1cf1d320..c9ceae857 100644
--- a/src/theory/arrays/theory_arrays_rewriter.cpp
+++ b/src/theory/arrays/theory_arrays_rewriter.cpp
@@ -2,9 +2,9 @@
/*! \file theory_arrays_rewriter.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King
+ ** Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index e63c224a0..4a05f3789 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Clark Barrett, Morgan Deters, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/arrays/theory_arrays_type_rules.h b/src/theory/arrays/theory_arrays_type_rules.h
index 082fa2580..4d3112129 100644
--- a/src/theory/arrays/theory_arrays_type_rules.h
+++ b/src/theory/arrays/theory_arrays_type_rules.h
@@ -2,9 +2,9 @@
/*! \file theory_arrays_type_rules.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Clark Barrett, Guy Katz
+ ** Morgan Deters, Clark Barrett, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/arrays/type_enumerator.h b/src/theory/arrays/type_enumerator.h
index 25a8ca3f2..4314fad83 100644
--- a/src/theory/arrays/type_enumerator.h
+++ b/src/theory/arrays/type_enumerator.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Clark Barrett, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/arrays/union_find.cpp b/src/theory/arrays/union_find.cpp
index 7899e85d5..73bedf6fc 100644
--- a/src/theory/arrays/union_find.cpp
+++ b/src/theory/arrays/union_find.cpp
@@ -2,9 +2,9 @@
/*! \file union_find.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King
+ ** Morgan Deters, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/arrays/union_find.h b/src/theory/arrays/union_find.h
index 5d59e8dcd..e896784ef 100644
--- a/src/theory/arrays/union_find.h
+++ b/src/theory/arrays/union_find.h
@@ -2,9 +2,9 @@
/*! \file union_find.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King
+ ** Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/assertion.cpp b/src/theory/assertion.cpp
index 99ddbc6e9..8c9de809c 100644
--- a/src/theory/assertion.cpp
+++ b/src/theory/assertion.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/atom_requests.cpp b/src/theory/atom_requests.cpp
index e3f30cc6e..5605a6754 100644
--- a/src/theory/atom_requests.cpp
+++ b/src/theory/atom_requests.cpp
@@ -2,9 +2,9 @@
/*! \file atom_requests.cpp
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/atom_requests.h b/src/theory/atom_requests.h
index 7f6194192..f36d23dc9 100644
--- a/src/theory/atom_requests.h
+++ b/src/theory/atom_requests.h
@@ -2,9 +2,9 @@
/*! \file atom_requests.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 8e9116543..11b6185ab 100644
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -2,9 +2,9 @@
/*! \file circuit_propagator.cpp
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 5a6e46269..03c811eee 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Clark Barrett
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index de27fc834..afe673449 100644
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -2,9 +2,9 @@
/*! \file theory_bool.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Dejan Jovanovic, Tim King
+ ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index 353143c43..9d5966628 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -2,9 +2,9 @@
/*! \file theory_bool.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King, Dejan Jovanovic
+ ** Morgan Deters, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp
index 32f69e037..b5f7e37d4 100644
--- a/src/theory/booleans/theory_bool_rewriter.cpp
+++ b/src/theory/booleans/theory_bool_rewriter.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tim King, Dejan Jovanovic, Kshitij Bansal
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/booleans/theory_bool_rewriter.h b/src/theory/booleans/theory_bool_rewriter.h
index b7512ad09..d5b2aba21 100644
--- a/src/theory/booleans/theory_bool_rewriter.h
+++ b/src/theory/booleans/theory_bool_rewriter.h
@@ -2,9 +2,9 @@
/*! \file theory_bool_rewriter.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Dejan Jovanovic, Tim King
+ ** Morgan Deters, Dejan Jovanovic, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index 050796e50..7de38b6af 100644
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Christopher L. Conway
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/booleans/type_enumerator.h b/src/theory/booleans/type_enumerator.h
index e91f47317..b0759cbb2 100644
--- a/src/theory/booleans/type_enumerator.h
+++ b/src/theory/booleans/type_enumerator.h
@@ -2,9 +2,9 @@
/*! \file type_enumerator.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King, Andrew Reynolds
+ ** Morgan Deters, Paul Meng, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index cea66dafe..5f3f1c843 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -2,9 +2,9 @@
/*! \file theory_builtin.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King
+ ** Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 205db5b4d..cfc59272c 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -2,9 +2,9 @@
/*! \file theory_builtin.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King
+ ** Morgan Deters, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index a2fb3f3f6..32b35dfe8 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -2,9 +2,9 @@
/*! \file theory_builtin_rewriter.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Dejan Jovanovic, Tim King
+ ** Morgan Deters, Dejan Jovanovic, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index 9ac259027..8ca2c538e 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -2,9 +2,9 @@
/*! \file theory_builtin_rewriter.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Dejan Jovanovic, Tim King
+ ** Morgan Deters, Dejan Jovanovic, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 85adfb41c..7f86c7d0d 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Christopher L. Conway
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
index 6ee540004..1ab732710 100644
--- a/src/theory/builtin/type_enumerator.h
+++ b/src/theory/builtin/type_enumerator.h
@@ -2,9 +2,9 @@
/*! \file type_enumerator.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds, Tim King
+ ** Morgan Deters, Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/abstraction.cpp b/src/theory/bv/abstraction.cpp
index dc5520411..4ef484594 100644
--- a/src/theory/bv/abstraction.cpp
+++ b/src/theory/bv/abstraction.cpp
@@ -2,9 +2,9 @@
/*! \file abstraction.cpp
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King, Morgan Deters
+ ** Liana Hadarean, Guy Katz, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/abstraction.h b/src/theory/bv/abstraction.h
index 5d48b926e..ed4b8aeb6 100644
--- a/src/theory/bv/abstraction.h
+++ b/src/theory/bv/abstraction.h
@@ -2,9 +2,9 @@
/*! \file abstraction.h
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King
+ ** Liana Hadarean, Guy Katz, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index 35cd48058..fad1ea89b 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -2,9 +2,9 @@
/*! \file aig_bitblaster.cpp
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King, Morgan Deters
+ ** Liana Hadarean, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast_strategies_template.h
index 3a9106984..a93e3416c 100644
--- a/src/theory/bv/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast_strategies_template.h
@@ -2,9 +2,9 @@
/*! \file bitblast_strategies_template.h
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King, Morgan Deters
+ ** Liana Hadarean, Tim King, Clark Barrett
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bitblast_utils.h b/src/theory/bv/bitblast_utils.h
index baa85f64b..1d6920007 100644
--- a/src/theory/bv/bitblast_utils.h
+++ b/src/theory/bv/bitblast_utils.h
@@ -2,9 +2,9 @@
/*! \file bitblast_utils.h
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King
+ ** Liana Hadarean, Paul Meng, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h
index 8a7ccf8c6..b6b2e2926 100644
--- a/src/theory/bv/bitblaster_template.h
+++ b/src/theory/bv/bitblaster_template.h
@@ -2,9 +2,9 @@
/*! \file bitblaster_template.h
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King, Morgan Deters
+ ** Liana Hadarean, Tim King, Clark Barrett
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_eager_solver.cpp b/src/theory/bv/bv_eager_solver.cpp
index cad59f5ca..05b314fad 100644
--- a/src/theory/bv/bv_eager_solver.cpp
+++ b/src/theory/bv/bv_eager_solver.cpp
@@ -2,9 +2,9 @@
/*! \file bv_eager_solver.cpp
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King
+ ** Liana Hadarean, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_eager_solver.h b/src/theory/bv/bv_eager_solver.h
index 7ac05379b..380d06349 100644
--- a/src/theory/bv/bv_eager_solver.h
+++ b/src/theory/bv/bv_eager_solver.h
@@ -2,9 +2,9 @@
/*! \file bv_eager_solver.h
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King
+ ** Liana Hadarean, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_inequality_graph.cpp b/src/theory/bv/bv_inequality_graph.cpp
index f03d3a683..d0b299d3b 100644
--- a/src/theory/bv/bv_inequality_graph.cpp
+++ b/src/theory/bv/bv_inequality_graph.cpp
@@ -2,9 +2,9 @@
/*! \file bv_inequality_graph.cpp
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King, Morgan Deters
+ ** Liana Hadarean, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_inequality_graph.h b/src/theory/bv/bv_inequality_graph.h
index 72f6dbfd1..f85d8a835 100644
--- a/src/theory/bv/bv_inequality_graph.h
+++ b/src/theory/bv/bv_inequality_graph.h
@@ -2,9 +2,9 @@
/*! \file bv_inequality_graph.h
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King
+ ** Liana Hadarean, Tim King, Clark Barrett
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_quick_check.cpp b/src/theory/bv/bv_quick_check.cpp
index 0a9ae819d..b347ddccf 100644
--- a/src/theory/bv/bv_quick_check.cpp
+++ b/src/theory/bv/bv_quick_check.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_quick_check.h b/src/theory/bv/bv_quick_check.h
index 96f9c246e..dcd3f1062 100644
--- a/src/theory/bv/bv_quick_check.h
+++ b/src/theory/bv/bv_quick_check.h
@@ -2,9 +2,9 @@
/*! \file bv_quick_check.h
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King, Morgan Deters
+ ** Liana Hadarean, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index 3c5777af9..4f074a202 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Dejan Jovanovic, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 60515b2d1..c5313b9e7 100644
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_subtheory_algebraic.h b/src/theory/bv/bv_subtheory_algebraic.h
index 0e0e02151..3730ebc90 100644
--- a/src/theory/bv/bv_subtheory_algebraic.h
+++ b/src/theory/bv/bv_subtheory_algebraic.h
@@ -2,9 +2,9 @@
/*! \file bv_subtheory_algebraic.h
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Morgan Deters, Tim King
+ ** Liana Hadarean, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index 7b7d38307..77e596d1f 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Dejan Jovanovic, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_subtheory_bitblast.h b/src/theory/bv/bv_subtheory_bitblast.h
index fe16d2702..c9fb81195 100644
--- a/src/theory/bv/bv_subtheory_bitblast.h
+++ b/src/theory/bv/bv_subtheory_bitblast.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Dejan Jovanovic, Liana Hadarean, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index ccce819e6..54f454dca 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_subtheory_core.h b/src/theory/bv/bv_subtheory_core.h
index 22219b5d0..662f8835e 100644
--- a/src/theory/bv/bv_subtheory_core.h
+++ b/src/theory/bv/bv_subtheory_core.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index 1fe096214..d662f056b 100644
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -2,9 +2,9 @@
/*! \file bv_subtheory_inequality.cpp
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Andrew Reynolds, Tim King
+ ** Liana Hadarean, Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_subtheory_inequality.h b/src/theory/bv/bv_subtheory_inequality.h
index 617e3b761..37d3723ac 100644
--- a/src/theory/bv/bv_subtheory_inequality.h
+++ b/src/theory/bv/bv_subtheory_inequality.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index 5b7fe160c..9718e9a2f 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -2,9 +2,9 @@
/*! \file bv_to_bool.cpp
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King
+ ** Liana Hadarean, Clark Barrett, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bv_to_bool.h b/src/theory/bv/bv_to_bool.h
index 7e351c9c6..a934cf045 100644
--- a/src/theory/bv/bv_to_bool.h
+++ b/src/theory/bv/bv_to_bool.h
@@ -2,9 +2,9 @@
/*! \file bv_to_bool.h
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King
+ ** Liana Hadarean, Clark Barrett, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bvintropow2.cpp b/src/theory/bv/bvintropow2.cpp
index 022aaf2fd..e7b6caaef 100644
--- a/src/theory/bv/bvintropow2.cpp
+++ b/src/theory/bv/bvintropow2.cpp
@@ -2,9 +2,9 @@
/*! \file bvintropow2.cpp
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Morgan Deters, Tim King
+ ** Liana Hadarean, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/bvintropow2.h b/src/theory/bv/bvintropow2.h
index 09d3d9259..935cbb7ed 100644
--- a/src/theory/bv/bvintropow2.h
+++ b/src/theory/bv/bvintropow2.h
@@ -2,9 +2,9 @@
/*! \file bvintropow2.h
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Morgan Deters, Tim King
+ ** Liana Hadarean, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/cd_set_collection.h b/src/theory/bv/cd_set_collection.h
index 456552ebd..397c872b2 100644
--- a/src/theory/bv/cd_set_collection.h
+++ b/src/theory/bv/cd_set_collection.h
@@ -2,9 +2,9 @@
/*! \file cd_set_collection.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 053986b8c..29f6e7800 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Tim King, Guy Katz
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index e89cacb40..32aff1fb0 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index 150f73ac9..bf5152893 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -2,9 +2,9 @@
/*! \file slicer.cpp
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King, Morgan Deters
+ ** Liana Hadarean, Tim King, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/slicer.h b/src/theory/bv/slicer.h
index 4eae27963..b594d5fec 100644
--- a/src/theory/bv/slicer.h
+++ b/src/theory/bv/slicer.h
@@ -2,9 +2,9 @@
/*! \file slicer.h
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King
+ ** Liana Hadarean, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 9db909c22..1a59687db 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -2,9 +2,9 @@
/*! \file theory_bv.cpp
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King, Dejan Jovanovic
+ ** Liana Hadarean, Andrew Reynolds, Clark Barrett
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 62eb6f6b5..f8d3e6509 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Morgan Deters, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 39e8e38cd..9f148d823 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Dejan Jovanovic, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index 3605a6970..b53f7bb08 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Clark Barrett, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index 395949f03..5b8eaea60 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Dejan Jovanovic, Liana Hadarean, Clark Barrett
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 89bb3d7ac..46297cb68 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Clark Barrett, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 052bc8c1a..f73c4fb0f 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Clark Barrett, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index c49319387..c7247f260 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Clark Barrett, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp
index df21093c1..a96777954 100644
--- a/src/theory/bv/theory_bv_rewriter.cpp
+++ b/src/theory/bv/theory_bv_rewriter.cpp
@@ -2,9 +2,9 @@
/*! \file theory_bv_rewriter.cpp
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Morgan Deters, Clark Barrett
+ ** Liana Hadarean, Clark Barrett, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 8c3a20661..4fe4f4708 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Morgan Deters, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 1c59ff8b1..957d15ec4 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -2,9 +2,9 @@
/*! \file theory_bv_type_rules.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Dejan Jovanovic, Liana Hadarean
+ ** Tim King, Dejan Jovanovic, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index f743e2d64..6697f9060 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -2,9 +2,9 @@
/*! \file theory_bv_utils.cpp
** \verbatim
** Top contributors (to current version):
- ** Liana Hadarean, Tim King
+ ** Liana Hadarean, Tim King, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 1210e8495..5bae1af4f 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Liana Hadarean, Dejan Jovanovic, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/bv/type_enumerator.h b/src/theory/bv/type_enumerator.h
index 3c984def8..ad18f901c 100644
--- a/src/theory/bv/type_enumerator.h
+++ b/src/theory/bv/type_enumerator.h
@@ -2,9 +2,9 @@
/*! \file type_enumerator.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King, Andrew Reynolds
+ ** Morgan Deters, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 30cdf8893..e8ec72b37 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -2,9 +2,9 @@
/*! \file datatypes_rewriter.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Tim King
+ ** Andrew Reynolds, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index f5ae05bc3..e308ad845 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/datatypes/datatypes_sygus.h b/src/theory/datatypes/datatypes_sygus.h
index 155b15e52..739cbb5e0 100644
--- a/src/theory/datatypes/datatypes_sygus.h
+++ b/src/theory/datatypes/datatypes_sygus.h
@@ -2,9 +2,9 @@
/*! \file datatypes_sygus.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 1a466ff8a..22065e082 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 98d8d53b1..ae299029a 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 0540044b5..2d7866b7b 100644
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -2,9 +2,9 @@
/*! \file theory_datatypes_type_rules.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds, Tim King
+ ** Tim King, Morgan Deters, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp
index 60d319da3..ee03b7815 100644
--- a/src/theory/datatypes/type_enumerator.cpp
+++ b/src/theory/datatypes/type_enumerator.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 5889090aa..8cf4ab3d9 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -2,9 +2,9 @@
/*! \file type_enumerator.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Tim King
+ ** Andrew Reynolds, Morgan Deters, Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/example/ecdata.cpp b/src/theory/example/ecdata.cpp
index a85db3cc9..427146429 100644
--- a/src/theory/example/ecdata.cpp
+++ b/src/theory/example/ecdata.cpp
@@ -2,9 +2,9 @@
/*! \file ecdata.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King
+ ** Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/example/ecdata.h b/src/theory/example/ecdata.h
index cd582c150..475d0e615 100644
--- a/src/theory/example/ecdata.h
+++ b/src/theory/example/ecdata.h
@@ -2,9 +2,9 @@
/*! \file ecdata.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King
+ ** Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/example/theory_uf_tim.cpp b/src/theory/example/theory_uf_tim.cpp
index 825c8fbe4..da87058fe 100644
--- a/src/theory/example/theory_uf_tim.cpp
+++ b/src/theory/example/theory_uf_tim.cpp
@@ -2,9 +2,9 @@
/*! \file theory_uf_tim.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King
+ ** Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/example/theory_uf_tim.h b/src/theory/example/theory_uf_tim.h
index 7470b4d57..a62d9fbe5 100644
--- a/src/theory/example/theory_uf_tim.h
+++ b/src/theory/example/theory_uf_tim.h
@@ -2,9 +2,9 @@
/*! \file theory_uf_tim.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King
+ ** Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index f3212277b..6c8e49e74 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -2,9 +2,9 @@
/*! \file theory_fp.cpp
** \verbatim
** Top contributors (to current version):
- ** Martin Brain, Tim King
+ ** Martin Brain, Tim King, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index b1915e3b7..0355ed811 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -2,9 +2,9 @@
/*! \file theory_fp.h
** \verbatim
** Top contributors (to current version):
- ** Martin Brain, Tim King
+ ** Martin Brain, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 612112db7..ba4bf9228 100644
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -2,10 +2,10 @@
/*! \file theory_fp_rewriter.cpp
** \verbatim
** Top contributors (to current version):
- ** Martin Brain, Tim King, Clark Barrett
+ ** Martin Brain, Paul Meng, Tim King
** Copyright (c) 2013 University of Oxford
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/fp/theory_fp_rewriter.h b/src/theory/fp/theory_fp_rewriter.h
index 93547b4de..d2a9a0466 100644
--- a/src/theory/fp/theory_fp_rewriter.h
+++ b/src/theory/fp/theory_fp_rewriter.h
@@ -2,9 +2,9 @@
/*! \file theory_fp_rewriter.h
** \verbatim
** Top contributors (to current version):
- ** Martin Brain
+ ** Martin Brain, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
index edda93de8..296a2f475 100644
--- a/src/theory/fp/theory_fp_type_rules.h
+++ b/src/theory/fp/theory_fp_type_rules.h
@@ -2,9 +2,9 @@
/*! \file theory_fp_type_rules.h
** \verbatim
** Top contributors (to current version):
- ** Martin Brain
+ ** Martin Brain, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/idl/idl_assertion.cpp b/src/theory/idl/idl_assertion.cpp
index 1d42f771d..7738c6c2f 100644
--- a/src/theory/idl/idl_assertion.cpp
+++ b/src/theory/idl/idl_assertion.cpp
@@ -2,9 +2,9 @@
/*! \file idl_assertion.cpp
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/idl/idl_assertion.h b/src/theory/idl/idl_assertion.h
index 5db1db0fe..e70e2d4b8 100644
--- a/src/theory/idl/idl_assertion.h
+++ b/src/theory/idl/idl_assertion.h
@@ -2,9 +2,9 @@
/*! \file idl_assertion.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/idl/idl_assertion_db.cpp b/src/theory/idl/idl_assertion_db.cpp
index c08cb644f..55ef29bbc 100644
--- a/src/theory/idl/idl_assertion_db.cpp
+++ b/src/theory/idl/idl_assertion_db.cpp
@@ -2,9 +2,9 @@
/*! \file idl_assertion_db.cpp
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/idl/idl_assertion_db.h b/src/theory/idl/idl_assertion_db.h
index 6481deba5..a89c8e483 100644
--- a/src/theory/idl/idl_assertion_db.h
+++ b/src/theory/idl/idl_assertion_db.h
@@ -2,9 +2,9 @@
/*! \file idl_assertion_db.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/idl/idl_model.cpp b/src/theory/idl/idl_model.cpp
index 4d2071962..5096c1197 100644
--- a/src/theory/idl/idl_model.cpp
+++ b/src/theory/idl/idl_model.cpp
@@ -2,9 +2,9 @@
/*! \file idl_model.cpp
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/idl/idl_model.h b/src/theory/idl/idl_model.h
index 35663a256..e4a9f05ef 100644
--- a/src/theory/idl/idl_model.h
+++ b/src/theory/idl/idl_model.h
@@ -2,9 +2,9 @@
/*! \file idl_model.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/idl/theory_idl.cpp b/src/theory/idl/theory_idl.cpp
index 8f85dc9b0..60d04fe4d 100644
--- a/src/theory/idl/theory_idl.cpp
+++ b/src/theory/idl/theory_idl.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Dejan Jovanovic, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/idl/theory_idl.h b/src/theory/idl/theory_idl.h
index 1d2aecad6..625770869 100644
--- a/src/theory/idl/theory_idl.h
+++ b/src/theory/idl/theory_idl.h
@@ -2,9 +2,9 @@
/*! \file theory_idl.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/interrupted.h b/src/theory/interrupted.h
index e56f3513c..d53ee9d54 100644
--- a/src/theory/interrupted.h
+++ b/src/theory/interrupted.h
@@ -2,9 +2,9 @@
/*! \file interrupted.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King
+ ** Morgan Deters, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/ite_utilities.cpp b/src/theory/ite_utilities.cpp
index 419e5b4dd..e32fa1e71 100644
--- a/src/theory/ite_utilities.cpp
+++ b/src/theory/ite_utilities.cpp
@@ -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-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/ite_utilities.h b/src/theory/ite_utilities.h
index 98141d4e3..29f4f7f1f 100644
--- a/src/theory/ite_utilities.h
+++ b/src/theory/ite_utilities.h
@@ -2,9 +2,9 @@
/*! \file ite_utilities.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters
+ ** Tim King, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/logic_info.cpp b/src/theory/logic_info.cpp
index 3a89ca048..ad3a010c0 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Tim King, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/logic_info.h b/src/theory/logic_info.h
index 6efdd4615..a502041f5 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -2,9 +2,9 @@
/*! \file logic_info.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King, Dejan Jovanovic
+ ** Morgan Deters, Tim King, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/output_channel.h b/src/theory/output_channel.h
index 4ca113eed..355936d77 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Liana Hadarean, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index a5fd34c64..6af5bd92f 100644
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/alpha_equivalence.h b/src/theory/quantifiers/alpha_equivalence.h
index 8e7556eb6..3c04393d2 100644
--- a/src/theory/quantifiers/alpha_equivalence.h
+++ b/src/theory/quantifiers/alpha_equivalence.h
@@ -2,9 +2,9 @@
/*! \file alpha_equivalence.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index bc638080f..1bab682f4 100644
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -2,9 +2,9 @@
/*! \file ambqi_builder.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King, Andrew Reynolds
+ ** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h
index 68cb27038..89cd8b6a8 100644
--- a/src/theory/quantifiers/ambqi_builder.h
+++ b/src/theory/quantifiers/ambqi_builder.h
@@ -2,9 +2,9 @@
/*! \file ambqi_builder.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King, Clark Barrett
+ ** Morgan Deters, Tim King, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/anti_skolem.cpp b/src/theory/quantifiers/anti_skolem.cpp
index 908aeecfd..e63dc6abb 100644
--- a/src/theory/quantifiers/anti_skolem.cpp
+++ b/src/theory/quantifiers/anti_skolem.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/anti_skolem.h b/src/theory/quantifiers/anti_skolem.h
index c996b171e..078675420 100644
--- a/src/theory/quantifiers/anti_skolem.h
+++ b/src/theory/quantifiers/anti_skolem.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-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 41face8f7..6920fc539 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -2,9 +2,9 @@
/*! \file bounded_integers.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h
index f367b328c..f0a3a85f5 100644
--- a/src/theory/quantifiers/bounded_integers.h
+++ b/src/theory/quantifiers/bounded_integers.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp
index 17c8e0300..01e71be95 100644
--- a/src/theory/quantifiers/candidate_generator.cpp
+++ b/src/theory/quantifiers/candidate_generator.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/candidate_generator.h b/src/theory/quantifiers/candidate_generator.h
index 4fc6969fc..dd71ef56e 100644
--- a/src/theory/quantifiers/candidate_generator.h
+++ b/src/theory/quantifiers/candidate_generator.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Clark Barrett
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 08d705fa8..e82af63e4 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 9eef7f070..56a71e43e 100644
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.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-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 33dfa19bc..41b262ddf 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 449ab7189..daa298610 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -2,9 +2,9 @@
/*! \file ce_guided_single_inv.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King, Clark Barrett
+ ** Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/ce_guided_single_inv_ei.cpp b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp
index 6394fca3d..1d0dc7bd4 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_ei.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_ei.cpp
@@ -2,9 +2,9 @@
/*! \file ce_guided_single_inv_ei.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/ce_guided_single_inv_ei.h b/src/theory/quantifiers/ce_guided_single_inv_ei.h
index 42e0b0820..9964d32f2 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_ei.h
+++ b/src/theory/quantifiers/ce_guided_single_inv_ei.h
@@ -2,9 +2,9 @@
/*! \file ce_guided_single_inv_ei.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 8ecd32ab1..79b4f2c0e 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -2,9 +2,9 @@
/*! \file ce_guided_single_inv_sol.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h
index cb6f6bc41..61ade265f 100644
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h
@@ -2,9 +2,9 @@
/*! \file ce_guided_single_inv_sol.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp
index 521f1c978..05e86c9e8 100644
--- a/src/theory/quantifiers/ceg_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_instantiator.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h
index f9a711704..aed1be3a4 100644
--- a/src/theory/quantifiers/ceg_instantiator.h
+++ b/src/theory/quantifiers/ceg_instantiator.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-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp
index 3282872d6..23b0b85fe 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.cpp
+++ b/src/theory/quantifiers/ceg_t_instantiator.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
index 2df7946d5..787c2547a 100644
--- a/src/theory/quantifiers/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp
index a0c607e0e..c25c52243 100644
--- a/src/theory/quantifiers/conjecture_generator.cpp
+++ b/src/theory/quantifiers/conjecture_generator.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Clark Barrett, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index c89d0f2ee..e4246e2ab 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -2,9 +2,9 @@
/*! \file conjecture_generator.h
** \verbatim
** Top contributors (to current version):
- ** Clark Barrett, Tim King, Andrew Reynolds
+ ** Clark Barrett, Paul Meng, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp
index 5190025ee..66ca38e8c 100644
--- a/src/theory/quantifiers/equality_infer.cpp
+++ b/src/theory/quantifiers/equality_infer.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h
index 80d6ef98b..4c1c93c17 100644
--- a/src/theory/quantifiers/equality_infer.h
+++ b/src/theory/quantifiers/equality_infer.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-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 612646b42..0ffa0c115 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index e4adfc8bd..8a00c70f6 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -2,9 +2,9 @@
/*! \file first_order_model.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Tim King
+ ** Andrew Reynolds, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index c41d09187..82a1c6626 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index 3e7c9918e..c5d005969 100644
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/fun_def_engine.cpp b/src/theory/quantifiers/fun_def_engine.cpp
index cf1d14663..354d90b8b 100644
--- a/src/theory/quantifiers/fun_def_engine.cpp
+++ b/src/theory/quantifiers/fun_def_engine.cpp
@@ -2,9 +2,9 @@
/*! \file fun_def_engine.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/fun_def_engine.h b/src/theory/quantifiers/fun_def_engine.h
index 3b95281c0..ea1dbbc59 100644
--- a/src/theory/quantifiers/fun_def_engine.h
+++ b/src/theory/quantifiers/fun_def_engine.h
@@ -2,9 +2,9 @@
/*! \file fun_def_engine.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp
index 20a7ed00f..064d6c8d9 100644
--- a/src/theory/quantifiers/fun_def_process.cpp
+++ b/src/theory/quantifiers/fun_def_process.cpp
@@ -2,9 +2,9 @@
/*! \file fun_def_process.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/fun_def_process.h b/src/theory/quantifiers/fun_def_process.h
index 28a1f3cfa..e7a53324d 100644
--- a/src/theory/quantifiers/fun_def_process.h
+++ b/src/theory/quantifiers/fun_def_process.h
@@ -2,9 +2,9 @@
/*! \file fun_def_process.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 9a3fe379c..e24b8f96a 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index 4c62dd296..8d41c75d8 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -2,9 +2,9 @@
/*! \file inst_match.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Tim King
+ ** Andrew Reynolds, Morgan Deters, Francois Bobot
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp
index 8d7b321c8..9202062a4 100644
--- a/src/theory/quantifiers/inst_match_generator.cpp
+++ b/src/theory/quantifiers/inst_match_generator.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h
index 910cde131..882d786fb 100644
--- a/src/theory/quantifiers/inst_match_generator.h
+++ b/src/theory/quantifiers/inst_match_generator.h
@@ -2,9 +2,9 @@
/*! \file inst_match_generator.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds, Clark Barrett
+ ** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/inst_propagator.cpp b/src/theory/quantifiers/inst_propagator.cpp
index 6457de145..49de464b1 100644
--- a/src/theory/quantifiers/inst_propagator.cpp
+++ b/src/theory/quantifiers/inst_propagator.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h
index 6201cf152..6c058c258 100644
--- a/src/theory/quantifiers/inst_propagator.h
+++ b/src/theory/quantifiers/inst_propagator.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 58bebef35..0c2822cd9 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -2,9 +2,9 @@
/*! \file inst_strategy_cbqi.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Tim King
+ ** Andrew Reynolds, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index 6c2dc9275..a1e6a2bdc 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp
index 2a7b589d0..582b6ba7c 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.cpp
+++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/inst_strategy_e_matching.h b/src/theory/quantifiers/inst_strategy_e_matching.h
index e6d993294..5a4f8e499 100644
--- a/src/theory/quantifiers/inst_strategy_e_matching.h
+++ b/src/theory/quantifiers/inst_strategy_e_matching.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp
index afeed1e5d..c90a3c386 100644
--- a/src/theory/quantifiers/instantiation_engine.cpp
+++ b/src/theory/quantifiers/instantiation_engine.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h
index 79963cb45..308024f4d 100644
--- a/src/theory/quantifiers/instantiation_engine.h
+++ b/src/theory/quantifiers/instantiation_engine.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp
index 09ed99735..cf5fe3b50 100644
--- a/src/theory/quantifiers/local_theory_ext.cpp
+++ b/src/theory/quantifiers/local_theory_ext.cpp
@@ -2,9 +2,9 @@
/*! \file local_theory_ext.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h
index 04a6bc9c8..68b6a562a 100644
--- a/src/theory/quantifiers/local_theory_ext.h
+++ b/src/theory/quantifiers/local_theory_ext.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-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 99dbb7ab9..6b071f8f7 100644
--- a/src/theory/quantifiers/macros.cpp
+++ b/src/theory/quantifiers/macros.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/macros.h b/src/theory/quantifiers/macros.h
index 60af7ad0a..bd6a96cc0 100644
--- a/src/theory/quantifiers/macros.h
+++ b/src/theory/quantifiers/macros.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 055c9e31c..41c68a117 100644
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/model_builder.h b/src/theory/quantifiers/model_builder.h
index 3f548c9fd..2900320bb 100644
--- a/src/theory/quantifiers/model_builder.h
+++ b/src/theory/quantifiers/model_builder.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 2faf13f1a..c43187163 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/model_engine.h b/src/theory/quantifiers/model_engine.h
index 728539e91..ad77ae8dc 100644
--- a/src/theory/quantifiers/model_engine.h
+++ b/src/theory/quantifiers/model_engine.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index f462535dd..20d470de3 100644
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -2,9 +2,9 @@
/*! \file quant_conflict_find.cpp
** \verbatim
** Top contributors (to current version):
- ** Clark Barrett, Tim King, Andrew Reynolds
+ ** Clark Barrett, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h
index dc8a9acb2..794787bfc 100644
--- a/src/theory/quantifiers/quant_conflict_find.h
+++ b/src/theory/quantifiers/quant_conflict_find.h
@@ -2,9 +2,9 @@
/*! \file quant_conflict_find.h
** \verbatim
** Top contributors (to current version):
- ** Clark Barrett, Tim King, Andrew Reynolds
+ ** Clark Barrett, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp
index 46a8b7ce2..b40212872 100644
--- a/src/theory/quantifiers/quant_equality_engine.cpp
+++ b/src/theory/quantifiers/quant_equality_engine.cpp
@@ -2,9 +2,9 @@
/*! \file quant_equality_engine.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h
index 26654de4d..f827b4fd7 100644
--- a/src/theory/quantifiers/quant_equality_engine.h
+++ b/src/theory/quantifiers/quant_equality_engine.h
@@ -2,9 +2,9 @@
/*! \file quant_equality_engine.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp
index 63935f170..282ff3bc4 100644
--- a/src/theory/quantifiers/quant_split.cpp
+++ b/src/theory/quantifiers/quant_split.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/quant_split.h b/src/theory/quantifiers/quant_split.h
index 3e3b08814..daf4114bc 100644
--- a/src/theory/quantifiers/quant_split.h
+++ b/src/theory/quantifiers/quant_split.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-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 0ddc447be..21ad032f3 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index fcc162a7a..42fb7381c 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -2,9 +2,9 @@
/*! \file quant_util.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds, Tim King
+ ** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index b797f4ce9..2261fd036 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -2,9 +2,9 @@
/*! \file quantifiers_attributes.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Tim King
+ ** Andrew Reynolds, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 53cef796a..93a4ef408 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -2,9 +2,9 @@
/*! \file quantifiers_attributes.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds, Tim King
+ ** Morgan Deters, Paul Meng, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 4c395f59d..2d4a6e99c 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index bb1d77dfe..0edea5fae 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 63231dec7..9bc47a507 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/relevant_domain.h b/src/theory/quantifiers/relevant_domain.h
index be6ebcd9d..6594b7352 100644
--- a/src/theory/quantifiers/relevant_domain.h
+++ b/src/theory/quantifiers/relevant_domain.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp
index 3e6b0ffa9..f60d27cb9 100644
--- a/src/theory/quantifiers/rewrite_engine.cpp
+++ b/src/theory/quantifiers/rewrite_engine.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/rewrite_engine.h b/src/theory/quantifiers/rewrite_engine.h
index ef3337e53..34994f993 100644
--- a/src/theory/quantifiers/rewrite_engine.h
+++ b/src/theory/quantifiers/rewrite_engine.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/symmetry_breaking.cpp b/src/theory/quantifiers/symmetry_breaking.cpp
index 2a2b13583..a8218480b 100644
--- a/src/theory/quantifiers/symmetry_breaking.cpp
+++ b/src/theory/quantifiers/symmetry_breaking.cpp
@@ -2,9 +2,9 @@
/*! \file symmetry_breaking.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Tim King, Morgan Deters
+ ** Andrew Reynolds, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h
index e682955e7..466e6d9a9 100644
--- a/src/theory/quantifiers/symmetry_breaking.h
+++ b/src/theory/quantifiers/symmetry_breaking.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-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 30b17d42c..7d4f5b433 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Francois Bobot, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index c018172b5..912961e19 100644
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index 7321f00c4..64160dc71 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 38552d333..d1412500e 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Tim King, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/theory_quantifiers_type_rules.h b/src/theory/quantifiers/theory_quantifiers_type_rules.h
index 6ba57afb4..f3e68b9f9 100644
--- a/src/theory/quantifiers/theory_quantifiers_type_rules.h
+++ b/src/theory/quantifiers/theory_quantifiers_type_rules.h
@@ -2,9 +2,9 @@
/*! \file theory_quantifiers_type_rules.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Tim King
+ ** Andrew Reynolds, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 5b02a877a..20933c7f7 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers/trigger.h b/src/theory/quantifiers/trigger.h
index 8d8f01926..afab98cee 100644
--- a/src/theory/quantifiers/trigger.h
+++ b/src/theory/quantifiers/trigger.h
@@ -2,9 +2,9 @@
/*! \file trigger.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters, Andrew Reynolds
+ ** Andrew Reynolds, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 501d77ecf..faf14e0c7 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index fff446eda..92dfcdae5 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/rep_set.cpp b/src/theory/rep_set.cpp
index c308b9c67..cd1fac290 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/rep_set.h b/src/theory/rep_set.h
index 9368d3681..41044b526 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/rewriter.cpp b/src/theory/rewriter.cpp
index 0df122571..27ab7615c 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Dejan Jovanovic, Morgan Deters, Liana Hadarean
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/rewriter.h b/src/theory/rewriter.h
index aed93a451..ba8b12fb6 100644
--- a/src/theory/rewriter.h
+++ b/src/theory/rewriter.h
@@ -2,9 +2,9 @@
/*! \file rewriter.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/rewriter_attributes.h b/src/theory/rewriter_attributes.h
index 5f709de6a..ec120ff0c 100644
--- a/src/theory/rewriter_attributes.h
+++ b/src/theory/rewriter_attributes.h
@@ -2,9 +2,9 @@
/*! \file rewriter_attributes.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h
index 4d41c023d..9ea9a9695 100644
--- a/src/theory/rewriter_tables_template.h
+++ b/src/theory/rewriter_tables_template.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Dejan Jovanovic, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 4c6cd3eb4..93d4124d9 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -2,9 +2,9 @@
/*! \file theory_sep.cpp
** \verbatim
** Top contributors (to current version):
- ** none
+ ** Andrew Reynolds, Tim King, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sep/theory_sep.h b/src/theory/sep/theory_sep.h
index 00e67f5ff..1786584d4 100644
--- a/src/theory/sep/theory_sep.h
+++ b/src/theory/sep/theory_sep.h
@@ -2,9 +2,9 @@
/*! \file theory_sep.h
** \verbatim
** Top contributors (to current version):
- ** none
+ ** Andrew Reynolds, Mathias Preiner, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index 2e6a54ebd..513eada3f 100644
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -2,9 +2,9 @@
/*! \file theory_sep_rewriter.cpp
** \verbatim
** Top contributors (to current version):
- ** none
+ ** Andrew Reynolds, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sep/theory_sep_rewriter.h b/src/theory/sep/theory_sep_rewriter.h
index c71248319..61b2ee36a 100644
--- a/src/theory/sep/theory_sep_rewriter.h
+++ b/src/theory/sep/theory_sep_rewriter.h
@@ -2,9 +2,9 @@
/*! \file theory_sep_rewriter.h
** \verbatim
** Top contributors (to current version):
- ** none
+ ** Andrew Reynolds, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h
index 8de0783e2..e9177e004 100644
--- a/src/theory/sep/theory_sep_type_rules.h
+++ b/src/theory/sep/theory_sep_type_rules.h
@@ -2,9 +2,9 @@
/*! \file theory_sep_type_rules.h
** \verbatim
** Top contributors (to current version):
- ** none
+ ** Andrew Reynolds, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sets/normal_form.h b/src/theory/sets/normal_form.h
index 6379fb299..bb715ff8c 100644
--- a/src/theory/sets/normal_form.h
+++ b/src/theory/sets/normal_form.h
@@ -2,9 +2,9 @@
/*! \file normal_form.h
** \verbatim
** Top contributors (to current version):
- ** Kshitij Bansal, Tim King
+ ** Kshitij Bansal, Tim King, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sets/rels_utils.h b/src/theory/sets/rels_utils.h
index 9863b9734..5f4c7d79d 100644
--- a/src/theory/sets/rels_utils.h
+++ b/src/theory/sets/rels_utils.h
@@ -2,9 +2,9 @@
/*! \file rels_utils.h
** \verbatim
** Top contributors (to current version):
- ** none
+ ** Andrew Reynolds, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 9cf355f15..4992f654f 100644
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -2,9 +2,9 @@
/*! \file theory_sets.cpp
** \verbatim
** Top contributors (to current version):
- ** Kshitij Bansal, Tim King, Morgan Deters
+ ** Kshitij Bansal, Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sets/theory_sets.h b/src/theory/sets/theory_sets.h
index 8f81b9d2a..bbc6ae0c4 100644
--- a/src/theory/sets/theory_sets.h
+++ b/src/theory/sets/theory_sets.h
@@ -2,9 +2,9 @@
/*! \file theory_sets.h
** \verbatim
** Top contributors (to current version):
- ** Kshitij Bansal, Tim King
+ ** Kshitij Bansal, Paul Meng, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index a0748f2b9..f70db9823 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -2,9 +2,9 @@
/*! \file theory_sets_private.cpp
** \verbatim
** Top contributors (to current version):
- ** Kshitij Bansal, Tim King, Andrew Reynolds
+ ** Andrew Reynolds, Kshitij Bansal, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 667b7f253..7bc17c927 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -2,9 +2,9 @@
/*! \file theory_sets_private.h
** \verbatim
** Top contributors (to current version):
- ** Kshitij Bansal, Tim King, Andrew Reynolds
+ ** Andrew Reynolds, Kshitij Bansal, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 5f9243b33..34c17a34c 100644
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -2,9 +2,9 @@
/*! \file theory_sets_rels.cpp
** \verbatim
** Top contributors (to current version):
- ** none
+ ** Paul Meng, Andrew Reynolds, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h
index 24c744203..16770671a 100644
--- a/src/theory/sets/theory_sets_rels.h
+++ b/src/theory/sets/theory_sets_rels.h
@@ -2,9 +2,9 @@
/*! \file theory_sets_rels.h
** \verbatim
** Top contributors (to current version):
- ** none
+ ** Andrew Reynolds, Paul Meng, Mathias Preiner
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp
index e42a3347d..3cce08398 100644
--- a/src/theory/sets/theory_sets_rewriter.cpp
+++ b/src/theory/sets/theory_sets_rewriter.cpp
@@ -2,9 +2,9 @@
/*! \file theory_sets_rewriter.cpp
** \verbatim
** Top contributors (to current version):
- ** Kshitij Bansal, Tim King
+ ** Andrew Reynolds, Paul Meng, Kshitij Bansal
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
index 50128b63d..5cf0f8e19 100644
--- a/src/theory/sets/theory_sets_rewriter.h
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -2,9 +2,9 @@
/*! \file theory_sets_rewriter.h
** \verbatim
** Top contributors (to current version):
- ** Kshitij Bansal, Tim King
+ ** Kshitij Bansal, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h
index f2d6bae68..f261ac3fa 100644
--- a/src/theory/sets/theory_sets_type_enumerator.h
+++ b/src/theory/sets/theory_sets_type_enumerator.h
@@ -2,9 +2,9 @@
/*! \file theory_sets_type_enumerator.h
** \verbatim
** Top contributors (to current version):
- ** Kshitij Bansal, Morgan Deters, Andrew Reynolds
+ ** Kshitij Bansal, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index e2830b57e..1fd5f08be 100644
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -2,9 +2,9 @@
/*! \file theory_sets_type_rules.h
** \verbatim
** Top contributors (to current version):
- ** Kshitij Bansal, Tim King, Morgan Deters
+ ** Kshitij Bansal, Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index b78109dfb..8e4bd5399 100644
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Dejan Jovanovic, Morgan Deters, Clark Barrett
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/shared_terms_database.h b/src/theory/shared_terms_database.h
index cc8959165..6b78a1698 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Dejan Jovanovic, Morgan Deters, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sort_inference.cpp b/src/theory/sort_inference.cpp
index 6dabf9a13..73a50bc7a 100644
--- a/src/theory/sort_inference.cpp
+++ b/src/theory/sort_inference.cpp
@@ -2,9 +2,9 @@
/*! \file sort_inference.cpp
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Tim King
+ ** Andrew Reynolds, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/sort_inference.h b/src/theory/sort_inference.h
index ae3342f92..ae4131fa8 100644
--- a/src/theory/sort_inference.h
+++ b/src/theory/sort_inference.h
@@ -2,9 +2,9 @@
/*! \file sort_inference.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds, Tim King
+ ** Morgan Deters, Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp
index a665a02c1..ec788fa78 100644
--- a/src/theory/strings/regexp_operation.cpp
+++ b/src/theory/strings/regexp_operation.cpp
@@ -2,9 +2,9 @@
/*! \file regexp_operation.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tianyi Liang, Tim King
+ ** Morgan Deters, Tianyi Liang, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h
index 075391370..4a0ce150c 100644
--- a/src/theory/strings/regexp_operation.h
+++ b/src/theory/strings/regexp_operation.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Tianyi Liang, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 6526b68cf..9b74c3513 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tianyi Liang, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index a905189af..ac45bb731 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tianyi Liang, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp
index d8d8e393c..ca49727ef 100644
--- a/src/theory/strings/theory_strings_preprocess.cpp
+++ b/src/theory/strings/theory_strings_preprocess.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Tianyi Liang, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h
index faaeb53c3..60bfd6fab 100644
--- a/src/theory/strings/theory_strings_preprocess.h
+++ b/src/theory/strings/theory_strings_preprocess.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/strings/theory_strings_rewriter.cpp b/src/theory/strings/theory_strings_rewriter.cpp
index 6daaddcd7..de9b60d87 100644
--- a/src/theory/strings/theory_strings_rewriter.cpp
+++ b/src/theory/strings/theory_strings_rewriter.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tianyi Liang, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/strings/theory_strings_rewriter.h b/src/theory/strings/theory_strings_rewriter.h
index e166bfaeb..d5a35926e 100644
--- a/src/theory/strings/theory_strings_rewriter.h
+++ b/src/theory/strings/theory_strings_rewriter.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tianyi Liang, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/strings/theory_strings_type_rules.h b/src/theory/strings/theory_strings_type_rules.h
index 6dc207b6b..b02257d38 100644
--- a/src/theory/strings/theory_strings_type_rules.h
+++ b/src/theory/strings/theory_strings_type_rules.h
@@ -2,9 +2,9 @@
/*! \file theory_strings_type_rules.h
** \verbatim
** Top contributors (to current version):
- ** Tianyi Liang, Tim King, Morgan Deters
+ ** Tianyi Liang, Paul Meng, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/strings/type_enumerator.h b/src/theory/strings/type_enumerator.h
index 22dc903ab..c7a36f2f5 100644
--- a/src/theory/strings/type_enumerator.h
+++ b/src/theory/strings/type_enumerator.h
@@ -2,9 +2,9 @@
/*! \file type_enumerator.h
** \verbatim
** Top contributors (to current version):
- ** Tianyi Liang, Tim King, Andrew Reynolds
+ ** Tianyi Liang, Paul Meng, Andres Noetzli
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/substitutions.cpp b/src/theory/substitutions.cpp
index 7dbfb2678..ffb1cd1cb 100644
--- a/src/theory/substitutions.cpp
+++ b/src/theory/substitutions.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Clark Barrett, Dejan Jovanovic, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/substitutions.h b/src/theory/substitutions.h
index 019fbd17e..5a6618175 100644
--- a/src/theory/substitutions.h
+++ b/src/theory/substitutions.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Clark Barrett
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index e758002fa..1e1a2e8e6 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Dejan Jovanovic, Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index 6d04910f6..39cce27f9 100644
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -2,9 +2,9 @@
/*! \file term_registration_visitor.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/theory.cpp b/src/theory/theory.cpp
index 37d65972e..f010798cd 100644
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -2,9 +2,9 @@
/*! \file theory.cpp
** \verbatim
** Top contributors (to current version):
- ** Tim King, Dejan Jovanovic, Clark Barrett
+ ** Tim King, Andrew Reynolds, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/theory.h b/src/theory/theory.h
index 37d818eac..3ddb18754 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -2,9 +2,9 @@
/*! \file theory.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Morgan Deters, Dejan Jovanovic, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/theory_engine.cpp b/src/theory/theory_engine.cpp
index f99de0c3b..7369b7c1f 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -2,9 +2,9 @@
/*! \file theory_engine.cpp
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Tim King
+ ** Dejan Jovanovic, Morgan Deters, Guy Katz
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/theory_engine.h b/src/theory/theory_engine.h
index e821b4017..82283ef7b 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/theory_model.cpp b/src/theory/theory_model.cpp
index c064040d9..b9a08e3ac 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Clark Barrett, Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/theory_model.h b/src/theory/theory_model.h
index 1d3906eee..126de1e46 100644
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Clark Barrett, Morgan Deters, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/theory_registrar.h b/src/theory/theory_registrar.h
index d0e3a5b0d..df576a694 100644
--- a/src/theory/theory_registrar.h
+++ b/src/theory/theory_registrar.h
@@ -2,9 +2,9 @@
/*! \file theory_registrar.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters, Liana Hadarean
+ ** Tim King, Morgan Deters, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/theory_test_utils.h b/src/theory/theory_test_utils.h
index 031c51d22..f5c85fc35 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Tim King, Morgan Deters, Liana Hadarean
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/theory_traits_template.h b/src/theory/theory_traits_template.h
index 0d2d0b8e2..5fbf10e93 100644
--- a/src/theory/theory_traits_template.h
+++ b/src/theory/theory_traits_template.h
@@ -2,9 +2,9 @@
/*! \file theory_traits_template.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Dejan Jovanovic, Tim King
+ ** Morgan Deters, Dejan Jovanovic, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/type_enumerator.h b/src/theory/type_enumerator.h
index 258bf6a3a..197363c1f 100644
--- a/src/theory/type_enumerator.h
+++ b/src/theory/type_enumerator.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp
index 2dfefa1a8..a2bc8ab86 100644
--- a/src/theory/type_enumerator_template.cpp
+++ b/src/theory/type_enumerator_template.cpp
@@ -2,9 +2,9 @@
/*! \file type_enumerator_template.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Tim King, Andrew Reynolds
+ ** Morgan Deters, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index f7084bec3..a73425a80 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Dejan Jovanovic, Guy Katz, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 46ec7403b..7c8e27575 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Dejan Jovanovic, Morgan Deters, Guy Katz
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index 346aebca7..ed0afa904 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -2,9 +2,9 @@
/*! \file equality_engine_types.h
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Andrew Reynolds, Guy Katz
+ ** Dejan Jovanovic, Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/uf/symmetry_breaker.cpp b/src/theory/uf/symmetry_breaker.cpp
index ca7284689..cffa367cf 100644
--- a/src/theory/uf/symmetry_breaker.cpp
+++ b/src/theory/uf/symmetry_breaker.cpp
@@ -2,9 +2,9 @@
/*! \file symmetry_breaker.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Liana Hadarean, Tim King
+ ** Morgan Deters, Liana Hadarean, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/uf/symmetry_breaker.h b/src/theory/uf/symmetry_breaker.h
index b706f340f..a814c670b 100644
--- a/src/theory/uf/symmetry_breaker.h
+++ b/src/theory/uf/symmetry_breaker.h
@@ -2,9 +2,9 @@
/*! \file symmetry_breaker.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Liana Hadarean, Tim King
+ ** Morgan Deters, Liana Hadarean, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 8166e3574..783585f8f 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -2,9 +2,9 @@
/*! \file theory_uf.cpp
** \verbatim
** Top contributors (to current version):
- ** Dejan Jovanovic, Morgan Deters, Andrew Reynolds
+ ** Morgan Deters, Andrew Reynolds, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 28db0195d..bd10f5961 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Dejan Jovanovic, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/uf/theory_uf_model.cpp b/src/theory/uf/theory_uf_model.cpp
index f6568ad7f..b7572eaa1 100644
--- a/src/theory/uf/theory_uf_model.cpp
+++ b/src/theory/uf/theory_uf_model.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Andrew Reynolds, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/uf/theory_uf_model.h b/src/theory/uf/theory_uf_model.h
index 39e7ee6f0..0b55c926e 100644
--- a/src/theory/uf/theory_uf_model.h
+++ b/src/theory/uf/theory_uf_model.h
@@ -2,9 +2,9 @@
/*! \file theory_uf_model.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Andrew Reynolds, Tim King
+ ** Morgan Deters, Andrew Reynolds, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
index bce6003eb..0bd502205 100644
--- a/src/theory/uf/theory_uf_rewriter.h
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -2,9 +2,9 @@
/*! \file theory_uf_rewriter.h
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Dejan Jovanovic, Tim King
+ ** Morgan Deters, Dejan Jovanovic, Paul Meng
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 51648fb26..77459715f 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Andrew Reynolds, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index 4130a7d41..b477a7eb5 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -2,9 +2,9 @@
/*! \file theory_uf_strong_solver.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Tim King
+ ** Tim King, Andrew Reynolds, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 6f97a9662..a3c775a2a 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -2,9 +2,9 @@
/*! \file theory_uf_type_rules.h
** \verbatim
** Top contributors (to current version):
- ** Andrew Reynolds, Morgan Deters, Dejan Jovanovic
+ ** Tim King, Morgan Deters, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/unconstrained_simplifier.cpp b/src/theory/unconstrained_simplifier.cpp
index 57d95d801..6c2c791cf 100644
--- a/src/theory/unconstrained_simplifier.cpp
+++ b/src/theory/unconstrained_simplifier.cpp
@@ -2,9 +2,9 @@
/*! \file unconstrained_simplifier.cpp
** \verbatim
** Top contributors (to current version):
- ** Clark Barrett, Peter Collingbourne, Tim King
+ ** Clark Barrett, Tim King, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/unconstrained_simplifier.h b/src/theory/unconstrained_simplifier.h
index e10be1a8f..a32dd076e 100644
--- a/src/theory/unconstrained_simplifier.h
+++ b/src/theory/unconstrained_simplifier.h
@@ -2,9 +2,9 @@
/*! \file unconstrained_simplifier.h
** \verbatim
** Top contributors (to current version):
- ** Clark Barrett, Tim King
+ ** Clark Barrett, Paul Meng, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/valuation.cpp b/src/theory/valuation.cpp
index 7e13668cd..7151b4aaf 100644
--- a/src/theory/valuation.cpp
+++ b/src/theory/valuation.cpp
@@ -2,9 +2,9 @@
/*! \file valuation.cpp
** \verbatim
** Top contributors (to current version):
- ** Morgan Deters, Dejan Jovanovic, Tim King
+ ** Morgan Deters, Dejan Jovanovic, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 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/valuation.h b/src/theory/valuation.h
index 54af14fdd..e78a629e1 100644
--- a/src/theory/valuation.h
+++ b/src/theory/valuation.h
@@ -4,7 +4,7 @@
** Top contributors (to current version):
** Morgan Deters, Dejan Jovanovic, Andrew Reynolds
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback