Merge branch 'sygusComp2018-2' into replaceSubstitutereplaceSubstitute

45 files changed, 84 insertions, 76 deletions

diff --git a/src/options/argument_extender.h b/src/options/argument_extender.h
index eea8eca56..9e52691ed 100644
--- a/src/options/argument_extender.h
+++ b/src/options/argument_extender.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Paul Meng, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/argument_extender_implementation.cpp b/src/options/argument_extender_implementation.cpp
index 9c38b348b..7c8549627 100644
--- a/src/options/argument_extender_implementation.cpp
+++ b/src/options/argument_extender_implementation.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Paul Meng
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/argument_extender_implementation.h b/src/options/argument_extender_implementation.h
index efcd55cae..66b21ce8c 100644
--- a/src/options/argument_extender_implementation.h
+++ b/src/options/argument_extender_implementation.h
@@ -2,9 +2,9 @@
 /*! \file argument_extender_implementation.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Paul Meng
+ **   Paul Meng, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/arith_heuristic_pivot_rule.cpp b/src/options/arith_heuristic_pivot_rule.cpp
index b07b400f1..00ac7ab5d 100644
--- a/src/options/arith_heuristic_pivot_rule.cpp
+++ b/src/options/arith_heuristic_pivot_rule.cpp
@@ -2,9 +2,9 @@
 /*! \file arith_heuristic_pivot_rule.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Paul Meng
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/arith_heuristic_pivot_rule.h b/src/options/arith_heuristic_pivot_rule.h
index ebfbf5ee9..f79a796b9 100644
--- a/src/options/arith_heuristic_pivot_rule.h
+++ b/src/options/arith_heuristic_pivot_rule.h
@@ -2,9 +2,9 @@
 /*! \file arith_heuristic_pivot_rule.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Paul Meng
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/arith_propagation_mode.cpp b/src/options/arith_propagation_mode.cpp
index 67e6f51dc..09a78b92a 100644
--- a/src/options/arith_propagation_mode.cpp
+++ b/src/options/arith_propagation_mode.cpp
@@ -2,9 +2,9 @@
 /*! \file arith_propagation_mode.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Paul Meng, Tim King
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/arith_propagation_mode.h b/src/options/arith_propagation_mode.h
index fad89cce5..0d54d901b 100644
--- a/src/options/arith_propagation_mode.h
+++ b/src/options/arith_propagation_mode.h
@@ -2,9 +2,9 @@
 /*! \file arith_propagation_mode.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Paul Meng, Tim King
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/arith_unate_lemma_mode.cpp b/src/options/arith_unate_lemma_mode.cpp
index ca076a791..a1f8d5613 100644
--- a/src/options/arith_unate_lemma_mode.cpp
+++ b/src/options/arith_unate_lemma_mode.cpp
@@ -2,9 +2,9 @@
 /*! \file arith_unate_lemma_mode.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Paul Meng, Tim King
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/arith_unate_lemma_mode.h b/src/options/arith_unate_lemma_mode.h
index bab7cfa72..4cec65011 100644
--- a/src/options/arith_unate_lemma_mode.h
+++ b/src/options/arith_unate_lemma_mode.h
@@ -2,9 +2,9 @@
 /*! \file arith_unate_lemma_mode.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Paul Meng
+ **   Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/base_handlers.h b/src/options/base_handlers.h
index 874516265..0f1d735d1 100644
--- a/src/options/base_handlers.h
+++ b/src/options/base_handlers.h
@@ -2,9 +2,9 @@
 /*! \file base_handlers.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Paul Meng
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/bv_bitblast_mode.cpp b/src/options/bv_bitblast_mode.cpp
index e9f9b60f9..9cfa2d6d3 100644
--- a/src/options/bv_bitblast_mode.cpp
+++ b/src/options/bv_bitblast_mode.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Liana Hadarean, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/bv_bitblast_mode.h b/src/options/bv_bitblast_mode.h
index 79f859cd4..530632674 100644
--- a/src/options/bv_bitblast_mode.h
+++ b/src/options/bv_bitblast_mode.h
@@ -2,9 +2,9 @@
 /*! \file bv_bitblast_mode.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Tim King
+ **   Liana Hadarean, Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/datatypes_modes.h b/src/options/datatypes_modes.h
index 3576ffc72..5f41ce11d 100644
--- a/src/options/datatypes_modes.h
+++ b/src/options/datatypes_modes.h
@@ -2,9 +2,9 @@
 /*! \file datatypes_modes.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King, Morgan Deters
+ **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/decision_mode.cpp b/src/options/decision_mode.cpp
index 118ff8d68..cd0bc8180 100644
--- a/src/options/decision_mode.cpp
+++ b/src/options/decision_mode.cpp
@@ -2,9 +2,9 @@
 /*! \file decision_mode.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Paul Meng, Tim King
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/decision_mode.h b/src/options/decision_mode.h
index 0d9c96e34..eb10ba8e8 100644
--- a/src/options/decision_mode.h
+++ b/src/options/decision_mode.h
@@ -2,9 +2,9 @@
 /*! \file decision_mode.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Kshitij Bansal, Paul Meng
+ **   Morgan Deters, Kshitij Bansal, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/decision_weight.h b/src/options/decision_weight.h
index 83401428e..90f6affa5 100644
--- a/src/options/decision_weight.h
+++ b/src/options/decision_weight.h
@@ -2,9 +2,9 @@
 /*! \file decision_weight.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Kshitij Bansal, Tim King, Paul Meng
+ **   Kshitij Bansal, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/didyoumean.cpp b/src/options/didyoumean.cpp
index 40836ddd4..3f5278b7e 100644
--- a/src/options/didyoumean.cpp
+++ b/src/options/didyoumean.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Kshitij Bansal, Tim King, Clark Barrett
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/didyoumean.h b/src/options/didyoumean.h
index 712912644..4d7734771 100644
--- a/src/options/didyoumean.h
+++ b/src/options/didyoumean.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Kshitij Bansal, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/didyoumean_test.cpp b/src/options/didyoumean_test.cpp
index 76578b6c4..b01b52777 100644
--- a/src/options/didyoumean_test.cpp
+++ b/src/options/didyoumean_test.cpp
@@ -2,9 +2,9 @@
 /*! \file didyoumean_test.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Kshitij Bansal, Morgan Deters, Paul Meng
+ **   Kshitij Bansal, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/language.cpp b/src/options/language.cpp
index e4f0f58c5..089633519 100644
--- a/src/options/language.cpp
+++ b/src/options/language.cpp
@@ -2,9 +2,9 @@
 /*! \file language.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Paul Meng
+ **   Morgan Deters, Andrew Reynolds, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/language.h b/src/options/language.h
index c573c4aef..87a05a24f 100644
--- a/src/options/language.h
+++ b/src/options/language.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Andrew Reynolds, Francois Bobot
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/module_template.cpp b/src/options/module_template.cpp
index 191833706..636dbe89b 100644
--- a/src/options/module_template.cpp
+++ b/src/options/module_template.cpp
@@ -1,8 +1,8 @@
 /*********************                                                        */
