mergecav2019strings_countRewRed

56 files changed, 219 insertions, 201 deletions

diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp
index 472fd8127..7c3ce6aaf 100644
--- a/src/util/abstract_value.cpp
+++ b/src/util/abstract_value.cpp
@@ -2,9 +2,9 @@
 /*! \file abstract_value.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King
+ **   Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h
index 7117a58d2..8091a7ee5 100644
--- a/src/util/abstract_value.h
+++ b/src/util/abstract_value.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h
index d547530b1..d6a7c95d7 100644
--- a/src/util/bin_heap.h
+++ b/src/util/bin_heap.h
@@ -2,9 +2,9 @@
 /*! \file bin_heap.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters
+ **   Tim King, Morgan Deters, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -20,8 +20,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__BIN_HEAP_H
-#define __CVC4__BIN_HEAP_H
+#ifndef CVC4__BIN_HEAP_H
+#define CVC4__BIN_HEAP_H
 
 #include <limits>
 #include <functional>
@@ -365,4 +365,4 @@ const size_t BinaryHeap<Elem,CmpFcn>::MAX_SIZE = (std::numeric_limits<size_t>::m
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__BIN_HEAP_H */
+#endif /* CVC4__BIN_HEAP_H */
diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
index def9fd90f..a561fe088 100644
--- a/src/util/bitvector.cpp
+++ b/src/util/bitvector.cpp
@@ -2,9 +2,9 @@
 /*! \file bitvector.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Andres Noetzli
+ **   Aina Niemetz, Liana Hadarean, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 13c1f14dd..f13db5417 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -2,9 +2,9 @@
 /*! \file bitvector.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Dejan Jovanovic, Liana Hadarean
+ **   Aina Niemetz, Dejan Jovanovic, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__BITVECTOR_H
-#define __CVC4__BITVECTOR_H
+#ifndef CVC4__BITVECTOR_H
+#define CVC4__BITVECTOR_H
 
 #include <cstdint>
 #include <iosfwd>
@@ -66,11 +66,29 @@ class CVC4_PUBLIC BitVector
   {
   }
 
+  /**
+   * BitVector constructor.
+   *
+   * The value of the bit-vector is passed in as string of base 2, 10 or 16.
+   * The size of resulting bit-vector is
+   * - base  2: the size of the binary string
+   * - base 10: the min. size required to represent the decimal as a bit-vector
+   * - base 16: the max. size required to represent the hexadecimal as a
+   *            bit-vector (4 * size of the given value string)
+   *
+   * @param num The value of the bit-vector in string representation.
+   * @param base The base of the string representation.
+   */
   BitVector(const std::string& num, unsigned base = 2)
   {
-    CheckArgument(base == 2 || base == 16, base);
-    d_size = base == 2 ? num.size() : num.size() * 4;
+    CheckArgument(base == 2 || base == 10 || base == 16, base);
     d_value = Integer(num, base);
+    switch (base)
+    {
+      case 10: d_size = d_value.length(); break;
+      case 16: d_size = num.size() * 4; break;
+      default: d_size = num.size();
+    }
   }
 
   ~BitVector() {}
@@ -416,4 +434,4 @@ inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv)
 
 }  // namespace CVC4
 
