Update copyright headers.

diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index 0ac33c6dc6ca40bbbadccbd74748dcc714e7cff2..f4dc72e5675933c4195d00873d6131901778644a 100644 (file)
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -2,7 +2,7 @@
 /*! \file combination.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Tim King, Andrew Reynolds
+ **   Aina Niemetz, Tim King, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp
index 2e70460af59fb03fe1ae0c556473cd604cef4090..77c1e196f37eb2ce72c82f5ded0e6a69c790bd66 100644 (file)
--- a/examples/api/linear_arith.cpp
+++ b/examples/api/linear_arith.cpp
@@ -2,7 +2,7 @@
 /*! \file linear_arith.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Tim King
+ **   Aina Niemetz, Tim King, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py
index f063d8c4e0af42a163a9cb4437aeb090d7d4503f..7733437a1c150a03bd34d98c52c83f101a0f2a89 100644 (file)
--- a/examples/api/python/combination.py
+++ b/examples/api/python/combination.py
@@ -2,7 +2,7 @@
 #####################
 ## combination.py
 ## Top contributors (to current version):
-##   Makai Mann, Aina Niemetz, Andrew Reynolds
+##   Makai Mann, Mudathir Mohamed, Aina Niemetz
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py
index 94ce730a3fc978a89e8938e3c28d8b19591a1343..f539d1e054d06583a2a8c450d2abc0da4a35a84d 100644 (file)
--- a/examples/api/python/linear_arith.py
+++ b/examples/api/python/linear_arith.py
@@ -2,7 +2,7 @@
 #####################
 ## linear_arith.py
 ## Top contributors (to current version):
-##   Makai Mann, Aina Niemetz
+##   Makai Mann, Mudathir Mohamed, Aina Niemetz
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py
index 7ed5448cdb88c86888bc31b37e793e7c27c7e66c..9e3e45dc2d183101a580debf570f5f22bb6e6887 100644 (file)
--- a/examples/api/python/sequences.py
+++ b/examples/api/python/sequences.py
@@ -2,7 +2,7 @@
 #####################
 ## sequences.py
 ## Top contributors (to current version):
-##   Andres Noetzli, Makai Mann
+##   Andres Noetzli, Makai Mann, Mudathir Mohamed
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py
index e4350ea1b8b4ed755af470c164d2f2342c0a06cc..5d2f842f50362843e6f8a9765da36a351656725d 100644 (file)
--- a/examples/api/python/sets.py
+++ b/examples/api/python/sets.py
@@ -2,7 +2,7 @@
 #####################
 ## sets.py
 ## Top contributors (to current version):
-##   Makai Mann, Aina Niemetz
+##   Makai Mann, Mudathir Mohamed, Aina Niemetz
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py
index 1e85c56bb9eec1d569cd096442e7306c610e7638..518a7b9939668e0145522f79ffdb473f5c7a8d43 100644 (file)
--- a/examples/api/python/strings.py
+++ b/examples/api/python/strings.py
@@ -2,7 +2,7 @@
 #####################
 ## strings.py
 ## Top contributors (to current version):
-##   Makai Mann, Andres Noetzli
+##   Makai Mann, Mudathir Mohamed, Andres Noetzli
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py
index a85902961db0bc2467d631788b99e3cc2996483a..9fb7f4648999550e00ca9ea6dab1f5e93b458a96 100644 (file)
--- a/examples/api/python/sygus-fun.py
+++ b/examples/api/python/sygus-fun.py
@@ -2,7 +2,7 @@
 #####################
 ## sygus-fun.py
 ## Top contributors (to current version):
-##   Yoni Zohar, Andres Noetzli
+##   Yoni Zohar, Andres Noetzli, Mudathir Mohamed
 ## Copyright (c) 2009-2018 by the authors listed in the file AUTHkinds.OrS
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS

diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py
index cfa342f35cbefac643b4f2000c907befbfa62db1..1410e67393a51fcb4a982ba1a083d6f0a5519c2a 100644 (file)
--- a/examples/api/python/sygus-grammar.py
+++ b/examples/api/python/sygus-grammar.py
@@ -2,7 +2,7 @@
 #####################
 ## sygus-grammar.py
 ## Top contributors (to current version):
-##   Yoni Zohar
+##   Yoni Zohar, Mudathir Mohamed
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py
index 4e7465382e5aa6b5b792ae4f17506b79784ded48..ac28f8f1bbcc9903844b2d76d44dc49f1eda1a39 100644 (file)
--- a/examples/api/python/sygus-inv.py
+++ b/examples/api/python/sygus-inv.py
@@ -2,7 +2,7 @@
 #####################
 ## sygus-inv.py
 ## Top contributors (to current version):
-##   Yoni Zohar
+##   Yoni Zohar, Mudathir Mohamed
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index f8053a756fbb1adeab4c82c1ca4a33eb90e8419a..6033fb94ec004f70137bbbf88c51d64b5bddd475 100644 (file)
--- a/examples/api/sets.cpp
+++ b/examples/api/sets.cpp
@@ -2,7 +2,7 @@
 /*! \file sets.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Kshitij Bansal
+ **   Aina Niemetz, Kshitij Bansal, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp
index 556c49c8e37a787c3497b145651c9389ae1ac9f6..c95600c3024321e7a6db8b800358efeeb2976065 100644 (file)
--- a/examples/api/strings.cpp
+++ b/examples/api/strings.cpp
@@ -2,7 +2,7 @@
 /*! \file strings.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Tianyi Liang, Andres Noetzli
+ **   Aina Niemetz, Tianyi Liang, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/examples/api/sygus-fun.cpp b/examples/api/sygus-fun.cpp
index b2d6e92152b428d5aeb9ef878beb433f767cb2fa..a5b421fae365742428af630e070aa35b29707730 100644 (file)
--- a/examples/api/sygus-fun.cpp
+++ b/examples/api/sygus-fun.cpp
@@ -2,7 +2,7 @@
 /*! \file sygus-fun.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Abdalrhman Mohamed
+ **   Abdalrhman Mohamed, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/examples/api/sygus-grammar.cpp b/examples/api/sygus-grammar.cpp
index ea8256c70cba5ceecfc0ca03b5b36fa6a42152d6..e5481676ab8c2dd70f6fe965b3381e6bae5079b3 100644 (file)
--- a/examples/api/sygus-grammar.cpp
+++ b/examples/api/sygus-grammar.cpp
@@ -2,7 +2,7 @@
 /*! \file sygus-grammar.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Abdalrhman Mohamed
+ **   Abdalrhman Mohamed, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/examples/api/sygus-inv.cpp b/examples/api/sygus-inv.cpp
index d57d9be4e1baf316025209be76d34c3a88131ee7..f903b02429bc7daf895cebd2b480dbf4d9c965d2 100644 (file)
--- a/examples/api/sygus-inv.cpp
+++ b/examples/api/sygus-inv.cpp
@@ -2,7 +2,7 @@
 /*! \file sygus-inv.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Abdalrhman Mohamed
+ **   Abdalrhman Mohamed, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index e648b99949eda89e9aedb9b0a57898370df1c6d0..94bbee564ea4deb05a06adf4ac62d87839ac6a63 100644 (file)
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -2,7 +2,7 @@
 /*! \file simple_vc_cxx.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli, Morgan Deters
+ **   Andres Noetzli, Morgan Deters, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp
index 538cb359f3e313eb7b3f5c7697f484dbbb786987..b2dd0d3e65026db8da12deca12825b2cbbcb2089 100644 (file)
--- a/examples/simple_vc_quant_cxx.cpp
+++ b/examples/simple_vc_quant_cxx.cpp
@@ -2,7 +2,7 @@
 /*! \file simple_vc_quant_cxx.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli, Andrew Reynolds
+ **   Andres Noetzli, Andrew Reynolds, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt
index 391db4bd46a67a213f55ceb9abdd2ab25f9e20df..f0825f1805f850d9e629cf3fdfba37fb288364a0 100644 (file)
--- a/src/expr/CMakeLists.txt
+++ b/src/expr/CMakeLists.txt
@@ -1,7 +1,7 @@
 #####################
 ## CMakeLists.txt
 ## Top contributors (to current version):
-##   Mathias Preiner, Aina Niemetz, Andrew Reynolds
+##   Mathias Preiner, Andrew Reynolds, Aina Niemetz
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/ascription_type.cpp b/src/expr/ascription_type.cpp
index d9466fdbf282e7233a428dbce80120ec073f64a7..cc5fc8557877d013d87449440f515b5a30dbcced 100644 (file)
--- a/src/expr/ascription_type.cpp
+++ b/src/expr/ascription_type.cpp
@@ -2,7 +2,7 @@
 /*! \file ascription_type.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Mathias Preiner
+ **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/ascription_type.h b/src/expr/ascription_type.h
index 800f46e0ae772016d02a50a536bf82c409680f0a..13715a6d77c75c6cdb9dd50ef3a93ac590351fb6 100644 (file)
--- a/src/expr/ascription_type.h
+++ b/src/expr/ascription_type.h
@@ -2,7 +2,7 @@
 /*! \file ascription_type.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Mathias Preiner
+ **   Morgan Deters, Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/buffered_proof_generator.cpp b/src/expr/buffered_proof_generator.cpp
index aa0fe19bdaff814e62e92fe593423cef61b9503b..f6753a60142cfa45d80e8aba3d2542ae7887027b 100644 (file)
--- a/src/expr/buffered_proof_generator.cpp
+++ b/src/expr/buffered_proof_generator.cpp
@@ -5,7 +5,7 @@
  **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/expr/buffered_proof_generator.h b/src/expr/buffered_proof_generator.h
index 987bd2465ed65c6f87841b0a365f76651951371c..f774e383dd2e658b0677f60c1d0a476801ffb7ca 100644 (file)
--- a/src/expr/buffered_proof_generator.h
+++ b/src/expr/buffered_proof_generator.h
@@ -2,10 +2,10 @@
 /*! \file buffered_proof_generator.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Haniel Barbosa
+ **   Haniel Barbosa, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/expr/emptybag.cpp b/src/expr/emptybag.cpp
index 888b3b92a1d9d38f309b5596df64f23fab19ff71..8e59a8eb17665ee9492d9c2fe1f8f4342f1d52fb 100644 (file)
--- a/src/expr/emptybag.cpp
+++ b/src/expr/emptybag.cpp
@@ -5,9 +5,11 @@
  **   Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
+ **
+ ** \brief A class for empty bags
  **/
 
 #include "expr/emptybag.h"

diff --git a/src/expr/emptybag.h b/src/expr/emptybag.h
index a16c12d863677e5da2412f95769b8dd899bc6092..8a9776f42ee1a38aad2bb0a71cc482fc05f6c9fb 100644 (file)
--- a/src/expr/emptybag.h
+++ b/src/expr/emptybag.h
@@ -5,11 +5,11 @@
  **   Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief a class for empty bags
+ ** \brief A class for empty bags
  **/
 
 #include "cvc4_public.h"