-/*! \file ${filename}$.cpp
+/*! \file module_template.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Mathias Preiner
+ **   Morgan Deters, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
diff --git a/src/options/module_template.h b/src/options/module_template.h
index 47c9ec3fd..00bb74490 100644
--- a/src/options/module_template.h
+++ b/src/options/module_template.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file ${filename}$.h
+/*! \file module_template.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Mathias Preiner
diff --git a/src/options/open_ostream.cpp b/src/options/open_ostream.cpp
index ab3675cda..a05ff63c3 100644
--- a/src/options/open_ostream.cpp
+++ b/src/options/open_ostream.cpp
@@ -2,9 +2,9 @@
 /*! \file open_ostream.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Paul Meng
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/open_ostream.h b/src/options/open_ostream.h
index 9359d5cda..b72c3a400 100644
--- a/src/options/open_ostream.h
+++ b/src/options/open_ostream.h
@@ -2,9 +2,9 @@
 /*! \file open_ostream.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Paul Meng
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/option_exception.h b/src/options/option_exception.h
index 12c69193e..97a9de770 100644
--- a/src/options/option_exception.h
+++ b/src/options/option_exception.h
@@ -2,9 +2,9 @@
 /*! \file option_exception.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Paul Meng, Tim King
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/options.h b/src/options/options.h
index d48f16f66..8ca713642 100644
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Morgan Deters, Paul Meng
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/options_handler.cpp b/src/options/options_handler.cpp
index 270daa13f..0066375a8 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -2,9 +2,9 @@
 /*! \file options_handler.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Andrew Reynolds, Liana Hadarean
+ **   Tim King, Andrew Reynolds, Aina Niemetz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/options_handler.h b/src/options/options_handler.h
index c0ec284c7..ab107ae78 100644
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Andrew Reynolds, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/options_holder_template.h b/src/options/options_holder_template.h
index 910f08e31..438d1c7cc 100644
--- a/src/options/options_holder_template.h
+++ b/src/options/options_holder_template.h
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file options_holder.h
+/*! \file options_holder_template.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Paul Meng
+ **   Morgan Deters, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/options_public_functions.cpp b/src/options/options_public_functions.cpp
index b8db9d9da..d95335c76 100644
--- a/src/options/options_public_functions.cpp
+++ b/src/options/options_public_functions.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Paul Meng
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/options_template.cpp b/src/options/options_template.cpp
index 46f9e0741..d2ccd37ca 100644
--- a/src/options/options_template.cpp
+++ b/src/options/options_template.cpp
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file options.cpp
+/*! \file options_template.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Morgan Deters, Kshitij Bansal
+ **   Morgan Deters, Tim King, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/printer_modes.cpp b/src/options/printer_modes.cpp
index ef4dc6b73..499646bbf 100644
--- a/src/options/printer_modes.cpp
+++ b/src/options/printer_modes.cpp
@@ -2,9 +2,9 @@
 /*! \file printer_modes.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Andrew Reynolds, Paul Meng
+ **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/printer_modes.h b/src/options/printer_modes.h
index db3efe63a..456a7980b 100644
--- a/src/options/printer_modes.h
+++ b/src/options/printer_modes.h
@@ -2,9 +2,9 @@
 /*! \file printer_modes.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds, Morgan Deters, Paul Meng
+ **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/quantifiers_modes.cpp b/src/options/quantifiers_modes.cpp
index 0b89260e9..1814a363d 100644
--- a/src/options/quantifiers_modes.cpp
+++ b/src/options/quantifiers_modes.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/quantifiers_modes.h b/src/options/quantifiers_modes.h
index 47d5ea35a..819e7ae93 100644
--- a/src/options/quantifiers_modes.h
+++ b/src/options/quantifiers_modes.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds, Tim King, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 055dfd545..f04f5abfd 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1502,6 +1502,14 @@ header = "options/quantifiers_options.h"
   help       = "linearize adder chains for variables"
 
 [[option]]
+  name       = "cbqiBvSolveNl"
+  category   = "regular"
+  long       = "cbqi-bv-solve-nl"
+  type       = "bool"
+  default    = "false"
+  help       = "try to solve non-linear bv literals using model value projections"
+
+[[option]]
   name       = "cbqiBvConcInv"
   category   = "regular"
   long       = "cbqi-bv-concat-inv"
diff --git a/src/options/set_language.cpp b/src/options/set_language.cpp
index 18546b2e3..c4690db36 100644
--- a/src/options/set_language.cpp
+++ b/src/options/set_language.cpp
@@ -2,9 +2,9 @@
 /*! \file set_language.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Paul Meng
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/set_language.h b/src/options/set_language.h
index e3db0c461..ca691e9e5 100644
--- a/src/options/set_language.h
+++ b/src/options/set_language.h
@@ -2,9 +2,9 @@
 /*! \file set_language.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Paul Meng
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/simplification_mode.cpp b/src/options/simplification_mode.cpp
index 1a3470b8b..6b6fc842d 100644
--- a/src/options/simplification_mode.cpp
+++ b/src/options/simplification_mode.cpp
@@ -2,9 +2,9 @@
 /*! \file simplification_mode.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Paul Meng, Tim King
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/simplification_mode.h b/src/options/simplification_mode.h
index 4bf9166a4..52bf25fa1 100644
--- a/src/options/simplification_mode.h
+++ b/src/options/simplification_mode.h
@@ -2,9 +2,9 @@
 /*! \file simplification_mode.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Paul Meng, Tim King
+ **   Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/sygus_out_mode.h b/src/options/sygus_out_mode.h
index 9f94be27f..863e4d4bc 100644
--- a/src/options/sygus_out_mode.h
+++ b/src/options/sygus_out_mode.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/theoryof_mode.cpp b/src/options/theoryof_mode.cpp
index 3fe7db532..59919a272 100644
--- a/src/options/theoryof_mode.cpp
+++ b/src/options/theoryof_mode.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Paul Meng
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/theoryof_mode.h b/src/options/theoryof_mode.h
index d1306defd..0dc7194e9 100644
--- a/src/options/theoryof_mode.h
+++ b/src/options/theoryof_mode.h
@@ -2,9 +2,9 @@
 /*! \file theoryof_mode.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Morgan Deters, Paul Meng
+ **   Dejan Jovanovic, Morgan Deters, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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/options/ufss_mode.h b/src/options/ufss_mode.h
index 4cbf18cc0..fa7fad6be 100644
--- a/src/options/ufss_mode.h
+++ b/src/options/ufss_mode.h
@@ -2,9 +2,9 @@
 /*! \file ufss_mode.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Paul Meng
+ **   Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 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