re-generated comment headers of source files

diff --git a/src/expr/declaration_scope.cpp b/src/expr/declaration_scope.cpp
index 761dd6d24adff5543e2fe25738577fd5acf0544b..edc4c5fa89137e133aed5ea65857bfa83a7963c4 100644 (file)
--- a/src/expr/declaration_scope.cpp
+++ b/src/expr/declaration_scope.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): dejan, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index a6947c53620b9bd3919e173be099250e3369ee12..2318699e73e80aed08517b49ad18d199f87204a3 100644 (file)
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): dejan, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/expr/expr_manager_scope.h b/src/expr/expr_manager_scope.h
index cb983b006289664b58d36d2b078a33a039c554f7..b0b704de46cf65c03dd1264005f4aa475ffc7904 100644 (file)
--- a/src/expr/expr_manager_scope.h
+++ b/src/expr/expr_manager_scope.h
@@ -2,7 +2,7 @@
 /*! \file expr_manager_scope.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 80bf372204fad42c64a9285c16e6211b3a108689..ad698975f907c2b8c66d015871bc3b51b1744921 100644 (file)
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): dejan, cconway
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp
index 8add462e0c308e39ffb75ebb666fa9e650c889c9..a10b43c480122bf1eba863f3a81ce14ccbc69d3a 100644 (file)
--- a/src/expr/node_value.cpp
+++ b/src/expr/node_value.cpp
@@ -2,8 +2,8 @@
 /*! \file node_value.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 069f38ce0ffa37446afa168a0cfbda3d4f6f424d..225e5f9e0a7798e83158fefda807c87af406cfb5 100644 (file)
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -2,8 +2,8 @@
 /*! \file type.cpp
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: dejan
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters, dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/expr/type.h b/src/expr/type.h
index 2862286aecc77647ee09d8d1a32b289a69571a75..be8a57be3d07d48ffe4e56e7c5326174272b1c2e 100644 (file)
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -2,8 +2,8 @@
 /*! \file type.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: dejan
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters, dejan
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/expr/type_constant.h b/src/expr/type_constant.h
index 0f5b522b623af6821bb9b767aaa902ae5b18d78d..3d5ca229a7205542eed0ee0e4313a8c3024dde91 100644 (file)
--- a/src/expr/type_constant.h
+++ b/src/expr/type_constant.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 43d3c761e54546f33ea6bc88ce5874da1b640b1c..b32555b9dd726d27b59bc6518ee34318bb270ace 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -2,7 +2,7 @@
 /*! \file type_node.cpp
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index a58d9dc89cd41de98b3fd5c1c0dfb9c86cd2b182..1d5f89c601ade3b88e045f99599a3c857119a76a 100644 (file)
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -2,7 +2,7 @@
 /*! \file type_node.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 4dc62f8d35fff13117d4ab576ab9c850dad8879d..855bcbddeeb0d4de7966bbbf50faa83f246ec96d 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: mdeters
  ** Major contributors: cconway
- ** Minor contributors (to current version): barrett, dejan
+ ** Minor contributors (to current version): barrett, dejan, taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/main/usage.h b/src/main/usage.h
index b56f083a5bf050fd3b2c65023c6a8fa99d59db0c..9fdc6a67b9b983572ab2641731fda10c859da676 100644 (file)
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -2,8 +2,8 @@
 /*! \file usage.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: cconway
- ** Minor contributors (to current version): none
+ ** Major contributors: none
+ ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index e621c92de90cc6ce76469fe98a028d4b7b7dbb35..740d7fae592d8fe3a3e027d3265bfb41bf8745a6 100644 (file)
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index ca9b2b747b08806f86b45dbd43e6845ddb3cf671..0d5fda89ac4f99836a3db3d5afb599c137d06561 100644 (file)
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): mdeters, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/bounded_token_buffer.h b/src/parser/bounded_token_buffer.h
index 9634f016b3827410ca5eb80156a88f5db61ac432..fede14bd1725431e85a75707833fe0c7c4341cd1 100644 (file)
--- a/src/parser/bounded_token_buffer.h
+++ b/src/parser/bounded_token_buffer.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 3e10f632fc3a76e917538477de610b2991a566a5..1c02aa482279496ce3f5648dc90755caa7a7344e 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters, dejan
+ ** Minor contributors (to current version): dejan, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index 3b62cbc5712fc41020c44ac8b8fd5e72674afa2d..139795494a4ab426941f13a2e16900e81c258fe7 100644 (file)
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index ed1ab807bb0ab64b245634d2473756fb1300d814..b63f39d789ed1cec77063be780f8345c9cbd9389 100644 (file)
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index bbec3299f71e63c30dc059307806763b067205f9..bb592857aee9c3472e1b745c989c32f79ffeca6b 100644 (file)
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/smt/smt.h b/src/parser/smt/smt.h
index d08e25ba944e35d26755a4660b8b6126b45ea514..23881c8b94a4ec155eabbf1edaec3aeb6250930d 100644 (file)
--- a/src/parser/smt/smt.h
+++ b/src/parser/smt/smt.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 79d5ccb3aec179f2fca376e0e35b234560f23876..e25b8217ba8eea6c0a8a2037fd8335582babc450 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index b54fe82e9033a224dba8ed7b3b532c999e84517b..fe152a7f652cbf8dcaf702eb7bcdd3aed9db2cbf 100644 (file)
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index 829d6a5f8c5e88ac5c37654e56ccf8ade8bfcc05..5156ea2e53aeaf9e4f612b5a65ed3f96d6925fea 100644 (file)
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index 1fa8cff1cc2d1a732309fb819cee5257c4a76ad4..c9d0d5ec573789fed47ebbdcc7af761546b67b76 100644 (file)
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index ba87cf269fe6255577e93bbd4c8e4cad0ec3b42f..c88b1e265f835ef4e4c39a7396b1cbd02e9b4a35 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -2,8 +2,8 @@
 /*! \file cnf_stream.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: cconway, dejan
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): mdeters, cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 64efedd8acabed2c7a948bcbd25724568d2e8c7c..4cc7f19027ab6cff9cb6790a9717418af241eaa9 100644 (file)
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -2,7 +2,7 @@
 /*! \file sat.cpp
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
+ ** Major contributors: mdeters, taking
  ** Minor contributors (to current version): dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/prop/sat.h b/src/prop/sat.h
index 992d8ecd242781c62df6384b4172fa30857aab46..9e09727e398799488385d207b3b3bec3069c9454 100644 (file)
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -2,7 +2,7 @@
 /*! \file sat.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: dejan, cconway
+ ** Major contributors: taking, dejan, cconway
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/arith/arith_activity.h b/src/theory/arith/arith_activity.h
index 1dc0e900bfb1debc9d2916eb2b871f30010fe840..f347105e305a88d9600127b80d7be54c08dcad45 100644 (file)
--- a/src/theory/arith/arith_activity.h
+++ b/src/theory/arith/arith_activity.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file arith_activity.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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
+ **/
+
 
 #include "cvc4_private.h"
 

diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h
index c34e861910d4ff1052b91033c4d1dc93a783ec8f..4a8fec56ff3897f670afe491f0ed95cd99822955 100644 (file)
--- a/src/theory/arith/arith_constants.h
+++ b/src/theory/arith/arith_constants.h
@@ -2,7 +2,7 @@
 /*! \file arith_constants.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/arith/arith_propagator.cpp b/src/theory/arith/arith_propagator.cpp
index e4057505406bc8a3168aa89dc64715d24b8d5685..c5068c9fb513406442452902da8854c1c4b9bf7e 100644 (file)
--- a/src/theory/arith/arith_propagator.cpp
+++ b/src/theory/arith/arith_propagator.cpp
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file arith_propagator.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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
+ **/
+
 #include "theory/arith/arith_propagator.h"
 #include "theory/arith/arith_utilities.h"
 

diff --git a/src/theory/arith/arith_propagator.h b/src/theory/arith/arith_propagator.h
index a623517fb653ad8caf0372d50dc0f3cd1081da85..7ffcec747104a4f1f4fa3bd92adc0e54f9e5abd1 100644 (file)
--- a/src/theory/arith/arith_propagator.h
+++ b/src/theory/arith/arith_propagator.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file arith_propagator.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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
+ **/
+
 
 
 #include "cvc4_private.h"

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 5c2a1e996056c5452aa1f97e04b7da5d16583d52..9cd65b2d9121ee29c975c844a61ce8df0f53a6b0 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 704b57ca6c6bd5c81a101d17ee89e266df98959e..38c72d38da2a7917e389c70a04f8aa5e4ec0cb0b 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
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index dcfedb7e8669f1b7833fa285983f2bd079faad1a..fa3356c6075f1f346eeb37d35437c8435ef2888f 100644 (file)
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -2,7 +2,7 @@
 /*! \file arith_utilities.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/arith/basic.h b/src/theory/arith/basic.h
index 963f2b9693fcd0cabafef87e667167c88d6b1369..11f0f71f0840341f283a8029c5a0201808168866 100644 (file)
--- a/src/theory/arith/basic.h
+++ b/src/theory/arith/basic.h
@@ -2,7 +2,7 @@
 /*! \file basic.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp
index 55e6b3dc9e6e5d85b2d7009e889de856beb6514d..f6a460fee3b7192ba9369d20dbf9f8525ec55a6d 100644 (file)
--- a/src/theory/arith/delta_rational.cpp
+++ b/src/theory/arith/delta_rational.cpp
@@ -2,7 +2,7 @@
 /*! \file delta_rational.cpp
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index 78d5fb66580c6674ed8ee13d6124419115ea222f..26212ec66f564ef7f3ea6529696f7abd9e094c41 100644 (file)
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -2,7 +2,7 @@
 /*! \file delta_rational.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/arith/ordered_bounds_list.h b/src/theory/arith/ordered_bounds_list.h
index d21283afa4df781206c0ca88aa7d7046925db4b3..4393a382e48f1ddc96bd8f1f7e1e09245c760d1f 100644 (file)
--- a/src/theory/arith/ordered_bounds_list.h
+++ b/src/theory/arith/ordered_bounds_list.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file ordered_bounds_list.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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
+ **/
+
 
 
 #include "cvc4_private.h"

diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index bd2d5d61e7ad472ab30c5f72802b2c16f4daaf9e..18993c748a40fbd2c8b33573e41e4af540504e94 100644 (file)
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 44631fdef550ac05a578e1d3a4912dbc92ef930f..bd945002e76602c88843a913ed09cf259029f209 100644 (file)
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/arith/slack.h b/src/theory/arith/slack.h
index 5cf391e64533fccac10334cd6fddf7ed1806345f..87bf83e32df934a893b6de5dfa98bdd0cbb2f9e2 100644 (file)
--- a/src/theory/arith/slack.h
+++ b/src/theory/arith/slack.h
@@ -2,7 +2,7 @@
 /*! \file slack.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index f270dacb4d18f1ef999aa0549d4c9d78b978a6e2..7f414db66a5d30c5068ebaec6c4a5e492d566642 100644 (file)
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index cb9dc85f7ba9ce9b42d8acad815af63ba37cc03a..5d719aa6fd2af089c70a7537219f79550a17a6df 100644 (file)
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index 9b22b14bb6a2213e905f70e714b7ab6307f0a112..9fb30bdb4565f565949bf18cb1a3ac4249b17cc1 100644 (file)
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -1,8 +1,9 @@
 /*********************                                                        */
-/*! \file theory_arith_type_rules.cpp
+/*! \file theory_arith_type_rules.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 106d1a8da3a4e3f779f4a41e00ff1f26f1b7b0c7..ab72a0a8c758cb7d5b2a41352f3d60bcf2560978 100644 (file)
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -2,8 +2,8 @@
 /*! \file theory_arrays.cpp
  ** \verbatim
  ** Original author: barrett
- ** Major contributors: 
- ** Minor contributors (to current version): 
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 69498cfb2eca1cb76a09020bd4f0f92cf27f3dfd..7bc57bcfbe74ad35df68b20ed3602fd1275ecd67 100644 (file)
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -2,7 +2,7 @@
 /*! \file theory_arrays.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: barrett
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/booleans/theory_bool_type_rules.h b/src/theory/booleans/theory_bool_type_rules.h
index 8843a38c1af99fd5c9ccbb9563542de84e8f6a82..b947cee109cca11d0e1eb934e19f64bb6e7a9d4c 100644 (file)
--- a/src/theory/booleans/theory_bool_type_rules.h
+++ b/src/theory/booleans/theory_bool_type_rules.h
@@ -1,8 +1,9 @@
 /*********************                                                        */