diff --git a/src/expr/expr_iomanip.cpp b/src/expr/expr_iomanip.cpp
index 0ff29663c7d337001baa0c77db4907b20d97f565..0395a9b07685a19346788647ce9aaaaccb5374c1 100644 (file)
--- a/src/expr/expr_iomanip.cpp
+++ b/src/expr/expr_iomanip.cpp
@@ -2,7 +2,7 @@
 /*! \file expr_iomanip.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Kshitij Bansal
+ **   Morgan Deters, Tim King, Kshitij Bansal
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index 5c096767bf993ef10d0e93fde1eb879f876b37b8..a98ba7453aa6652bce5dcfda78410fca5959a1e3 100644 (file)
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -2,10 +2,10 @@
 /*! \file lazy_proof_chain.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/expr/lazy_proof_chain.h b/src/expr/lazy_proof_chain.h
index 28de3cea0d47b950914972eb4b309f80749ce369..59cab72c98dbe7da591d76c52d074a6c39ec4b0e 100644 (file)
--- a/src/expr/lazy_proof_chain.h
+++ b/src/expr/lazy_proof_chain.h
@@ -2,10 +2,10 @@
 /*! \file lazy_proof_chain.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index fde92c4e1cbeaaf47ba7f5faa4f359d35294376a..49f460f45bddaf076755d2df44f99dca4287a49d 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -2,7 +2,7 @@
 /*! \file node_manager.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-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index bbb076fbcd0df96a50d7ee691caeb8f1cd9c00c8..1dd495ba2781ce515d581f8129551dd6e3e2a33f 100644 (file)
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -2,7 +2,7 @@
 /*! \file node_manager.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway, Andrew Reynolds
+ **   Morgan Deters, Andrew Reynolds, Christopher L. Conway
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 8ceb5476a1d7364438fff1aecc08289d5ec4eb62..9964d7aec6c8c84b0cd982d66cbb0949371c890f 100644 (file)
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -2,7 +2,7 @@
 /*! \file node_value.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Aina Niemetz, Tim King
+ **   Morgan Deters, Aina Niemetz, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
index 6d7db7b2586db53978b64bc56438385a35e09239..0c36deada35e4e3952972057fb68923014fc3c0a 100644 (file)
--- a/src/expr/proof_node.h
+++ b/src/expr/proof_node.h
@@ -2,7 +2,7 @@
 /*! \file proof_node.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp
index b21bdec230c9c988eae41ec34564383881e3ce6d..c3e0aa5b02738675e636e8f939f89ecb776c75e6 100644 (file)
--- a/src/expr/proof_node_algorithm.cpp
+++ b/src/expr/proof_node_algorithm.cpp
@@ -2,7 +2,7 @@
 /*! \file proof_node_algorithm.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h
index d6bd1963c7a485f5974366f6d6909691b491350b..43d06ea919e20223458946c761dcd813db8222da 100644 (file)
--- a/src/expr/proof_node_algorithm.h
+++ b/src/expr/proof_node_algorithm.h
@@ -2,7 +2,7 @@
 /*! \file proof_node_algorithm.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp
index 4682bbebb55c18bfbf9d81305d8678ba6752d57b..cacd2c101695af4f1233569d8ed7b950b06474be 100644 (file)
--- a/src/expr/proof_node_manager.cpp
+++ b/src/expr/proof_node_manager.cpp
@@ -2,7 +2,7 @@
 /*! \file proof_node_manager.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h
index dae0266bb59946b03514c197cbbf4ed28d08fbb3..3ad56c92decfffb4033e1bdc659fd8406170bd2f 100644 (file)
--- a/src/expr/proof_node_manager.h
+++ b/src/expr/proof_node_manager.h
@@ -2,7 +2,7 @@
 /*! \file proof_node_manager.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp
index ac04baa6ff8144340457023f68d26fbcea6974e9..834f4381f0bf9712691d43fe6ee08a721c32bc02 100644 (file)
--- a/src/expr/proof_node_updater.cpp
+++ b/src/expr/proof_node_updater.cpp
@@ -2,7 +2,7 @@
 /*! \file proof_node_updater.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h
index d4c2e87565b1894f03f8eaa2dad7c0c290c9fe08..82c2ee068fd1c06196db6fe117d164da4bcdc1eb 100644 (file)
--- a/src/expr/proof_node_updater.h
+++ b/src/expr/proof_node_updater.h
@@ -2,7 +2,7 @@
 /*! \file proof_node_updater.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/proof_set.h b/src/expr/proof_set.h
index 20ef67efe078187fbd8a9f995da9d13304d3e89d..9c6c21ec42d122bd14a5890e0e6f9058ddd29555 100644 (file)
--- a/src/expr/proof_set.h
+++ b/src/expr/proof_set.h
@@ -2,7 +2,7 @@
 /*! \file proof_set.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Gereon Kremer, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/record.cpp b/src/expr/record.cpp
index 08944912a1bf43894a2146bbe7247ade1ac1ebae..cddfd7a22a98f14ecace90292716d4de186108af 100644 (file)
--- a/src/expr/record.cpp
+++ b/src/expr/record.cpp
@@ -2,7 +2,7 @@
 /*! \file record.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Piotr Trojanek
+ **   Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/record.h b/src/expr/record.h
index a0d545a56800b5d1fa25e847d584813e8e95df66..4e1ff677266ef864fdccad167ca821a51211a245 100644 (file)
--- a/src/expr/record.h
+++ b/src/expr/record.h
@@ -2,7 +2,7 @@
 /*! \file record.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Mathias Preiner
+ **   Morgan Deters, Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index d6a632ac504f49710d0c2f8a3df8d8b394a28bd8..0e30d6d73a9886b212f5ebe093a0288d666d0dea 100644 (file)
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -2,7 +2,7 @@
 /*! \file symbol_table.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Tim King
+ **   Andrew Reynolds, Morgan Deters, Christopher L. Conway
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/expr/tconv_seq_proof_generator.cpp b/src/expr/tconv_seq_proof_generator.cpp
index b22170b3870081a4a5c1d36bf0b0c9bc6db69be3..8bd8504888cefb30e841ec34207b0cc33db882f4 100644 (file)
--- a/src/expr/tconv_seq_proof_generator.cpp
+++ b/src/expr/tconv_seq_proof_generator.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file tconv_seq_proof_generator.h
+/*! \file tconv_seq_proof_generator.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Andrew Reynolds

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index b1a7c70b514f3b6ca5cf4c9cefdc327be46104e3..af95ca20f51512c5d21d8bdc2449660c8026433f 100644 (file)
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -2,7 +2,7 @@
 /*! \file command_executor.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Kshitij Bansal, Morgan Deters, Tim King
+ **   Kshitij Bansal, Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 4023b86debe201f9b5627955238347a8401cde39..db2248454df18d0e52616fdde10c1b8e937775a0 100644 (file)
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -2,7 +2,7 @@
 /*! \file command_executor.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Kshitij Bansal, Morgan Deters
+ **   Andrew Reynolds, Kshitij Bansal, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/parser/antlr_tracing.h b/src/parser/antlr_tracing.h
index b8a18aba854c582ac0f740b7bd07247419e60183..7030e11775bd7373b0fbac99e277f562a39f4f5d 100644 (file)
--- a/src/parser/antlr_tracing.h
+++ b/src/parser/antlr_tracing.h
@@ -2,7 +2,7 @@
 /*! \file antlr_tracing.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Mathias Preiner
+ **   Morgan Deters, Mathias Preiner, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 9adb46af1ff8ce520ad5a0b593a26a01944b74b7..b9d0cb41518bdb6b64cc7370574484b284c21052 100644 (file)
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -2,7 +2,7 @@
 /*! \file parser_builder.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters, Aina Niemetz
+ **   Christopher L. Conway, Morgan Deters, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index bf205b13a003e2282648f38eec6ff0349ff4b3c1..c28a76879956fe5479ff76d7433c268f4365783b 100644 (file)
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -2,7 +2,7 @@
 /*! \file parser_builder.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway, Aina Niemetz
+ **   Morgan Deters, Christopher L. Conway, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp
index cd7aadf9a2c1ce3cb214edf022d48997af4881f7..3b304c8b9f9568a15b623383db10a2c8f2f9a093 100644 (file)
--- a/src/preprocessing/assertion_pipeline.cpp
+++ b/src/preprocessing/assertion_pipeline.cpp
@@ -2,7 +2,7 @@
 /*! \file assertion_pipeline.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli, Andrew Reynolds, Haniel Barbosa
+ **   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/assertion_pipeline.h b/src/preprocessing/assertion_pipeline.h
index 75f3704501f18eafc92314f8f471a0d098dfea9e..fcfce0e871f1423123c8b24062ece51638671300 100644 (file)
--- a/src/preprocessing/assertion_pipeline.h
+++ b/src/preprocessing/assertion_pipeline.h
@@ -2,7 +2,7 @@
 /*! \file assertion_pipeline.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli, Andrew Reynolds, Justin Xu
+ **   Andres Noetzli, Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp
index 06821ab566219e2fea5168c82afb7ca1a12bae73..92f31b0b8f95d32569f41544e1e50da7a2aca84b 100644 (file)
--- a/src/preprocessing/passes/apply_substs.cpp
+++ b/src/preprocessing/passes/apply_substs.cpp
@@ -2,7 +2,7 @@
 /*! \file apply_substs.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Andres Noetzli, Mathias Preiner
+ **   Aina Niemetz, Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/passes/bv_gauss.cpp b/src/preprocessing/passes/bv_gauss.cpp
index eaba90561af4eb9a5f5859644c4bedcc47ea65de..02a08b13382fe8026f564f3cd40e278275b1af51 100644 (file)
--- a/src/preprocessing/passes/bv_gauss.cpp
+++ b/src/preprocessing/passes/bv_gauss.cpp
@@ -2,7 +2,7 @@
 /*! \file bv_gauss.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Mathias Preiner, Andres Noetzli
+ **   Aina Niemetz, Mathias Preiner, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index dbe7514156b3352d7c645b14eb5df422a4d76b01..7ffe1bc76fed42842e20b1c3e3050412adcf2396 100644 (file)
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -2,7 +2,7 @@
 /*! \file bv_to_int.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Yoni Zohar, Ahmed Irfan, Andres Noetzli
+ **   Yoni Zohar, Andrew Reynolds, Andres Noetzli
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/passes/fun_def_fmf.cpp b/src/preprocessing/passes/fun_def_fmf.cpp
index 6095be228720c58727eeb9a8896b9bfb4a163c4c..8c7a7102192c9364db227c46725e931356dadd9f 100644 (file)
--- a/src/preprocessing/passes/fun_def_fmf.cpp
+++ b/src/preprocessing/passes/fun_def_fmf.cpp
@@ -2,7 +2,7 @@
 /*! \file fun_def_fmf.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/passes/global_negate.h b/src/preprocessing/passes/global_negate.h
index 208b8d990e2438b5e0135e5b09f48606dcb35815..af8ae504824e67b471d684b1be943be3ee80cf93 100644 (file)
--- a/src/preprocessing/passes/global_negate.h
+++ b/src/preprocessing/passes/global_negate.h
@@ -2,7 +2,7 @@
 /*! \file global_negate.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Yoni Zohar, Mathias Preiner
+ **   Yoni Zohar, Mathias Preiner, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/passes/ho_elim.cpp b/src/preprocessing/passes/ho_elim.cpp
index 445cac18e5c779cedb79642f970c3b4559b50c34..8cf4ad2eda97d263daf88f4e479121248eed3d8a 100644 (file)
--- a/src/preprocessing/passes/ho_elim.cpp
+++ b/src/preprocessing/passes/ho_elim.cpp
@@ -2,7 +2,7 @@
 /*! \file ho_elim.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Andres Noetzli
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/passes/ho_elim.h b/src/preprocessing/passes/ho_elim.h
index 2edc9607400b6e066308ee5a7bcdc03af5853dad..a1dc05b835c513537a9695f91767f981509adfca 100644 (file)
--- a/src/preprocessing/passes/ho_elim.h
+++ b/src/preprocessing/passes/ho_elim.h
@@ -2,7 +2,7 @@
 /*! \file ho_elim.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Andres Noetzli
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/passes/ite_simp.cpp b/src/preprocessing/passes/ite_simp.cpp
index 8c99493ba2c4614dc6d9cd6f163f7f5136e1d077..5568dcad0ae22b8af9f86cf9029088279de96509 100644 (file)
--- a/src/preprocessing/passes/ite_simp.cpp
+++ b/src/preprocessing/passes/ite_simp.cpp
@@ -2,7 +2,7 @@
 /*! \file ite_simp.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Tim King, Mathias Preiner
+ **   Aina Niemetz, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index f55665bc56cbf95a45a2fd25de97ff7dc8f5b2eb..4ed2aede97e75e6edb855a893ac62319efccfdf0 100644 (file)
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -2,7 +2,7 @@
 /*! \file miplib_trick.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Mathias Preiner, Tim King, Morgan Deters
+ **   Mathias Preiner, Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/passes/non_clausal_simp.cpp b/src/preprocessing/passes/non_clausal_simp.cpp
index cedee6d3cca3a98ba381c790dc6334e31878453e..7ace55c0a149fa3c93cfc3ad9eff91f27b1de662 100644 (file)
--- a/src/preprocessing/passes/non_clausal_simp.cpp
+++ b/src/preprocessing/passes/non_clausal_simp.cpp
@@ -2,7 +2,7 @@
 /*! \file non_clausal_simp.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Haniel Barbosa, Andrew Reynolds
+ **   Aina Niemetz, Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/passes/non_clausal_simp.h b/src/preprocessing/passes/non_clausal_simp.h
index d3a9e0b1aca5c32a76a135a3b443e8687babc4d3..f94eb2d700925bbe293de1a7f354d641cfb883ef 100644 (file)
--- a/src/preprocessing/passes/non_clausal_simp.h
+++ b/src/preprocessing/passes/non_clausal_simp.h
@@ -2,7 +2,7 @@
 /*! \file non_clausal_simp.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Mathias Preiner
+ **   Andrew Reynolds, Aina Niemetz, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/passes/theory_preprocess.cpp b/src/preprocessing/passes/theory_preprocess.cpp
index bf9c3e9fed4cc2186d5f41373e385981d58bc3f1..e888e7a2b7bc02fcd06f664c13b769959dab5361 100644 (file)
--- a/src/preprocessing/passes/theory_preprocess.cpp
+++ b/src/preprocessing/passes/theory_preprocess.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_preprocess.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Mathias Preiner
+ **   Mathias Preiner, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 78b0022c65d8c571769c34e5d1d0054912cc6957..169f10c9df2c442d89908bad2c159c1c357f94b3 100644 (file)
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -2,7 +2,7 @@
 /*! \file preprocessing_pass.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Justin Xu, Andres Noetzli
+ **   Justin Xu, Abdalrhman Mohamed, Andres Noetzli
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 5893635cfb445d71772fe59726bc249b33f2f153..ff4a0e6ca1b14419bd9737b62892b20f5980ff8a 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -2,7 +2,7 @@
 /*! \file preprocessing_pass_context.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Mathias Preiner, Andrew Reynolds
+ **   Aina Niemetz, Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 30b09acae630a164f0886b325022dad6ef75456f..ea0d1b267db882aed9dbd6a4981de3e671fff1ef 100644 (file)
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -2,7 +2,7 @@
 /*! \file ast_printer.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Abdalrhman Mohamed, Tim King
+ **   Morgan Deters, Abdalrhman Mohamed, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index e0bc7b6bffd57561c9958ddaea0b533cc65b8cdd..732933bb4b14836af020654ea4c6da2608794d90 100644 (file)
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -2,7 +2,7 @@
 /*! \file ast_printer.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Abdalrhman Mohamed, Tim King, Morgan Deters
+ **   Abdalrhman Mohamed, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index c681a223f8e0b5f716c79db3debad9fca4b8aa28..6c9009e584ffd8a4274bff4e63f44e9eee1f8d92 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -2,7 +2,7 @@
 /*! \file cvc_printer.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Dejan Jovanovic, Andrew Reynolds
+ **   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index 799bba8d2c6c7fd118b9b7366d1b7973549433a4..58e47dbac9fa92bfaf9cf4472d968fd6c81d837b 100644 (file)
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -2,7 +2,7 @@
 /*! \file cvc_printer.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Abdalrhman Mohamed, Tim King, Morgan Deters
+ **   Abdalrhman Mohamed, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/printer/let_binding.cpp b/src/printer/let_binding.cpp
index 2efc98318313ab33ca6db3be42a3fffbd2af91a0..afe926a2a2a95af114576176a74a70b4641cb2fb 100644 (file)
--- a/src/printer/let_binding.cpp
+++ b/src/printer/let_binding.cpp
@@ -5,7 +5,7 @@
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/printer/let_binding.h b/src/printer/let_binding.h
index d81274c8727a7bbd7fe284af9510d1343e9ec4f1..45a09d07f70479756341b3e620bd62a13756428e 100644 (file)
--- a/src/printer/let_binding.h
+++ b/src/printer/let_binding.h
@@ -5,7 +5,7 @@
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 7225721c0d5f7366a303829f51fba53362e3a62c..9f8451ba803c9d4a27e9767d35a153a5c44b89b9 100644 (file)
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -2,7 +2,7 @@
 /*! \file printer.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Abdalrhman Mohamed, Morgan Deters, Aina Niemetz
+ **   Abdalrhman Mohamed, Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/printer/printer.h b/src/printer/printer.h
index 5bcccedb865ea63d8881dd405ebccd9106c007d2..068c793305e3c381c7b8404445ae9900784d39bb 100644 (file)
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -2,7 +2,7 @@
 /*! \file printer.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Abdalrhman Mohamed, Tim King, Aina Niemetz
+ **   Abdalrhman Mohamed, Andrew Reynolds, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 3d90cee06dc4c456074e7d55bedb2ec1c38990a1..287a8128632a221918082993ac67fdee36f1356b 100644 (file)
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -2,7 +2,7 @@
 /*! \file smt2_printer.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Abdalrhman Mohamed, Tim King, Andrew Reynolds
+ **   Abdalrhman Mohamed, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/printer/tptp/tptp_printer.cpp b/src/printer/tptp/tptp_printer.cpp
index f9384b0cb5c0952a78aa9fa6fc0271251fb34c35..1c37c3edc5c62ffc8582fce3ba1ac07e66b9f20d 100644 (file)
--- a/src/printer/tptp/tptp_printer.cpp
+++ b/src/printer/tptp/tptp_printer.cpp
@@ -2,7 +2,7 @@
 /*! \file tptp_printer.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Morgan Deters
+ **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/printer/tptp/tptp_printer.h b/src/printer/tptp/tptp_printer.h
index 38a56bcb5b55dc9b8c86881e9b9f54b4242935a6..46c3184ffb2e13ed75b6e0c2c22915a342321c64 100644 (file)
--- a/src/printer/tptp/tptp_printer.h
+++ b/src/printer/tptp/tptp_printer.h
@@ -2,7 +2,7 @@
 /*! \file tptp_printer.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Abdalrhman Mohamed, Morgan Deters
+ **   Andrew Reynolds, Tim King, Abdalrhman Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 7276f640205da34df348395f8e500b991751a1cd..c7eb2282bcd90e1c155ab5ced14b111b83e22f6c 100644 (file)
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -2,7 +2,7 @@
 /*! \file proof_manager.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Guy Katz, Haniel Barbosa
+ **   Liana Hadarean, Haniel Barbosa, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index dd470b29907a6a501464a8a9c600aa310334d415..7b0b50605a4f88156283d5b4a0531ae1a24ec64b 100644 (file)
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -2,7 +2,7 @@
 /*! \file unsat_core.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Clark Barrett, Tim King
+ **   Morgan Deters, Andrew Reynolds, Clark Barrett
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h
index fb3401876b2112edea9a9fa52a4b7f110b95e68f..3fdbcc4b57b32cb769a859751a9598eb3fe83d71 100644 (file)
--- a/src/proof/unsat_core.h
+++ b/src/proof/unsat_core.h
@@ -2,7 +2,7 @@
 /*! \file unsat_core.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Mathias Preiner
+ **   Andrew Reynolds, Morgan Deters, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 7dcd3f91075e19ed7ac27febed73b5dd414f064e..e5b778365bcf41c6d484abc1a09f862d3020032d 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -2,7 +2,7 @@
 /*! \file cnf_stream.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Liana Hadarean, Tim King
+ **   Dejan Jovanovic, Haniel Barbosa, Liana Hadarean
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 74ead0d228f973f73808f71861ea8485e8712440..e92532f08c8ef23fb6a60120bd2537841514c674 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -2,7 +2,7 @@
 /*! \file cnf_stream.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Morgan Deters
+ **   Dejan Jovanovic, Tim King, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/prop/proof_cnf_stream.cpp b/src/prop/proof_cnf_stream.cpp
index 790e5aeb2d0e16b6303efba4a19083258fe5e381..d98de2a8a8cccdd0b0140a3c06abc3b84d0191f0 100644 (file)
--- a/src/prop/proof_cnf_stream.cpp
+++ b/src/prop/proof_cnf_stream.cpp
@@ -2,10 +2,10 @@
 /*! \file proof_cnf_stream.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/prop/proof_cnf_stream.h b/src/prop/proof_cnf_stream.h
index 80be0723199adb8875dc79de64bd559921298250..d05dd2f16696a78d2cda5b99ce6812fb7e0c7e8c 100644 (file)
--- a/src/prop/proof_cnf_stream.h
+++ b/src/prop/proof_cnf_stream.h
@@ -2,10 +2,10 @@
 /*! \file proof_cnf_stream.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Haniel Barbosa, Dejan Jovanovic, Liana Hadarean
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/prop/prop_proof_manager.cpp b/src/prop/prop_proof_manager.cpp
index aa58ffa2caa760dc9839cabdbde0c5283280cc63..fc5f92434ba46451d337176e1db9097c8fc54da0 100644 (file)
--- a/src/prop/prop_proof_manager.cpp
+++ b/src/prop/prop_proof_manager.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file prop_proof_manager
+/*! \file prop_proof_manager.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Haniel Barbosa

diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index 36913fda8b013cd1b6cbf9e8f6b5727d0b76c26b..985763c8465bacf822b88a720f95e532f51213f5 100644 (file)
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -5,7 +5,7 @@
  **   Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h
index da67f0c1ea9d919d10c4203d97d0835cacc95eef..79dc095493d4ee01af1e03cb3b2a62320cdc4dc8 100644 (file)
--- a/src/prop/sat_proof_manager.h
+++ b/src/prop/sat_proof_manager.h
@@ -5,7 +5,7 @@
  **   Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 65da2fc7c9528031e413419592eb9d39c636864d..d0d593f8ab469c0392ed15e53eeab5ce31a4cc52 100644 (file)
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_proxy.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Kshitij Bansal, Dejan Jovanovic
+ **   Kshitij Bansal, Tim King, Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/check_models.cpp b/src/smt/check_models.cpp
index 56d54eec99bef05b9c306228e0091ecfb67a69a8..a41c750eca027594e203180e4f6cf5e2a87dca3f 100644 (file)
--- a/src/smt/check_models.cpp
+++ b/src/smt/check_models.cpp
@@ -2,7 +2,7 @@
 /*! \file check_models.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Morgan Deters, Yoni Zohar
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 14b9ed0aa8be703bd5bba53fd69fc96d042ed3de..d02c1631e70b31ca3485d4846b19118b65c78041 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2,7 +2,7 @@
 /*! \file command.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Andrew Reynolds
+ **   Tim King, Abdalrhman Mohamed, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/command.h b/src/smt/command.h
index bfe5e737a7e86d13ddb50923e527fc92451ffc0b..399050d947a3640f044d49a13588c4cb7dd8b76b 100644 (file)
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -2,7 +2,7 @@
 /*! \file command.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Abdalrhman Mohamed
+ **   Abdalrhman Mohamed, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/dump_manager.cpp b/src/smt/dump_manager.cpp
index 51fcf8b5b3693441ab368de5e10cd3b0fb238345..706c2e8861a511e59fae16ff5493c607b1df10ee 100644 (file)
--- a/src/smt/dump_manager.cpp
+++ b/src/smt/dump_manager.cpp
@@ -2,7 +2,7 @@
 /*! \file dump_manager.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed
+ **   Andrew Reynolds, Gereon Kremer, Abdalrhman Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/dump_manager.h b/src/smt/dump_manager.h
index eaedf39a180363afb1bb3e2cb3d6b1fe843db783..3238d3a8d18b1159c0451f94a0f23c945ed78bdd 100644 (file)
--- a/src/smt/dump_manager.h
+++ b/src/smt/dump_manager.h
@@ -2,7 +2,7 @@
 /*! \file dump_manager.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed
+ **   Andrew Reynolds, Morgan Deters, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/expand_definitions.cpp b/src/smt/expand_definitions.cpp
index b0460fcc5996c2a5a3ca03ab89e7aff84552245f..4f49e1bbee3defffa08b925c3f29866a22def8cc 100644 (file)
--- a/src/smt/expand_definitions.cpp
+++ b/src/smt/expand_definitions.cpp
@@ -2,7 +2,7 @@
 /*! \file expand_definitions.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Haniel Barbosa
+ **   Andrew Reynolds, Morgan Deters, Andres Noetzli
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/expand_definitions.h b/src/smt/expand_definitions.h
index 5b75ddaddde9d0018cd2d0d130058691bcb48ded..486aa0c3a15f06c1828d49865bd3d1148d3cb767 100644 (file)
--- a/src/smt/expand_definitions.h
+++ b/src/smt/expand_definitions.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
-/*! \file process_assertions.h
+/*! \file expand_definitions.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Morgan Deters
+ **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/interpolation_solver.cpp b/src/smt/interpolation_solver.cpp
index c47d999512c00bbcc859333d145fc84d446ac9d7..09ddfde7555699545e9f9ec6f33ec5d02f50a594 100644 (file)
--- a/src/smt/interpolation_solver.cpp
+++ b/src/smt/interpolation_solver.cpp
@@ -2,10 +2,10 @@
 /*! \file interpolation_solver.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Ying Sheng
+ **   Ying Sheng, Andrew Reynolds, Abdalrhman Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/smt/interpolation_solver.h b/src/smt/interpolation_solver.h
index 096cf89833d8aee796e5c4eadca20d0fac403e53..c52614f744119f8545fcd32a09b3d297ae3c02c2 100644 (file)
--- a/src/smt/interpolation_solver.h
+++ b/src/smt/interpolation_solver.h
@@ -2,10 +2,10 @@
 /*! \file interpolation_solver.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Ying Sheng
+ **   Ying Sheng, Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/smt/listeners.h b/src/smt/listeners.h
index 150ee7ba8b8dbfb915d246edefec81825945a336..ce174e87214a44ee96de6f82f1c990a8acc95760 100644 (file)
--- a/src/smt/listeners.h
+++ b/src/smt/listeners.h
@@ -2,7 +2,7 @@
 /*! \file listeners.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner
+ **   Andrew Reynolds, Abdalrhman Mohamed, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/managed_ostreams.cpp b/src/smt/managed_ostreams.cpp
index 27a90cb56dabb5a350ae9beae296a6f89561c399..6056dd3d901e6fbe0ac23956574fef8e251541ea 100644 (file)
--- a/src/smt/managed_ostreams.cpp
+++ b/src/smt/managed_ostreams.cpp
@@ -2,7 +2,7 @@
 /*! \file managed_ostreams.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King
+ **   Tim King, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/model.cpp b/src/smt/model.cpp
index ccf73dda05bbdfc401c5fc7ac1baba3d56f1e230..557f9959f87b955510f85e11b15f4022e2af7f23 100644 (file)
--- a/src/smt/model.cpp
+++ b/src/smt/model.cpp
@@ -2,7 +2,7 @@
 /*! \file model.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-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/model_core_builder.cpp b/src/smt/model_core_builder.cpp
index cb8494e850b561dc3c76f8926e82287cf472fb9e..c2d92d3940e587e83f33583a884190225f1da538 100644 (file)
--- a/src/smt/model_core_builder.cpp
+++ b/src/smt/model_core_builder.cpp
@@ -2,7 +2,7 @@
 /*! \file model_core_builder.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner, Haniel Barbosa
+ **   Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/node_command.cpp b/src/smt/node_command.cpp
index 815f9913217e786ab016890886299d20b592cffd..33b5d995341d9399ddfad6de5ee189d74e64549e 100644 (file)
--- a/src/smt/node_command.cpp
+++ b/src/smt/node_command.cpp
@@ -2,7 +2,7 @@
 /*! \file node_command.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Abdalrhman Mohamed
+ **   Abdalrhman Mohamed, Yoni Zohar, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/options_manager.cpp b/src/smt/options_manager.cpp
index e028068ee962d11f47ba183536372cf58aa54f51..f449e79cb1f7b664e122e00ffcf12e3b95dfa5c5 100644 (file)
--- a/src/smt/options_manager.cpp
+++ b/src/smt/options_manager.cpp
@@ -2,7 +2,7 @@
 /*! \file options_manager.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/preprocess_proof_generator.cpp b/src/smt/preprocess_proof_generator.cpp
index bab56a0d2aa30e0ea4218bad899fd702b32c0116..cb2887ec0640b5f0a83104448e29d5d64a711d13 100644 (file)
--- a/src/smt/preprocess_proof_generator.cpp
+++ b/src/smt/preprocess_proof_generator.cpp
@@ -2,7 +2,7 @@
 /*! \file preprocess_proof_generator.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/preprocess_proof_generator.h b/src/smt/preprocess_proof_generator.h
index 41add5583be7b6dd1ca9a86353cf573a27a65bf0..01d9c89da6e072ebcd53dfe1b592eb113705c769 100644 (file)
--- a/src/smt/preprocess_proof_generator.h
+++ b/src/smt/preprocess_proof_generator.h
@@ -2,7 +2,7 @@
 /*! \file preprocess_proof_generator.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/preprocessor.cpp b/src/smt/preprocessor.cpp
index 9f2c8f3e7888be355a019da274166f3855cb82b8..c2b8f73f15589df6c210f94a45dc93233d66d620 100644 (file)
--- a/src/smt/preprocessor.cpp
+++ b/src/smt/preprocessor.cpp
@@ -2,7 +2,7 @@
 /*! \file preprocessor.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Aina Niemetz
+ **   Andrew Reynolds, Morgan Deters, Abdalrhman Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/process_assertions.cpp b/src/smt/process_assertions.cpp
index c68b73336d88e2b85a2f84561fcff9161b6562ff..fe3dbc62b2dbf0c40ba8cb839e577292ba50e24c 100644 (file)
--- a/src/smt/process_assertions.cpp
+++ b/src/smt/process_assertions.cpp
@@ -2,7 +2,7 @@
 /*! \file process_assertions.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Haniel Barbosa
+ **   Andrew Reynolds, Yoni Zohar, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index 53608fa0a89dcd04c6b92d37f74fb00b5222921d..049eb02c0ed50032a904047499047f1331c76043 100644 (file)
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -2,7 +2,7 @@
 /*! \file proof_post_processor.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/proof_post_processor.h b/src/smt/proof_post_processor.h
index 3c0d4fbaad09ed6309440cfb20058696ccab31cc..885608b38cded64184ef0d48dc6bc99645a6584a 100644 (file)
--- a/src/smt/proof_post_processor.h
+++ b/src/smt/proof_post_processor.h
@@ -2,7 +2,7 @@
 /*! \file proof_post_processor.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index aaff29479f8bf03c7f761c54ee37eceb842a274c..7e6bed464b0778f97ce5b4881ff7a9b53002c075 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -2,7 +2,7 @@
 /*! \file set_defaults.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
+ **   Andrew Reynolds, Andres Noetzli, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index dada78d9a3f1dfd54276c9bb5966debf34091d1c..e51d17c446f337b6927669828cb9738c8ab8b097 100644 (file)
--- a/src/smt/smt_engine_state.cpp
+++ b/src/smt/smt_engine_state.cpp
@@ -2,7 +2,7 @@
 /*! \file smt_engine_state.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Aina Niemetz
+ **   Andrew Reynolds, Morgan Deters, Ying Sheng
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/smt_engine_state.h b/src/smt/smt_engine_state.h
index f033be0317aec6f46e4c34dbdd340b89bd962f43..b085c26a3938f9c4f67b935861da48ae85fbe73f 100644 (file)
--- a/src/smt/smt_engine_state.h
+++ b/src/smt/smt_engine_state.h
@@ -2,7 +2,7 @@
 /*! \file smt_engine_state.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Aina Niemetz, Morgan Deters
+ **   Andrew Reynolds, Ying Sheng, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/sygus_solver.cpp b/src/smt/sygus_solver.cpp
index 0b40bf8948de5056fd7c82b3167a8dff08d11274..42dbcd43ef2ae5e64aab9b2cb040e0f314813589 100644 (file)
--- a/src/smt/sygus_solver.cpp
+++ b/src/smt/sygus_solver.cpp
@@ -2,7 +2,7 @@
 /*! \file sygus_solver.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Haniel Barbosa, Andres Noetzli
+ **   Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/sygus_solver.h b/src/smt/sygus_solver.h
index b523ff5b75b6375fbb743accf4013599eaaca7c2..c9de7b7e9e480ef0e3b9b67045f929f1145f52dc 100644 (file)
--- a/src/smt/sygus_solver.h
+++ b/src/smt/sygus_solver.h
@@ -2,7 +2,7 @@
 /*! \file sygus_solver.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Haniel Barbosa, Morgan Deters
+ **   Andrew Reynolds, Haniel Barbosa, Abdalrhman Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/smt/update_ostream.h b/src/smt/update_ostream.h
index fd33beec75b9127aab537d425c991d343a94713e..98aaead882bbdd06b0869363fcb5ccaffd875448 100644 (file)
--- a/src/smt/update_ostream.h
+++ b/src/smt/update_ostream.h
@@ -2,7 +2,7 @@
 /*! \file update_ostream.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Mathias Preiner
+ **   Tim King, Mathias Preiner, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index 2432e6945fc1f61961944f60e7154ac5532f1ccc..49cf9fe0a296972019061186b6f9616fe3e9a12d 100644 (file)
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -2,7 +2,7 @@
 /*! \file approx_simplex.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Mathias Preiner, Morgan Deters
+ **   Tim King, Aina Niemetz, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index a65fbd961f1b9b3fa21a3fb7bc6e54377d612028..a990b426fdc78243b50c0c2fc8b34759fc843be7 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -2,7 +2,7 @@
 /*! \file arith_rewriter.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andrew Reynolds, Morgan Deters
+ **   Andrew Reynolds, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 8f35acd1cf7250c65d12dceb3b6afdef65345c9c..6c858d1ebc6c8e0984fd6e8a4e45728170612c45 100644 (file)
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -2,7 +2,7 @@
 /*! \file arith_rewriter.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Andres Noetzli
+ **   Dejan Jovanovic, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/arith_utilities.cpp b/src/theory/arith/arith_utilities.cpp
index 1a5bc356f9e4807fe9bd1473c61399f337c42dcc..fc34d2a6d324b30abbb91491bab21af4f5f24bd0 100644 (file)
--- a/src/theory/arith/arith_utilities.cpp
+++ b/src/theory/arith/arith_utilities.cpp
@@ -2,7 +2,7 @@
 /*! \file arith_utilities.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
+ **   Andrew Reynolds, Alex Ozdemir, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index 22802b5583b9061ba0f1d256b872a47f103723ec..72f8e49fffca8944acb53b9c1bc9fcdfc0245f5e 100644 (file)
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.cpp
@@ -2,7 +2,7 @@
 /*! \file attempt_solution_simplex.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Mathias Preiner
+ **   Tim King, Aina Niemetz, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/bound_inference.cpp b/src/theory/arith/bound_inference.cpp
index c8a9527c7a4e94d864e82ab5dfad3fbd9159d742..29be87d7bb8fd421869377f89347de083abd0717 100644 (file)
--- a/src/theory/arith/bound_inference.cpp
+++ b/src/theory/arith/bound_inference.cpp
@@ -4,8 +4,8 @@
  ** Top contributors (to current version):
  **   Gereon Kremer
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/bound_inference.h b/src/theory/arith/bound_inference.h
index 174ba3a0f16c256175df349f6ea47adb73601061..9d78d88c91629723896ba74c5c8bfa0c19c13b78 100644 (file)
--- a/src/theory/arith/bound_inference.h
+++ b/src/theory/arith/bound_inference.h
@@ -4,8 +4,8 @@
  ** Top contributors (to current version):
  **   Gereon Kremer
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 57214e0f897b490cce045c6ec230773dc9a0c002..03dc28d6a07b44a5c563ef8a962c3bfd6c16e6c0 100644 (file)
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -2,7 +2,7 @@
 /*! \file congruence_manager.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andrew Reynolds, Dejan Jovanovic
+ **   Tim King, Alex Ozdemir, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 3698f46d828715f242c73bd6e35b43707f996c64..80e1ef8befed32065b0539f4b323be3ebd151a35 100644 (file)
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -2,7 +2,7 @@
 /*! \file congruence_manager.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andrew Reynolds, Mathias Preiner
+ **   Alex Ozdemir, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index 4ac3034ff6013ef42f48bce0d5eeda1fecfd1f8b..374b17d887b7f1969deeb384c9d17e248dbe4faa 100644 (file)
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -2,7 +2,7 @@
 /*! \file dual_simplex.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Mathias Preiner
+ **   Tim King, Aina Niemetz, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 33f01eba14bd1ddffb3d736836aa8edb2dbea28c..85af862fad47c38e9f0eb8368934b4c2b0eaec5a 100644 (file)
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -2,7 +2,7 @@
 /*! \file fc_simplex.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Mathias Preiner, Morgan Deters
+ **   Tim King, Aina Niemetz, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/inference_id.cpp b/src/theory/arith/inference_id.cpp
index a93a980ba7fb120ebb31700e083107ac4e77a6f9..0c2ead445a984b9a1eeb87e6d7ca6a5f103535f6 100644 (file)
--- a/src/theory/arith/inference_id.cpp
+++ b/src/theory/arith/inference_id.cpp
@@ -2,7 +2,7 @@
 /*! \file inference_id.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Gereon Kremer, Yoni Zohar
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/inference_id.h b/src/theory/arith/inference_id.h
index c01cd2c8e78d2600cfa30ad1be5fcbacaa1099d1..ea7fd6fe9cb3563c2dab8f3943479df4792947d0 100644 (file)
--- a/src/theory/arith/inference_id.h
+++ b/src/theory/arith/inference_id.h
@@ -2,7 +2,7 @@
 /*! \file inference_id.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Gereon Kremer
+ **   Andrew Reynolds, Gereon Kremer, Yoni Zohar
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/ext/constraint.h b/src/theory/arith/nl/ext/constraint.h
index 699d5b3500abac4fc2cfa879d64d229f24dd6da8..7b7c604bfb2750f157bd0037e0e1323935d4e93a 100644 (file)
--- a/src/theory/arith/nl/ext/constraint.h
+++ b/src/theory/arith/nl/ext/constraint.h
@@ -2,7 +2,7 @@
 /*! \file constraint.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/ext/ext_state.cpp b/src/theory/arith/nl/ext/ext_state.cpp
index 3ac4699a7860a1fe88eb6950401b63bf291d386f..d850ff34e8fe05c711002acf5f291452bb8312f4 100644 (file)
--- a/src/theory/arith/nl/ext/ext_state.cpp
+++ b/src/theory/arith/nl/ext/ext_state.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
-/*! \file shared_check_data.cpp
+/*! \file ext_state.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Andrew Reynolds, Gereon Kremer, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/ext/ext_state.h b/src/theory/arith/nl/ext/ext_state.h
index 64c9c6b94af7871502f461bbe6ef59908cae3442..adf576c8bbc15322bc6fec9e6edc544bca6845b7 100644 (file)
--- a/src/theory/arith/nl/ext/ext_state.h
+++ b/src/theory/arith/nl/ext/ext_state.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
-/*! \file shared_check_data.h
+/*! \file ext_state.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Gereon Kremer, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/ext/factoring_check.cpp b/src/theory/arith/nl/ext/factoring_check.cpp
index e329db121ccd85d612506e0cd7dbb58662c069eb..71c584e91983a3d80eb6c78d5f28cb406854729e 100644 (file)
--- a/src/theory/arith/nl/ext/factoring_check.cpp
+++ b/src/theory/arith/nl/ext/factoring_check.cpp
@@ -2,7 +2,7 @@
 /*! \file factoring_check.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Andrew Reynolds, Gereon Kremer, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/ext/factoring_check.h b/src/theory/arith/nl/ext/factoring_check.h
index 8474ac6102fefbeb09ec2b1613036ce23434c97f..9f879aa39cdefb7dc30656f300dd2a9796ea7bc8 100644 (file)
--- a/src/theory/arith/nl/ext/factoring_check.h
+++ b/src/theory/arith/nl/ext/factoring_check.h
@@ -2,7 +2,7 @@
 /*! \file factoring_check.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Andrew Reynolds, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/ext/monomial.h b/src/theory/arith/nl/ext/monomial.h
index 93a291ca0fc03c68c3710b18d217dafe249e49aa..a1cc8d7ff91387bfbfcc9cf062cbd476b8ad704a 100644 (file)
--- a/src/theory/arith/nl/ext/monomial.h
+++ b/src/theory/arith/nl/ext/monomial.h
@@ -2,7 +2,7 @@
 /*! \file monomial.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
+ **   Andrew Reynolds, Tim King, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.cpp b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
index de6a3c65dc0fd0bdbfff39e22df86c6c0f645bc4..9eb496de8a75b119b1e5cca6ae1fbbb85b029bd6 100644 (file)
--- a/src/theory/arith/nl/ext/monomial_bounds_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.cpp
@@ -2,7 +2,7 @@
 /*! \file monomial_bounds_check.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Andrew Reynolds, Gereon Kremer, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/ext/monomial_bounds_check.h b/src/theory/arith/nl/ext/monomial_bounds_check.h
index d919b12723469758f4c6ba3980e485bcfa335f5c..9977d75340e95afc7a4c24b97ac0d2c6ea385635 100644 (file)
--- a/src/theory/arith/nl/ext/monomial_bounds_check.h
+++ b/src/theory/arith/nl/ext/monomial_bounds_check.h
@@ -2,7 +2,7 @@
 /*! \file monomial_bounds_check.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Andrew Reynolds, Gereon Kremer, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/ext/monomial_check.cpp b/src/theory/arith/nl/ext/monomial_check.cpp
index 3b8d52c13b1519409939060ce4804798ec29d7fb..a70fa1bc0bbf55a9589a3c329bacd02ab744c19b 100644 (file)
--- a/src/theory/arith/nl/ext/monomial_check.cpp
+++ b/src/theory/arith/nl/ext/monomial_check.cpp
@@ -2,7 +2,7 @@
 /*! \file monomial_check.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Andrew Reynolds, Gereon Kremer, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/ext/monomial_check.h b/src/theory/arith/nl/ext/monomial_check.h
index 89b5847a29603e61350644e8938dbda2bebab708..ed8639ef28ad7e9d6470fa40fe5fcb30f0092f5c 100644 (file)
--- a/src/theory/arith/nl/ext/monomial_check.h
+++ b/src/theory/arith/nl/ext/monomial_check.h
@@ -2,7 +2,7 @@
 /*! \file monomial_check.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Andrew Reynolds, Gereon Kremer, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/ext/split_zero_check.h b/src/theory/arith/nl/ext/split_zero_check.h
index 1a9f0a44d6253f7e0ae4b57fafa460facc9840bb..131ad4c99d13e957700a46c3b206549bcbbcc568 100644 (file)
--- a/src/theory/arith/nl/ext/split_zero_check.h
+++ b/src/theory/arith/nl/ext/split_zero_check.h
@@ -2,7 +2,7 @@
 /*! \file split_zero_check.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Gereon Kremer, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/ext/tangent_plane_check.cpp b/src/theory/arith/nl/ext/tangent_plane_check.cpp
index 3849c84242358776781c4d201c10984005be566c..de6176272e7dc42f197e0c22e8a8f81152f5fd39 100644 (file)
--- a/src/theory/arith/nl/ext/tangent_plane_check.cpp
+++ b/src/theory/arith/nl/ext/tangent_plane_check.cpp
@@ -2,7 +2,7 @@
 /*! \file tangent_plane_check.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Andrew Reynolds, Gereon Kremer, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/ext/tangent_plane_check.h b/src/theory/arith/nl/ext/tangent_plane_check.h
index 748ab63726c89b1f751fab801149352571fede8b..84b6c0ba4e4bb05f74de28fb5e315a39c0c4d155 100644 (file)
--- a/src/theory/arith/nl/ext/tangent_plane_check.h
+++ b/src/theory/arith/nl/ext/tangent_plane_check.h
@@ -2,7 +2,7 @@
 /*! \file tangent_plane_check.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Andrew Reynolds, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index e33cfa6cddd2f0b567efcb279819470d51c9435b..4d17080a6fb4fcc045d579f774844c19fe0cdcb9 100644 (file)
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -2,7 +2,7 @@
 /*! \file iand_solver.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Gereon Kremer, Tim King
+ **   Andrew Reynolds, Yoni Zohar, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index e00cb92a9b483a81789c302d874019a4cc9d1088..8d91cc28a25301f754912d2f4b2d67cb1e48b408 100644 (file)
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -2,7 +2,7 @@
 /*! \file iand_solver.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Tianyi Liang
+ **   Andrew Reynolds, Yoni Zohar, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/iand_table.cpp b/src/theory/arith/nl/iand_table.cpp
index 050e6baed305c5135d696b645eb2b11ba68de639..550f36d92cf8f7d2dc8cc02b1a4a26d6816c459c 100644 (file)
--- a/src/theory/arith/nl/iand_table.cpp
+++ b/src/theory/arith/nl/iand_table.cpp
@@ -5,7 +5,7 @@
  **   Yoni Zohar
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/nl/iand_table.h b/src/theory/arith/nl/iand_table.h
index 6387885b7e76548e766e1682546370f47e524402..39eb82355b7ca663b750410d680197053be1a82c 100644 (file)
--- a/src/theory/arith/nl/iand_table.h
+++ b/src/theory/arith/nl/iand_table.h
@@ -5,7 +5,7 @@
  **   Yoni Zohar
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/nl/icp/candidate.cpp b/src/theory/arith/nl/icp/candidate.cpp
index df8e18818009544436d8b23508e8a273b459cb21..5dc2443d0422548f8fb2d5fba207e7bc4c2aa7f9 100644 (file)
--- a/src/theory/arith/nl/icp/candidate.cpp
+++ b/src/theory/arith/nl/icp/candidate.cpp
@@ -4,8 +4,8 @@
  ** Top contributors (to current version):
  **   Gereon Kremer
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/nl/icp/candidate.h b/src/theory/arith/nl/icp/candidate.h
index 7980e5c971919b0d34b0a0704c79dcf7dd0040ec..a2160472d738a8142121dcc9956af271110a2215 100644 (file)
--- a/src/theory/arith/nl/icp/candidate.h
+++ b/src/theory/arith/nl/icp/candidate.h
@@ -4,8 +4,8 @@
  ** Top contributors (to current version):
  **   Gereon Kremer
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/nl/icp/contraction_origins.cpp b/src/theory/arith/nl/icp/contraction_origins.cpp
index 779c000b76e0531cee4919e935606ec69670fb15..8589155370f519d2db4c36c9d04da93e4f36d26a 100644 (file)
--- a/src/theory/arith/nl/icp/contraction_origins.cpp
+++ b/src/theory/arith/nl/icp/contraction_origins.cpp
@@ -4,8 +4,8 @@
  ** Top contributors (to current version):
  **   Gereon Kremer
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/nl/icp/contraction_origins.h b/src/theory/arith/nl/icp/contraction_origins.h
index 885fc740a48c2ffe08c0079b523adc613a5c62f1..360641704589ffda6dd5165b25a2b17c54d554b7 100644 (file)
--- a/src/theory/arith/nl/icp/contraction_origins.h
+++ b/src/theory/arith/nl/icp/contraction_origins.h
@@ -4,8 +4,8 @@
  ** Top contributors (to current version):
  **   Gereon Kremer
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/nl/icp/icp_solver.cpp b/src/theory/arith/nl/icp/icp_solver.cpp
index b4cb54216a79147dc926f1c54cef2170adccb273..ec32656e086f0a8f19f496a9962201ceaec1581b 100644 (file)
--- a/src/theory/arith/nl/icp/icp_solver.cpp
+++ b/src/theory/arith/nl/icp/icp_solver.cpp
@@ -2,10 +2,10 @@
 /*! \file icp_solver.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Gereon Kremer, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/nl/icp/icp_solver.h b/src/theory/arith/nl/icp/icp_solver.h
index 32861c6410dad24356b2cb4d60825938c862de26..176549d8b92c1b281f80385865d3692bbb774a8e 100644 (file)
--- a/src/theory/arith/nl/icp/icp_solver.h
+++ b/src/theory/arith/nl/icp/icp_solver.h
@@ -2,10 +2,10 @@
 /*! \file icp_solver.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Gereon Kremer, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/nl/icp/intersection.cpp b/src/theory/arith/nl/icp/intersection.cpp
index 148059db0ef3c2a487052896baefdbec1abf4341..aa8fcf543bb8760036c05cadb6f722a0f4640e27 100644 (file)
--- a/src/theory/arith/nl/icp/intersection.cpp
+++ b/src/theory/arith/nl/icp/intersection.cpp
@@ -4,8 +4,8 @@
  ** Top contributors (to current version):
  **   Gereon Kremer
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/nl/icp/intersection.h b/src/theory/arith/nl/icp/intersection.h
index 8d772cb7ac3ad605970e8b3ad561d7018390ccb5..0df6caf34b0fb00456cbabc72e31fffb0946e2eb 100644 (file)
--- a/src/theory/arith/nl/icp/intersection.h
+++ b/src/theory/arith/nl/icp/intersection.h
@@ -4,8 +4,8 @@
  ** Top contributors (to current version):
  **   Gereon Kremer
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/nl/icp/interval.h b/src/theory/arith/nl/icp/interval.h
index 374067961ca96050c652810a71e94e337d8dc5ae..d2b0fd4f5808479f557203cb41950595ef6ce383 100644 (file)
--- a/src/theory/arith/nl/icp/interval.h
+++ b/src/theory/arith/nl/icp/interval.h
@@ -4,8 +4,8 @@
  ** Top contributors (to current version):
  **   Gereon Kremer
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h
index b563384a5bf489f2a3dfc0570fb00d76b88e7746..88706350ba4d4fbd88873b7a00239168967f10a5 100644 (file)
--- a/src/theory/arith/nl/nonlinear_extension.h
+++ b/src/theory/arith/nl/nonlinear_extension.h
@@ -2,7 +2,7 @@
 /*! \file nonlinear_extension.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Gereon Kremer
+ **   Andrew Reynolds, Gereon Kremer, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/strategy.cpp b/src/theory/arith/nl/strategy.cpp
index 627500d6812f8104fcc0c0d0ff9789a951935d0e..90ab14ac59b7cc0a7d2bc73cc00201399f92fd4f 100644 (file)
--- a/src/theory/arith/nl/strategy.cpp
+++ b/src/theory/arith/nl/strategy.cpp
@@ -2,10 +2,10 @@
 /*! \file strategy.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Gereon Kremer
+ **   Gereon Kremer, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/nl/strategy.h b/src/theory/arith/nl/strategy.h
index ad96d94420dbf2e2abd27a192489ef61e69e0e67..526ae36f12ccbb3f5c3a1236034132748fb751fd 100644 (file)
--- a/src/theory/arith/nl/strategy.h
+++ b/src/theory/arith/nl/strategy.h
@@ -5,7 +5,7 @@
  **   Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arith/nl/transcendental/exponential_solver.cpp b/src/theory/arith/nl/transcendental/exponential_solver.cpp
index 482e3bc21408071ec25aee65923841b0bf2ab20f..0726e03b33e8ab93363a6f6e10e7771c246e5986 100644 (file)
--- a/src/theory/arith/nl/transcendental/exponential_solver.cpp
+++ b/src/theory/arith/nl/transcendental/exponential_solver.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
-/*! \file transcendental_solver.cpp
+/*! \file exponential_solver.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Gereon Kremer
+ **   Gereon Kremer, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/transcendental/exponential_solver.h b/src/theory/arith/nl/transcendental/exponential_solver.h
index b4d08559a04b099b230eb8c264cebf5cc5ae4c46..f1a30b17746d31398f7d22e35763fef4930f88c2 100644 (file)
--- a/src/theory/arith/nl/transcendental/exponential_solver.h
+++ b/src/theory/arith/nl/transcendental/exponential_solver.h
@@ -2,7 +2,7 @@
 /*! \file exponential_solver.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
+ **   Gereon Kremer, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/transcendental/sine_solver.cpp b/src/theory/arith/nl/transcendental/sine_solver.cpp
index cba85b80ea9fd0347a24192aa9f59422e725579a..5eed810b37d2567e8f83405338f4a3e5c5cf536b 100644 (file)
--- a/src/theory/arith/nl/transcendental/sine_solver.cpp
+++ b/src/theory/arith/nl/transcendental/sine_solver.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
-/*! \file transcendental_solver.cpp
+/*! \file sine_solver.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Gereon Kremer
+ **   Gereon Kremer, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/transcendental/sine_solver.h b/src/theory/arith/nl/transcendental/sine_solver.h
index e41e6bd4ffba1cd9d3ec0d04a663401b09ddd56f..15f7d46e838dccedb4ff62520710feaf731af1bb 100644 (file)
--- a/src/theory/arith/nl/transcendental/sine_solver.h
+++ b/src/theory/arith/nl/transcendental/sine_solver.h
@@ -2,7 +2,7 @@
 /*! \file sine_solver.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
+ **   Gereon Kremer, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/transcendental/taylor_generator.cpp b/src/theory/arith/nl/transcendental/taylor_generator.cpp
index 1b7257f8f39fac130c17190e8d7a412e3081c1d9..745cba17a84fd8c805ca3b5cc9ba5c9500f4a7c5 100644 (file)
--- a/src/theory/arith/nl/transcendental/taylor_generator.cpp
+++ b/src/theory/arith/nl/transcendental/taylor_generator.cpp
@@ -2,7 +2,7 @@
 /*! \file taylor_generator.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
+ **   Andrew Reynolds, Gereon Kremer, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/transcendental/taylor_generator.h b/src/theory/arith/nl/transcendental/taylor_generator.h
index 2dbfcccdedf4eb396d13db70a11385bb90505f7c..261583ca96c37bd1bf22cdf4cfced99b3670ca48 100644 (file)
--- a/src/theory/arith/nl/transcendental/taylor_generator.h
+++ b/src/theory/arith/nl/transcendental/taylor_generator.h
@@ -2,7 +2,7 @@
 /*! \file taylor_generator.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
+ **   Andrew Reynolds, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.cpp b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
index ad3f49576f8951fc5958e25a904a3953a8330c59..2a22853a2cffa347b245a2641f37cddba2ecdef4 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_solver.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.cpp
@@ -2,7 +2,7 @@
 /*! \file transcendental_solver.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Gereon Kremer
+ **   Andrew Reynolds, Gereon Kremer, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/transcendental/transcendental_solver.h b/src/theory/arith/nl/transcendental/transcendental_solver.h
index b0db79b6a08608151ccf6e2c32ef306fd74e32f9..80def6f05aebd7c2f13a6e65dbf1faa63fe9e4f2 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_solver.h
+++ b/src/theory/arith/nl/transcendental/transcendental_solver.h
@@ -1,3 +1,19 @@
+/*********************                                                        */
+/*! \file transcendental_solver.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds, Gereon Kremer, Tim King
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
 
 /*********************                                                        */
 /*! \file transcendental_solver.h

diff --git a/src/theory/arith/nl/transcendental/transcendental_state.cpp b/src/theory/arith/nl/transcendental/transcendental_state.cpp
index 69678c6218af76a689dc115db5d47d0e0d087630..0e47f425773ac5692b40cf1759caa02e9df43dd1 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_state.cpp
+++ b/src/theory/arith/nl/transcendental/transcendental_state.cpp
@@ -2,7 +2,7 @@
 /*! \file transcendental_state.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Gereon Kremer
+ **   Andrew Reynolds, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/nl/transcendental/transcendental_state.h b/src/theory/arith/nl/transcendental/transcendental_state.h
index e1510c3b371ff715e23444e5aefb605129d55524..7062e8183307b1535cdb93cfb1918ce9644d71ed 100644 (file)
--- a/src/theory/arith/nl/transcendental/transcendental_state.h
+++ b/src/theory/arith/nl/transcendental/transcendental_state.h
@@ -2,7 +2,7 @@
 /*! \file transcendental_state.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
+ **   Gereon Kremer, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index fc9a86f498a3c4d9e74a1d5b940a7a38ad845491..ed02a8d4ed11eddfe3d1da2392b5fb56163b0116 100644 (file)
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -2,7 +2,7 @@
 /*! \file normal_form.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andrew Reynolds, Morgan Deters
+ **   Tim King, Gereon Kremer, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 79cae2fff8358c5bc6182f3e56f745c023e0d872..ea20de71dea43b1d4066204053c3205ee89fa910 100644 (file)
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -2,7 +2,7 @@
 /*! \file normal_form.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Mathias Preiner
+ **   Tim King, Morgan Deters, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 3f2fca50f114ebcb2a03b665d52bf47af61d6f5c..18169474d7901d7ea06ff2738c12dd1867b35d2b 100644 (file)
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -2,7 +2,7 @@
 /*! \file soi_simplex.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Mathias Preiner
+ **   Tim King, Aina Niemetz, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index b5c0d1bd027c9e41f2e9ebe13c5a7ba857c31302..247772897cfac64a12c42a4d5cc27879d62a9c67 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_arith.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Dejan Jovanovic
+ **   Andrew Reynolds, Tim King, Alex Ozdemir
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 74f2bdbd3d2b560d441d10b0a58c88dd9f37caa0..ce0445d1f120df79dcb4b9930ea8352300d4a051 100644 (file)
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_arith_private.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andrew Reynolds, Mathias Preiner
+ **   Tim King, Alex Ozdemir, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/arrays/inference_manager.cpp b/src/theory/arrays/inference_manager.cpp
index f429140be563a42a52ef2294defe4cd0e788ad71..ec6890293027f8dda484ab333a7088b35abfbe9f 100644 (file)
--- a/src/theory/arrays/inference_manager.cpp
+++ b/src/theory/arrays/inference_manager.cpp
@@ -5,7 +5,7 @@
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arrays/inference_manager.h b/src/theory/arrays/inference_manager.h
index 2073fac6a772ecfc440dd4c4319cd1efa69e9550..b4ae228be2d93623e595a00972d5e7316872faae 100644 (file)
--- a/src/theory/arrays/inference_manager.h
+++ b/src/theory/arrays/inference_manager.h
@@ -2,10 +2,10 @@
 /*! \file inference_manager.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arrays/proof_checker.cpp b/src/theory/arrays/proof_checker.cpp
index a3cd82678ebb236be938ee322e5467ba9031cafc..e529d981cd102935f59d35d2e3e867518a1f00a6 100644 (file)
--- a/src/theory/arrays/proof_checker.cpp
+++ b/src/theory/arrays/proof_checker.cpp
@@ -2,10 +2,10 @@
 /*! \file proof_checker.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Haniel Barbosa
+ **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arrays/proof_checker.h b/src/theory/arrays/proof_checker.h
index 3bf7afecb93b71de2d858d48dafc435883ad6e97..7fa574eeba53284b6c04639555638274553e8e94 100644 (file)
--- a/src/theory/arrays/proof_checker.h
+++ b/src/theory/arrays/proof_checker.h
@@ -5,7 +5,7 @@
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arrays/skolem_cache.cpp b/src/theory/arrays/skolem_cache.cpp
index 70217a4d7f692ef9fb328c5f4b2efcbeddaa279c..4028a53a8893c15e720c733d96ddf12233418450 100644 (file)
--- a/src/theory/arrays/skolem_cache.cpp
+++ b/src/theory/arrays/skolem_cache.cpp
@@ -2,10 +2,10 @@
 /*! \file skolem_cache.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/arrays/skolem_cache.h b/src/theory/arrays/skolem_cache.h
index b07e87dc667aec30cb5ba79bd5f5a3e9cce5a6a2..dd4ac2e5bbcab25fdca2ea3f5fb91f7b75036ec8 100644 (file)
--- a/src/theory/arrays/skolem_cache.h
+++ b/src/theory/arrays/skolem_cache.h
@@ -2,10 +2,10 @@
 /*! \file skolem_cache.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bags/bags_rewriter.cpp b/src/theory/bags/bags_rewriter.cpp
index 9479d2cc287caf25c9433edf4cc7426234e3ef80..aee57c74d7c6192dea471d20853ade665f0510f6 100644 (file)
--- a/src/theory/bags/bags_rewriter.cpp
+++ b/src/theory/bags/bags_rewriter.cpp
@@ -5,7 +5,7 @@
  **   Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bags/bags_rewriter.h b/src/theory/bags/bags_rewriter.h
index a9b3b90bb5874afe54b8f45467a556290690f813..8425e3b1fa1729c591388ea1f587ce341c1c03cc 100644 (file)
--- a/src/theory/bags/bags_rewriter.h
+++ b/src/theory/bags/bags_rewriter.h
@@ -5,7 +5,7 @@
  **   Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bags/inference_manager.cpp b/src/theory/bags/inference_manager.cpp
index 4d18ad92652f14ee1ea01582385a2b82ea010633..eb695725e9e334e762042ab004a350ea370e76ff 100644 (file)
--- a/src/theory/bags/inference_manager.cpp
+++ b/src/theory/bags/inference_manager.cpp
@@ -2,10 +2,10 @@
 /*! \file inference_manager.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Mudathir Mohamed
+ **   Mudathir Mohamed, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bags/inference_manager.h b/src/theory/bags/inference_manager.h
index 4b4edbaefb43e170f4ac99991a13787e604c5bf7..90d188d333de2206390fefea8a7ef1dc61fcc9af 100644 (file)
--- a/src/theory/bags/inference_manager.h
+++ b/src/theory/bags/inference_manager.h
@@ -5,7 +5,7 @@
  **   Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bags/make_bag_op.cpp b/src/theory/bags/make_bag_op.cpp
index b6082278372aab3938c50ea2922c2df972d179ae..ac3d8942a65cb104de4b3156b2a77181110ef9cc 100644 (file)
--- a/src/theory/bags/make_bag_op.cpp
+++ b/src/theory/bags/make_bag_op.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file bag_op.cpp
+/*! \file make_bag_op.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Mudathir Mohamed

diff --git a/src/theory/bags/make_bag_op.h b/src/theory/bags/make_bag_op.h
index b479308794cac45d0fd6b6ccdf9a61dd86e2bb6b..a53000651e117e63c51daec8e7b9c4cca0ba1999 100644 (file)
--- a/src/theory/bags/make_bag_op.h
+++ b/src/theory/bags/make_bag_op.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file mk_bag_op.h
+/*! \file make_bag_op.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Mudathir Mohamed

diff --git a/src/theory/bags/normal_form.cpp b/src/theory/bags/normal_form.cpp
index 081ed77aaf5e7c814b5184c24fc5295943e951ee..88c41a96127251ce82c9017938849a06ca14eeec 100644 (file)
--- a/src/theory/bags/normal_form.cpp
+++ b/src/theory/bags/normal_form.cpp
@@ -1,15 +1,16 @@
-/*************************                                                    */
+/*********************                                                        */
 /*! \file normal_form.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
+ **
+ ** \brief Normal form for bag constants.
  **/
