mergecav2019strings_countRewRed

65 files changed, 139 insertions, 147 deletions

diff --git a/src/theory/arith/approx_simplex.cpp b/src/theory/arith/approx_simplex.cpp
index bc7efdaf7..e621131d5 100644
--- a/src/theory/arith/approx_simplex.cpp
+++ b/src/theory/arith/approx_simplex.cpp
@@ -2,9 +2,9 @@
 /*! \file approx_simplex.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andres Noetzli, 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
diff --git a/src/theory/arith/approx_simplex.h b/src/theory/arith/approx_simplex.h
index a0982169d..2914c2da8 100644
--- a/src/theory/arith/approx_simplex.h
+++ b/src/theory/arith/approx_simplex.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 5b51e162d..3980b41b8 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Aina Niemetz, 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/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h
index 2c6a30758..a9e7aa92c 100644
--- a/src/theory/arith/arith_ite_utils.h
+++ b/src/theory/arith/arith_ite_utils.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, 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
@@ -19,8 +19,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
-#define __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
+#ifndef CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
+#define CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H
 
 #include <unordered_map>
 
@@ -115,4 +115,4 @@ private:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */
+#endif /* CVC4__THEORY__ARITH__ARITH_ITE_UTILS_H */
diff --git a/src/theory/arith/arith_msum.cpp b/src/theory/arith/arith_msum.cpp
index f08b4c0ba..7f13ce07d 100644
--- a/src/theory/arith/arith_msum.cpp
+++ b/src/theory/arith/arith_msum.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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/theory/arith/arith_msum.h b/src/theory/arith/arith_msum.h
index 195db38c9..8a9dbf791 100644
--- a/src/theory/arith/arith_msum.h
+++ b/src/theory/arith/arith_msum.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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
@@ -14,8 +14,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__ARITH__MSUM_H
-#define __CVC4__THEORY__ARITH__MSUM_H
+#ifndef CVC4__THEORY__ARITH__MSUM_H
+#define CVC4__THEORY__ARITH__MSUM_H
 
 #include <map>
 
@@ -185,4 +185,4 @@ class ArithMSum
 } /* CVC4::theory namespace */
 } /* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__MSUM_H */
+#endif /* CVC4__THEORY__ARITH__MSUM_H */
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index c3327e620..267fcc383 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Andrew Reynolds, 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/theory/arith/arith_rewriter.h b/src/theory/arith/arith_rewriter.h
index 7d137bdfd..de6b3f228 100644
--- a/src/theory/arith/arith_rewriter.h
+++ b/src/theory/arith/arith_rewriter.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Dejan Jovanovic, 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_private.h"
 
-#ifndef __CVC4__THEORY__ARITH__ARITH_REWRITER_H
-#define __CVC4__THEORY__ARITH__ARITH_REWRITER_H
+#ifndef CVC4__THEORY__ARITH__ARITH_REWRITER_H
+#define CVC4__THEORY__ARITH__ARITH_REWRITER_H
 
 #include "theory/theory.h"
 #include "theory/rewriter.h"
@@ -76,4 +76,4 @@ private:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__ARITH_REWRITER_H */
+#endif /* CVC4__THEORY__ARITH__ARITH_REWRITER_H */
diff --git a/src/theory/arith/arith_static_learner.cpp b/src/theory/arith/arith_static_learner.cpp
index 4bfc1a4f9..2138b513e 100644
--- a/src/theory/arith/arith_static_learner.cpp
+++ b/src/theory/arith/arith_static_learner.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, 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
diff --git a/src/theory/arith/arith_static_learner.h b/src/theory/arith/arith_static_learner.h
index a6b57411b..bc77f8ec0 100644
--- a/src/theory/arith/arith_static_learner.h
+++ b/src/theory/arith/arith_static_learner.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, 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
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
-#define __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
+#ifndef CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
+#define CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H
 
 #include <set>
 
@@ -72,4 +72,4 @@ private:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H */
+#endif /* CVC4__THEORY__ARITH__ARITH_STATIC_LEARNER_H */
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index 14c7fcefe..c8e92dfd3 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Andrew Reynolds, 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_private.h"
 
-#ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
-#define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H
+#ifndef CVC4__THEORY__ARITH__ARITH_UTILITIES_H
+#define CVC4__THEORY__ARITH__ARITH_UTILITIES_H
 
 #include <unordered_map>
 #include <unordered_set>
