Goodbye CVC4, hello cvc5! (#6371)

This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.

23 files changed, 103 insertions, 164 deletions

diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 2552d455c..a7ca31a7a 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -15,16 +15,16 @@
 
 cmake_minimum_required(VERSION 3.4)
 
-project(cvc4-examples)
+project(cvc5-examples)
 
 set(CMAKE_CXX_STANDARD 11)
 
 enable_testing()
 
-# Find CVC4 package. If CVC4 is not installed into the default system location
+# Find cvc5 package. If cvc5 is not installed into the default system location
 # use `cmake .. -DCMAKE_PREFIX_PATH=path/to/lib/cmake` to specify the location
-# of CVC4Config.cmake.
-find_package(CVC4)
+# of cvc5Config.cmake.
+find_package(cvc5)
 
 # Some of the examples require boost. Enable these examples if boost is
 # installed.
@@ -41,7 +41,7 @@ set(EXAMPLES_BIN_DIR ${CMAKE_BINARY_DIR}/bin)
 #               empty string) for the examples root directory (this)
 # > ARGN: Any additional arguments passed to the macro are interpreted as
 #         as arguments to the test executable.
-macro(cvc4_add_example name src_files output_dir)
+macro(cvc5_add_example name src_files output_dir)
   # The build target is created without the path prefix (not supported),
   # e.g., for '<output_dir>/myexample.cpp'
   #   we create build target 'myexample'
@@ -54,7 +54,7 @@ macro(cvc4_add_example name src_files output_dir)
   endif()
 
   add_executable(${name} ${src_files_list})
-  target_link_libraries(${name} CVC4::cvc4 CVC4::cvc4parser)
+  target_link_libraries(${name} cvc5::cvc5 cvc5::cvc5parser)
 
   # The test target is prefixed with the path,
   # e.g., for '<output_dir>/myexample.cpp'
@@ -71,10 +71,10 @@ macro(cvc4_add_example name src_files output_dir)
   add_test(${example_test} ${example_bin_dir}/${name} ${ARGN})
 endmacro()
 
-cvc4_add_example(simple_vc_cxx "" "")
-cvc4_add_example(simple_vc_quant_cxx "" "")
+cvc5_add_example(simple_vc_cxx "" "")
+cvc5_add_example(simple_vc_quant_cxx "" "")
 # TODO(project issue $206): Port example to new API
-# cvc4_add_example(translator "" ""
+# cvc5_add_example(translator "" ""
 #     # argument to binary (for testing)
 #     ${CMAKE_CURRENT_SOURCE_DIR}/translator-example-input.smt2)
 
@@ -83,12 +83,12 @@ add_subdirectory(api)
 # add_subdirectory(nra-translate)
 # add_subdirectory(sets-translate)
 
-if(TARGET CVC4::cvc4jar)
+if(TARGET cvc5::cvc5jar)
   find_package(Java REQUIRED)
   include(UseJava)
 
   ## disabled until bindings for the new API are in place (issue #2284)
-  # get_target_property(CVC5_JAR CVC4::cvc4jar JAR_FILE)
+  # get_target_property(CVC5_JAR cvc5::cvc5jar JAR_FILE)
   #
   # add_jar(SimpleVC SimpleVC.java INCLUDE_JARS "${CVC5_JAR}")
   #
diff --git a/examples/README.md b/examples/README.md
index 18834719e..8532a6d3c 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -1,6 +1,6 @@
-# CVC4 API Examples
+# cvc5 API Examples
 
-This directory contains usage examples of CVC4's different language
+This directory contains usage examples of cvc5's different language
 bindings, library APIs, and also tutorial examples from the tutorials
 available at http://cvc4.cs.stanford.edu/wiki/Tutorials
 
@@ -21,9 +21,9 @@ The examples provided in this directory are not built by default.
   bin/api/bitvectors
 ```
 
-**Note:** If you installed CVC4 in a non-standard location you have to
+**Note:** If you installed cvc5 in a non-standard location you have to
 additionally specify `CMAKE_PREFIX_PATH` to point to the location of
-`CVC4Config.cmake` (usually `<your-install-prefix>/lib/cmake`) as follows:
+`cvc5Config.cmake` (usually `<your-install-prefix>/lib/cmake`) as follows:
 
 ```
   cmake .. -DCMAKE_PREFIX_PATH=<your-install-prefix>/lib/cmake
@@ -33,7 +33,7 @@ The examples binaries are built into `<build_dir>/bin`.
 
 ## SimpleVC*, simple_vc*
 
-These are examples of how to use CVC4 with each of its library
+These are examples of how to use cvc5 with each of its library
 interfaces (APIs) and language bindings.  They are essentially "hello
 world" examples, and do not fully demonstrate the interfaces, but
 function as a starting point to using simple expressions and solving
diff --git a/examples/SimpleVC.py b/examples/SimpleVC.py
deleted file mode 100644
index 05857e737..000000000
--- a/examples/SimpleVC.py
+++ /dev/null
@@ -1,61 +0,0 @@
-#! /usr/bin/python
-###############################################################################
-# Top contributors (to current version):
-#   Morgan Deters, Aina Niemetz
-#
-# This file is part of the cvc5 project.
-#
-# Copyright (c) 2009-2021 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.
-# #############################################################################
-#
-# A simple demonstration of the Python interface
-#
-# A simple demonstration of the Python interface.  Compare to the
-# C++ interface in simple_vc_cxx.cpp; they are quite similar.
-#
-# To run from a build directory, use something like:
-#
-#   PYTHONPATH=src/bindings/python python ../examples/SimpleVC.py
-##
-
-import CVC4
-from CVC4 import ExprManager, SmtEngine, Rational, Expr
-
-import sys
-
-def main():
-  em = ExprManager()
-  smt = SmtEngine(em)
-
-  # Prove that for integers x and y:
-  #   x > 0 AND y > 0  =>  2x + y >= 3
-
-  integer = em.integerType()
-
-  x = em.mkVar("x", integer)
-  y = em.mkVar("y", integer)
-  zero = em.mkConst(Rational(0))
-
-  x_positive = em.mkExpr(CVC4.GT, x, zero)
-  y_positive = em.mkExpr(CVC4.GT, y, zero)
-
-  two = em.mkConst(Rational(2))
-  twox = em.mkExpr(CVC4.MULT, two, x)
-  twox_plus_y = em.mkExpr(CVC4.PLUS, twox, y)
-
-  three = em.mkConst(Rational(3))
-  twox_plus_y_geq_3 = em.mkExpr(CVC4.GEQ, twox_plus_y, three)
-
-  formula = Expr(em.mkExpr(CVC4.AND, x_positive, y_positive)).impExpr(Expr(twox_plus_y_geq_3))
-
-  print("Checking entailment of formula " + formula.toString() + " with CVC4.")
-  print("CVC4 should report ENTAILED .")
-  print("Result from CVC4 is: " + smt.checkEntailed(formula).toString())
-
-  return 0
-
-if __name__ == '__main__':
-  sys.exit(main())
diff --git a/examples/api/CMakeLists.txt b/examples/api/CMakeLists.txt
index e05039e43..7b713e6e7 100644
--- a/examples/api/CMakeLists.txt
+++ b/examples/api/CMakeLists.txt
@@ -30,5 +30,5 @@ set(CVC5_EXAMPLES_API
 )
 
 foreach(example ${CVC5_EXAMPLES_API})
-  cvc4_add_example(${example} "" "api")
+  cvc5_add_example(${example} "" "api")
 endforeach()
diff --git a/examples/api/java/CMakeLists.txt b/examples/api/java/CMakeLists.txt
index 915ce817c..29ca63b93 100644
--- a/examples/api/java/CMakeLists.txt
+++ b/examples/api/java/CMakeLists.txt
@@ -17,7 +17,7 @@ set(EXAMPLES_API_JAVA
   ## disabled until bindings for the new API are in place (issue #2284)
   # BitVectors
   # BitVectorsAndArrays
-  # CVC4Streams
+  # CVC5Streams
   # Combination
   # Datatypes
   # Exceptions
diff --git a/examples/api/python/bitvectors.py b/examples/api/python/bitvectors.py
index 15973472c..1ddb02d8e 100644
--- a/examples/api/python/bitvectors.py
+++ b/examples/api/python/bitvectors.py
@@ -16,11 +16,11 @@
 # bitvectors-new.cpp.
 ##
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 if __name__ == "__main__":
-    slv = pycvc4.Solver()
+    slv = pycvc5.Solver()
     slv.setLogic("QF_BV") # Set the logic
     # The following example has been adapted from the book A Hacker's Delight by
     # Henry S. Warren.
@@ -38,7 +38,7 @@ if __name__ == "__main__":
     #
     #(2) x = a + b - x;
     #
-    # We will use CVC4 to prove that the three pieces of code above are all
+    # We will use cvc5 to prove that the three pieces of code above are all
     # equivalent by encoding the problem in the bit-vector theory.
 
     # Creating a bit-vector type of width 32
@@ -69,7 +69,7 @@ if __name__ == "__main__":
     assignment0 = slv.mkTerm(kinds.Equal, new_x, ite)
 
     # Assert the encoding of code (0)
-    print("Asserting {} to CVC4".format(assignment0))
+    print("Asserting {} to cvc5".format(assignment0))
     slv.assertFormula(assignment0)
     print("Pushing a new context.")
     slv.push()
@@ -79,14 +79,14 @@ if __name__ == "__main__":
     a_xor_b_xor_x = slv.mkTerm(kinds.BVXor, a, b, x)
     assignment1 = slv.mkTerm(kinds.Equal, new_x_, a_xor_b_xor_x)
 
-    # Assert encoding to CVC4 in current context
-    print("Asserting {} to CVC4".format(assignment1))
+    # Assert encoding to cvc5 in current context
+    print("Asserting {} to cvc5".format(assignment1))
     slv.assertFormula(assignment1)
     new_x_eq_new_x_ = slv.mkTerm(kinds.Equal, new_x, new_x_)
 
     print("Checking entailment assuming:", new_x_eq_new_x_)
     print("Expect ENTAILED.")
-    print("CVC4:", slv.checkEntailed(new_x_eq_new_x_))
+    print("cvc5:", slv.checkEntailed(new_x_eq_new_x_))
     print("Popping context.")
     slv.pop()
 
@@ -96,20 +96,20 @@ if __name__ == "__main__":
     a_plus_b_minus_x = slv.mkTerm(kinds.BVSub, a_plus_b, x)
     assignment2 = slv.mkTerm(kinds.Equal, new_x_, a_plus_b_minus_x)
 
-    # Assert encoding to CVC4 in current context
-    print("Asserting {} to CVC4".format(assignment2))
+    # Assert encoding to cvc5 in current context
+    print("Asserting {} to cvc5".format(assignment2))
     slv.assertFormula(assignment2)
 
     print("Checking entailment assuming:", new_x_eq_new_x_)
     print("Expect ENTAILED.")
-    print("CVC4:", slv.checkEntailed(new_x_eq_new_x_))
+    print("cvc5:", slv.checkEntailed(new_x_eq_new_x_))
 
 
     x_neq_x = slv.mkTerm(kinds.Equal, x, x).notTerm()
     v = [new_x_eq_new_x_, x_neq_x]
     print("Check entailment assuming: ", v)
     print("Expect NOT_ENTAILED.")
-    print("CVC4:", slv.checkEntailed(v))
+    print("cvc5:", slv.checkEntailed(v))
 
     # Assert that a is odd
     extract_op = slv.mkOp(kinds.BVExtract, 0, 0)
@@ -120,4 +120,4 @@ if __name__ == "__main__":
     print("Check satisifiability")
     slv.assertFormula(a_odd)
     print("Expect sat")
-    print("CVC4:", slv.checkSat())
+    print("cvc5:", slv.checkSat())
diff --git a/examples/api/python/bitvectors_and_arrays.py b/examples/api/python/bitvectors_and_arrays.py
index 8f76ac709..be38077ca 100644
--- a/examples/api/python/bitvectors_and_arrays.py
+++ b/examples/api/python/bitvectors_and_arrays.py
@@ -16,13 +16,13 @@
 # translation of bitvectors_and_arrays-new.cpp.
 ##
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 import math
 
 if __name__ == "__main__":
-    slv = pycvc4.Solver()
+    slv = pycvc5.Solver()
     slv.setOption("produce-models", "true")
     slv.setOption("output-language", "smtlib")
     slv.setLogic("QF_AUFBV")
@@ -82,10 +82,10 @@ if __name__ == "__main__":
 
     query = slv.mkTerm(kinds.Not, slv.mkTerm(kinds.And, assertions))
 
-    print("Asserting {} to CVC4".format(query))
+    print("Asserting {} to cvc5".format(query))
     slv.assertFormula(query)
     print("Expect sat.")
-    print("CVC4:", slv.checkSatAssuming(slv.mkTrue()))
+    print("cvc5:", slv.checkSatAssuming(slv.mkTrue()))
 
     # Getting the model
     print("The satisfying model is: ")
diff --git a/examples/api/python/combination.py b/examples/api/python/combination.py
index adeba3a3c..54429feff 100644
--- a/examples/api/python/combination.py
+++ b/examples/api/python/combination.py
@@ -16,8 +16,8 @@
 # combination-new.cpp.
 ##
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 def prefixPrintGetValue(slv, t, level=0):
     print("slv.getValue({}): {}".format(t, slv.getValue(t)))
@@ -25,7 +25,7 @@ def prefixPrintGetValue(slv, t, level=0):
         prefixPrintGetValue(slv, c, level + 1)
 
 if __name__ == "__main__":
-    slv = pycvc4.Solver()
+    slv = pycvc5.Solver()
     slv.setOption("produce-models", "true")  # Produce Models
     slv.setOption("output-language", "cvc") # Set the output-language to CVC's
     slv.setOption("dag-thresh", "0") # Disable dagifying the output
diff --git a/examples/api/python/datatypes.py b/examples/api/python/datatypes.py
index e15fe709c..5b897c1b2 100644
--- a/examples/api/python/datatypes.py
+++ b/examples/api/python/datatypes.py
@@ -16,8 +16,8 @@
 # datatypes-new.cpp.
 ##
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 def test(slv, consListSort):
     # Now our old "consListSpec" is useless--the relevant information
@@ -88,11 +88,11 @@ def test(slv, consListSort):
     print("Assert", assertion)
     slv.assertFormula(assertion)
     print("Expect sat.")
-    print("CVC4:", slv.checkSat())
+    print("cvc5:", slv.checkSat())
 
 
 if __name__ == "__main__":
-    slv = pycvc4.Solver()
+    slv = pycvc5.Solver()
 
     # This example builds a simple "cons list" of integers, with
     # two constructors, "cons" and "nil."
@@ -113,7 +113,7 @@ if __name__ == "__main__":
     print("spec is {}".format(consListSpec))
 
     # Keep in mind that "DatatypeDecl" is the specification class for
-    # datatypes---"DatatypeDecl" is not itself a CVC4 Sort.
+    # datatypes---"DatatypeDecl" is not itself a cvc5 Sort.
     # Now that our Datatype is fully specified, we can get a Sort for it.
     # This step resolves the "SelfSort" reference and creates
     # symbols for all the constructors, etc.
diff --git a/examples/api/python/exceptions.py b/examples/api/python/exceptions.py
index c779390d9..a4597d12b 100644
--- a/examples/api/python/exceptions.py
+++ b/examples/api/python/exceptions.py
@@ -16,13 +16,13 @@
 # A simple demonstration of catching cvc5 exceptions with the legacy Python API.
 ##
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 import sys
 
 
 def main():
-    slv = pycvc4.Solver()
+    slv = pycvc5.Solver()
 
     slv.setOption("produce-models", "true")
 
diff --git a/examples/api/python/extract.py b/examples/api/python/extract.py
index d708a7045..4e7026e97 100644
--- a/examples/api/python/extract.py
+++ b/examples/api/python/extract.py
@@ -16,8 +16,8 @@
 # extract-new.cpp.
 ##
 
-from pycvc4 import Solver
-from pycvc4.kinds import BVExtract, Equal
+from pycvc5 import Solver
+from pycvc5.kinds import BVExtract, Equal
 
 if __name__ == "__main__":
     slv = Solver()
@@ -49,4 +49,4 @@ if __name__ == "__main__":
     eq2 = slv.mkTerm(Equal, x_31_31, x_0_0)
     print("Check entailment assuming:", eq2)
     print("Expect ENTAILED")
-    print("CVC4:", slv.checkEntailed(eq2))
+    print("cvc5:", slv.checkEntailed(eq2))
diff --git a/examples/api/python/floating_point.py b/examples/api/python/floating_point.py
index 5444a7df3..44a3d66d2 100644
--- a/examples/api/python/floating_point.py
+++ b/examples/api/python/floating_point.py
@@ -16,16 +16,16 @@
 # Darulova. This requires building cvc5 with symfpu.
 ##
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 if __name__ == "__main__":
-    slv = pycvc4.Solver()
+    slv = pycvc5.Solver()
 
     if not slv.supportsFloatingPoint():
-        # CVC4 must be built with SymFPU to support the theory of
+        # cvc5 must be built with SymFPU to support the theory of
         # floating-point numbers
-        print("CVC4 was not built with floating-point support.")
+        print("cvc5 was not built with floating-point support.")
         exit()
 
     slv.setOption("produce-models", "true")
@@ -35,7 +35,7 @@ if __name__ == "__main__":
     fp32 = slv.mkFloatingPointSort(8, 24)
 
     # the standard rounding mode
-    rm = slv.mkRoundingMode(pycvc4.RoundNearestTiesToEven)
+    rm = slv.mkRoundingMode(pycvc5.RoundNearestTiesToEven)
 
     # create a few single-precision variables
     x = slv.mkConst(fp32, 'x')
@@ -49,7 +49,7 @@ if __name__ == "__main__":
     slv.assertFormula(slv.mkTerm(kinds.Not, commutative))
     print("Checking floating-point commutativity")
     print("Expect SAT (property does not hold for NaN and Infinities).")
-    print("CVC4:", slv.checkSat())
+    print("cvc5:", slv.checkSat())
     print("Model for x:", slv.getValue(x))
     print("Model for y:", slv.getValue(y))
 
@@ -61,7 +61,7 @@ if __name__ == "__main__":
 
     print("Checking floating-point commutativity assuming x and y are not NaN or Infinity")
     print("Expect UNSAT.")
-    print("CVC4:", slv.checkSat())
+    print("cvc5:", slv.checkSat())
 
     # check floating-point arithmetic is not associative
     slv.pop()
@@ -84,7 +84,7 @@ if __name__ == "__main__":
 
     print("Checking floating-point associativity")
     print("Expect SAT.")
-    print("CVC4:", slv.checkSat())
+    print("cvc5:", slv.checkSat())
     print("Model for x:", slv.getValue(x))
     print("Model for y:", slv.getValue(y))
     print("Model for z:", slv.getValue(z))
diff --git a/examples/api/python/helloworld.py b/examples/api/python/helloworld.py
index 8e585073c..6e6ce32ab 100644
--- a/examples/api/python/helloworld.py
+++ b/examples/api/python/helloworld.py
@@ -14,10 +14,10 @@
 # A very simple example, adapted from helloworld-new.cpp
 ##
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 if __name__ == "__main__":
-    slv = pycvc4.Solver()
+    slv = pycvc5.Solver()
     helloworld = slv.mkConst(slv.getBooleanSort(), "Hello World!")
     print(helloworld, "is", slv.checkEntailed(helloworld))
diff --git a/examples/api/python/linear_arith.py b/examples/api/python/linear_arith.py
index bc48b452e..f8dad6a71 100644
--- a/examples/api/python/linear_arith.py
+++ b/examples/api/python/linear_arith.py
@@ -16,11 +16,11 @@
 # linear_arith-new.cpp.
 ##
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 if __name__ == "__main__":
-    slv = pycvc4.Solver()
+    slv = pycvc5.Solver()
     slv.setLogic("QF_LIRA")
 
     # Prove that if given x (Integer) and y (Real) and some constraints
@@ -55,9 +55,9 @@ if __name__ == "__main__":
 
     slv.push()
     diff_leq_two_thirds = slv.mkTerm(kinds.Leq, diff, two_thirds)
-    print("Prove that", diff_leq_two_thirds, "with CVC4")
-    print("CVC4 should report ENTAILED")
-    print("Result from CVC4 is:",
+    print("Prove that", diff_leq_two_thirds, "with cvc5")
+    print("cvc5 should report ENTAILED")
+    print("Result from cvc5 is:",
           slv.checkEntailed(diff_leq_two_thirds))
     slv.pop()
 
@@ -66,7 +66,7 @@ if __name__ == "__main__":
     slv.push()
     diff_is_two_thirds = slv.mkTerm(kinds.Equal, diff, two_thirds)
     slv.assertFormula(diff_is_two_thirds)
-    print("Show that the assertions are consistent with\n", diff_is_two_thirds, "with CVC4")
-    print("CVC4 should report SAT")
-    print("Result from CVC4 is:", slv.checkSat())
+    print("Show that the assertions are consistent with\n", diff_is_two_thirds, "with cvc5")
+    print("cvc5 should report SAT")
+    print("Result from cvc5 is:", slv.checkSat())
     slv.pop()
diff --git a/examples/api/python/sequences.py b/examples/api/python/sequences.py
index fa8c1bc4f..f9fd925fb 100644
--- a/examples/api/python/sequences.py
+++ b/examples/api/python/sequences.py
@@ -15,11 +15,11 @@
 # through the Python API. This is a direct translation of sequences.cpp.
 ##
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 if __name__ == "__main__":
-    slv = pycvc4.Solver()
+    slv = pycvc5.Solver()
     # Set the logic
     slv.setLogic("QF_SLIA")
     # Produce models
@@ -54,7 +54,7 @@ if __name__ == "__main__":
 
     # Check satisfiability
     result = slv.checkSatAssuming(q)
-    print("CVC4 reports:", q, "is", result)
+    print("cvc5 reports:", q, "is", result)
 
     if result:
         print("x = {}".format(slv.getValue(x)))
diff --git a/examples/api/python/sets.py b/examples/api/python/sets.py
index 01c14cb87..b41b2ad5a 100644
--- a/examples/api/python/sets.py
+++ b/examples/api/python/sets.py
@@ -15,11 +15,11 @@
 # through the Python API. This is a direct translation of sets-new.cpp.
 ##
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 if __name__ == "__main__":
-    slv = pycvc4.Solver()
+    slv = pycvc5.Solver()
 
     # Optionally, set the logic. We need at least UF for equality predicate,
     # integers (LIA) and sets (FS).
@@ -48,7 +48,7 @@ if __name__ == "__main__":
 
     theorem = slv.mkTerm(kinds.Equal, lhs, rhs)
 
-    print("CVC4 reports: {} is {}".format(theorem,
+    print("cvc5 reports: {} is {}".format(theorem,
                                           slv.checkEntailed(theorem)))
 
     # Verify emptset is a subset of any set
@@ -58,7 +58,7 @@ if __name__ == "__main__":
 
     theorem = slv.mkTerm(kinds.Subset, emptyset, A)
 
-    print("CVC4 reports: {} is {}".format(theorem,
+    print("cvc5 reports: {} is {}".format(theorem,
                                           slv.checkEntailed(theorem)))
 
     # Find me an element in 1, 2 intersection 2, 3, if there is one.
@@ -80,7 +80,7 @@ if __name__ == "__main__":
 
     result = slv.checkSatAssuming(e)
 
-    print("CVC4 reports: {} is {}".format(e, result))
+    print("cvc5 reports: {} is {}".format(e, result))
 
     if result:
         print("For instance, {} is a member".format(slv.getValue(x)))
diff --git a/examples/api/python/strings.py b/examples/api/python/strings.py
index aa540f89c..64ce06548 100644
--- a/examples/api/python/strings.py
+++ b/examples/api/python/strings.py
@@ -15,11 +15,11 @@
 # through the Python API. This is a direct translation of strings-new.cpp.
 ##
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 if __name__ == "__main__":
-    slv = pycvc4.Solver()
+    slv = pycvc5.Solver()
     # Set the logic
     slv.setLogic("QF_SLIA")
     # Produce models
@@ -81,7 +81,7 @@ if __name__ == "__main__":
 
     # check sat
     result = slv.checkSatAssuming(q)
-    print("CVC4 reports:", q, "is", result)
+    print("cvc5 reports:", q, "is", result)
 
     if result:
         print("x = ", slv.getValue(x))
diff --git a/examples/api/python/sygus-fun.py b/examples/api/python/sygus-fun.py
index 8c490f47e..6e1440d66 100644
--- a/examples/api/python/sygus-fun.py
+++ b/examples/api/python/sygus-fun.py
@@ -16,11 +16,11 @@
 ##
 
 import copy
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 if __name__ == "__main__":
-  slv = pycvc4.Solver()
+  slv = pycvc5.Solver()
 
   # required options
   slv.setOption("lang", "sygus2")
diff --git a/examples/api/python/sygus-grammar.py b/examples/api/python/sygus-grammar.py
index 0bcc0815d..406646f9f 100644
--- a/examples/api/python/sygus-grammar.py
+++ b/examples/api/python/sygus-grammar.py
@@ -17,11 +17,11 @@
 ##
 
 import copy
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 if __name__ == "__main__":
-  slv = pycvc4.Solver()
+  slv = pycvc5.Solver()
 
   # required options
   slv.setOption("lang", "sygus2")
diff --git a/examples/api/python/sygus-inv.py b/examples/api/python/sygus-inv.py
index 08a50ce63..0fa752b1e 100644
--- a/examples/api/python/sygus-inv.py
+++ b/examples/api/python/sygus-inv.py
@@ -16,11 +16,11 @@
 # translation of sygus-inv.cpp .
 ##
 
-import pycvc4
-from pycvc4 import kinds
+import pycvc5
+from pycvc5 import kinds
 
 if __name__ == "__main__":
-  slv = pycvc4.Solver()
+  slv = pycvc5.Solver()
 
   # required options
   slv.setOption("lang", "sygus2")
diff --git a/examples/nra-translate/CMakeLists.txt b/examples/nra-translate/CMakeLists.txt
index 94af86090..dda47206e 100644
--- a/examples/nra-translate/CMakeLists.txt
+++ b/examples/nra-translate/CMakeLists.txt
@@ -26,7 +26,7 @@ set(CVC5_EXAMPLES_NRA_TRANSLATE
 )
 
 foreach(example ${CVC5_EXAMPLES_NRA_TRANSLATE})
-  cvc4_add_example(${example} "" "nra-translate"
+  cvc5_add_example(${example} "" "nra-translate"
     # arguments to binary (for testing)
     # input file is required by all tests
     ${CMAKE_CURRENT_SOURCE_DIR}/nra-translate-example-input.smt2
diff --git a/examples/sets-translate/CMakeLists.txt b/examples/sets-translate/CMakeLists.txt
index b5b78d63e..d1a8650ce 100644
--- a/examples/sets-translate/CMakeLists.txt
+++ b/examples/sets-translate/CMakeLists.txt
@@ -14,12 +14,12 @@
 ##
 
 if(Boost_FOUND)
-  cvc4_add_example(sets2arrays
+  cvc5_add_example(sets2arrays
     "sets_translate.cpp" "sets-translate"
     # argument to binary (for testing)
     ${CMAKE_CURRENT_SOURCE_DIR}/sets-translate-example-input.smt2)
 
-  cvc4_add_example(sets2axioms
+  cvc5_add_example(sets2axioms
     "sets_translate.cpp" "sets-translate"
     # argument to binary (for testing)
     ${CMAKE_CURRENT_SOURCE_DIR}/sets-translate-example-input.smt2)
diff --git a/examples/simple_vc_quant_cxx.cpp b/examples/simple_vc_quant_cxx.cpp
index 9ef48bf76..1bdadfca2 100644
--- a/examples/simple_vc_quant_cxx.cpp
+++ b/examples/simple_vc_quant_cxx.cpp
@@ -48,10 +48,10 @@ int main() {
 
   slv.assertFormula(formula);
 
-  std::cout << "Checking SAT after asserting " << formula << " to CVC4."
+  std::cout << "Checking SAT after asserting " << formula << " to cvc5."
             << std::endl;
-  std::cout << "CVC4 should report unsat." << std::endl;
-  std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl;
+  std::cout << "cvc5 should report unsat." << std::endl;
+  std::cout << "Result from cvc5 is: " << slv.checkSat() << std::endl;
 
   slv.resetAssertions();
 
@@ -66,10 +66,10 @@ int main() {
 
   slv.assertFormula(formula_pattern);
 
-  std::cout << "Checking SAT after asserting " << formula_pattern << " to CVC4."
+  std::cout << "Checking SAT after asserting " << formula_pattern << " to cvc5."
             << std::endl;
-  std::cout << "CVC4 should report unsat." << std::endl;
-  std::cout << "Result from CVC4 is: " << slv.checkSat() << std::endl;
+  std::cout << "cvc5 should report unsat." << std::endl;
+  std::cout << "Result from cvc5 is: " << slv.checkSat() << std::endl;
 
   return 0;
 }