mergecav2019strings_countRewRed

44 files changed, 118 insertions, 110 deletions

diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java
index 50f226ed6..125b4f848 100644
--- a/examples/SimpleVC.java
+++ b/examples/SimpleVC.java
@@ -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
diff --git a/examples/api/bitvectors-new.cpp b/examples/api/bitvectors-new.cpp
index 7070f6748..d0c26f134 100644
--- a/examples/api/bitvectors-new.cpp
+++ b/examples/api/bitvectors-new.cpp
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file bitvectors.cpp
+/*! \file bitvectors-new.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Liana Hadarean, Morgan Deters
+ **   Aina Niemetz, Makai Mann
  ** 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,7 +16,7 @@
 
 #include <iostream>
 
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
 #include "api/cvc4cpp.h"
 
 using namespace std;
@@ -50,9 +50,9 @@ int main()
   Sort bitvector32 = slv.mkBitVectorSort(32);
 
   // Variables
-  Term x = slv.mkVar("x", bitvector32);
-  Term a = slv.mkVar("a", bitvector32);
-  Term b = slv.mkVar("b", bitvector32);
+  Term x = slv.mkConst(bitvector32, "x");
+  Term a = slv.mkConst(bitvector32, "a");
+  Term b = slv.mkConst(bitvector32, "b");
 
   // First encode the assumption that x must be equal to a or b
   Term x_eq_a = slv.mkTerm(EQUAL, x, a);
@@ -63,9 +63,9 @@ int main()
   slv.assertFormula(assumption);
 
   // Introduce a new variable for the new value of x after assignment.
-  Term new_x = slv.mkVar("new_x", bitvector32);  // x after executing code (0)
+  Term new_x = slv.mkConst(bitvector32, "new_x");  // x after executing code (0)
   Term new_x_ =
-      slv.mkVar("new_x_", bitvector32);  // x after executing code (1) or (2)
+      slv.mkConst(bitvector32, "new_x_");  // x after executing code (1) or (2)
 
   // Encoding code (0)
   // new_x = x == a ? b : a;
diff --git a/examples/api/bitvectors.cpp b/examples/api/bitvectors.cpp
index e058dcef8..59257976d 100644
--- a/examples/api/bitvectors.cpp
+++ b/examples/api/bitvectors.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Liana Hadarean, 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/examples/api/bitvectors_and_arrays-new.cpp b/examples/api/bitvectors_and_arrays-new.cpp
index 3d4e6bca0..955a83cff 100644
--- a/examples/api/bitvectors_and_arrays-new.cpp
+++ b/examples/api/bitvectors_and_arrays-new.cpp
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file bitvectors_and_arrays.cpp
+/*! \file bitvectors_and_arrays-new.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Aina Niemetz, Morgan Deters
+ **   Aina Niemetz, Makai Mann
  ** 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,7 +16,8 @@
 
 #include <iostream>
 #include <cmath>
-// #include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+
+// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
 #include "api/cvc4cpp.h"
 
 using namespace std;
@@ -52,7 +53,7 @@ int main()
   Sort arraySort = slv.mkArraySort(indexSort, elementSort);
 
   // Variables
-  Term current_array = slv.mkVar("current_array", arraySort);
+  Term current_array = slv.mkConst(arraySort, "current_array");
 
   // Making a bit-vector constant
   Term zero = slv.mkBitVector(index_size, 0u);
diff --git a/examples/api/bitvectors_and_arrays.cpp b/examples/api/bitvectors_and_arrays.cpp
index e6af948b9..983da71db 100644
--- a/examples/api/bitvectors_and_arrays.cpp
+++ b/examples/api/bitvectors_and_arrays.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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/examples/api/combination-new.cpp b/examples/api/combination-new.cpp
index 8c968c95e..e78e8919f 100644
--- a/examples/api/combination-new.cpp
+++ b/examples/api/combination-new.cpp
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file combination.cpp
+/*! \file combination-new.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Tim King
+ **   Aina Niemetz, Makai Mann
  ** 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,7 +18,7 @@
 
 #include <iostream>
 
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
 #include "api/cvc4cpp.h"
 
 using namespace std;
@@ -51,12 +51,12 @@ int main()
   Sort intPred = slv.mkFunctionSort(integer, boolean);
 
   // Variables
-  Term x = slv.mkVar("x", u);
-  Term y = slv.mkVar("y", u);
+  Term x = slv.mkConst(u, "x");
+  Term y = slv.mkConst(u, "y");
 
   // Functions
-  Term f = slv.mkVar("f", uToInt);
-  Term p = slv.mkVar("p", intPred);
+  Term f = slv.mkConst(uToInt, "f");
+  Term p = slv.mkConst(intPred, "p");
 
   // Constants
   Term zero = slv.mkReal(0);
diff --git a/examples/api/combination.cpp b/examples/api/combination.cpp
index 67371e4c2..0d8ae0494 100644
--- a/examples/api/combination.cpp
+++ b/examples/api/combination.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Makai Mann
  ** 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/examples/api/datatypes-new.cpp b/examples/api/datatypes-new.cpp
index 14ddcd383..08918fc87 100644
--- a/examples/api/datatypes-new.cpp
+++ b/examples/api/datatypes-new.cpp
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file datatypes.cpp
+/*! \file datatypes-new.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Morgan Deters, Tim King
+ **   Aina Niemetz, Makai Mann
  ** 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,9 +15,10 @@
  **/
 
 #include <iostream>