-#endif /* __CVC4__BITVECTOR_H */
+#endif /* CVC4__BITVECTOR_H */
diff --git a/src/util/bool.h b/src/util/bool.h
index 68a416f94..32f3741f8 100644
--- a/src/util/bool.h
+++ b/src/util/bool.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__BOOL_H
-#define __CVC4__BOOL_H
+#ifndef CVC4__BOOL_H
+#define CVC4__BOOL_H
 
 namespace CVC4 {
 
@@ -29,4 +29,4 @@ struct BoolHashFunction {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__BOOL_H */
+#endif /* CVC4__BOOL_H */
diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index 4584c46ab..ce1763ba1 100644
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 956468e30..b06d72286 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Tim King, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__CARDINALITY_H
-#define __CVC4__CARDINALITY_H
+#ifndef CVC4__CARDINALITY_H
+#define CVC4__CARDINALITY_H
 
 #include <iostream>
 #include <utility>
@@ -225,4 +225,4 @@ std::ostream& operator<<(std::ostream& out, const Cardinality& c) CVC4_PUBLIC;
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__CARDINALITY_H */
+#endif /* CVC4__CARDINALITY_H */
diff --git a/src/util/channel.h b/src/util/channel.h
index 8587800c1..00776921f 100644
--- a/src/util/channel.h
+++ b/src/util/channel.h
@@ -22,8 +22,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__CHANNEL_H
-#define __CVC4__CHANNEL_H
+#ifndef CVC4__CHANNEL_H
+#define CVC4__CHANNEL_H
 
 #include <boost/circular_buffer.hpp>
 #include <boost/thread/mutex.hpp>
@@ -118,4 +118,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__CHANNEL_H */
+#endif /* CVC4__CHANNEL_H */
diff --git a/src/util/debug.h b/src/util/debug.h
index ef887ef24..e25ca8168 100644
--- a/src/util/debug.h
+++ b/src/util/debug.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -20,8 +20,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__DEBUG_H
-#define __CVC4__DEBUG_H
+#ifndef CVC4__DEBUG_H
+#define CVC4__DEBUG_H
 
 #include <cassert>
 
@@ -34,4 +34,4 @@
 #  define cvc4assert(x) /*__builtin_expect( ( x ), true )*/
 #endif /* CVC4_ASSERTIONS */
 
-#endif /* __CVC4__DEBUG_H */
+#endif /* CVC4__DEBUG_H */
diff --git a/src/util/dense_map.h b/src/util/dense_map.h
index 410fcc8fa..cc1a094eb 100644
--- a/src/util/dense_map.h
+++ b/src/util/dense_map.h
@@ -2,9 +2,9 @@
 /*! \file dense_map.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Dejan Jovanovic
+ **   Tim King, Dejan Jovanovic, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/divisible.cpp b/src/util/divisible.cpp
index 33437b91e..f336a318c 100644
--- a/src/util/divisible.cpp
+++ b/src/util/divisible.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/divisible.h b/src/util/divisible.h
index 65731fcaa..a0c730436 100644
--- a/src/util/divisible.h
+++ b/src/util/divisible.h
@@ -2,9 +2,9 @@
 /*! \file divisible.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King
+ **   Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__DIVISIBLE_H
-#define __CVC4__DIVISIBLE_H
+#ifndef CVC4__DIVISIBLE_H
+#define CVC4__DIVISIBLE_H
 
 #include <iosfwd>
 
@@ -60,4 +60,4 @@ inline std::ostream& operator <<(std::ostream& os, const Divisible& d) {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__DIVISIBLE_H */
+#endif /* CVC4__DIVISIBLE_H */
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index 1de5e358a..4aed27c30 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -2,10 +2,10 @@
 /*! \file floatingpoint.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Martin Brain, Tim King
+ **   Martin Brain, Martin Brain, Tim King
  ** Copyright (c) 2013  University of Oxford
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/floatingpoint.h.in b/src/util/floatingpoint.h.in
index d283d985f..bac0fbd59 100644
--- a/src/util/floatingpoint.h.in
+++ b/src/util/floatingpoint.h.in
@@ -2,10 +2,10 @@
 /*! \file floatingpoint.h.in
  ** \verbatim
  ** Top contributors (to current version):
- **   Martin Brain, Tim King, Andres Noetzli
+ **   Martin Brain, Martin Brain, Tim King
  ** Copyright (c) 2013  University of Oxford
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
  **/
 #include "cvc4_public.h"
 
-#ifndef __CVC4__FLOATINGPOINT_H
-#define __CVC4__FLOATINGPOINT_H
+#ifndef CVC4__FLOATINGPOINT_H
+#define CVC4__FLOATINGPOINT_H
 
 #include "util/bitvector.h"
 #include "util/rational.h"
@@ -551,4 +551,4 @@ namespace CVC4 {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__FLOATINGPOINT_H */
+#endif /* CVC4__FLOATINGPOINT_H */
diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h
index d09174b47..3ba388564 100644
--- a/src/util/gmp_util.h
+++ b/src/util/gmp_util.h
@@ -2,9 +2,9 @@
 /*! \file gmp_util.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Morgan Deters, Andres Noetzli
+ **   Tim King, Andres Noetzli, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__GMP_UTIL_H
-#define __CVC4__GMP_UTIL_H
+#ifndef CVC4__GMP_UTIL_H
+#define CVC4__GMP_UTIL_H
 
 /*
  * Older versions of GMP in combination with newer versions of GCC and C++11
@@ -44,4 +44,4 @@ inline size_t gmpz_hash(const mpz_t toHash) {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__GMP_UTIL_H */
+#endif /* CVC4__GMP_UTIL_H */
diff --git a/src/util/hash.h b/src/util/hash.h
index af604dc3a..14167bc82 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -2,9 +2,9 @@
 /*! \file hash.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Andres Noetzli, Christopher L. Conway
+ **   Morgan Deters, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__HASH_H
-#define __CVC4__HASH_H
+#ifndef CVC4__HASH_H
+#define CVC4__HASH_H
 
 #include <cstdint>
 #include <functional>
@@ -67,4 +67,4 @@ struct PairHashFunction {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__HASH_H */
+#endif /* CVC4__HASH_H */
diff --git a/src/util/index.cpp b/src/util/index.cpp
index e48cea6b5..6f036d537 100644
--- a/src/util/index.cpp
+++ b/src/util/index.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/index.h b/src/util/index.h
index 5ddc8fcf0..2ee6ff19e 100644
--- a/src/util/index.h
+++ b/src/util/index.h
@@ -2,9 +2,9 @@
 /*! \file index.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__INDEX_H
-#define __CVC4__INDEX_H
+#ifndef CVC4__INDEX_H
+#define CVC4__INDEX_H
 
 #include <cstdint>
 
@@ -28,4 +28,4 @@ using Index = uint32_t;
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__INDEX_H */
+#endif /* CVC4__INDEX_H */
diff --git a/src/util/integer.h.in b/src/util/integer.h.in
index ad6c059ed..87a5e35d3 100644
--- a/src/util/integer.h.in
+++ b/src/util/integer.h.in
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
index 15d517f72..6439708b9 100644
--- a/src/util/integer_cln_imp.cpp
+++ b/src/util/integer_cln_imp.cpp
@@ -2,9 +2,9 @@
 /*! \file integer_cln_imp.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Aina Niemetz, Clark Barrett
+ **   Tim King, Aina Niemetz, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 49f625425..aba5b6a3a 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Morgan Deters, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__INTEGER_H
-#define __CVC4__INTEGER_H
+#ifndef CVC4__INTEGER_H
+#define CVC4__INTEGER_H
 
 #include <cln/input.h>
 #include <cln/integer.h>
@@ -559,4 +559,4 @@ inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__INTEGER_H */
+#endif /* CVC4__INTEGER_H */
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
index 50e23a572..ed206bb45 100644
--- a/src/util/integer_gmp_imp.cpp
+++ b/src/util/integer_gmp_imp.cpp
@@ -2,9 +2,9 @@
 /*! \file integer_gmp_imp.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Aina Niemetz, Clark Barrett
+ **   Tim King, Aina Niemetz, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index a93888e31..144e88536 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Liana Hadarean, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__INTEGER_H
-#define __CVC4__INTEGER_H
+#ifndef CVC4__INTEGER_H
+#define CVC4__INTEGER_H
 
 #include <string>
 #include <iosfwd>
@@ -540,4 +540,4 @@ inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__INTEGER_H */
+#endif /* CVC4__INTEGER_H */
diff --git a/src/util/maybe.h b/src/util/maybe.h
index dff0b4dea..33c6c6511 100644
--- a/src/util/maybe.h
+++ b/src/util/maybe.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -24,8 +24,8 @@
  **/
 #include "cvc4_public.h"
 
-#ifndef __CVC4__UTIL__MAYBE_H
-#define __CVC4__UTIL__MAYBE_H
+#ifndef CVC4__UTIL__MAYBE_H
+#define CVC4__UTIL__MAYBE_H
 
 #include <ostream>
 
@@ -86,4 +86,4 @@ inline std::ostream& operator<<(std::ostream& out, const Maybe<T>& m){
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__UTIL__MAYBE_H */
+#endif /* CVC4__UTIL__MAYBE_H */
diff --git a/src/util/ostream_util.cpp b/src/util/ostream_util.cpp
index 6cbaa530e..3ada604ca 100644
--- a/src/util/ostream_util.cpp
+++ b/src/util/ostream_util.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/ostream_util.h b/src/util/ostream_util.h
index a295dd273..45d30a01c 100644
--- a/src/util/ostream_util.h
+++ b/src/util/ostream_util.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__UTIL__OSTREAM_UTIL_H
-#define __CVC4__UTIL__OSTREAM_UTIL_H
+#ifndef CVC4__UTIL__OSTREAM_UTIL_H
+#define CVC4__UTIL__OSTREAM_UTIL_H
 
 #include <ios>
 #include <ostream>
@@ -46,4 +46,4 @@ class StreamFormatScope
 
 }  // namespace CVC4
 
-#endif /* __CVC4__UTIL__OSTREAM_UTIL_H */
+#endif /* CVC4__UTIL__OSTREAM_UTIL_H */
diff --git a/src/util/proof.h b/src/util/proof.h
index 98afe19b3..ac129e3aa 100644
--- a/src/util/proof.h
+++ b/src/util/proof.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Tim King, Guy Katz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__PROOF_H
-#define __CVC4__PROOF_H
+#ifndef CVC4__PROOF_H
+#define CVC4__PROOF_H
 
 #include <iosfwd>
 #include <unordered_map>
@@ -41,4 +41,4 @@ class CVC4_PUBLIC Proof
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PROOF_H */
+#endif /* CVC4__PROOF_H */
diff --git a/src/util/random.cpp b/src/util/random.cpp
index 7c6abd33e..72a8fbc24 100644
--- a/src/util/random.cpp
+++ b/src/util/random.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/random.h b/src/util/random.h
index e6443c3da..0b46a1f04 100644
--- a/src/util/random.h
+++ b/src/util/random.h
@@ -2,9 +2,9 @@
 /*! \file random.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz
+ **   Aina Niemetz, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__UTIL__RANDOM_H
-#define __CVC4__UTIL__RANDOM_H
+#ifndef CVC4__UTIL__RANDOM_H
+#define CVC4__UTIL__RANDOM_H
 
 namespace CVC4 {
 
diff --git a/src/util/rational.h.in b/src/util/rational.h.in
index 1b67dbf0e..5da7a501e 100644
--- a/src/util/rational.h.in
+++ b/src/util/rational.h.in
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp
index 3dc76f1a4..ca67dd6cb 100644
--- a/src/util/rational_cln_imp.cpp
+++ b/src/util/rational_cln_imp.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Christopher L. Conway, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index 826f6ff3f..660c4b075 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -2,9 +2,9 @@
 /*! \file rational_cln_imp.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Aina Niemetz
+ **   Tim King, Morgan Deters, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__RATIONAL_H
-#define __CVC4__RATIONAL_H
+#ifndef CVC4__RATIONAL_H
+#define CVC4__RATIONAL_H
 
 #include <gmp.h>
 #include <string>
@@ -373,4 +373,4 @@ CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__RATIONAL_H */
+#endif /* CVC4__RATIONAL_H */
diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp
index 7e9cc67f8..229b51db7 100644
--- a/src/util/rational_gmp_imp.cpp
+++ b/src/util/rational_gmp_imp.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Christopher L. Conway, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index 1d47cb1ba..ff8a0f776 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -2,9 +2,9 @@
 /*! \file rational_gmp_imp.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Aina Niemetz
+ **   Tim King, Morgan Deters, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__RATIONAL_H
-#define __CVC4__RATIONAL_H
+#ifndef CVC4__RATIONAL_H
+#define CVC4__RATIONAL_H
 
 /*
  * Older versions of GMP in combination with newer versions of GCC and C++11
@@ -358,4 +358,4 @@ CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__RATIONAL_H */
+#endif /* CVC4__RATIONAL_H */
diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp
index 34175a775..ed9455e6d 100644
--- a/src/util/regexp.cpp
+++ b/src/util/regexp.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Tianyi Liang, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 1588b5174..f7c6fb2ae 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, Tianyi Liang
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__REGEXP_H
-#define __CVC4__REGEXP_H
+#ifndef CVC4__REGEXP_H
+#define CVC4__REGEXP_H
 
 #include <cstddef>
 #include <functional>
@@ -246,4 +246,4 @@ std::ostream& operator<<(std::ostream& os, const String& s) CVC4_PUBLIC;
 
 }  // namespace CVC4
 
-#endif /* __CVC4__REGEXP_H */
+#endif /* CVC4__REGEXP_H */
diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp
index 041d765cb..6d7e08736 100644
--- a/src/util/resource_manager.cpp
+++ b/src/util/resource_manager.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Liana Hadarean, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h
index 3ca2babcf..264565a76 100644
--- a/src/util/resource_manager.h
+++ b/src/util/resource_manager.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Liana Hadarean, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__RESOURCE_MANAGER_H
-#define __CVC4__RESOURCE_MANAGER_H
+#ifndef CVC4__RESOURCE_MANAGER_H
+#define CVC4__RESOURCE_MANAGER_H
 
 #include <cstddef>
 #include <sys/time.h>
@@ -197,4 +197,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__RESOURCE_MANAGER_H */
+#endif /* CVC4__RESOURCE_MANAGER_H */
diff --git a/src/util/result.cpp b/src/util/result.cpp
index 69598074a..e76f428a5 100644
--- a/src/util/result.cpp
+++ b/src/util/result.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Morgan Deters, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/result.h b/src/util/result.h
index 31d997c21..f34a9bb5a 100644
--- a/src/util/result.h
+++ b/src/util/result.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__RESULT_H
-#define __CVC4__RESULT_H
+#ifndef CVC4__RESULT_H
+#define CVC4__RESULT_H
 
 #include <iostream>
 #include <string>
@@ -151,4 +151,4 @@ bool operator!=(enum Result::Validity v, const Result& r) CVC4_PUBLIC;
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__RESULT_H */
+#endif /* CVC4__RESULT_H */
diff --git a/src/util/safe_print.cpp b/src/util/safe_print.cpp
index 00dedd3bc..beb1a1673 100644
--- a/src/util/safe_print.cpp
+++ b/src/util/safe_print.cpp
@@ -2,9 +2,9 @@
 /*! \file safe_print.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli
+ **   Andres Noetzli, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/safe_print.h b/src/util/safe_print.h
index 8cd1b7367..75a517b18 100644
--- a/src/util/safe_print.h
+++ b/src/util/safe_print.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -29,8 +29,8 @@
 
 #include "cvc4_private_library.h"
 
-#ifndef __CVC4__SAFE_PRINT_H
-#define __CVC4__SAFE_PRINT_H
+#ifndef CVC4__SAFE_PRINT_H
+#define CVC4__SAFE_PRINT_H
 
 #if __cplusplus >= 201103L
 // For c++11 and newer
@@ -96,4 +96,4 @@ void safe_print_right_aligned(int fd, uint64_t i, ssize_t width);
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__SAFE_PRINT_H */
+#endif /* CVC4__SAFE_PRINT_H */
diff --git a/src/util/sampler.cpp b/src/util/sampler.cpp
index e64ab56df..948b4dfd3 100644
--- a/src/util/sampler.cpp
+++ b/src/util/sampler.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/sampler.h b/src/util/sampler.h
index f8f11dff2..aa473ba0c 100644
--- a/src/util/sampler.h
+++ b/src/util/sampler.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__UTIL_FLOATINGPOINT_SAMPLER_H
-#define __CVC4__UTIL_FLOATINGPOINT_SAMPLER_H
+#ifndef CVC4__UTIL_FLOATINGPOINT_SAMPLER_H
+#define CVC4__UTIL_FLOATINGPOINT_SAMPLER_H
 
 #include "util/floatingpoint.h"
 #include "util/random.h"
@@ -55,4 +55,4 @@ class Sampler
 
 }  // namespace CVC4
 
-#endif /* __CVC4__UTIL_FLOATINGPOINT_SAMPLER_H */
+#endif /* CVC4__UTIL_FLOATINGPOINT_SAMPLER_H */
diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp
index a7e38ee61..9de42a4e6 100644
--- a/src/util/sexpr.cpp
+++ b/src/util/sexpr.cpp
@@ -2,9 +2,9 @@
 /*! \file sexpr.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andrew Reynolds
+ **   Tim King, Morgan Deters, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index bad6cdb2b..bdc85df41 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Morgan Deters, Christopher L. Conway
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -23,8 +23,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__SEXPR_H
-#define __CVC4__SEXPR_H
+#ifndef CVC4__SEXPR_H
+#define CVC4__SEXPR_H
 
 #include <iomanip>
 #include <iosfwd>
@@ -301,4 +301,4 @@ std::ostream& operator<<(std::ostream& out, PrettySExprs ps);
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__SEXPR_H */
+#endif /* CVC4__SEXPR_H */
diff --git a/src/util/smt2_quote_string.cpp b/src/util/smt2_quote_string.cpp
index fec0962ae..626767f5f 100644
--- a/src/util/smt2_quote_string.cpp
+++ b/src/util/smt2_quote_string.cpp
@@ -2,9 +2,9 @@
 /*! \file smt2_quote_string.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King
+ **   Tim King, Morgan Deters, Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/smt2_quote_string.h b/src/util/smt2_quote_string.h
index c1fcfe2a4..f91874a2e 100644
--- a/src/util/smt2_quote_string.h
+++ b/src/util/smt2_quote_string.h
@@ -2,9 +2,9 @@
 /*! \file smt2_quote_string.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__UTIL__SMT2_QUOTE_STRING_H
-#define __CVC4__UTIL__SMT2_QUOTE_STRING_H
+#ifndef CVC4__UTIL__SMT2_QUOTE_STRING_H
+#define CVC4__UTIL__SMT2_QUOTE_STRING_H
 
 #include <string>
 
@@ -30,4 +30,4 @@ std::string quoteSymbol(const std::string& s);
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__UTIL__SMT2_QUOTE_STRING_H */
+#endif /* CVC4__UTIL__SMT2_QUOTE_STRING_H */
diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp
index d078473ad..c61520df9 100644
--- a/src/util/statistics.cpp
+++ b/src/util/statistics.cpp
@@ -2,9 +2,9 @@
 /*! \file statistics.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Andres Noetzli
+ **   Morgan Deters, Andres Noetzli, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/util/statistics.h b/src/util/statistics.h
index eee4ce6fd..68d8d6fda 100644
--- a/src/util/statistics.h
+++ b/src/util/statistics.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Andres Noetzli, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__STATISTICS_H
-#define __CVC4__STATISTICS_H
+#ifndef CVC4__STATISTICS_H
+#define CVC4__STATISTICS_H
 
 #include <iterator>
 #include <ostream>
@@ -132,4 +132,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__STATISTICS_H */
+#endif /* CVC4__STATISTICS_H */
diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp
index 53f18f07b..2ccbc2971 100644
--- a/src/util/statistics_registry.cpp
+++ b/src/util/statistics_registry.cpp
@@ -2,9 +2,9 @@
 /*! \file statistics_registry.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andres Noetzli, Aina Niemetz
+ **   Morgan Deters, Tim King, Kshitij Bansal
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -26,9 +26,9 @@
 #include "util/ostream_util.h"
 
 #ifdef CVC4_STATISTICS_ON
-#  define __CVC4_USE_STATISTICS true
+#  define CVC4_USE_STATISTICS true
 #else
-#  define __CVC4_USE_STATISTICS false
+#  define CVC4_USE_STATISTICS false
 #endif
 
 
@@ -148,7 +148,7 @@ std::ostream& operator<<(std::ostream& os, const timespec& t) {
 StatisticsRegistry::StatisticsRegistry(const std::string& name) : Stat(name)
 {
   d_prefix = name;
-  if(__CVC4_USE_STATISTICS) {
+  if(CVC4_USE_STATISTICS) {
     PrettyCheckArgument(d_name.find(s_regDelim) == std::string::npos, name,
                         "StatisticsRegistry names cannot contain the string \"%s\"",
                     s_regDelim.c_str());
@@ -194,7 +194,7 @@ void StatisticsRegistry::safeFlushInformation(int fd) const {
 }
 
 void TimerStat::start() {
-  if(__CVC4_USE_STATISTICS) {
+  if(CVC4_USE_STATISTICS) {
     PrettyCheckArgument(!d_running, *this, "timer already running");
     clock_gettime(CLOCK_MONOTONIC, &d_start);
     d_running = true;
@@ -202,7 +202,7 @@ void TimerStat::start() {
 }/* TimerStat::start() */
 
 void TimerStat::stop() {
-  if(__CVC4_USE_STATISTICS) {
+  if(CVC4_USE_STATISTICS) {
     CVC4_CHECK(d_running) << "timer not running";
     ::timespec end;
     clock_gettime(CLOCK_MONOTONIC, &end);
@@ -217,7 +217,7 @@ bool TimerStat::running() const {
 
 timespec TimerStat::getData() const {
   ::timespec data = d_data;
-  if(__CVC4_USE_STATISTICS && d_running) {
+  if(CVC4_USE_STATISTICS && d_running) {
     ::timespec end;
     clock_gettime(CLOCK_MONOTONIC, &end);
     data += end - d_start;
@@ -227,7 +227,7 @@ timespec TimerStat::getData() const {
 
 SExpr TimerStat::getValue() const {
   ::timespec data = d_data;
-  if(__CVC4_USE_STATISTICS && d_running) {
+  if(CVC4_USE_STATISTICS && d_running) {
     ::timespec end;
     clock_gettime(CLOCK_MONOTONIC, &end);
     data += end - d_start;
@@ -253,4 +253,4 @@ RegisterStatistic::~RegisterStatistic() {
 
 }/* CVC4 namespace */
 
-#undef __CVC4_USE_STATISTICS
+#undef CVC4_USE_STATISTICS
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h
index d7f105b65..a369be272 100644
--- a/src/util/statistics_registry.h
+++ b/src/util/statistics_registry.h
@@ -2,9 +2,9 @@
 /*! \file statistics_registry.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Andres Noetzli
+ **   Morgan Deters, Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -33,8 +33,8 @@
 
 #include "cvc4_private_library.h"
 
-#ifndef __CVC4__STATISTICS_REGISTRY_H
-#define __CVC4__STATISTICS_REGISTRY_H
+#ifndef CVC4__STATISTICS_REGISTRY_H
+#define CVC4__STATISTICS_REGISTRY_H
 
 #include <stdint.h>
 
@@ -60,9 +60,9 @@ namespace CVC4 {
 std::ostream& operator<<(std::ostream& os, const timespec& t) CVC4_PUBLIC;
 
 #ifdef CVC4_STATISTICS_ON
-#  define __CVC4_USE_STATISTICS true
+#  define CVC4_USE_STATISTICS true
 #else
-#  define __CVC4_USE_STATISTICS false
+#  define CVC4_USE_STATISTICS false
 #endif
 
 
@@ -93,7 +93,7 @@ public:
    */
   Stat(const std::string& name) : d_name(name)
   {
-    if(__CVC4_USE_STATISTICS) {
+    if(CVC4_USE_STATISTICS) {
       CheckArgument(d_name.find(", ") == std::string::npos, name,
                     "Statistics names cannot include a comma (',')");
     }
@@ -122,7 +122,7 @@ public:
    * May be redefined by a child class
    */
   virtual void flushStat(std::ostream& out) const {
-    if(__CVC4_USE_STATISTICS) {
+    if(CVC4_USE_STATISTICS) {
       out << d_name << ", ";
       flushInformation(out);
     }
@@ -135,7 +135,7 @@ public:
    * May be redefined by a child class
    */
   virtual void safeFlushStat(int fd) const {
-    if (__CVC4_USE_STATISTICS) {
+    if (CVC4_USE_STATISTICS) {
       safe_print(fd, d_name);
       safe_print(fd, ", ");
       safeFlushInformation(fd);
@@ -230,14 +230,14 @@ public:
   /** Flush the value of the statistic to the given output stream. */
   void flushInformation(std::ostream& out) const override
   {
-    if(__CVC4_USE_STATISTICS) {
+    if(CVC4_USE_STATISTICS) {
       out << getData();
     }
   }
 
   void safeFlushInformation(int fd) const override
   {
-    if (__CVC4_USE_STATISTICS) {
+    if (CVC4_USE_STATISTICS) {
       safe_print<T>(fd, getDataRef());
     }
   }
@@ -317,7 +317,7 @@ public:
   /** Set this reference statistic to refer to the given data cell. */
   void setData(const T& t) override
   {
-    if(__CVC4_USE_STATISTICS) {
+    if(CVC4_USE_STATISTICS) {
       d_data = &t;
     }
   }
@@ -352,14 +352,14 @@ public:
   /** Set the underlying data value to the given value. */
   void setData(const T& t) override
   {
-    if(__CVC4_USE_STATISTICS) {
+    if(CVC4_USE_STATISTICS) {
       d_data = t;
     }
   }
 
   /** Identical to setData(). */
   BackedStat<T>& operator=(const T& t) {
-    if(__CVC4_USE_STATISTICS) {
+    if(CVC4_USE_STATISTICS) {
       d_data = t;
     }
     return *this;
@@ -443,7 +443,7 @@ public:
 
   /** Increment the underlying integer statistic. */
   IntStat& operator++() {
-    if(__CVC4_USE_STATISTICS) {
+    if(CVC4_USE_STATISTICS) {
       ++d_data;
     }
     return *this;
@@ -451,7 +451,7 @@ public:
 
   /** Increment the underlying integer statistic by the given amount. */
   IntStat& operator+=(int64_t val) {
-    if(__CVC4_USE_STATISTICS) {
+    if(CVC4_USE_STATISTICS) {
       d_data += val;
     }
     return *this;
@@ -459,7 +459,7 @@ public:
 
   /** Keep the maximum of the current statistic value and the given one. */
   void maxAssign(int64_t val) {
-    if(__CVC4_USE_STATISTICS) {
+    if(CVC4_USE_STATISTICS) {
       if(d_data < val) {
         d_data = val;
       }
@@ -468,7 +468,7 @@ public:
 
   /** Keep the minimum of the current statistic value and the given one. */
   void minAssign(int64_t val) {
-    if(__CVC4_USE_STATISTICS) {
+    if(CVC4_USE_STATISTICS) {
       if(d_data > val) {
         d_data = val;
       }
@@ -530,7 +530,7 @@ public:
 
   /** Add an entry to the running-average calculation. */
   void addEntry(double e) {
-    if(__CVC4_USE_STATISTICS) {
+    if(CVC4_USE_STATISTICS) {
       ++d_count;
       d_sum += e;
       setData(d_sum / d_count);
@@ -589,7 +589,7 @@ public:
 
   void flushInformation(std::ostream& out) const override
   {
-    if(__CVC4_USE_STATISTICS) {
+    if(CVC4_USE_STATISTICS) {
       typename Histogram::const_iterator i = d_hist.begin();
       typename Histogram::const_iterator end =  d_hist.end();
       out << "[";
@@ -608,7 +608,7 @@ public:
 
   void safeFlushInformation(int fd) const override
   {
-    if (__CVC4_USE_STATISTICS) {
+    if (CVC4_USE_STATISTICS) {
       typename Histogram::const_iterator i = d_hist.begin();
       typename Histogram::const_iterator end = d_hist.end();
       safe_print(fd, "[");
@@ -630,7 +630,7 @@ public:
   }
 
   HistogramStat& operator<<(const T& val){
-    if(__CVC4_USE_STATISTICS) {
+    if(CVC4_USE_STATISTICS) {
       if(d_hist.find(val) == d_hist.end()){
         d_hist.insert(std::make_pair(val,0));
       }
@@ -797,8 +797,8 @@ private:
 
 };/* class RegisterStatistic */
 
-#undef __CVC4_USE_STATISTICS
+#undef CVC4_USE_STATISTICS
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__STATISTICS_REGISTRY_H */
+#endif /* CVC4__STATISTICS_REGISTRY_H */
diff --git a/src/util/tuple.h b/src/util/tuple.h
index a60393ca0..13b605794 100644
--- a/src/util/tuple.h
+++ b/src/util/tuple.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__TUPLE_H
-#define __CVC4__TUPLE_H
+#ifndef CVC4__TUPLE_H
+#define CVC4__TUPLE_H
 
 #include <iostream>
 #include <string>
@@ -50,4 +50,4 @@ inline std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) {
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__TUPLE_H */
+#endif /* CVC4__TUPLE_H */
diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h
index 1cf54b7f1..5c8360cdf 100644
--- a/src/util/unsafe_interrupt_exception.h
+++ b/src/util/unsafe_interrupt_exception.h
@@ -2,9 +2,9 @@
 /*! \file unsafe_interrupt_exception.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Tim King
+ **   Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -15,8 +15,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
-#define __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
+#ifndef CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
+#define CVC4__UNSAFE_INTERRUPT_EXCEPTION_H
 
 #include "base/exception.h"
 
@@ -40,4 +40,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__UNSAFE_INTERRUPT_EXCEPTION_H */
+#endif /* CVC4__UNSAFE_INTERRUPT_EXCEPTION_H */
diff --git a/src/util/utility.h b/src/util/utility.h
index 56a68ca40..275efd9d0 100644
--- a/src/util/utility.h
+++ b/src/util/utility.h
@@ -2,9 +2,9 @@
 /*! \file utility.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Aina Niemetz
+ **   Morgan Deters, Andres Noetzli, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__UTILITY_H
-#define __CVC4__UTILITY_H
+#ifndef CVC4__UTILITY_H
+#define CVC4__UTILITY_H
 
 #include <algorithm>
 #include <utility>
@@ -87,4 +87,4 @@ void container_to_stream(std::ostream& out,
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__UTILITY_H */
+#endif /* CVC4__UTILITY_H */