@@ -307,4 +307,4 @@ inline Node mkPi()
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__ARITH_UTILITIES_H */
+#endif /* CVC4__THEORY__ARITH__ARITH_UTILITIES_H */
diff --git a/src/theory/arith/arithvar.cpp b/src/theory/arith/arithvar.cpp
index 8ac72276d..2eb349984 100644
--- a/src/theory/arith/arithvar.cpp
+++ b/src/theory/arith/arithvar.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/theory/arith/arithvar.h b/src/theory/arith/arithvar.h
index cb1fb7b5f..9ab452947 100644
--- a/src/theory/arith/arithvar.h
+++ b/src/theory/arith/arithvar.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
diff --git a/src/theory/arith/arithvar_node_map.h b/src/theory/arith/arithvar_node_map.h
index 0606eb65d..03b061504 100644
--- a/src/theory/arith/arithvar_node_map.h
+++ b/src/theory/arith/arithvar_node_map.h
@@ -2,9 +2,9 @@
 /*! \file arithvar_node_map.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Dejan Jovanovic
+ **   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_private.h"
 
-#ifndef __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
-#define __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
+#ifndef CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
+#define CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H
 
 
 #include "theory/arith/arithvar.h"
@@ -92,4 +92,4 @@ public:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H */
+#endif /* CVC4__THEORY__ARITH__ARITHVAR_NODE_MAP_H */
diff --git a/src/theory/arith/attempt_solution_simplex.cpp b/src/theory/arith/attempt_solution_simplex.cpp
index 025571650..f269847de 100644
--- a/src/theory/arith/attempt_solution_simplex.cpp
+++ b/src/theory/arith/attempt_solution_simplex.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/theory/arith/attempt_solution_simplex.h b/src/theory/arith/attempt_solution_simplex.h
index 7e5b41936..1fd8ee146 100644
--- a/src/theory/arith/attempt_solution_simplex.h
+++ b/src/theory/arith/attempt_solution_simplex.h
@@ -2,9 +2,9 @@
 /*! \file attempt_solution_simplex.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Mathias Preiner
+ **   Tim King, Morgan Deters, 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/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h
index 7debbad13..7bd69190e 100644
--- a/src/theory/arith/bound_counts.h
+++ b/src/theory/arith/bound_counts.h
@@ -2,9 +2,9 @@
 /*! \file bound_counts.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Clark Barrett
+ **   Tim King, Clark Barrett
  ** 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/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index 86240b949..a11dd729b 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.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/theory/arith/callbacks.h b/src/theory/arith/callbacks.h
index 8b79ff659..ee39c76f9 100644
--- a/src/theory/arith/callbacks.h
+++ b/src/theory/arith/callbacks.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Mathias Preiner, Clark Barrett
  ** 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/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index bf251660d..ce45141ef 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Paul Meng, Dejan Jovanovic
  ** 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/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 11c229399..bccd2e943 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -2,9 +2,9 @@
 /*! \file congruence_manager.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Paul Meng, Mathias Preiner
+ **   Tim King, Mathias Preiner, Paul Meng
  ** 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/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index 297e3de37..c7251d4c4 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -2,9 +2,9 @@
 /*! \file constraint.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters
+ **   Tim King, Alex Ozdemir, 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/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 51575bb2f..f2c0c4b02 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -2,9 +2,9 @@
 /*! \file constraint.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters
+ **   Tim King, Alex Ozdemir, 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
@@ -72,8 +72,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__ARITH__CONSTRAINT_H
-#define __CVC4__THEORY__ARITH__CONSTRAINT_H
+#ifndef CVC4__THEORY__ARITH__CONSTRAINT_H
+#define CVC4__THEORY__ARITH__CONSTRAINT_H
 
 #include <unordered_map>
 #include <list>
@@ -1209,4 +1209,4 @@ private:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__CONSTRAINT_H */
+#endif /* CVC4__THEORY__ARITH__CONSTRAINT_H */
diff --git a/src/theory/arith/constraint_forward.h b/src/theory/arith/constraint_forward.h
index b08b572be..5f3f2251d 100644
--- a/src/theory/arith/constraint_forward.h
+++ b/src/theory/arith/constraint_forward.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 @@
  ** minimize interaction between header files.
  **/
 
-#ifndef __CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H
-#define __CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H
+#ifndef CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H
+#define CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H
 
 #include "cvc4_private.h"
 #include <vector>
