* 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)

diff --git a/configure.ac b/configure.ac
index 8c1141b9d50712dcd078883cb4ac09a26f248346..d75ce6309d15468138a6726c6010b1cd2d03ba0c 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -453,10 +453,16 @@ LDFLAGS="${LDFLAGS:+$LDFLAGS }$CVC4LDFLAGS"
 mk_include=include
 AC_SUBST(mk_include)
 
+# CVC4_FALSE
+#
+# This is used to _always_ comment out rules in automake makefiles, but
+# still trigger certain automake behavior; see test/unit/Makefile.am.
+AM_CONDITIONAL([CVC4_FALSE], [false])
+
 AC_CONFIG_FILES([
   Makefile.builds
   Makefile]
-  m4_esyscmd([find contrib/ doc/ src/ test/ -name Makefile.am | sort | sed 's,\.am$,,'])
+  m4_esyscmd([find contrib/ src/ test/ -name Makefile.am | sort | sed 's,\.am$,,'])
 )
 
 AC_OUTPUT

diff --git a/contrib/get-authors b/contrib/get-authors
index a42f8a25ba5fb9ca57b0a1d7f6530b878cce68fc..40aaf6a6d607be5802ab4ddc9aca3e7a63e3bcd1 100755 (executable)
--- a/contrib/get-authors
+++ b/contrib/get-authors
@@ -20,7 +20,7 @@ while [ $# -gt 0 ]; do
     ( while read lines author; do
         pct=$((100*$lines/$total_lines))
         if [ "$author" != "$original_author" ]; then
-          if [ $pct -gt 10 ]; then
+          if [ $pct -ge 10 ]; then
             major_contributors="${major_contributors:+$major_contributors, }$author"
           else
             minor_contributors="${minor_contributors:+$minor_contributors, }$author"

diff --git a/src/context/context.h b/src/context/context.h
index 1af4480f9a59306ce91ec35555104d00ec68a0bf..403235bc9832c2983204004b14bb7fd765000d2e 100644 (file)
--- 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 1d27052409b03ab524398f4b832785a81616ff4a..54500d0d5a27bc98b9bc52a1cc97a8cb1c138f4a 100644 (file)
--- 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 18c0fdbab850f2176bf06cdc273a73f906effe40..c29b7e448657cff6e097c0f1329b513e3cb80e19 100644 (file)
--- 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 dd4d0e9d73a138d060b27ffdc7599d4fd97d2ab6..096094aff56906afd9c3c3e563482bbbc3728d3a 100644 (file)
--- 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 506c118bce54873a98f02f844c07513c6f3c3a31..71368c101d8841c0c196e11090e9f27b9e478a32 100644 (file)
--- 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 edfc18c8d793fc6687d96547e38a44e38267abc3..d84cf76be325632dd8ea917336659419ee10c027 100644 (file)
--- 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 79490d58efb4cfd7fe61f13a02218fdfa2ba8767..90dd867129dc23ee8ead5d732d1cf76200f6cfaa 100644 (file)
--- 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 12a6d1732111556da54c8a28cf234a51d29bddfe..c6aee3dea0681f5a6e98a11a3e0506d8649ad3a6 100644 (file)
--- 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 18a95f041d9f893a01e9bcc83f7ed44eccbcbffe..97f5ba9cd666c22641dd622d51d31fa03670e2f4 100644 (file)
--- 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 fe71a4d1a5717ea420156c605b7961c0505d8689..0bf9b47cfa44f7e9b72a88a11e67ed06d020a742 100644 (file)
--- 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 d4662d420506578400cf2bcf9617073e27ad3faa..368a3fe44f37a6187b9a9b36f0cb7f12456e4063 100644 (file)
--- 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 19d0c831e43885e90f230299ed5ebf39a8a095ef..fd485602ed7ee9895c06ffc2e5be5f489673cd5c 100644 (file)
--- 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 190f7bbf30f4a9c2243e8d91d3904066689207a7..7ca889592b975ede2dd73c9db059d89cd231113a 100644 (file)
--- 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 6ebe895a5fff64b9ab52deb114f6e87bf211be69..a12c69df79a6500f5d713bf7c40512f494bb7db2 100644 (file)
--- 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 9a8175e2a4e26ae1e0ee4668dfc9076818a4e06e..6c44fef5ad65c1665505e2a1959b37473589fa80 100644 (file)
--- 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 30fb33a325a3f92e44d92b6d8faa77aca31500f9..0fdde07ff2753befe9f3ec56aaed533da79a9f95 100644 (file)
--- 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 0cdf9f36b3674754aeb92d23a051d7d7941c96a2..bfdc4c0f252b81abc8514a922ec49ed7909f4d76 100644 (file)
--- 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 b9e2d576e6e300c38541d2e0c319f23d9ec6d202..84796f0935af2ecc3cc143236e6eb5423a94b4cd 100644 (file)
--- 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 170e1af31225756d93f0f34ea2da087ac8bacf92..da2c630ca049f46cd1cfecfdc1d41da7ff87ccd9 100644 (file)
--- 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 d790a1c84d305543e97850e15128348f204c51f5..dd110c4c16bd1e73733cd05b0acf4ae3e57928f0 100644 (file)
--- 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 80a8819b91fd26207ad920babaeb1a4ddf1c786b..5dd57610d892a335c08ad5a1c21c9d8091ee7a28 100644 (file)
--- 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 9aa1ecff851111d9b1bf1a8329a075e84c4c9757..d4007e73a44903e8d8dcae674dc56a40d022694f 100644 (file)
--- 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 350537d8f218b712282a231cb6f3c58bbd8317ae..a9696162a497a8e91e200d19c371dae98958b1e3 100644 (file)
--- 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 36954ace46fc3e3a7be848da26cc2d5df965761e..bb3e8c0585c1e850dce5c9a66446f25b46f67df5 100644 (file)
--- 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 0e7e951f8fda31d5f1399f72c74f03873b02e049..838f9cd7a3fecbcc68b2213065f0e861ea867e76 100644 (file)
--- 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 dffc9905304d99dc96a6d2c8904f98cb7317107e..831a185f8314b8bd47206f1a91ffa672e6947e39 100644 (file)
--- 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 a22faf61ed9fceefb5c17b7d09450c3e14be94a8..cb7add487e6831aee8066ac67b7ecc10667c24d5 100644 (file)
--- 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 fd0855beecddedcc22c5eff59c80110002ec04e4..c8303a24559d1257da74af09132f0b9e6a6f8455 100644 (file)
--- 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 840c7b51e437203fe255afa1285175dbeb197cf0..1f4d80b9be3ad5be9ab84f90c7a67384c18e6eb9 100644 (file)
--- 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 06b0ee4f843864376056ac646e88b92e61a4fcc8..0ab51ca2cf6cebb96effde548242301beab728bb 100644 (file)
--- 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 b761f1f22f9d6485c935d612fa6c4e3cdec78b5d..20d00a5f88ec4526c3f913d186ded67388ef37fc 100644 (file)
--- 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 cad00a61bf8b054ccb8b76e4c92d25801d821aea..404700a8556ebc141df6e1767cd26e072c36d487 100644 (file)
--- 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 ad42416d89ef0fb476fe252fbb0468a6139b82fc..d0db064f0b06e5dbe141cf3222a461aa30436b31 100644 (file)
--- 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

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index c145cf7522a8f3a769fef921cd8852c79ab02da8..591a852021c6ffb6ff19565942a1eafa387e73d3 100644 (file)
--- a/test/unit/Makefile.am
+++ b/test/unit/Makefile.am
@@ -51,11 +51,6 @@ EXTRA_DIST = \
        no_cxxtest \
        $(TEST_DEPS_DIST)
 
-# without these here, LTCXXCOMPILE, CXXLINK, etc., aren't set :-(
-noinst_LTLIBRARIES = libdummy.la
-libdummy_la_SOURCES = expr/node_black.cpp
-libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
-
 MOSTLYCLEANFILES = $(UNIT_TESTS) $(UNIT_TESTS:%=%.cpp)
 
 @mk_include@ @srcdir@/Makefile.tests
@@ -88,6 +83,13 @@ EXTRA_DIST = \
 
 endif
 
+# trick automake into setting LTCXXCOMPILE, CXXLINK, etc.
+if CVC4_FALSE
+noinst_LTLIBRARIES = libdummy.la
+libdummy_la_SOURCES = expr/node_black.cpp
+libdummy_la_LIBADD = @abs_top_builddir@/src/libcvc4.la
+endif
+
 # synonyms for "check"
 .PHONY: regress test
 regress test: check

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index dbf434ed28d6aa211369328548c27478679f3e4e..150d883064ede2a8cd657d049450306bc6ff1038 100644 (file)
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -1,8 +1,8 @@
 /*********************                                                        */
 /** parser_black.h
  ** Original author: cconway
- ** Major contributors: dejan
- ** Minor contributors (to current version): mdeters
+ ** Major contributors: none
+ ** 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