-/*! \file theory_bool_type_rules.cpp
+/*! \file theory_bool_type_rules.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 0f4fda1a6b3b31f2a5c0c7a7d3e0b551608f719e..19d6e268b0c1841335353f5899033ec6803581e5 100644 (file)
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -1,8 +1,9 @@
 /*********************                                                        */
-/*! \file builtin_type_rules.cpp
+/*! \file theory_builtin_type_rules.h
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 7dd6c3e60011f21dcf5e4e67ca9e481cb3ebb68b..7aaae7349a0cf311c94e8a7588d735cc0b033383 100644 (file)
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -2,7 +2,7 @@
 /*! \file theory_bv_type_rules.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp
index 5e83d3728df509b635b398bd3d32f68e9c444853..ba46e18e25d2218aa5d2ed5ff5a766b2476f3a4b 100644 (file)
--- a/src/theory/theory.cpp
+++ b/src/theory/theory.cpp
@@ -2,7 +2,7 @@
 /*! \file theory.cpp
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: taking
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 79eec430176d20d7ac8fa995a135032b2ba1a8c9..865fd83a920bdae2fa28f2e0d70f64e2bbf2410f 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -2,7 +2,7 @@
 /*! \file theory_engine.h
  ** \verbatim
  ** Original author: mdeters
- ** Major contributors: taking, dejan
+ ** Major contributors: dejan, taking
  ** Minor contributors (to current version): cconway
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)

diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index cd0b4ef663a2c98660aa82298ad40952908beed1..a7f6e98ae72fd23ff541098eb1ee9b026df5a9a5 100644 (file)
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file theory_test_utils.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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
+ **/
+
 
 
 #include "cvc4_public.h"

diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 419e3d0782755b8a56be100ee01bc25a5d71f512..e77de7d33fc0bb1598b9295824e3b8a85436ccc0 100644 (file)
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -2,7 +2,8 @@
 /*! \file theory_uf_type_rules.h
  ** \verbatim
  ** Original author: dejan
- ** Major contributors: none
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
index 9440b6df361f7e21c72d380122cbd36722dbcd2e..7c837083c9c44d61370f8a79ffaf4e119e95f053 100644 (file)
--- a/src/util/bitvector.cpp
+++ b/src/util/bitvector.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 0febfddfd37383c6ef62575812106cc420072550..928592d9ec7e054674abf4ce64fcc9225f2f8777 100644 (file)
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: cconway
- ** Minor contributors (to current version): mdeters
+ ** Minor contributors (to current version): taking, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
index 692d3d7421b0cbc8e6fc041bf646ca1a35b61ea4..a425690a57debf447a183b014760f4b219f68c6c 100644 (file)
--- a/src/util/gmp_util.h
+++ b/src/util/gmp_util.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: dejan
  ** Major contributors: mdeters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/hash.h b/src/util/hash.h
index 6a6130886ceb2925fd9048b6e1fffa1b3b07d369..73c7939512e6e889eae4e2005f466a3a3e152a15 100644 (file)
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: mdeters
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): taking
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/integer.h b/src/util/integer.h
index f3431334d44699def1241d4573a574754a95d604..d1921f59778ba26bcc0e95e4ce8911dae18cbdea 100644 (file)
--- a/src/util/integer.h
+++ b/src/util/integer.h
@@ -2,8 +2,8 @@
 /*! \file integer.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan, cconway
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan, cconway, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 607075658ae06cdab85490e8b2d05fc366c282eb..6b32c46bba13c267ff2d3a0321e3d221a7fb46d6 100644 (file)
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Minor contributors (to current version): taking, mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/stats.cpp b/src/util/stats.cpp
index 1677e0ce56bd8af86446cc6a21a4866412d26713..8ce82ee7fbf97a68e47aca800332da284229cdf3 100644 (file)
--- a/src/util/stats.cpp
+++ b/src/util/stats.cpp
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/src/util/stats.h b/src/util/stats.h
index 6efe7f85666c02fc9783e8b5eb872416638acfb6..f917e8b525636c1ac93cf3c93183b83060727920 100644 (file)
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: taking
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/test/unit/expr/declaration_scope_black.h b/test/unit/expr/declaration_scope_black.h
index 923df2afb1281702914c89aa2a8efc831551412c..b1e77c6148c486feedef7a604158f948e7b0a8df 100644 (file)
--- a/test/unit/expr/declaration_scope_black.h
+++ b/test/unit/expr/declaration_scope_black.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): mdeters, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/test/unit/expr/expr_manager_public.h b/test/unit/expr/expr_manager_public.h
index 4d3958278d17408ad78205e48760125719163354..3b1e96084138fe28d795acecd3f8583f3f1c8260 100644 (file)
--- a/test/unit/expr/expr_manager_public.h
+++ b/test/unit/expr/expr_manager_public.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h
index e839360d7ae1ab67494210790866728cf31279ca..b130501f530e9cb86308b028e6c09705027fb5c2 100644 (file)
--- a/test/unit/parser/parser_builder_black.h
+++ b/test/unit/parser/parser_builder_black.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index def0a12eddd2c9344d7c5a5429c1edf92f4d351a..ee3d9c2002cbf9f825bc9b4f5574ab4f1126b3e4 100644 (file)
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -3,7 +3,7 @@
  ** \verbatim
  ** Original author: cconway
  ** Major contributors: none
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): mdeters, dejan
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h
index d6614b87edd1c18dfca44c20f869797320fac31d..d8c41bf3a18bcc8de80d7d031f8d4e5ee800c3ca 100644 (file)
--- a/test/unit/theory/theory_arith_white.h
+++ b/test/unit/theory/theory_arith_white.h
@@ -1,3 +1,22 @@
+/*********************                                                        */
+/*! \file theory_arith_white.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** 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
+ **/
+
 
 #include <cxxtest/TestSuite.h>
 

diff --git a/test/unit/util/bitvector_black.h b/test/unit/util/bitvector_black.h
index c4e77852bb7a8f3a647475d9bc95218a841d1745..14fb3406a06b612e7b181c11a3d77faeea0b63f0 100644 (file)
--- a/test/unit/util/bitvector_black.h
+++ b/test/unit/util/bitvector_black.h
@@ -2,8 +2,8 @@
 /*! \file bitvector_black.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/test/unit/util/integer_white.h b/test/unit/util/integer_white.h
index cd92449969216bc2bb8f5d896d99110d02780425..1c6b03cdfd8a4a8860e3c5839beaed9b2dc08283 100644 (file)
--- a/test/unit/util/integer_white.h
+++ b/test/unit/util/integer_white.h
@@ -2,8 +2,8 @@
 /*! \file integer_white.h
  ** \verbatim
  ** Original author: taking
- ** Major contributors: none
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences

diff --git a/test/unit/util/rational_black.h b/test/unit/util/rational_black.h
index 17bd7b245f7b37347cb63063fbe657dce92f5c9d..dcae800d1ec658f3c1a5f7726664934c0fa2a71c 100644 (file)
--- a/test/unit/util/rational_black.h
+++ b/test/unit/util/rational_black.h
@@ -2,7 +2,7 @@
 /*! \file rational_black.h
  ** \verbatim
  ** Original author: cconway
- ** Major contributors: none
+ ** Major contributors: mdeters
  ** Minor contributors (to current version): none
  ** This file is part of the CVC4 prototype.
  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)