-
 #include "normal_form.h"
 
 #include "theory/sets/normal_form.h"
@@ -653,4 +654,4 @@ Node NormalForm::evaluateToSet(TNode n)
 
 }  // namespace bags
 }  // namespace theory
-}  // namespace CVC4
\ No newline at end of file
+}  // namespace CVC4

diff --git a/src/theory/bags/normal_form.h b/src/theory/bags/normal_form.h
index 5a7936fa3dc36a2845f41ebd4542cff9bd8b243a..e88fe6fefce79932fa2b7b99130c041209fa8e4a 100644 (file)
--- a/src/theory/bags/normal_form.h
+++ b/src/theory/bags/normal_form.h
@@ -5,7 +5,7 @@
  **   Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bags/solver_state.cpp b/src/theory/bags/solver_state.cpp
index 77204ae76ffedbf5c277e0785b795415d7698d31..d58b686579ab5910c64e2557afe642f7d1043727 100644 (file)
--- a/src/theory/bags/solver_state.cpp
+++ b/src/theory/bags/solver_state.cpp
@@ -2,10 +2,10 @@
 /*! \file solver_state.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Mudathir Mohamed
+ **   Mudathir Mohamed, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bags/solver_state.h b/src/theory/bags/solver_state.h
index f5b67cb7873645a951c84f6ea196f534f6c7bdc4..9a4bfdae7d5b92e1bf7b81c4e78166c8b6f545df 100644 (file)
--- a/src/theory/bags/solver_state.h
+++ b/src/theory/bags/solver_state.h
@@ -5,7 +5,7 @@
  **   Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bags/term_registry.cpp b/src/theory/bags/term_registry.cpp
index 60beef29f9d31b019510e578cdd48523ae9d74ba..c413a7f90e7390206ce452bf834255615c9156ae 100644 (file)
--- a/src/theory/bags/term_registry.cpp
+++ b/src/theory/bags/term_registry.cpp
@@ -2,10 +2,10 @@
 /*! \file term_registry.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Mudathir Mohamed
+ **   Mudathir Mohamed, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bags/term_registry.h b/src/theory/bags/term_registry.h
index d284126eef7f13bdc1466d65e0fffd7cc239a7d0..abf6f180cb607baf23ae3f927a7ccb2ad5110c1b 100644 (file)
--- a/src/theory/bags/term_registry.h
+++ b/src/theory/bags/term_registry.h
@@ -5,7 +5,7 @@
  **   Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bags/theory_bags.cpp b/src/theory/bags/theory_bags.cpp
index 9f62ea1c62ffb5941adf42fbe2a6bc30c164fe95..6ba1ad87a19c62c0e4385331c970b58f156aaea6 100644 (file)
--- a/src/theory/bags/theory_bags.cpp
+++ b/src/theory/bags/theory_bags.cpp
@@ -5,7 +5,7 @@
  **   Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bags/theory_bags.h b/src/theory/bags/theory_bags.h
index 08bc5f33aa8c78e68145a592afa22f4e198a8d30..03676c2d2c367d34b6a4ba91591588f3df4442cb 100644 (file)
--- a/src/theory/bags/theory_bags.h
+++ b/src/theory/bags/theory_bags.h
@@ -5,7 +5,7 @@
  **   Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bags/theory_bags_type_enumerator.cpp b/src/theory/bags/theory_bags_type_enumerator.cpp
index 727407937cd40f13cba30a85c98d7ef47e1b1ed6..a1a1d13c2c735bb81cfdfb97f92908a0c37c7ba7 100644 (file)
--- a/src/theory/bags/theory_bags_type_enumerator.cpp
+++ b/src/theory/bags/theory_bags_type_enumerator.cpp
@@ -5,7 +5,7 @@
  **   Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bags/theory_bags_type_enumerator.h b/src/theory/bags/theory_bags_type_enumerator.h
index a1ba896c1d943e2bd4b89045e479b321702ad3ef..dda87c85e720bfc7ce3c2bf62c5e9c7e5c3c1a19 100644 (file)
--- a/src/theory/bags/theory_bags_type_enumerator.h
+++ b/src/theory/bags/theory_bags_type_enumerator.h
@@ -5,7 +5,7 @@
  **   Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bags/theory_bags_type_rules.h b/src/theory/bags/theory_bags_type_rules.h
index cece40c9ea0bb3641b3e4383b50ca70f74f84059..dd8c75328aa9330e15c6428609e58da581f5a23d 100644 (file)
--- a/src/theory/bags/theory_bags_type_rules.h
+++ b/src/theory/bags/theory_bags_type_rules.h
@@ -4,8 +4,8 @@
  ** Top contributors (to current version):
  **   Mudathir Mohamed
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/booleans/circuit_propagator.cpp b/src/theory/booleans/circuit_propagator.cpp
index 270c0b9a93e01f8f468afe7dfc1bce0845d9d74c..24e821e33cf42e6c90b358b13eccbec59b36bb94 100644 (file)
--- a/src/theory/booleans/circuit_propagator.cpp
+++ b/src/theory/booleans/circuit_propagator.cpp
@@ -2,7 +2,7 @@
 /*! \file circuit_propagator.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Morgan Deters, Andrew Reynolds
+ **   Gereon Kremer, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 4c7c2d124eeecca858c3b9e54acf4c85afa3226c..3546a4d35d04eb3da730f7a7f04aad28491a15a5 100644 (file)
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -2,7 +2,7 @@
 /*! \file circuit_propagator.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters, Dejan Jovanovic
+ **   Morgan Deters, Aina Niemetz, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/booleans/theory_bool.cpp b/src/theory/booleans/theory_bool.cpp
index c08012b619a7ad5e454125a2db980cd6b28c23d1..90de1d8dac53b04c3b8bc97cff6fb97d9a0ce35b 100644 (file)
--- a/src/theory/booleans/theory_bool.cpp
+++ b/src/theory/booleans/theory_bool.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_bool.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
+ **   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index 5fe4b159d6410a1bde7a02b027277a8db1c8103d..f02cc66ebe350b9122a40dd39da4704f2be9b81d 100644 (file)
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -2,7 +2,7 @@
 /*! \file theory_builtin_rewriter.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Andres Noetzli, Dejan Jovanovic
+ **   Andrew Reynolds, Andres Noetzli, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp
index 59c1ecd650d120d33e81a9714af7677e6e08a349..450d4a569a8f9174c64d0b9094ec410d85dd6cca 100644 (file)
--- a/src/theory/builtin/theory_builtin_type_rules.cpp
+++ b/src/theory/builtin/theory_builtin_type_rules.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_builtin_type_rules.cpp
  ** \verbatim
  ** Top contributors (to current version):
- ** Andrew Reynolds
+ **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp
index e03feedfc9e36e821030a45eac57fa0191b6f0f3..153d85df59e44fe81bffcc9d88e3f44aafd206af 100644 (file)
--- a/src/theory/bv/bv_solver_simple.cpp
+++ b/src/theory/bv/bv_solver_simple.cpp
@@ -5,7 +5,7 @@
  **   Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h
index 59239a52c2ac2fff830040abfe9ff040edbeea2b..d4010cb9528e310d50c744f9be3711df54b93f0e 100644 (file)
--- a/src/theory/bv/bv_solver_simple.h
+++ b/src/theory/bv/bv_solver_simple.h
@@ -2,10 +2,10 @@
 /*! \file bv_solver_simple.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Mathias Preiner
+ **   Mathias Preiner, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 50a509517808b9b12d7cffa398372c79e7a6d528..e1230a56cbb99cd20548d3aa82087ca88eec9615 100644 (file)
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -2,7 +2,7 @@
 /*! \file bv_subtheory_algebraic.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Aina Niemetz, Mathias Preiner
+ **   Liana Hadarean, Aina Niemetz, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index fa228131ccb710f210cefdd62e4491f942583585..093a35a1b69c4681b0a0e24a040e596636e3197d 100644 (file)
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -2,7 +2,7 @@
 /*! \file theory_bv.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner, Tim King
+ **   Mathias Preiner, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp
index 747ed89b7cba52353e11cd128fbe3aa345a4f482..4dbf26062120d30f0e3fef8dc8ab05be888aa444 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.cpp
+++ b/src/theory/datatypes/datatypes_rewriter.cpp
@@ -2,7 +2,7 @@
 /*! \file datatypes_rewriter.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Mathias Preiner
+ **   Andrew Reynolds, Mathias Preiner, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/datatypes/infer_proof_cons.cpp b/src/theory/datatypes/infer_proof_cons.cpp
index 443218bf402e9301c0daa777b0d1c5cd484eded4..f483291ca857e18b8afa187d0496901074900f12 100644 (file)
--- a/src/theory/datatypes/infer_proof_cons.cpp
+++ b/src/theory/datatypes/infer_proof_cons.cpp
@@ -4,8 +4,8 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/datatypes/infer_proof_cons.h b/src/theory/datatypes/infer_proof_cons.h
index 34e042237f3416dec1d32062184784ff678cd358..af6efc0a874e443b0eaa89f2245282fb08f75270 100644 (file)
--- a/src/theory/datatypes/infer_proof_cons.h
+++ b/src/theory/datatypes/infer_proof_cons.h
@@ -4,8 +4,8 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/datatypes/inference.cpp b/src/theory/datatypes/inference.cpp
index 806dfd418f09c12fb1a254110748462838b81546..308222146bd1cdd27773f14e29f731408c2ca20a 100644 (file)
--- a/src/theory/datatypes/inference.cpp
+++ b/src/theory/datatypes/inference.cpp
@@ -2,7 +2,7 @@
 /*! \file inference.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Gereon Kremer
+ **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/datatypes/inference_manager.cpp b/src/theory/datatypes/inference_manager.cpp
index f391cacd9620c14c0c72dcbcecffc9d8ff979c83..e9496ab0ab4fcc4a82b13e341f0b13148b84fe6c 100644 (file)
--- a/src/theory/datatypes/inference_manager.cpp
+++ b/src/theory/datatypes/inference_manager.cpp
@@ -2,7 +2,7 @@
 /*! \file inference_manager.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Gereon Kremer
+ **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/datatypes/proof_checker.cpp b/src/theory/datatypes/proof_checker.cpp
index 98060480b6716e28b7bdaa02fbd132e6f8dcef66..6bfa2015169b0fb5c9434414123a75e96df51525 100644 (file)
--- a/src/theory/datatypes/proof_checker.cpp
+++ b/src/theory/datatypes/proof_checker.cpp
@@ -5,7 +5,7 @@
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/datatypes/proof_checker.h b/src/theory/datatypes/proof_checker.h
index e5bd7cad5b1e1a992ec15dd169f16dc8d27b9143..1e47dd751f1863355caaffebc7cca3a2b1618d2d 100644 (file)
--- a/src/theory/datatypes/proof_checker.h
+++ b/src/theory/datatypes/proof_checker.h
@@ -5,7 +5,7 @@
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 45ce76504a0a178bf879376fb4dd1c7021c528f5..5bff5d305659a36f70703f3696be5bab454d79d0 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -2,7 +2,7 @@
 /*! \file theory_datatypes.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner, Tim King
+ **   Andrew Reynolds, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/fp/fp_converter.h b/src/theory/fp/fp_converter.h
index 6688e86071fd98e472e893d53c0aee002b972433..8b5f7905fe7c6cb3f0ab27f65b78dce680b12173 100644 (file)
--- a/src/theory/fp/fp_converter.h
+++ b/src/theory/fp/fp_converter.h
@@ -2,7 +2,7 @@
 /*! \file fp_converter.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Martin Brain, Mathias Preiner
+ **   Martin Brain, Mathias Preiner, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index fe91a39bdc1f759b1cfcd52bf16292b0fc32f2ac..341955cffeecf3eaf1eea1f9ab5ab917baa036be 100644 (file)
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -2,7 +2,7 @@
 /*! \file theory_fp.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Martin Brain, Andrew Reynolds, Mathias Preiner
+ **   Andrew Reynolds, Martin Brain, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/fp/theory_fp_rewriter.cpp b/src/theory/fp/theory_fp_rewriter.cpp
index 78aba415bb6f62fcec984c0c87225f40d1984c82..763ca662cb6522d0525abd828bd619e713048505 100644 (file)
--- a/src/theory/fp/theory_fp_rewriter.cpp
+++ b/src/theory/fp/theory_fp_rewriter.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_fp_rewriter.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Martin Brain, Andres Noetzli, Andrew Reynolds
+ **   Martin Brain, Andres Noetzli, Aina Niemetz
  ** Copyright (c) 2013  University of Oxford
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS

diff --git a/src/theory/fp/theory_fp_type_rules.h b/src/theory/fp/theory_fp_type_rules.h
index d632e80c81ddf015108cdfd7b119ce4d9d9b2075..f09f1b449a60936f5c3f9594f8a7bb1636f31cbc 100644 (file)
--- a/src/theory/fp/theory_fp_type_rules.h
+++ b/src/theory/fp/theory_fp_type_rules.h
@@ -2,7 +2,7 @@
 /*! \file theory_fp_type_rules.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Martin Brain, Tim King, Andres Noetzli
+ **   Martin Brain, Tim King, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/fp/type_enumerator.h b/src/theory/fp/type_enumerator.h
index 47266eda89896a89c082a6336607cae336ca21d2..79322a314d5f09fb798883d90098b5790220b9df 100644 (file)
--- a/src/theory/fp/type_enumerator.h
+++ b/src/theory/fp/type_enumerator.h
@@ -2,7 +2,7 @@
 /*! \file type_enumerator.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Martin Brain, Andrew Reynolds
+ **   Tim King, Martin Brain, Aina Niemetz
  ** Copyright (c) 2009-2015  New York University and The University of Iowa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS

diff --git a/src/theory/quantifiers/alpha_equivalence.cpp b/src/theory/quantifiers/alpha_equivalence.cpp
index 20fcaad490a7baa226bfa3f5b7889d53cef0d5bc..b4f9ee01556e5bd68bb184d1895058956d421870 100644 (file)
--- a/src/theory/quantifiers/alpha_equivalence.cpp
+++ b/src/theory/quantifiers/alpha_equivalence.cpp
@@ -2,7 +2,7 @@
 /*! \file alpha_equivalence.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner, Morgan Deters
+ **   Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 1d917b8f4095b82dfb99be929f012e7415a43da5..4884b4e3ba1bdd5eecccf2f1371c03ebe1507140 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -2,7 +2,7 @@
 /*! \file inst_strategy_cegqi.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Mathias Preiner
+ **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/quantifiers/quantifiers_modules.cpp b/src/theory/quantifiers/quantifiers_modules.cpp
index 1efd6d38f8c9ada797e811bccef4bc7280b457c8..9dbca674e2a4fbe3b016151e2aa54eeaf0a4edd2 100644 (file)
--- a/src/theory/quantifiers/quantifiers_modules.cpp
+++ b/src/theory/quantifiers/quantifiers_modules.cpp
@@ -2,10 +2,10 @@
 /*! \file quantifiers_modules.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/quantifiers/quantifiers_modules.h b/src/theory/quantifiers/quantifiers_modules.h
index 87d8af37b620b11e655efc8f32410328bb097758..a4c5dfb6e3305c109ad510d05d98083894e436d8 100644 (file)
--- a/src/theory/quantifiers/quantifiers_modules.h
+++ b/src/theory/quantifiers/quantifiers_modules.h
@@ -2,10 +2,10 @@
 /*! \file quantifiers_modules.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index 4469fe8513f86618da85ab3d6fa144297388baec..cb81a5c3a51786ab2e4ca6d240f7d12ab13ba176 100644 (file)
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -2,7 +2,7 @@
 /*! \file skolemize.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner
+ **   Andrew Reynolds, Mathias Preiner, Abdalrhman Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp
index d5ab0e51f0f7e3bae622d7c3f2f31063a217876b..9fdb3370047d792f072a537ad400bd07fa86f6cb 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_interpol.cpp
+++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp
@@ -2,7 +2,7 @@
 /*! \file sygus_interpol.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Ying Sheng, Andrew Reynolds
+ **   Ying Sheng, Abdalrhman Mohamed, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/quantifiers/sygus/sygus_interpol.h b/src/theory/quantifiers/sygus/sygus_interpol.h
index 4db5f261af9e7eeca96f86b0ef843441863f4738..a8b887172c6f0a6d815b2bd672c3d172469d3b32 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_interpol.h
+++ b/src/theory/quantifiers/sygus/sygus_interpol.h
@@ -2,7 +2,7 @@
 /*! \file sygus_interpol.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Ying Sheng
+ **   Ying Sheng, Abdalrhman Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
index 1a92cfc7fb8cd2d54e3f649199f8c7fce36bc49c..b039db48217047f37ef1c65c0cddf1b66d6eae53 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
+++ b/src/theory/quantifiers/sygus/sygus_qe_preproc.cpp
@@ -2,7 +2,7 @@
 /*! \file sygus_qe_preproc.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Mathias Preiner, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/quantifiers/sygus/synth_engine.cpp b/src/theory/quantifiers/sygus/synth_engine.cpp
index 3e40d66549405a4e692a554c2db1a2111f6ea6ce..f49cc962f23faa1e8d16b52964840c99979d7571 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_engine.cpp
+++ b/src/theory/quantifiers/sygus/synth_engine.cpp
@@ -2,7 +2,7 @@
 /*! \file synth_engine.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner, Haniel Barbosa
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp
index 2f6964f3ac3287bda31d6fe3dae5e8888c1b8b1f..0ac984aa36bb3ee7ffb04f95aba4ede99f0dfd85 100644 (file)
--- a/src/theory/quantifiers/sygus/template_infer.cpp
+++ b/src/theory/quantifiers/sygus/template_infer.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
-/*! \file template_infer.cpp 
+/*! \file template_infer.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner, Tim King
+ **   Andrew Reynolds, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/quantifiers/sygus_inst.cpp b/src/theory/quantifiers/sygus_inst.cpp
index 119cd925c7e5bf385e34d24eb182dc15683341de..50c983ee7b8aa9856c5e46cd6b0f183fb72d0f74 100644 (file)
--- a/src/theory/quantifiers/sygus_inst.cpp
+++ b/src/theory/quantifiers/sygus_inst.cpp
@@ -2,7 +2,7 @@
 /*! \file sygus_inst.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Mathias Preiner, Andrew Reynolds
+ **   Mathias Preiner, Aina Niemetz, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index 4a7f4367e3102aff4b356ed51d8b713305b3e2ec..d03cc857039f3f99714237074dcb70a47aad7332 100644 (file)
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_sep.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Dejan Jovanovic
+ **   Andrew Reynolds, Tim King, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/sep/theory_sep_rewriter.cpp b/src/theory/sep/theory_sep_rewriter.cpp
index 78837508ef24cd0ca0dba41356192202aa748b5d..2373bb6afd87151076d07e0eee81172eab921b16 100644 (file)
--- a/src/theory/sep/theory_sep_rewriter.cpp
+++ b/src/theory/sep/theory_sep_rewriter.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_sep_rewriter.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Andres Noetzli
+ **   Andrew Reynolds, Mudathir Mohamed, Andres Noetzli
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/sets/normal_form.h b/src/theory/sets/normal_form.h
index 2654344f3cf7ae93c35a8da38d14e4606e5191cc..08f0c2d1c0e1c6abaae5eab68ec7877993319ea7 100644 (file)
--- a/src/theory/sets/normal_form.h
+++ b/src/theory/sets/normal_form.h
@@ -2,7 +2,7 @@
 /*! \file normal_form.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Kshitij Bansal, Andrew Reynolds, Tim King
+ **   Andrew Reynolds, Kshitij Bansal, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/sets/solver_state.cpp b/src/theory/sets/solver_state.cpp
index 1d58945a58d44ef61f52e89e4cc205ac28b94b03..18b384f6a339bdad962ea6555bf74915b101e0a8 100644 (file)
--- a/src/theory/sets/solver_state.cpp
+++ b/src/theory/sets/solver_state.cpp
@@ -2,7 +2,7 @@
 /*! \file solver_state.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Mudathir Mohamed
+ **   Andrew Reynolds, Mudathir Mohamed, Paul Meng
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp
index 763024d5fcb2834d6310aad60f2c7133906e02b8..0e6ab1b18997bd55672cea4f0fc69c611bd1fd9f 100644 (file)
--- a/src/theory/sets/theory_sets.cpp
+++ b/src/theory/sets/theory_sets.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_sets.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Mudathir Mohamed, Kshitij Bansal
+ **   Andrew Reynolds, Kshitij Bansal, Andres Noetzli
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h
index e7d031b6fb940a2d23ee82bc29b490dcf1c42907..35139331c54d211dc5e6afb82ed7d676ea13b89f 100644 (file)
--- a/src/theory/sets/theory_sets_rewriter.h
+++ b/src/theory/sets/theory_sets_rewriter.h
@@ -2,7 +2,7 @@
 /*! \file theory_sets_rewriter.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Kshitij Bansal, Andres Noetzli, Mathias Preiner
+ **   Kshitij Bansal, Andrew Reynolds, Andres Noetzli
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h
index c5e86f10cc95359d9b6c8340e9237ed6a90e0747..3844248f2d1e7401837ece3b3d7782576e13bba4 100644 (file)
--- a/src/theory/sets/theory_sets_type_rules.h
+++ b/src/theory/sets/theory_sets_type_rules.h
@@ -2,7 +2,7 @@
 /*! \file theory_sets_type_rules.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Kshitij Bansal, Paul Meng
+ **   Andrew Reynolds, Kshitij Bansal, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/shared_solver.cpp b/src/theory/shared_solver.cpp
index 24d7d29cfe66e81d1f1138ecdcf9cd322c19b2b1..01dd37f19cedbc994c4eab8367a2afcf0e6af768 100644 (file)
--- a/src/theory/shared_solver.cpp
+++ b/src/theory/shared_solver.cpp
@@ -5,7 +5,7 @@
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/shared_solver.h b/src/theory/shared_solver.h
index c3d95f3c44daa0481aa3913acc3428069082dedb..46009e23cfc132cf45b0b053052328da8b5859d3 100644 (file)
--- a/src/theory/shared_solver.h
+++ b/src/theory/shared_solver.h
@@ -5,7 +5,7 @@
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/shared_solver_distributed.cpp b/src/theory/shared_solver_distributed.cpp
index c868ed2061cf766e71a8312ec33a3f45482263cd..fd0071b64c6f28367e6bfa36215d8933a7fd62d3 100644 (file)
--- a/src/theory/shared_solver_distributed.cpp
+++ b/src/theory/shared_solver_distributed.cpp
@@ -5,7 +5,7 @@
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/shared_solver_distributed.h b/src/theory/shared_solver_distributed.h
index de6e29743b67624f489d7ec58be23023b4e8f269..a4af0834cbe7250e7c091363e0717ee516a8b65f 100644 (file)
--- a/src/theory/shared_solver_distributed.h
+++ b/src/theory/shared_solver_distributed.h
@@ -5,7 +5,7 @@
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/shared_terms_database.cpp b/src/theory/shared_terms_database.cpp
index edf512e4b71f73eacde47bb15e0c019846865850..29bdc03f84d865cc3769855bcbec7dcc27169fb7 100644 (file)
--- a/src/theory/shared_terms_database.cpp
+++ b/src/theory/shared_terms_database.cpp
@@ -2,7 +2,7 @@
 /*! \file shared_terms_database.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Andrew Reynolds, Morgan Deters
+ **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/strings/infer_proof_cons.cpp b/src/theory/strings/infer_proof_cons.cpp
index 66f71bf14f26ecea8ecae2cd47c47ba5e8fa7826..902b906151fa358c110ccff6b3f2339a179658f9 100644 (file)
--- a/src/theory/strings/infer_proof_cons.cpp
+++ b/src/theory/strings/infer_proof_cons.cpp
@@ -4,8 +4,8 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h
index 63e341dfe671d77203c6c5a1d8026818a770e4ea..1b066b4b3a7c89a9e3c654ce5ceb8a318d9ef905 100644 (file)
--- a/src/theory/strings/infer_proof_cons.h
+++ b/src/theory/strings/infer_proof_cons.h
@@ -4,8 +4,8 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/strings/regexp_elim.cpp b/src/theory/strings/regexp_elim.cpp
index aaa9ffc484414c6edcb53083f9a05494f5a25e61..770991286d30298e20c609829869d69d97da57a8 100644 (file)
--- a/src/theory/strings/regexp_elim.cpp
+++ b/src/theory/strings/regexp_elim.cpp
@@ -2,7 +2,7 @@
 /*! \file regexp_elim.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tianyi Liang, Mathias Preiner
+ **   Andrew Reynolds, Mathias Preiner, Andres Noetzli
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index d3e9e34f19bc2723c4bce9c0e1d3368cb67dd3c2..110ff9b2d880c5da73b942fdd8153460defba6ec 100644 (file)
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_strings.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tianyi Liang, Yoni Zohar
+ **   Andrew Reynolds, Tianyi Liang, Andres Noetzli
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/strings/theory_strings_utils.cpp b/src/theory/strings/theory_strings_utils.cpp
index 286c0dc041fd8ac3e46ab31adb7cf4fe88c771ac..b807fe1b3193cdee0fc8a1fb1a1bc85ef829208b 100644 (file)
--- a/src/theory/strings/theory_strings_utils.cpp
+++ b/src/theory/strings/theory_strings_utils.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_strings_utils.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Andres Noetzli
+ **   Andrew Reynolds, Andres Noetzli, Yoni Zohar
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 78fe6927f9a4a955abd08105d4a0216f3fc74d0a..08ad8ac873e8b34b585212537f471157add516b3 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -2,7 +2,7 @@
 /*! \file theory.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Dejan Jovanovic
+ **   Andrew Reynolds, Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/theory_eq_notify.h b/src/theory/theory_eq_notify.h
index 3df5d32cb311084dfd727296384e5056ea23d511..e5137d9e4297995f30f738461436564084364e2d 100644 (file)
--- a/src/theory/theory_eq_notify.h
+++ b/src/theory/theory_eq_notify.h
@@ -2,10 +2,10 @@
 /*! \file theory_eq_notify.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Mathias Preiner, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/src/theory/theory_id.cpp b/src/theory/theory_id.cpp
index 31b864e7f4b0a44332654bbc646e5285fdddcb90..e9111db8c164d021879d943579285dc6fdc10907 100644 (file)
--- a/src/theory/theory_id.cpp
+++ b/src/theory/theory_id.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_id.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Aina Niemetz, Tim King
+ **   Andrew Reynolds, Aina Niemetz, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/theory_inference_manager.h b/src/theory/theory_inference_manager.h
index 35d9031aea7a8165b8536f8fc0e5daca301d59a3..124b88e3ef12b9006944125d66bc5f4f4768d9a5 100644 (file)
--- a/src/theory/theory_inference_manager.h
+++ b/src/theory/theory_inference_manager.h
@@ -2,7 +2,7 @@
 /*! \file theory_inference_manager.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Mathias Preiner, Martin Brain
+ **   Andrew Reynolds, Mathias Preiner, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/theory_model.h b/src/theory/theory_model.h
index e8665bb838fba0aa85fac0f2beec061266a0c964..19e992dc67474b85ed2df793b250b710a2a8f2f5 100644 (file)
--- a/src/theory/theory_model.h
+++ b/src/theory/theory_model.h
@@ -2,7 +2,7 @@
 /*! \file theory_model.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Clark Barrett
+ **   Andrew Reynolds, Clark Barrett, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/theory_preprocessor.cpp b/src/theory/theory_preprocessor.cpp
index f5e5fa505ab0750e2201b97361710229661863e7..7d265fc6725a84359f181f0e32fd22477208137e 100644 (file)
--- a/src/theory/theory_preprocessor.cpp
+++ b/src/theory/theory_preprocessor.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_preprocessor.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
+ **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/theory_proof_step_buffer.cpp b/src/theory/theory_proof_step_buffer.cpp
index a08b159011fcd76c496852cf511ea2a5742a839f..f9ee77308189573d6f7d0879e295fc92b826c7bd 100644 (file)
--- a/src/theory/theory_proof_step_buffer.cpp
+++ b/src/theory/theory_proof_step_buffer.cpp
@@ -2,7 +2,7 @@
 /*! \file theory_proof_step_buffer.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Haniel Barbosa, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/theory_proof_step_buffer.h b/src/theory/theory_proof_step_buffer.h
index d67781428b0067ecbf774988c59ebdd93a4b7f0b..9dbd6dc3942524ccbfb925e448ddb46618c48356 100644 (file)
--- a/src/theory/theory_proof_step_buffer.h
+++ b/src/theory/theory_proof_step_buffer.h
@@ -2,7 +2,7 @@
 /*! \file theory_proof_step_buffer.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index 5d2711f1def786fb530d3b7cb72c6458f2c9b0f4..003e439ae85f2677712a4ef4d3079bd10aa9c396 100644 (file)
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -2,7 +2,7 @@
 /*! \file theory_test_utils.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Mathias Preiner
+ **   Tim King, Morgan Deters, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/trust_substitutions.cpp b/src/theory/trust_substitutions.cpp
index aaa3b44f7e61785852d495086f475909cd2ed645..b289d83cce9f62a5b74b76c3a86003ab961dc295 100644 (file)
--- a/src/theory/trust_substitutions.cpp
+++ b/src/theory/trust_substitutions.cpp
@@ -2,7 +2,7 @@
 /*! \file trust_substitutions.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/trust_substitutions.h b/src/theory/trust_substitutions.h
index c316f08c544d265773ad9aac1bbfb825f18f8207..08e2da895c29e170699fdd6f0152c45db9809e19 100644 (file)
--- a/src/theory/trust_substitutions.h
+++ b/src/theory/trust_substitutions.h
@@ -2,7 +2,7 @@
 /*! \file trust_substitutions.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/uf/proof_equality_engine.h b/src/theory/uf/proof_equality_engine.h
index 4148da1deb4aa199a340a13c8571c921077c0749..8e6ef9a5603d1f3433bf16eab1a928e14d5373d6 100644 (file)
--- a/src/theory/uf/proof_equality_engine.h
+++ b/src/theory/uf/proof_equality_engine.h
@@ -2,7 +2,7 @@
 /*! \file proof_equality_engine.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Haniel Barbosa
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 3f76919eb5514b20ff2715992f700125553b6681..497e394c77154db6afa3e767c5e04d33fe44585c 100644 (file)
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -2,7 +2,7 @@
 /*! \file theory_uf.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
+ **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 24e485f5ef17d23c0e1985d455c292cd4e7105c0..bc4536b7206ea82b2b9a93e130875363e0c4a61e 100644 (file)
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -1,7 +1,7 @@
 #####################
 ## CMakeLists.txt
 ## Top contributors (to current version):
-##   Mathias Preiner, Gereon Kremer, Andrew Reynolds
+##   Mathias Preiner, Gereon Kremer, Aina Niemetz
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index 5b291f3c5e5c6c5f1fca37df457df330afda8fc8..44f31e9169d27fabd78ae567af57c1a84fdb68bb 100644 (file)
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -2,7 +2,7 @@
 /*! \file floatingpoint.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Martin Brain, Aina Niemetz, Haniel Barbosa
+ **   Aina Niemetz, Martin Brain, Haniel Barbosa
  ** Copyright (c) 2013  University of Oxford
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS

diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp
index 77ab910fa1968158f2db52301aea1b877db2f229..d1e58495aaa10308aad19516f29a564d7e6712df 100644 (file)
--- a/src/util/floatingpoint_literal_symfpu.cpp
+++ b/src/util/floatingpoint_literal_symfpu.cpp
@@ -2,7 +2,7 @@
 /*! \file floatingpoint_literal_symfpu.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Martin Brain, Aina Niemetz
+ **   Martin Brain, Aina Niemetz, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
index 995579c3bbfb59361ca6a3ee5984869456df6069..80b178eab2062bb9e5a9e09184ca853d96640985 100644 (file)
--- a/src/util/gmp_util.h
+++ b/src/util/gmp_util.h
@@ -2,7 +2,7 @@
 /*! \file gmp_util.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andres Noetzli, Mathias Preiner
+ **   Tim King, Mathias Preiner, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index 88db707d975c15f3c3a679e95ba6bcc59f3fe757..27863b9f85c2f27cb15c1dfa27b6290e940d80cb 100644 (file)
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -2,7 +2,7 @@
 /*! \file integer_cln_imp.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Aina Niemetz, Morgan Deters
+ **   Aina Niemetz, Tim King, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 29a5248e3f55b1c5139ae20d4a80add4c3029ba8..050f05fc3d8c24b1197ed8e0e88ba95d19227064 100644 (file)
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -2,7 +2,7 @@
 /*! \file integer_cln_imp.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Gereon Kremer, Morgan Deters
+ **   Aina Niemetz, Tim King, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index 5a4fc9349899c8e146a7fdf2618eb950aee91e8b..fec71b26b6a25aee8aaacdcad4fc40e61d6ea7e0 100644 (file)
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -2,7 +2,7 @@
 /*! \file integer_gmp_imp.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Aina Niemetz, Liana Hadarean
+ **   Aina Niemetz, Tim King, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index a11a15f81fcb5d6018af0a425eed740baf833456..fe05dc982788c6d3419caf42d6a90da6b50e6fd9 100644 (file)
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -2,7 +2,7 @@
 /*! \file integer_gmp_imp.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Gereon Kremer, Liana Hadarean
+ **   Aina Niemetz, Tim King, Gereon Kremer
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 9afa79ef0bfaacdd8a692ae181e1b509401c3616..17dac50b3ca9dc11db699b0ca365d1e00d728022 100644 (file)
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -2,7 +2,7 @@
 /*! \file resource_manager.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Mathias Preiner, Gereon Kremer, Liana Hadarean
+ **   Gereon Kremer, Mathias Preiner, Liana Hadarean
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt
index 59df71010c36032a8f4293cc6c2fbced9a177d85..33d5f9c37ace2714cdc996852604adefd3e5c396 100644 (file)
--- a/test/api/CMakeLists.txt
+++ b/test/api/CMakeLists.txt
@@ -1,7 +1,7 @@
 #####################
 ## CMakeLists.txt
 ## Top contributors (to current version):
-##   Aina Niemetz, Andrew V. Jones, Andres Noetzli
+##   Aina Niemetz, Andrew V. Jones, Makai Mann
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/test/api/ouroborous.cpp b/test/api/ouroborous.cpp
index efca53ab338bd24b409955dc59c7830844fabc51..1a23acd297767574eb634def0197f294ad231bf3 100644 (file)
--- a/test/api/ouroborous.cpp
+++ b/test/api/ouroborous.cpp
@@ -2,7 +2,7 @@
 /*! \file ouroborous.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Aina Niemetz, Tim King
+ **   Morgan Deters, Andrew Reynolds, Tim King
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/api/python/test_grammar.py b/test/api/python/test_grammar.py
index 5a0d5101f2c6e578d1f40e3ea7a5f2eb8d26382a..54c30b767bb6df6462c648f96414129eaf914b40 100644 (file)
--- a/test/api/python/test_grammar.py
+++ b/test/api/python/test_grammar.py
@@ -1,7 +1,7 @@
 #####################
 ## test_grammar.py
 ## Top contributors (to current version):
-##   Yoni Zohar, Makai Mann
+##   Yoni Zohar, Makai Mann, Mudathir Mohamed
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/test/api/python/test_sort.py b/test/api/python/test_sort.py
index cff92ca8d027411022b08a234cec028d7d12eac0..20ddc6bc1214155f9e92cde5261fad44ea890684 100644 (file)
--- a/test/api/python/test_sort.py
+++ b/test/api/python/test_sort.py
@@ -1,7 +1,7 @@
 #####################
 ## test_sort.py
 ## Top contributors (to current version):
-##   Makai Mann, Andres Noetzli
+##   Makai Mann, Andres Noetzli, Mudathir Mohamed
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/test/api/python/test_to_python_obj.py b/test/api/python/test_to_python_obj.py
index eb15e74696a0e6740085a384110d2bace754b95c..eeafc48544c076a88cd8f8ddfd8f1a7d6a94bdc6 100644 (file)
--- a/test/api/python/test_to_python_obj.py
+++ b/test/api/python/test_to_python_obj.py
@@ -1,3 +1,13 @@
+#####################
+## test_to_python_obj.py
+## Top contributors (to current version):
+##   Makai Mann, Andres Noetzli, Mudathir Mohamed
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
 from fractions import Fraction
 import pytest
 

diff --git a/test/api/reset_assertions.cpp b/test/api/reset_assertions.cpp
index 2168d053e8e7f1f89731fce139c5a032bd4638e9..0662c7519c107fd3b483a7f2a12e9b4f500bec0f 100644 (file)
--- a/test/api/reset_assertions.cpp
+++ b/test/api/reset_assertions.cpp
@@ -2,7 +2,7 @@
 /*! \file reset_assertions.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli
+ **   Andres Noetzli, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/api/sep_log_api.cpp b/test/api/sep_log_api.cpp
index cc20f1ed1b7d2260431fb64773e52e3d7d621ee0..afe264d1f740878886435af79ffb34118d10e460 100644 (file)
--- a/test/api/sep_log_api.cpp
+++ b/test/api/sep_log_api.cpp
@@ -2,7 +2,7 @@
 /*! \file sep_log_api.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew V. Jones, Andres Noetzli
+ **   Andrew V. Jones, Andres Noetzli, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
old mode 100755 (executable)
new mode 100644 (file)

diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt
index c6c68236581088629ff701b18dfaacd218cea670..056f9d891b305cfe797c1ca8190331723f074db7 100644 (file)
--- a/test/unit/api/CMakeLists.txt
+++ b/test/unit/api/CMakeLists.txt
@@ -1,7 +1,7 @@
 #####################
 ## CMakeLists.txt
 ## Top contributors (to current version):
-##   Aina Niemetz, Andres Noetzli, Makai Mann
+##   Aina Niemetz, Andres Noetzli
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/api/grammar_black.cpp b/test/unit/api/grammar_black.cpp
index 2cfe67825f9d3651f7ce22d5b3aa717db90b0112..7e599b135e505ac6a58b0aa2c304a64a120fffb0 100644 (file)
--- a/test/unit/api/grammar_black.cpp
+++ b/test/unit/api/grammar_black.cpp
@@ -2,7 +2,7 @@
 /*! \file grammar_black.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Abdalrhman Mohamed, Aina Niemetz, Andrew Reynolds
+ **   Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/api/result_black.cpp b/test/unit/api/result_black.cpp
index 2608454955e05b6daad42c0af0b4ea8af95f09d4..05427c01d2c22e3ef61c6e77b2330d3f7b7d435d 100644 (file)
--- a/test/unit/api/result_black.cpp
+++ b/test/unit/api/result_black.cpp
@@ -2,7 +2,7 @@
 /*! \file result_black.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds
+ **   Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/api/sort_black.h b/test/unit/api/sort_black.h
index e6d71219193697ac748ecf28daa1b1ec59f4b3ba..baec0f3e9f953f57bcb626330142d30c31ec164a 100644 (file)
--- a/test/unit/api/sort_black.h
+++ b/test/unit/api/sort_black.h
@@ -2,7 +2,7 @@
 /*! \file sort_black.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds
+ **   Aina Niemetz, Andrew Reynolds, Mudathir Mohamed
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/api/term_black.cpp b/test/unit/api/term_black.cpp
index 71e1c7f6f2f8a49158a64ce59e19269220cb83b4..8627f6033c9a39d185fcceb796789ed33b4c53c8 100644 (file)
--- a/test/unit/api/term_black.cpp
+++ b/test/unit/api/term_black.cpp
@@ -2,7 +2,7 @@
 /*! \file term_black.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Andrew Reynolds, Makai Mann
+ **   Aina Niemetz, Makai Mann, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index 6c0abc4ab2754204a990a346cd6334f9200742bf..2c698f953eee45f509383d6c5076e9b60b411737 100644 (file)
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -1,7 +1,7 @@
 #####################
 ## CMakeLists.txt
 ## Top contributors (to current version):
-##   Aina Niemetz, Yoni Zohar, Alex Ozdemir
+##   Aina Niemetz
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/expr/symbol_table_black.h b/test/unit/expr/symbol_table_black.h
index 5233c7e098b14bcb7a93704582fe8c4504733b72..4aa1e4f65985c01dd7da8a9ed6a2d12b94056123 100644 (file)
--- a/test/unit/expr/symbol_table_black.h
+++ b/test/unit/expr/symbol_table_black.h
@@ -2,7 +2,7 @@
 /*! \file symbol_table_black.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway, Andres Noetzli
+ **   Morgan Deters, Christopher L. Conway, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/expr/type_node_white.h b/test/unit/expr/type_node_white.h
index 8ac17bbbdc0d3e7d6ef995b5f294d7c3c21adaef..042a7b1dab52f4e1af9578013101fe47a7f5ffff 100644 (file)
--- a/test/unit/expr/type_node_white.h
+++ b/test/unit/expr/type_node_white.h
@@ -2,7 +2,7 @@
 /*! \file type_node_white.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Andres Noetzli
+ **   Morgan Deters, Andrew Reynolds, Andres Noetzli
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/main/interactive_shell_black.h b/test/unit/main/interactive_shell_black.h
index df6a79bd889a1a060ff5ea6b2aca2a5e6b649317..d8cbc19cd9b56d225712383dbe29d952bd0dfab7 100644 (file)
--- a/test/unit/main/interactive_shell_black.h
+++ b/test/unit/main/interactive_shell_black.h
@@ -2,7 +2,7 @@
 /*! \file interactive_shell_black.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Aina Niemetz, Andres Noetzli
+ **   Christopher L. Conway, Aina Niemetz, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index ef8f2e3cf8e2c4edaf0e64bdbff4f0e34e50f9c7..d63f6b0293b0459041cdc3bbbaccd9ee2a601bf7 100644 (file)
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -2,7 +2,7 @@
 /*! \file parser_black.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Morgan Deters, Aina Niemetz
+ **   Christopher L. Conway, Morgan Deters, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index c101542d0d70da0aadc11a450279b64394384746..686fc74004a7b7a8d1ab36b4f4368d55349bec38 100644 (file)
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -2,7 +2,7 @@
 /*! \file parser_builder_black.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Christopher L. Conway, Aina Niemetz, Tim King
+ **   Christopher L. Conway, Andrew Reynolds, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/preprocessing/CMakeLists.txt b/test/unit/preprocessing/CMakeLists.txt
index a2381ba90803e9dc33d2f0f3ffc1062cd113d2ea..f2dc0ce797f46990fd0f7c2034ef55b40c7812a8 100644 (file)
--- a/test/unit/preprocessing/CMakeLists.txt
+++ b/test/unit/preprocessing/CMakeLists.txt
@@ -1,7 +1,7 @@
 #####################
 ## CMakeLists.txt
 ## Top contributors (to current version):
-##   Aina Niemetz, Yoni Zohar
+##   Aina Niemetz
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt
index 93c241af9dd6af9278e959bb77de573ca629420a..973488a3e2330583eb3f34e336c089e7a073da41 100644 (file)
--- a/test/unit/printer/CMakeLists.txt
+++ b/test/unit/printer/CMakeLists.txt
@@ -1,7 +1,7 @@
 #####################
 ## CMakeLists.txt
 ## Top contributors (to current version):
-##   Andres Noetzli
+##   Andres Noetzli, Aina Niemetz
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 334ded2d1d160187fb63e7c6e598d03b0d00a1a8..e7528453e90c0b74c5bbc0215aeebb504b042cd1 100644 (file)
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -1,7 +1,7 @@
 #####################
 ## CMakeLists.txt
 ## Top contributors (to current version):
-##   Aina Niemetz, Andres Noetzli, Andrew Reynolds
+##   Aina Niemetz
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/theory/theory_bags_normal_form_white.h b/test/unit/theory/theory_bags_normal_form_white.h
index 72fc4284e4004dde2ca30d29699a3a60914a34f0..eb1676f79fd8e31be873ad55c78703118300246e 100644 (file)
--- a/test/unit/theory/theory_bags_normal_form_white.h
+++ b/test/unit/theory/theory_bags_normal_form_white.h
@@ -2,10 +2,10 @@
 /*! \file theory_bags_normal_form_white.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Mudathir Mohamed
+ **   Mudathir Mohamed, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/test/unit/theory/theory_bags_rewriter_white.h b/test/unit/theory/theory_bags_rewriter_white.h
index a58e2cdada71dc1b4a10f31fdbaf778cdb683ed7..98e3cf88727fd413fdeb947bdbf5d1a172cc2185 100644 (file)
--- a/test/unit/theory/theory_bags_rewriter_white.h
+++ b/test/unit/theory/theory_bags_rewriter_white.h
@@ -2,10 +2,10 @@
 /*! \file theory_bags_rewriter_white.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Mudathir Mohamed
+ **   Mudathir Mohamed, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/test/unit/theory/theory_bags_type_rules_white.h b/test/unit/theory/theory_bags_type_rules_white.h
index 8d1db858d6d9ff5827dd5c3d1e7c5c54c2b270fb..825e526691466bc584fb89a6d56d1fd383ec1d86 100644 (file)
--- a/test/unit/theory/theory_bags_type_rules_white.h
+++ b/test/unit/theory/theory_bags_type_rules_white.h
@@ -1,11 +1,11 @@
 /*********************                                                        */