@@ -46,4 +46,4 @@ static const RationalVectorP RationalVectorPSentinel = NULL;
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H */
+#endif /* CVC4__THEORY__ARITH__CONSTRAINT_FORWARD_H */
diff --git a/src/theory/arith/cut_log.cpp b/src/theory/arith/cut_log.cpp
index dcdadd76f..e9df7559d 100644
--- a/src/theory/arith/cut_log.cpp
+++ b/src/theory/arith/cut_log.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/theory/arith/cut_log.h b/src/theory/arith/cut_log.h
index 5fd585588..44553a15b 100644
--- a/src/theory/arith/cut_log.h
+++ b/src/theory/arith/cut_log.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp
index 758f8af4a..35640ac1a 100644
--- a/src/theory/arith/delta_rational.cpp
+++ b/src/theory/arith/delta_rational.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h
index 9a8e4586e..831c631f8 100644
--- a/src/theory/arith/delta_rational.h
+++ b/src/theory/arith/delta_rational.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, 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
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 718034f62..b30dc515b 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Morgan Deters, Dejan Jovanovic
  ** 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/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h
index aeb82a82b..0c26f9c55 100644
--- a/src/theory/arith/dio_solver.h
+++ b/src/theory/arith/dio_solver.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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_private.h"
 
 
-#ifndef __CVC4__THEORY__ARITH__DIO_SOLVER_H
-#define __CVC4__THEORY__ARITH__DIO_SOLVER_H
+#ifndef CVC4__THEORY__ARITH__DIO_SOLVER_H
+#define CVC4__THEORY__ARITH__DIO_SOLVER_H
 
 #include <unordered_map>
 #include <utility>
