Merge branch '1.4.x'

8 files changed, 17 insertions, 12 deletions

diff --git a/AUTHORS b/AUTHORS
index 70baafd3c..5610fe063 100644
--- a/AUTHORS
+++ b/AUTHORS
@@ -26,7 +26,7 @@ CVC4 contains the doxygen.m4 autoconf module by Oren Ben-Kiki.
 CVC4 contains the pkg.m4 autoconf module by Scott James Remnant.
 
 CVC4 contains the ax_tls.m4 autoconf module by Alan Woodland and Diego Elio
-Petteno.
+Petteno`.
 
 CVC4 contains the boost.m4 autoconf module by Benoit Sigoure.
 
diff --git a/COPYING b/COPYING
index b07cc669e..dddf4ed59 100644
--- a/COPYING
+++ b/COPYING
@@ -120,7 +120,7 @@ http://www.gnu.org/software/autoconf-archive/ax_tls.html.
 See config/ax_tls.m4.  Its copyright:
 
   Copyright (c) 2008 Alan Woodland <ajw05@aber.ac.uk>
-  Copyright (c) 2010 Diego Elio Pettenò <flameeyes@gmail.com>
+  Copyright (c) 2010 Diego Elio Petteno` <flameeyes@gmail.com>
 
   This program is free software: you can redistribute it and/or modify it
   under the terms of the GNU General Public License as published by the
diff --git a/config/abc.m4 b/config/abc.m4
index 0d91a36a5..faeb68cf2 100644
--- a/config/abc.m4
+++ b/config/abc.m4
@@ -9,7 +9,7 @@ ABC_LIBS=
 ABC_LDFLAGS=
 if test "$with_abc" = no; then
   AC_MSG_RESULT([no, abc disabled by user])
-elif test "$with_abc" = yes; then
+elif test -n "$with_abc"; then
   AC_MSG_RESULT([yes, abc requested by user])
 
   # Get the location of all the ABC stuff
diff --git a/config/ax_tls.m4 b/config/ax_tls.m4
index 1d7736852..033e3b135 100644
--- a/config/ax_tls.m4
+++ b/config/ax_tls.m4
@@ -16,7 +16,7 @@
 # LICENSE
 #
 #   Copyright (c) 2008 Alan Woodland <ajw05@aber.ac.uk>
-#   Copyright (c) 2010 Diego Elio Pettenò <flameeyes@gmail.com>
+#   Copyright (c) 2010 Diego Elio Petteno` <flameeyes@gmail.com>
 #
 #   This program is free software: you can redistribute it and/or modify it
 #   under the terms of the GNU General Public License as published by the
@@ -44,7 +44,7 @@
 #   modified version of the Autoconf Macro, you may extend this special
 #   exception to the GPL to apply to your modified version as well.
 
-#serial 8
+#serial 10
 
 AC_DEFUN([AX_TLS], [
   AC_MSG_CHECKING(for thread local storage (TLS) class)
diff --git a/config/glpk.m4 b/config/glpk.m4
index 2799d5a77..8d16fceee 100644
--- a/config/glpk.m4
+++ b/config/glpk.m4
@@ -9,7 +9,7 @@ GLPK_LIBS=
 GLPK_LDFLAGS=
 if test "$with_glpk" = no; then
   AC_MSG_RESULT([no, glpk disabled by user])
-elif test "$with_glpk" = yes; then
+elif test -n "$with_glpk"; then
   AC_MSG_RESULT([yes, glpk requested by user])
 
   # Get the location of all the GLPK stuff
diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index 9bfa6f5fa..f3c4248ac 100755
--- a/contrib/update-copyright.pl
+++ b/contrib/update-copyright.pl
@@ -35,7 +35,7 @@
 #
 
 my $excluded_directories = '^(minisat|bvminisat|CVS|generated)$';
-my $excluded_paths = '^(src/parser/antlr_input_imports.cpp|src/bindings/compat/.*)$';
+my $excluded_paths = '^(src/parser/antlr_input_imports.cpp|src/bindings/compat/.*|src/util/channel.h)$';
 
 # Years of copyright for the template.  E.g., the string
 # "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever.
diff --git a/src/theory/bv/options b/src/theory/bv/options
index 81d88421b..a9c3b0f08 100644
--- a/src/theory/bv/options
+++ b/src/theory/bv/options
@@ -15,7 +15,7 @@ option bitblastMode bitblast --bitblast=MODE CVC4::theory::bv::BitblastMode :han
 option bitvectorAig --bitblast-aig bool :default false :predicate CVC4::theory::bv::abcEnabledBuild :predicate-include "theory/bv/options_handlers.h" :read-write :link --bitblast=eager :link --bv-aig-simp="balance;drw"
  bitblast by first converting to AIG (only if --bitblast=eager)
 
-expert-option bitvectorAigSimplifications --bv-aig-simp=FILE std::string :default "" :predicate CVC4::theory::bv::abcEnabledBuild :read-write :link --bitblast-aig
+expert-option bitvectorAigSimplifications --bv-aig-simp=COMMAND std::string :default "" :predicate CVC4::theory::bv::abcEnabledBuild :read-write :link --bitblast-aig
  abc command to run AIG simplifications
 
 # Options for lazy bit-blasting  
diff --git a/src/util/channel.h b/src/util/channel.h
index 3644f786a..710c3274b 100644
--- a/src/util/channel.h
+++ b/src/util/channel.h
@@ -4,10 +4,15 @@
  ** Original author: Morgan Deters
  ** Major contributors: none
  ** Minor contributors (to current version): none
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014  New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** This file is part of the CVC4 project but is excluded from the
+ ** standard CVC4 licensing because it is a derivative work of
+ ** circular_buffer.hpp in the BOOST 1.46.1 distribution.
+ ** Thus this file is covered by the Boost Software License, version 1.0.
+ ** See below.
+ **
+ ** The combined work is:
+ **   Copyright (c) 2009-2014  New York University and The University of Iowa
+ **   Copyright (c) 2003-2008  Jan Gaspar
  **
  ** \brief [[ Add one-line brief description here ]]
  **