-/*! \file theory_bags_type_rules_black.h
+/*! \file theory_bags_type_rules_white.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Mudathir Mohamed
+ **   Mudathir Mohamed, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/test/unit/theory/theory_sets_type_enumerator_white.h b/test/unit/theory/theory_sets_type_enumerator_white.h
index 1b5ba1dcb317d66f09c82456ac00d4c4634482d9..a100984ba637ad915e071b40bee52a51a6f07df3 100644 (file)
--- a/test/unit/theory/theory_sets_type_enumerator_white.h
+++ b/test/unit/theory/theory_sets_type_enumerator_white.h
@@ -2,7 +2,7 @@
 /*! \file theory_sets_type_enumerator_white.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Mudathir Mohamed, Andres Noetzli, Andrew Reynolds
+ **   Mudathir Mohamed, Andrew Reynolds, Andres Noetzli
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/theory/theory_sets_type_rules_white.h b/test/unit/theory/theory_sets_type_rules_white.h
index 00b012745f1e0abb284e02be4c8927fc422da111..59f8186acc4b0305ab6df5d6de0960caaab9b1bb 100644 (file)
--- a/test/unit/theory/theory_sets_type_rules_white.h
+++ b/test/unit/theory/theory_sets_type_rules_white.h
@@ -2,10 +2,10 @@
 /*! \file theory_sets_type_rules_white.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Mudathir Mohamed
+ **   Mudathir Mohamed, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
- ** in the top-level source directory) and their institutional affiliations.
+ ** in the top-level source directory and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **

diff --git a/test/unit/theory/theory_strings_skolem_cache_black.h b/test/unit/theory/theory_strings_skolem_cache_black.h
index dd70dd5b903f74fb3691928c6306a97c95948152..72a9b7e64691baeeb195d5e20bd316ec961ffa69 100644 (file)
--- a/test/unit/theory/theory_strings_skolem_cache_black.h
+++ b/test/unit/theory/theory_strings_skolem_cache_black.h
@@ -2,7 +2,7 @@
 /*! \file theory_strings_skolem_cache_black.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli
+ **   Andres Noetzli, Andrew Reynolds
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index f69830fd888acb2c0715eecb21484415cb312f9d..9f23dbad6a6720c91b3106b0b0a688e4470c85b2 100644 (file)
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -2,7 +2,7 @@
 /*! \file theory_white.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Clark Barrett
+ **   Tim King, Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index 148ae9910bd9edce434452ff2506db856c840891..3457578df6a7818e9f7f765ebd2e5d694a1d4972 100644 (file)
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -1,7 +1,7 @@
 #####################
 ## CMakeLists.txt
 ## Top contributors (to current version):
-##   Aina Niemetz, Gereon Kremer, Andres Noetzli
+##   Aina Niemetz, Yoni Zohar, Gereon Kremer
 ## This file is part of the CVC4 project.
 ## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
 ## in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h
index 5b6eecc5f6cf45d264db4f79421a5ba122475baa..417410c9ed9838551ea36f5afa63c3c213c938bc 100644 (file)
--- a/test/unit/util/bitvector_black.h
+++ b/test/unit/util/bitvector_black.h
@@ -2,7 +2,7 @@
 /*! \file bitvector_black.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli, Christopher L. Conway, Morgan Deters
+ **   Andres Noetzli, Christopher L. Conway, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.

diff --git a/test/unit/util/output_black.h b/test/unit/util/output_black.h
index 00580de63da96a0df314ce2c8a677535c4406f0f..298aad8124828c89db82df013f6a611fd7770ef1 100644 (file)
--- a/test/unit/util/output_black.h
+++ b/test/unit/util/output_black.h
@@ -2,7 +2,7 @@
 /*! \file output_black.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Andres Noetzli
+ **   Morgan Deters, Tim King, Aina Niemetz
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
  ** in the top-level source directory and their institutional affiliations.