@@ -423,4 +423,4 @@ public:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__DIO_SOLVER_H */
+#endif /* CVC4__THEORY__ARITH__DIO_SOLVER_H */
diff --git a/src/theory/arith/dual_simplex.cpp b/src/theory/arith/dual_simplex.cpp
index c2b95890a..47a196353 100644
--- a/src/theory/arith/dual_simplex.cpp
+++ b/src/theory/arith/dual_simplex.cpp
@@ -2,9 +2,9 @@
 /*! \file dual_simplex.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andres Noetzli
+ **   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
diff --git a/src/theory/arith/dual_simplex.h b/src/theory/arith/dual_simplex.h
index 56eaf9a50..ab04bc616 100644
--- a/src/theory/arith/dual_simplex.h
+++ b/src/theory/arith/dual_simplex.h
@@ -2,9 +2,9 @@
 /*! \file dual_simplex.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Mathias Preiner
+ **   Tim King, Mathias Preiner, 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/theory/arith/error_set.cpp b/src/theory/arith/error_set.cpp
index d5b86143d..80c1e03ec 100644
--- a/src/theory/arith/error_set.cpp
+++ b/src/theory/arith/error_set.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/theory/arith/error_set.h b/src/theory/arith/error_set.h
index 2eb2b60d2..8839739a2 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -2,9 +2,9 @@
 /*! \file error_set.h
  ** \verbatim
  ** Top contributors (to current version):
- **   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/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index 07c6b1691..827323302 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -2,9 +2,9 @@
 /*! \file fc_simplex.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andres Noetzli
+ **   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
diff --git a/src/theory/arith/fc_simplex.h b/src/theory/arith/fc_simplex.h
index 0fc646151..cfeef1d26 100644
--- a/src/theory/arith/fc_simplex.h
+++ b/src/theory/arith/fc_simplex.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Morgan Deters, 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/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp
index 501b3507c..5ce617061 100644
--- a/src/theory/arith/infer_bounds.cpp
+++ b/src/theory/arith/infer_bounds.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/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h
index 8a48cb8bc..bce9a07db 100644
--- a/src/theory/arith/infer_bounds.h
+++ b/src/theory/arith/infer_bounds.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
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index e424c714e..7f729751b 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -2,9 +2,9 @@
 /*! \file linear_equality.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   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/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 531b52c3a..1f5bb9ea4 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -2,9 +2,9 @@
 /*! \file linear_equality.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Mathias Preiner, Clark Barrett
+ **   Tim King, Mathias Preiner, 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/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp
index 5da2ab2f6..c6332fd23 100644
--- a/src/theory/arith/matrix.cpp
+++ b/src/theory/arith/matrix.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/theory/arith/matrix.h b/src/theory/arith/matrix.h
index ef045ea37..02b8dc194 100644
--- a/src/theory/arith/matrix.h
+++ b/src/theory/arith/matrix.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Mathias Preiner, 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/theory/arith/nonlinear_extension.cpp b/src/theory/arith/nonlinear_extension.cpp
index 929c7808d..29b1cf2fc 100644
--- a/src/theory/arith/nonlinear_extension.cpp
+++ b/src/theory/arith/nonlinear_extension.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, 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
@@ -2621,8 +2621,10 @@ void NonlinearExtension::mkPi(){
     d_pi_neg = Rewriter::rewrite(NodeManager::currentNM()->mkNode(
         MULT, d_pi, NodeManager::currentNM()->mkConst(Rational(-1))));
     //initialize bounds
-    d_pi_bound[0] = NodeManager::currentNM()->mkConst( Rational(333)/Rational(106) );
-    d_pi_bound[1] = NodeManager::currentNM()->mkConst( Rational(355)/Rational(113) );
+    d_pi_bound[0] =
+        NodeManager::currentNM()->mkConst(Rational(103993) / Rational(33102));
+    d_pi_bound[1] =
+        NodeManager::currentNM()->mkConst(Rational(104348) / Rational(33215));
   }
 }
 
@@ -4358,31 +4360,21 @@ bool NonlinearExtension::checkTfTangentPlanesFun(Node tf,
   {
     // compute tangent plane
     // Figure 3: T( x )
-    Node tplane;
-    Node poly_approx_deriv = getDerivative(poly_approx, d_taylor_real_fv);
-    Assert(!poly_approx_deriv.isNull());
-    poly_approx_deriv = Rewriter::rewrite(poly_approx_deriv);
-    Trace("nl-ext-tftp-debug2") << "...derivative of " << poly_approx << " is "
-                                << poly_approx_deriv << std::endl;
-    std::vector<Node> taylor_subs;
-    taylor_subs.push_back(c);
-    Assert(taylor_vars.size() == taylor_subs.size());
-    Node poly_approx_c_deriv = poly_approx_deriv.substitute(taylor_vars.begin(),
-                                                            taylor_vars.end(),
-                                                            taylor_subs.begin(),
-                                                            taylor_subs.end());
-    tplane = nm->mkNode(
-        PLUS,
-        poly_approx_c,
-        nm->mkNode(MULT, poly_approx_c_deriv, nm->mkNode(MINUS, tf[0], c)));
+    // We use zero slope tangent planes, since the concavity of the Taylor
+    // approximation cannot be easily established.
+    Node tplane = poly_approx_c;
 
     Node lem = nm->mkNode(concavity == 1 ? GEQ : LEQ, tf, tplane);
     std::vector<Node> antec;
+    int mdir = regionToMonotonicityDir(k, region);
     for (unsigned i = 0; i < 2; i++)
     {
-      if (!bounds[i].isNull())
+      // Tangent plane is valid in the interval [c,u) if the slope of the
+      // function matches its concavity, and is valid in (l, c] otherwise.
+      Node use_bound = (mdir == concavity) == (i == 0) ? c : bounds[i];
+      if (!use_bound.isNull())
       {
-        Node ant = nm->mkNode(i == 0 ? GEQ : LEQ, tf[0], bounds[i]);
+        Node ant = nm->mkNode(i == 0 ? GEQ : LEQ, tf[0], use_bound);
         antec.push_back(ant);
       }
     }
diff --git a/src/theory/arith/nonlinear_extension.h b/src/theory/arith/nonlinear_extension.h
index cb74502d6..7452e322b 100644
--- a/src/theory/arith/nonlinear_extension.h
+++ b/src/theory/arith/nonlinear_extension.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, 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
@@ -15,8 +15,8 @@
  ** multiplication via axiom instantiations.
  **/
 
-#ifndef __CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H
-#define __CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H
+#ifndef CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H
+#define CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H
 
 #include <stdint.h>
 
@@ -1013,4 +1013,4 @@ class NonlinearExtension {
 }  // namespace theory
 }  // namespace CVC4
 
-#endif /* __CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */
+#endif /* CVC4__THEORY__ARITH__NONLINEAR_EXTENSION_H */
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 12bf90f2e..ee298bc66 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Andrew Reynolds, 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/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index b4d9e9f13..a3d173cc7 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -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
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__ARITH__NORMAL_FORM_H
-#define __CVC4__THEORY__ARITH__NORMAL_FORM_H
+#ifndef CVC4__THEORY__ARITH__NORMAL_FORM_H
+#define CVC4__THEORY__ARITH__NORMAL_FORM_H
 
 #include <algorithm>
 #include <list>