-//#include <cvc4/cvc4.h> // To follow the wiki
 
+// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
 #include "api/cvc4cpp.h"
+
 using namespace CVC4::api;
 
 void test(Solver& slv, Sort& consListSort)
@@ -115,7 +116,7 @@ void test(Solver& slv, Sort& consListSort)
     }
   }
 
-  Term a = slv.declareFun("a", paramConsIntListSort);
+  Term a = slv.mkConst(paramConsIntListSort, "a");
   std::cout << "term " << a << " is of sort " << a.getSort() << std::endl;
 
   Term head_a = slv.mkTerm(
diff --git a/examples/api/datatypes.cpp b/examples/api/datatypes.cpp
index 200f1bb2c..3bf1df12f 100644
--- a/examples/api/datatypes.cpp
+++ b/examples/api/datatypes.cpp
@@ -2,9 +2,9 @@
 /*! \file datatypes.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Aina Niemetz, Tim King
+ **   Morgan Deters, 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/examples/api/extract-new.cpp b/examples/api/extract-new.cpp
index 96961458e..cb7d96fa5 100644
--- a/examples/api/extract-new.cpp
+++ b/examples/api/extract-new.cpp
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file extract.cpp
+/*! \file extract-new.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Clark Barrett, Aina Niemetz
+ **   Aina Niemetz, Makai Mann
  ** 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,7 +16,7 @@
 
 #include <iostream>
 
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
 #include "api/cvc4cpp.h"
 
 using namespace std;
@@ -29,7 +29,7 @@ int main()
 
   Sort bitvector32 = slv.mkBitVectorSort(32);
 
-  Term x = slv.mkVar("a", bitvector32);
+  Term x = slv.mkConst(bitvector32, "a");
 
   OpTerm ext_31_1 = slv.mkOpTerm(BITVECTOR_EXTRACT_OP, 31, 1);
   Term x_31_1 = slv.mkTerm(BITVECTOR_EXTRACT, ext_31_1, x);
diff --git a/examples/api/extract.cpp b/examples/api/extract.cpp
index 5aed0168c..c9240363e 100644
--- a/examples/api/extract.cpp
+++ b/examples/api/extract.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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/examples/api/helloworld-new.cpp b/examples/api/helloworld-new.cpp
index 484995143..a7fbe22e9 100644
--- a/examples/api/helloworld-new.cpp
+++ b/examples/api/helloworld-new.cpp
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file helloworld.cpp
+/*! \file helloworld-new.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Tim King, Kshitij Bansal
+ **   Aina Niemetz, Makai Mann
  ** 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,7 +16,7 @@
 
 #include <iostream>
 
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
 #include "api/cvc4cpp.h"
 
 using namespace CVC4::api;
@@ -24,7 +24,7 @@ using namespace CVC4::api;
 int main()
 {
   Solver slv;
-  Term helloworld = slv.mkVar("Hello World!", slv.getBooleanSort());
+  Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!");
   std::cout << helloworld << " is " << slv.checkValidAssuming(helloworld)
             << std::endl;
   return 0;
diff --git a/examples/api/helloworld.cpp b/examples/api/helloworld.cpp
index 667faed50..1235c4c55 100644
--- a/examples/api/helloworld.cpp
+++ b/examples/api/helloworld.cpp
@@ -2,9 +2,9 @@
 /*! \file helloworld.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Kshitij Bansal
+ **   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
diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java
index 2f5188bba..fec871357 100644
--- a/examples/api/java/BitVectors.java
+++ b/examples/api/java/BitVectors.java
@@ -2,9 +2,9 @@
 /*! \file BitVectors.java
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters
+ **   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
diff --git a/examples/api/java/BitVectorsAndArrays.java b/examples/api/java/BitVectorsAndArrays.java
index d92cba79a..11474d1e1 100644
--- a/examples/api/java/BitVectorsAndArrays.java
+++ b/examples/api/java/BitVectorsAndArrays.java
@@ -2,9 +2,9 @@
 /*! \file BitVectorsAndArrays.java
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters
+ **   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
diff --git a/examples/api/java/CVC4Streams.java b/examples/api/java/CVC4Streams.java
index 96a9e8aed..8e395b512 100644
--- a/examples/api/java/CVC4Streams.java
+++ b/examples/api/java/CVC4Streams.java
@@ -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
diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java
index 55743c62b..6d34e16c4 100644
--- a/examples/api/java/Combination.java
+++ b/examples/api/java/Combination.java
@@ -2,9 +2,9 @@
 /*! \file Combination.java
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters
+ **   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/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java
index 376d038d8..2c79bb75f 100644
--- a/examples/api/java/Datatypes.java
+++ b/examples/api/java/Datatypes.java
@@ -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
diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java
index 07ae34a3d..56acffa76 100644
--- a/examples/api/java/HelloWorld.java
+++ b/examples/api/java/HelloWorld.java
@@ -2,7 +2,13 @@
 /*! \file HelloWorld.java
  ** \verbatim
  ** Top contributors (to current version):
- **   
+ **   Morgan Deters, Tim King
+ ** This file is part of the CVC4 project.
+ ** 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
+ **
  ** 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/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java
index eab17ea43..368178155 100644
--- a/examples/api/java/LinearArith.java
+++ b/examples/api/java/LinearArith.java
@@ -2,9 +2,9 @@
 /*! \file LinearArith.java
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters
+ **   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/examples/api/java/PipedInput.java b/examples/api/java/PipedInput.java
index f19636f78..13883d033 100644
--- a/examples/api/java/PipedInput.java
+++ b/examples/api/java/PipedInput.java
@@ -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
diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java
index dd5d2938b..fe017980b 100644
--- a/examples/api/java/Strings.java
+++ b/examples/api/java/Strings.java
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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
diff --git a/examples/api/linear_arith-new.cpp b/examples/api/linear_arith-new.cpp
index d643b85bc..2edcaf71e 100644
--- a/examples/api/linear_arith-new.cpp
+++ b/examples/api/linear_arith-new.cpp
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file linear_arith.cpp
+/*! \file linear_arith-new.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Aina Niemetz
+ **   Aina Niemetz, Makai Mann
  ** 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,7 +17,7 @@
 
 #include <iostream>
 
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
 #include "api/cvc4cpp.h"
 
 using namespace std;
@@ -36,8 +36,8 @@ int main()
   Sort integer = slv.getIntegerSort();
 
   // Variables
-  Term x = slv.mkVar("x", integer);
-  Term y = slv.mkVar("y", real);
+  Term x = slv.mkConst(integer, "x");
+  Term y = slv.mkConst(real, "y");
 
   // Constants
   Term three = slv.mkReal(3);
diff --git a/examples/api/linear_arith.cpp b/examples/api/linear_arith.cpp
index 3a3dd9aa0..83a0064c9 100644
--- a/examples/api/linear_arith.cpp
+++ b/examples/api/linear_arith.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/examples/api/sets-new.cpp b/examples/api/sets-new.cpp
index 2dcfbbc02..60df7a82f 100644
--- a/examples/api/sets-new.cpp
+++ b/examples/api/sets-new.cpp
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file sets.cpp
+/*! \file sets-new.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Aina Niemetz, Kshitij Bansal
+ **   Aina Niemetz, Makai Mann
  ** 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,7 +16,7 @@
 
 #include <iostream>
 
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
 #include "api/cvc4cpp.h"
 
 using namespace std;
@@ -40,9 +40,9 @@ int main()
   // Verify union distributions over intersection
   // (A union B) intersection C = (A intersection C) union (B intersection C)
   {
-    Term A = slv.mkVar("A", set);
-    Term B = slv.mkVar("B", set);
-    Term C = slv.mkVar("C", set);
+    Term A = slv.mkConst(set, "A");
+    Term B = slv.mkConst(set, "B");
+    Term C = slv.mkConst(set, "C");
 
     Term unionAB = slv.mkTerm(UNION, A, B);
     Term lhs = slv.mkTerm(INTERSECTION, unionAB, C);
@@ -59,7 +59,7 @@ int main()
 
   // Verify emptset is a subset of any set
   {
-    Term A = slv.mkVar("A", set);
+    Term A = slv.mkConst(set, "A");
     Term emptyset = slv.mkEmptySet(set);
 
     Term theorem = slv.mkTerm(SUBSET, emptyset, A);
@@ -81,7 +81,7 @@ int main()
     Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three);
     Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three);
 
-    Term x = slv.mkVar("x", integer);
+    Term x = slv.mkConst(integer, "x");
 
     Term e = slv.mkTerm(MEMBER, x, intersection);
 
diff --git a/examples/api/sets.cpp b/examples/api/sets.cpp
index 17a93a905..3110c01e3 100644
--- a/examples/api/sets.cpp
+++ b/examples/api/sets.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Kshitij Bansal, 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/examples/api/strings-new.cpp b/examples/api/strings-new.cpp
index c88ccc9c0..42630dc0e 100644
--- a/examples/api/strings-new.cpp
+++ b/examples/api/strings-new.cpp
@@ -1,10 +1,10 @@
 /*********************                                                        */
-/*! \file strings.cpp
+/*! \file strings-new.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Clark Barrett, Paul Meng, Tim King
+ **   Aina Niemetz, Makai Mann
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 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,7 +16,7 @@
 
 #include <iostream>
 
-//#include <cvc4/cvc4.h> // use this after CVC4 is properly installed
+// #include "cvc4/api/cvc4cpp.h" // use this after CVC4 is properly installed
 #include "api/cvc4cpp.h"
 
 using namespace CVC4::api;
@@ -43,9 +43,9 @@ int main()
   Term ab  = slv.mkString(str_ab);
   Term abc = slv.mkString("abc");
   // String variables
-  Term x = slv.mkVar("x", string);
-  Term y = slv.mkVar("y", string);
-  Term z = slv.mkVar("z", string);
+  Term x = slv.mkConst(string, "x");
+  Term y = slv.mkConst(string, "y");
+  Term z = slv.mkConst(string, "z");
 
   // String concatenation: x.ab.y
   Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y);
@@ -70,8 +70,8 @@ int main()
     slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h")));
 
   // String variables
-  Term s1 = slv.mkVar("s1", string);
-  Term s2 = slv.mkVar("s2", string);
+  Term s1 = slv.mkConst(string, "s1");
+  Term s2 = slv.mkConst(string, "s2");
   // String concatenation: s1.s2
   Term s = slv.mkTerm(STRING_CONCAT, s1, s2);
 
diff --git a/examples/api/strings.cpp b/examples/api/strings.cpp
index 02e11d672..96f4dd400 100644
--- a/examples/api/strings.cpp
+++ b/examples/api/strings.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tianyi Liang, 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/examples/hashsmt/sha1.hpp b/examples/hashsmt/sha1.hpp
index 4e7f60e39..a09da39c4 100644
--- a/examples/hashsmt/sha1.hpp
+++ b/examples/hashsmt/sha1.hpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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
diff --git a/examples/hashsmt/sha1_collision.cpp b/examples/hashsmt/sha1_collision.cpp
index 2193c7b68..e26b2623b 100644
--- a/examples/hashsmt/sha1_collision.cpp
+++ b/examples/hashsmt/sha1_collision.cpp
@@ -2,9 +2,9 @@
 /*! \file sha1_collision.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King
+ **   Dejan Jovanovic, Aina Niemetz, 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/examples/hashsmt/sha1_inversion.cpp b/examples/hashsmt/sha1_inversion.cpp
index ef5191cb7..667c3c4e0 100644
--- a/examples/hashsmt/sha1_inversion.cpp
+++ b/examples/hashsmt/sha1_inversion.cpp
@@ -2,9 +2,9 @@
 /*! \file sha1_inversion.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Andres Noetzli
+ **   Dejan Jovanovic, 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
diff --git a/examples/hashsmt/word.cpp b/examples/hashsmt/word.cpp
index f067ef57b..189eaf485 100644
--- a/examples/hashsmt/word.cpp
+++ b/examples/hashsmt/word.cpp
@@ -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
diff --git a/examples/hashsmt/word.h b/examples/hashsmt/word.h
index 223a5b5d5..cbe53d549 100644
--- a/examples/hashsmt/word.h
+++ b/examples/hashsmt/word.h
@@ -2,9 +2,9 @@
 /*! \file word.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, 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/examples/nra-translate/normalize.cpp b/examples/nra-translate/normalize.cpp
index a6c146622..3ca09c5bf 100644
--- a/examples/nra-translate/normalize.cpp
+++ b/examples/nra-translate/normalize.cpp
@@ -2,9 +2,9 @@
 /*! \file normalize.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Aina Niemetz
+ **   Dejan Jovanovic, Aina Niemetz, 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/examples/nra-translate/smt2info.cpp b/examples/nra-translate/smt2info.cpp
index 55ddb0997..513b52a39 100644
--- a/examples/nra-translate/smt2info.cpp
+++ b/examples/nra-translate/smt2info.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Dejan Jovanovic, Aina Niemetz, 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/examples/nra-translate/smt2todreal.cpp b/examples/nra-translate/smt2todreal.cpp
index 04a33624c..11f5ad4f8 100644
--- a/examples/nra-translate/smt2todreal.cpp
+++ b/examples/nra-translate/smt2todreal.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Dejan Jovanovic, 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
diff --git a/examples/nra-translate/smt2toisat.cpp b/examples/nra-translate/smt2toisat.cpp
index c4649dcae..5992cd0dc 100644
--- a/examples/nra-translate/smt2toisat.cpp
+++ b/examples/nra-translate/smt2toisat.cpp
@@ -2,9 +2,9 @@
 /*! \file smt2toisat.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Aina Niemetz
+ **   Dejan Jovanovic, Andrew Reynolds, 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/examples/nra-translate/smt2tomathematica.cpp b/examples/nra-translate/smt2tomathematica.cpp
index fd344caa9..8f0764e92 100644
--- a/examples/nra-translate/smt2tomathematica.cpp
+++ b/examples/nra-translate/smt2tomathematica.cpp
@@ -2,9 +2,9 @@
 /*! \file smt2tomathematica.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Andrew Reynolds
+ **   Dejan Jovanovic, Andrew Reynolds, 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/examples/nra-translate/smt2toqepcad.cpp b/examples/nra-translate/smt2toqepcad.cpp
index acfd6bf97..28e699b6f 100644
--- a/examples/nra-translate/smt2toqepcad.cpp
+++ b/examples/nra-translate/smt2toqepcad.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Dejan Jovanovic, 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
diff --git a/examples/nra-translate/smt2toredlog.cpp b/examples/nra-translate/smt2toredlog.cpp
index feb5a583a..0629b5d1c 100644
--- a/examples/nra-translate/smt2toredlog.cpp
+++ b/examples/nra-translate/smt2toredlog.cpp
@@ -2,9 +2,9 @@
 /*! \file smt2toredlog.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Dejan Jovanovic, Tim King, Aina Niemetz
+ **   Dejan Jovanovic, Andrew Reynolds, 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/examples/sets-translate/sets_translate.cpp b/examples/sets-translate/sets_translate.cpp
index 7a1990545..f7513a401 100644
--- a/examples/sets-translate/sets_translate.cpp
+++ b/examples/sets-translate/sets_translate.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Kshitij Bansal, 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
@@ -204,7 +204,7 @@ class Mapper {
     } else {
       vector<Expr> children = e.getChildren();
       children.insert(children.begin(), setoperators[ make_pair(t, e.getKind()) ]);
-      ret = em->mkExpr(kind::APPLY, children);
+      ret = em->mkExpr(kind::APPLY_UF, children);
     }
     // cout << "returning " << ret  << endl;
     return ret;
diff --git a/examples/simple_vc_cxx.cpp b/examples/simple_vc_cxx.cpp
index d6b6212c0..ad18ae5b7 100644
--- a/examples/simple_vc_cxx.cpp
+++ b/examples/simple_vc_cxx.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   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/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp
index 4821e1464..a8bbfe29a 100644
--- a/examples/simple_vc_quant_cxx.cpp
+++ b/examples/simple_vc_quant_cxx.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/examples/translator.cpp b/examples/translator.cpp
index 5be837e63..82a206d4b 100644
--- a/examples/translator.cpp
+++ b/examples/translator.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, 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