* configure.ac: Remove doc/ from search path for Makefile.ams

* configure.ac, test/unit/Makefile.am: Resolved an issue where even
  when not testing, one unit test was built.

* Re-ran contrib/update-copyright.pl on all source files to ensure
  consistent and correct header comments.

* contrib/get-authors: Change definition of "minor contributor"
  to >= 10% of lines (rather than strictly greater than 10% of lines)

33 files changed, 89 insertions, 44 deletions

diff --git a/src/context/context.h b/src/context/context.h
index 1af4480f9..403235bc9 100644
--- a/src/context/context.h
+++ b/src/context/context.h
@@ -2,7 +2,7 @@
 /** context.h
  ** Original author: mdeters
  ** Major contributors: barrett
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): taking, 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/attribute.h b/src/expr/attribute.h
index 1d2705240..54500d0d5 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -1,7 +1,7 @@
-/*********************                                           -*- C++ -*-  */
+/*********************                                                        */
 /** attribute.h
  ** Original author: mdeters
- ** Major contributors: dejan
+ ** 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)
diff --git a/src/expr/expr.cpp b/src/expr/expr.cpp
index 18c0fdbab..c29b7e448 100644
--- a/src/expr/expr.cpp
+++ b/src/expr/expr.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** expr.cpp
  ** Original author: dejan
- ** Major contributors: taking
- ** Minor contributors (to current version): mdeters
+ ** 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/expr/expr.h b/src/expr/expr.h
index dd4d0e9d7..096094aff 100644
--- a/src/expr/expr.h
+++ b/src/expr/expr.h
@@ -2,7 +2,7 @@
 /** expr.h
  ** Original author: dejan
  ** Major contributors: none
- ** Minor contributors (to current version): mdeters, taking
+ ** 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/expr/expr_manager.cpp b/src/expr/expr_manager.cpp
index 506c118bc..71368c101 100644
--- a/src/expr/expr_manager.cpp
+++ b/src/expr/expr_manager.cpp
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /** expr_manager.cpp
  ** Original author: dejan
- ** Major contributors: mdeters
+ ** Major contributors: cconway, 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/expr_manager.h b/src/expr/expr_manager.h
index edfc18c8d..d84cf76be 100644
--- a/src/expr/expr_manager.h
+++ b/src/expr/expr_manager.h
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /** expr_manager.h
  ** Original author: dejan
- ** Major contributors: mdeters
+ ** Major contributors: cconway, 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/node.cpp b/src/expr/node.cpp
index 79490d58e..90dd86712 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** node.cpp
  ** Original author: mdeters
- ** Major contributors: taking, dejan
- ** Minor contributors (to current version): none
+ ** Major contributors: dejan
+ ** 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/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 12a6d1732..c6aee3dea 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** node_manager.cpp
  ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): dejan
+ ** Major contributors: 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/node_manager.h b/src/expr/node_manager.h
index 18a95f041..97f5ba9cd 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** node_manager.h
  ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): taking, dejan
+ ** Major contributors: dejan
+ ** 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/expr/soft_node.h b/src/expr/soft_node.h
index fe71a4d1a..0bf9b47cf 100644
--- a/src/expr/soft_node.h
+++ b/src/expr/soft_node.h
@@ -1,8 +1,8 @@
-/*********************                                           -*- C++ -*-  */
+/*********************                                                        */
 /** soft_node.h
  ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): 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
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index d4662d420..368a3fe44 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -1,5 +1,5 @@
-/*********************                                           -*- C++ -*-  */
-/** type.h
+/*********************                                                        */
+/** type.cpp
  ** Original author: cconway
  ** Major contributors: none
  ** Minor contributors (to current version): none
diff --git a/src/expr/type.h b/src/expr/type.h
index 19d0c831e..fd485602e 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -1,8 +1,8 @@
-/*********************                                           -*- C++ -*-  */
+/*********************                                                        */
 /** type.h
  ** 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/main/getopt.cpp b/src/main/getopt.cpp
index 190f7bbf3..7ca889592 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -2,7 +2,7 @@
 /** getopt.cpp
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): barrett, dejan
+ ** Minor contributors (to current version): barrett, dejan, 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/main/main.cpp b/src/main/main.cpp
index 6ebe895a5..a12c69df7 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -2,7 +2,7 @@
 /** main.cpp
  ** Original author: mdeters
  ** Major contributors: barrett, dejan
- ** Minor contributors (to current version): 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/main/usage.h b/src/main/usage.h
index 9a8175e2a..6c44fef5a 100644
--- a/src/main/usage.h
+++ b/src/main/usage.h
@@ -2,7 +2,7 @@
 /** usage.h
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): 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_parser.cpp b/src/parser/antlr_parser.cpp
index 30fb33a32..0fdde07ff 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** antlr_parser.cpp
  ** Original author: dejan
- ** Major contributors: mdeters, cconway
- ** Minor contributors (to current version): none
+ ** Major contributors: cconway
+ ** 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/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index 0cdf9f36b..bfdc4c0f2 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -1,8 +1,8 @@
 /* *******************                                                        */
 /*  cvc_parser.g
  ** Original author: dejan
- ** Major contributors: mdeters
- ** Minor contributors (to current version): cconway
+ ** Major contributors: cconway
+ ** 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.cpp b/src/parser/parser.cpp
index b9e2d576e..84796f093 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -2,7 +2,7 @@
 /** parser.cpp
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): 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/parser.h b/src/parser/parser.h
index 170e1af31..da2c630ca 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -2,7 +2,7 @@
 /** parser.h
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): 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/symbol_table.h b/src/parser/symbol_table.h
index d790a1c84..dd110c4c1 100644
--- a/src/parser/symbol_table.h
+++ b/src/parser/symbol_table.h
@@ -1,4 +1,4 @@
-/*********************                                           -*- C++ -*-  */
+/*********************                                                        */
 /** symbol_table.h
  ** Original author: cconway
  ** Major contributors: dejan, mdeters
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 80a8819b9..5dd57610d 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** prop_engine.cpp
  ** Original author: mdeters
- ** Major contributors: taking
- ** Minor contributors (to current version): none
+ ** Major contributors: dejan
+ ** 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/prop/prop_engine.h b/src/prop/prop_engine.h
index 9aa1ecff8..d4007e73a 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** prop_engine.h
  ** Original author: mdeters
- ** Major contributors: taking
- ** Minor contributors (to current version): dejan
+ ** Major contributors: taking, 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/prop/sat.h b/src/prop/sat.h
index 350537d8f..a9696162a 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /** sat.h
  ** Original author: mdeters
- ** Major contributors: none
+ ** Major contributors: 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)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 36954ace4..bb3e8c058 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2,7 +2,7 @@
 /** smt_engine.cpp
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): 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)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 0e7e951f8..838f9cd7a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -2,7 +2,7 @@
 /** smt_engine.h
  ** Original author: mdeters
  ** Major contributors: dejan
- ** Minor contributors (to current version): 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)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/theory/theory.h b/src/theory/theory.h
index dffc99053..831a185f8 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -2,7 +2,7 @@
 /** theory.h
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): dejan
+ ** Minor contributors (to current version): 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/theory/uf/ecdata.cpp b/src/theory/uf/ecdata.cpp
index a22faf61e..cb7add487 100644
--- a/src/theory/uf/ecdata.cpp
+++ b/src/theory/uf/ecdata.cpp
@@ -1,3 +1,18 @@
+/*********************                                                        */
+/** ecdata.cpp
+ ** 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.
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
 #include "theory/uf/ecdata.h"
 
 using namespace CVC4;
diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h
index fd0855bee..c8303a245 100644
--- a/src/theory/uf/ecdata.h
+++ b/src/theory/uf/ecdata.h
@@ -1,7 +1,7 @@
 /*********************                                                        */
 /** ecdata.h
  ** Original author: taking
- ** Major contributors: barrett
+ ** 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)
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 840c7b51e..1f4d80b9b 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -1,3 +1,18 @@
+/*********************                                                        */
+/** theory_uf.cpp
+ ** 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.
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
 
 #include "theory/uf/theory_uf.h"
 #include "theory/uf/ecdata.h"
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 06b0ee4f8..0ab51ca2c 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -1,3 +1,18 @@
+/*********************                                                        */
+/** theory_uf.h
+ ** 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.
+ **
+ ** [[ Add file-specific comments here ]]
+ **/
+
 
 #ifndef __CVC4__THEORY__THEORY_UF_H
 #define __CVC4__THEORY__THEORY_UF_H
diff --git a/src/util/configuration.h b/src/util/configuration.h
index b761f1f22..20d00a5f8 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -2,7 +2,7 @@
 /** configuration.h
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): 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)
  ** Courant Institute of Mathematical Sciences
diff --git a/src/util/options.h b/src/util/options.h
index cad00a61b..404700a85 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** options.h
  ** Original author: mdeters
- ** Major contributors: dejan
- ** Minor contributors (to current version): taking
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): taking, 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/util/output.h b/src/util/output.h
index ad42416d8..d0db064f0 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -2,7 +2,7 @@
 /** output.h
  ** Original author: mdeters
  ** Major contributors: none
- ** Minor contributors (to current version): 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