@@ -1393,4 +1393,4 @@ public:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__NORMAL_FORM_H */
+#endif /* CVC4__THEORY__ARITH__NORMAL_FORM_H */
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 4364b730a..855b673c5 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -2,9 +2,9 @@
 /*! \file partial_model.cpp
  ** \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
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index 9e8a51b9f..5006c6a9c 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
-#define __CVC4__THEORY__ARITH__PARTIAL_MODEL_H
+#ifndef CVC4__THEORY__ARITH__PARTIAL_MODEL_H
+#define CVC4__THEORY__ARITH__PARTIAL_MODEL_H
 
 #include <list>
 #include <vector>
@@ -416,4 +416,4 @@ private:
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__PARTIAL_MODEL_H */
+#endif /* CVC4__THEORY__ARITH__PARTIAL_MODEL_H */
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 4ee613f4c..77872fb55 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -2,9 +2,9 @@
 /*! \file simplex.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andres Noetzli, Morgan Deters
+ **   Tim King, 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/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 477e0c1fe..56a9bc95f 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -2,9 +2,9 @@
 /*! \file simplex.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Clark Barrett
+ **   Tim King, Clark Barrett
  ** 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/theory/arith/simplex_update.cpp b/src/theory/arith/simplex_update.cpp
index 634d17a55..011e07143 100644
--- a/src/theory/arith/simplex_update.cpp
+++ b/src/theory/arith/simplex_update.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/theory/arith/simplex_update.h b/src/theory/arith/simplex_update.h
index f823be36c..cfd00ac30 100644
--- a/src/theory/arith/simplex_update.h
+++ b/src/theory/arith/simplex_update.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index 31301df61..e23273a09 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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
diff --git a/src/theory/arith/soi_simplex.h b/src/theory/arith/soi_simplex.h
index 68af680d0..6fd8cf7c1 100644
--- a/src/theory/arith/soi_simplex.h
+++ b/src/theory/arith/soi_simplex.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Morgan Deters, 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/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index e0f5fc9e3..aa4c3d454 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.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/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 338baea7f..3f3bf883a 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -2,9 +2,9 @@
 /*! \file tableau.h
  ** \verbatim
  ** Top contributors (to current version):
- **   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/theory/arith/tableau_sizes.cpp b/src/theory/arith/tableau_sizes.cpp
index d7434529e..aec7b0384 100644
--- a/src/theory/arith/tableau_sizes.cpp
+++ b/src/theory/arith/tableau_sizes.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/theory/arith/tableau_sizes.h b/src/theory/arith/tableau_sizes.h
index 228ce06b8..95820dc93 100644
--- a/src/theory/arith/tableau_sizes.h
+++ b/src/theory/arith/tableau_sizes.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
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 9902121d0..6943c5546 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Dejan Jovanovic, 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/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index e4b1c5b26..b39ab961f 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -2,9 +2,9 @@
 /*! \file theory_arith.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Dejan Jovanovic
+ **   Tim King, Alex Ozdemir, 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/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 48d1b0188..c775a2611 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Andrew Reynolds, 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/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 2d8d61736..03cb81785 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -2,9 +2,9 @@
 /*! \file theory_arith_private.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andrew Reynolds, Martin Brain
+ **   Tim King, Andrew Reynolds, 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/theory/arith/theory_arith_private_forward.h b/src/theory/arith/theory_arith_private_forward.h
index 4bd242037..84dea1b4e 100644
--- a/src/theory/arith/theory_arith_private_forward.h
+++ b/src/theory/arith/theory_arith_private_forward.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
diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h
index bde1730a2..c32b612e2 100644
--- a/src/theory/arith/theory_arith_type_rules.h
+++ b/src/theory/arith/theory_arith_type_rules.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Dejan Jovanovic, 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
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
-#define __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
+#ifndef CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
+#define CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H
 
 namespace CVC4 {
 namespace theory {
@@ -185,4 +185,4 @@ class DivisibleOpTypeRule
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */
+#endif /* CVC4__THEORY__ARITH__THEORY_ARITH_TYPE_RULES_H */
diff --git a/src/theory/arith/type_enumerator.h b/src/theory/arith/type_enumerator.h
index ab0dff020..5c6bf63ce 100644
--- a/src/theory/arith/type_enumerator.h
+++ b/src/theory/arith/type_enumerator.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_private.h"
 
-#ifndef __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
-#define __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
+#ifndef CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
+#define CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H
 
 #include "expr/kind.h"
 #include "expr/type_node.h"
@@ -104,4 +104,4 @@ class IntegerEnumerator : public TypeEnumeratorBase<IntegerEnumerator> {
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */
+#endif /* CVC4__THEORY__ARITH__TYPE_ENUMERATOR_H */