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/.

38 files changed, 47 insertions, 1375 deletions

diff --git a/contrib/README b/contrib/README
index 47d4941bd..9b3ef11a0 100644
--- a/contrib/README
+++ b/contrib/README
@@ -1,4 +1,4 @@
-This directory is for contributions to CVC4 that aren't directly
+This directory is for contributions to cvc5 that aren't directly
 part of the main project.
 
 -- Morgan Deters <mdeters@cs.nyu.edu>  Mon, 09 Nov 2009 15:14:41 -0500
diff --git a/contrib/alttheoryskel/README.WHATS-NEXT b/contrib/alttheoryskel/README.WHATS-NEXT
deleted file mode 100644
index c0237c300..000000000
--- a/contrib/alttheoryskel/README.WHATS-NEXT
+++ /dev/null
@@ -1,25 +0,0 @@
-Congratulations, you now have a new theory of $dir !
-
-Your next steps will likely be:
-
-* to implement a decision procedure for your theory by implementing
-  Theory$camel::check() in theory_$dir.cpp. Before writing the actual
-  code, you will need :
-
-  * to determine which data structures are context dependent and use for
-    them context-dependent data structures (context/cd*.h)
-  * to choose which work will be done at QUICK_CHECK, STANDARD or at
-    FULL_EFFORT.
-
-You'll probably find the Developer's wiki useful:
-
-  http://cvc4.cs.stanford.edu/wiki/
-
-...and the Developer's Guide:
-
-  https://github.com/CVC4/CVC4/wiki/Developer-Guide
-
-which contains coding guidelines for the CVC4 project.
-
-Good luck, and please contact cvc4-devel@cs.stanford.edu for assistance
-should you need it!
diff --git a/contrib/alttheoryskel/kinds b/contrib/alttheoryskel/kinds
deleted file mode 100644
index 44efe1698..000000000
--- a/contrib/alttheoryskel/kinds
+++ /dev/null
@@ -1,8 +0,0 @@
-# kinds                                                               -*- sh -*-
-#
-# For documentation on this file format, please refer to
-# src/theory/builtin/kinds.
-#
-
-alternate THEORY_$alt_id "$dir" ::CVC4::theory::$dir::Theory$camel "theory/$dir/theory_$dir.h"
-
diff --git a/contrib/alttheoryskel/options b/contrib/alttheoryskel/options
deleted file mode 100644
index f627dc4a0..000000000
--- a/contrib/alttheoryskel/options
+++ /dev/null
@@ -1,8 +0,0 @@
-#
-# Option specification file for CVC4
-# See src/options/base_options for a description of this file format
-#
-
-module $id "theory/$dir/options.h" $camel
-
-endmodule
diff --git a/contrib/alttheoryskel/options_handlers.h b/contrib/alttheoryskel/options_handlers.h
deleted file mode 100644
index d384e84d9..000000000
--- a/contrib/alttheoryskel/options_handlers.h
+++ /dev/null
@@ -1,14 +0,0 @@
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__$id__OPTIONS_HANDLERS_H
-#define __CVC4__THEORY__$id__OPTIONS_HANDLERS_H
-
-namespace CVC4 {
-namespace theory {
-namespace $dir {
-
-}/* CVC4::theory::$dir namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__$id__OPTIONS_HANDLERS_H */
diff --git a/contrib/alttheoryskel/theory_DIR.cpp b/contrib/alttheoryskel/theory_DIR.cpp
deleted file mode 100644
index b1cd27c89..000000000
--- a/contrib/alttheoryskel/theory_DIR.cpp
+++ /dev/null
@@ -1,46 +0,0 @@
-#include "theory/$dir/theory_$dir.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace theory {
-namespace $dir {
-
-/** Constructs a new instance of Theory$camel w.r.t. the provided contexts. */
-Theory$camel::Theory$camel(context::Context* c,
-                           context::UserContext* u,
-                           OutputChannel& out,
-                           Valuation valuation,
-                           const LogicInfo& logicInfo) :
-    Theory(THEORY_$alt_id, c, u, out, valuation, logicInfo) {
-}/* Theory$camel::Theory$camel() */
-
-void Theory$camel::check(Effort level) {
-  if (done() && !fullEffort(level)) {
-    return;
-  }
-
-  TimerStat::CodeTimer checkTimer(d_checkTime);
-
-  while(!done()) {
-    // Get all the assertions
-    Assertion assertion = get();
-    TNode fact = assertion.assertion;
-
-    Debug("$dir") << "Theory$camel::check(): processing " << fact << std::endl;
-
-    // Do the work
-    switch(fact.getKind()) {
-
-    /* cases for all the theory's kinds go here... */
-
-    default:
-      Unhandled(fact.getKind());
-    }
-  }
-
-}/* Theory$camel::check() */
-
-}/* CVC4::theory::$dir namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/contrib/alttheoryskel/theory_DIR.h b/contrib/alttheoryskel/theory_DIR.h
deleted file mode 100644
index d8e652b7c..000000000
--- a/contrib/alttheoryskel/theory_DIR.h
+++ /dev/null
@@ -1,34 +0,0 @@
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__$id__THEORY_$id_H
-#define __CVC4__THEORY__$id__THEORY_$id_H
-
-#include "theory/theory.h"
-
-namespace CVC4 {
-namespace theory {
-namespace $dir {
-
-class Theory$camel : public Theory {
-public:
-
-  /** Constructs a new instance of Theory$camel w.r.t. the provided contexts. */
-  Theory$camel(context::Context* c,
-               context::UserContext* u,
-               OutputChannel& out,
-               Valuation valuation,
-               const LogicInfo& logicInfo);
-
-  void check(Effort);
-
-  std::string identify() const {
-    return "THEORY_$id";
-  }
-
-};/* class Theory$camel */
-
-}/* CVC4::theory::$dir namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__$id__THEORY_$id_H */
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index 3ca8bd32b..715f3fc6c 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-cvc4=./cvc4
+cvc5=./cvc5
 bench="$1"
 
 # Output other than "sat"/"unsat" is either written to stderr or to "err.log"
@@ -26,7 +26,7 @@ logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]
 # returns normally and prints the output of the solver to $out_file.
 function trywith {
   limit=$1; shift;
-  result="$({ ulimit -S -t "$limit"; $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench; } 2>&1)"
+  result="$({ ulimit -S -t "$limit"; $cvc5 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench; } 2>&1)"
   case "$result" in
     sat|unsat) echo "$result"; exit 0;;
     *)         echo "$result" &> "$out_file";;
@@ -34,10 +34,10 @@ function trywith {
 }
 
 # use: finishwith [params..]
-# to run cvc4. Only "sat" or "unsat" are output. Other outputs are written to
+# to run cvc5. Only "sat" or "unsat" are output. Other outputs are written to
 # $out_file.
 function finishwith {
-  result="$({ $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench; } 2>&1)"
+  result="$({ $cvc5 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench; } 2>&1)"
   case "$result" in
     sat|unsat) echo "$result"; exit 0;;
     *)         echo "$result" &> "$out_file";;
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
index 7861a4c85..e0b51bc46 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-cvc4=./cvc4
+cvc5=./cvc5
 
 line=""
 while [[ -z "$line" ]]; do
@@ -22,54 +22,54 @@ if [ -z "$logic" ]; then
 fi
 echo success
 
-function runcvc4 {
+function runcvc5 {
   # we run in this way for line-buffered input, otherwise memory's a
   # concern (plus it mimics what we'll end up getting from an
   # application-track trace runner?)
-  $cvc4 --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0-
+  $cvc5 --force-logic="$logic" -L smt2.6 --print-success --no-type-checking --no-interactive "$@" <&0-
 }
 
 case "$logic" in
 
 ALIA|ANIA|AUFNIRA|LIA|LRA|QF_ALIA|QF_ANIA|QF_AUFBVLIA|QF_AUFBVNIA|QF_LIA|QF_LRA|QF_NIA|QF_UFBVLIA|QF_UFLIA|QF_UFLRA|QF_UFNIA|UFLRA)
-  runcvc4 --tear-down-incremental=1
+  runcvc5 --tear-down-incremental=1
   ;;
 QF_AUFLIA)
-  runcvc4 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas
+  runcvc5 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas
   ;;
 QF_BV)
-  runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical
+  runcvc5 --incremental --bitblast=eager --bv-sat-solver=cadical
   ;;
 QF_UFBV)
-  runcvc4 --incremental
+  runcvc5 --incremental
   ;;
 QF_UF)
-  runcvc4 --incremental
+  runcvc5 --incremental
   ;;
 QF_AUFBV)
-  runcvc4 --incremental
+  runcvc5 --incremental
   ;;
 QF_ABV)
-  runcvc4 --incremental
+  runcvc5 --incremental
   ;;
 ABVFP)
-  runcvc4 --incremental
+  runcvc5 --incremental
   ;;
 BVFP)
-  runcvc4 --incremental
+  runcvc5 --incremental
   ;;
 QF_ABVFP)
-  runcvc4 --incremental
+  runcvc5 --incremental
   ;;
 QF_BVFP)
-  runcvc4 --incremental
+  runcvc5 --incremental
   ;;
 QF_FP)
-  runcvc4 --incremental
+  runcvc5 --incremental
   ;;
 *)
   # just run the default
-  runcvc4 --incremental
+  runcvc5 --incremental
   ;;
 
 esac
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation
index 9982a9e29..338215a52 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-model-validation
@@ -1,14 +1,14 @@
 #!/bin/bash
 
-cvc4=./cvc4
+cvc5=./cvc5
 bench="$1"
 
 logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
 
 # use: finishwith [params..]
-# to run cvc4 and let it output whatever it will to stdout.
+# to run cvc5 and let it output whatever it will to stdout.
 function finishwith {
-  $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench
+  $cvc5 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench
 }
 
 case "$logic" in
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
index 5cb2ab610..ab6e2a6fc 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
@@ -1,14 +1,14 @@
 #!/bin/bash
 
-cvc4=./cvc4
+cvc5=./cvc5
 bench="$1"
 
 logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
 
 # use: finishwith [params..]
-# to run cvc4 and let it output whatever it will to stdout.
+# to run cvc5 and let it output whatever it will to stdout.
 function finishwith {
-  $cvc4 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench
+  $cvc5 -L smt2.6 --no-incremental --no-type-checking --no-interactive "$@" $bench
 }
 
 case "$logic" in
diff --git a/contrib/cut-release b/contrib/cut-release
deleted file mode 100755
index f13d22298..000000000
--- a/contrib/cut-release
+++ /dev/null
@@ -1,345 +0,0 @@
-#!/bin/bash
-#
-# usage: cut-release [-n] version-designation [make-args...]
-#
-
-
-dryrun=false
-getantlr="./contrib/get-antlr-3.4"
-dogetantlr=false
-configantlr=""
-version=""
-cutrelease=`basename "$0"`
-
-function isthatright {
-  if $dryrun; then
-    echo -n "[DRY RUN] "
-  fi
-  if [ -z "$1" ]; then
-    echo -n "Does that look right? [y/n] "
-  else
-    echo -n "$1? [y/n] "
-  fi
-  while read yn; do
-    if [ "$yn" = y -o "$yn" = Y -o "$yn" = yes -o "$yn" = YES -o "$yn" = Yes ]; then
-      break
-    elif [ "$yn" = n -o "$yn" = N -o "$yn" = no -o "$yn" = NO -o "$yn" = No ]; then
-      echo "Aborting as per user request." >&2
-      exit 1
-    else
-      echo -n "[y/n] "
-    fi
-  done
-}
-
-function printusage {
-  echo "Usage: $cutrelease <options> version-designation [make-args...]" >&2
-  echo 
-  echo "Options:"
-  echo
-  echo "  -h, --help    print this message and exit"
-  echo
-  echo "  -n            do a dry run (do sanity checks and build "
-  echo "                but don not touch the repository)"
-  echo
-  echo "  -a            get local antlr to use for compilation"
-}
-
-function error {
-  echo "$cutrelease: ERROR: $1" >&2
-}
-
-function die {
-  error "$1"
-  exit 1
-}
-
-function internalerror {
-  echo "$cutrelease: INTERNAL ERROR: $1" >&2
-  exit 1
-}
-
-if ! [ -e src/expr/node.h -a -e .git ]; then
-  die "You should run this from the top-level of a CVC4 git working directory" 
-fi
-
-while [[ $# -gt 0 ]]
-do
-  arg="$1"
-  case $arg in
-    -h | --help) 
-      printusage
-      exit 0
-      ;;
-    -n) 
-      dryrun=true
-      shift
-      ;;
-    -a)
-      dogetantlr=true
-      shift
-      ;;
-    -*)
-      error "invalid option $arg"
-      echo
-      printusage
-      exit 1
-      ;;
-    *)
-      if [ "x$version" = "x" ]
-      then
-        version="$arg"
-        shift
-        if echo "$version" | grep '[^a-zA-Z0-9_.+(){}^%#-]' &>/dev/null
-        then
-          die "Version designation \`$version' contains illegal characters"
-        fi
-        break
-      fi
-  esac
-done
-makeargs="$@"
-
-if [ "x$version" = "x" ] 
-then
-  error "missing version-designation"
-  echo
-  printusage
-  exit 1
-fi
-
-if $dryrun
-then
-  echo
-  echo '************************* DRY RUN *************************'
-fi
-
-eval "declare -a vs=($(echo "$version" | sed 's,^\([0-9]*\)\.\([0-9]*\)\(\.\([0-9]*\)\)\?\(.*\),[0]=\1 [1]=\2 [2]=\4 [3]=\5,'))"
-major=${vs[0]}
-minor=${vs[1]}; if [ -z "$minor" ]; then minor=0; fi
-release=${vs[2]}; if [ -z "$release" ]; then release=0; fi
-extra=${vs[3]}
-echo
-echo "Major  : $major"
-echo "Minor  : $minor"
-echo "Release: $release"
-echo "Extra  : $extra"
-echo
-version="$major.$minor"
-if [ "$release" != 0 ]; then
-  version="$version.$release"
-fi
-version="$version$extra"
-echo "Version: $version"
-echo
-isthatright
-
-echo "Checking whether release \`$version' already exists..."
-if [ -n "`git tag -l "$version"`" ]; then
-  error "Git repo already contains a release \`$version'"
-  $dryrun || exit 1
-fi
-
-echo "Checking working directory for local modifications..."
-if $dryrun; then
-  if [ -n "$(git status -s configure.ac)" ]; then
-    die "In dry-run mode, cannot operate properly with local modifications to \"configure.ac\", sorry"
-  fi
-elif [ -n "$(git status -s | grep -v '^ *M *\(NEWS\|README\|AUTHORS\|RELEASE-NOTES\|INSTALL\|THANKS\|library_versions\|contrib/cut-release\)$')" ]; then
-  die "\"git status\" indicates there are local modifications; please commit first"
-fi
-
-echo "Checking repo for unmerged updates..."
-git fetch &>/dev/null
-if git status -sb | grep -q '^## .* \[.*behind '; then
-  error "This working directory isn't up to date"
-  $dryrun || exit 1
-fi
-
-echo "Checking sources for broken public headers..."
-suspect_files="\
-$(grep -r --exclude-dir=.git '^[ \t]*#[ \t]*include[ \t]*"[^/]*"' src |
-  grep -v '"cvc4parser_public\.h"' |
-  grep -v '"cvc4_public\.h"' |
-  grep -v '"cvc4_private\.h"' |
-  grep -v '"cvc4autoconfig\.h"' |
-  grep -v '"cvc4parser_private\.h"' |
-  cut -f1 -d: |
-  sort -u |
-  xargs grep -l '^[ \t]*#[ \t]*include[ \t]*"cvc4.*public\.h"' |
-  xargs echo)"
-if [ -n "$suspect_files" ]; then
-  error "The following publicly-installed headers appear"
-  error "  to have relative #includes and may be broken"
-  error "  after install: $suspect_files"
-  $dryrun || exit 1
-fi
-
-for updatefile in NEWS README AUTHORS RELEASE-NOTES INSTALL THANKS; do
-  echo "Checking $updatefile file for recent updates..."
-  if [ -n "$(git status -s $updatefile)" ]; then
-    echo "+ It's locally modified."
-  else
-    git log -n 1 --date=local --pretty=format:'+ Last changed on %ad (%ar)' $updatefile
-    echo
-    case $updatefile in
-      NEWS)
-        echo "You should make sure to put some notes in the NEWS file for"
-        echo "release $version, indicating the most important changes since the"
-        echo "last release."
-        ;;
-      AUTHORS)
-        echo "You should make sure there are no new authors to list for $version."
-        ;;
-      *)
-        echo "You should ensure that $updatefile is appropriately updated"
-        echo "for $version before continuing.  (Maybe it even lists the previous"
-        echo "version number!)"
-        ;;
-    esac
-    echo
-    isthatright "Continue without updating $updatefile"
-  fi
-done
-
-echo "Adjusting version info lines in configure.ac..."
-if ! grep '^m4_define(_CVC4_MAJOR,  *[0-9][0-9]* *)' configure.ac &>/dev/null ||
-   ! grep '^m4_define(_CVC4_MINOR,  *[0-9][0-9]* *)' configure.ac &>/dev/null ||
-   ! grep '^m4_define(_CVC4_RELEASE,  *[0-9][0-9]* *)' configure.ac &>/dev/null ||
-   ! grep '^m4_define(_CVC4_EXTRAVERSION,  *\[.*\] *)' configure.ac &>/dev/null; then
-  error "Cannot locate the version info lines of configure.ac"
-  $dryrun || exit 1
-fi
-perl -pi -e 's/^m4_define\(_CVC4_MAJOR, ( *)[0-9]+( *)\)/m4_define(_CVC4_MAJOR, ${1}'"$major"'$2)/;
-             s/^m4_define\(_CVC4_MINOR, ( *)[0-9]+( *)\)/m4_define(_CVC4_MINOR, ${1}'"$minor"'$2)/;
-             s/^m4_define\(_CVC4_RELEASE, ( *)[0-9]+( *)\)/m4_define(_CVC4_RELEASE, ${1}'"$release"'$2)/;
-             s/^m4_define\(_CVC4_EXTRAVERSION, ( *)\[.*\]( *)\)/m4_define(_CVC4_EXTRAVERSION, $1\['"$extra"'\]$2)/' configure.ac
-
-trap 'echo; echo; echo "Aborting in error."; git checkout -- configure.ac; echo' EXIT
-
-echo
-echo 'Made the following change to configure.ac:'
-echo
-git diff configure.ac
-echo
-isthatright
-
-if ! grep '^m4_define(_CVC4_MAJOR,  *'"$major"' *)' configure.ac &>/dev/null ||
-   ! grep '^m4_define(_CVC4_MINOR,  *'"$minor"' *)' configure.ac &>/dev/null ||
-   ! grep '^m4_define(_CVC4_RELEASE,  *'"$release"' *)' configure.ac &>/dev/null ||
-   ! grep '^m4_define(_CVC4_EXTRAVERSION,  *\['"$extra"'\] *)' configure.ac &>/dev/null; then
-  internalerror "Cannot find the modified version info lines in configure.ac, bailing..."
-fi
-if [ -z "$(git status -s configure.ac)" ]; then
-  internalerror "\"git status\" indicates there are no local modifications to configure.ac; I expected the ones I just made!"
-fi
-
-echo "Building and checking distribution \`cvc4-$version'..."
-
-if $dogetantlr 
-then
-  echo "Fetching and compiling antlr..."
-  $getantlr > /dev/null 2>&1
-  configantlr="--with-antlr-dir=$(pwd)/antlr-3.4 ANTLR=$(pwd)/antlr-3.4/bin/antlr3"
-fi
-
-if ! $SHELL -c '\
-	version="'$version'"; \
-	set -ex; \
-	./autogen.sh || echo "autoconf failed; does library_versions have something to match $version?"; \
-	mkdir "release-$version"; \
-	cd "release-$version"; \
-	../configure production-staticbinary --disable-shared --enable-unit-testing --with-portfolio --no-gpl '"$configantlr"'; \
-	make dist '"$makeargs"'; \
-	tar xf "cvc4-$version.tar.gz"; \
-	cd "cvc4-$version"; \
-	./configure production-staticbinary --disable-shared --enable-unit-testing --with-portfolio --no-gpl '"$configantlr"'; \
-	make check '"$makeargs"'; \
-	make distcheck '"$makeargs"'; \
-'; then
-  exit 1
-fi
-
-if ! [ -e release-$version/cvc4-$version.tar.gz ]; then
-  internalerror "Cannot find the distribution tarball I just built"
-fi
-if ! [ -e release-$version/cvc4-$version/builds/src/main/cvc4 ]; then
-  internalerror "Cannot find the binary I just built"
-fi
-
-echo
-echo 'This release of CVC4 will identify itself as:'
-echo
-release-$version/cvc4-$version/builds/src/main/cvc4 --version
-echo
-isthatright
-
-echo
-echo 'This binary release of CVC4 will identify itself as being configured like this:'
-echo
-release-$version/cvc4-$version/builds/src/main/cvc4 --show-config
-echo
-isthatright
-
-#echo
-#echo "Signing tarball..."
-#cp -p "release-$version/cvc4-$version.tar.gz" .
-#gpg -b --armor "cvc4-$version.tar.gz"
-
-#echo
-#echo "Signing cvc4 binary..."
-#cp -p "release-$version/cvc4-$version/builds/src/main/cvc4" "cvc4-$version"
-#gpg -b --armor "cvc4-$version"
-
-#echo
-#echo "Signing pcvc4 binary..."
-#cp -p "release-$version/src/main/pcvc4" "pcvc4-$version"
-#gpg -b --armor "pcvc4-$version"
-
-if $dryrun; then
-  echo
-  echo '************************* DRY RUN *************************'
-fi
-
-echo
-echo "About to run: git commit -am \"Cutting release $version.\""
-isthatright
-$dryrun || git commit -am "Cutting release $version."
-
-echo
-echo "About to run: git tag \"$version\""
-isthatright
-$dryrun || git tag "$version"
-
-echo
-andbranch=
-if git status -bs | grep -q '^## master\($\|  *\|\.\.\.\)'; then
-  if [ "$release" = 0 ]; then
-    echo "About to run: git branch \"$version.x\""
-    isthatright
-    $dryrun || git branch "$version.x"
-    andbranch=", the $version.x branch,"
-  else
-    echo "Not branching, because this is a minor release (i.e., not a \"dot-oh\""
-    echo "release), so I'm guessing you have a devel branch outside of master"
-    echo "somewhere?  You can still make a branch manually, of course."
-  fi
-else
-  echo "Not branching, because it appears there already is a branch"
-  echo "to work with for version $version ..?  (You're not on master.)"
-  echo "You can still make a branch manually, of course."
-fi
-
-echo
-echo "Done.  Next steps are to:"
-echo
-echo "1. push to GitHub (don't forget to push master$andbranch and the $version tag)"
-echo "2. upload source and binaries"
-echo "3. advertise these packages"
-echo "4. add a $version release and next-milestone to Bugzilla."
-echo "5. change $version to pre-release in master$andbranch"
-echo "   (in configure.ac) and update library_versions and NEWS."
-echo
-
-trap '' EXIT
-
diff --git a/contrib/cvc4_strict_smtlib b/contrib/cvc5_strict_smtlib
index 45c7cbe1a..e746f7504 100644
--- a/contrib/cvc4_strict_smtlib
+++ b/contrib/cvc5_strict_smtlib
@@ -1,8 +1,8 @@
 #!/bin/bash
 
-cvc4="${CVC4_HOME}/cvc4"
+cvc5="${CVC5_HOME}/cvc5"
 
 # This is the set of command line arguments that is required to be strictly
 # complaint with the input and output requirements of the current SMT-LIB
 # standard.
-"$cvc4" --lang=smt2 --output-lang=smt2 --strict-parsing --expr-depth=-1 --print-success --incremental --abstract-values $@
+"$cvc5" --lang=smt2 --output-lang=smt2 --strict-parsing --expr-depth=-1 --print-success --incremental --abstract-values $@
diff --git a/contrib/debug-keys b/contrib/debug-keys
deleted file mode 100755
index 6d2804974..000000000
--- a/contrib/debug-keys
+++ /dev/null
@@ -1,33 +0,0 @@
-#!/bin/bash
-#
-# Lists the Trace() and Debug() keys used in sources.
-#
-# e.g. if Debug("uf") occurs in the sources, then "uf" is printed by this script.
-
-if [ "$1" = "-h" -o "$1" = "-help" -o "$1" = "-?" -o "$1" = "--help" ]; then
-  echo "usage: `basename $0` [dirs...]" >&2
-  echo "This utility will print all Debug("foo") and Trace("foo") keys."
-  echo "With optional dirs..., use dirs instead of top-level \"src\"." >&2
-  exit 1
-fi
-
-if [ $# -eq 0 ]; then
-  cd `dirname "$0"`/..
-
-  if ! [ -d src ]; then
-    echo "`basename $0`: not in CVC4 directory tree?!" >&2
-    exit 1
-  fi
-
-  set src
-fi
-
-echo "Trace and debug flags used in $*:"
-
-while [ $# -gt 0 ]; do
-  dir="$1"
-  shift
-
-  test -r "$dir" && grep -r --exclude-dir=.svn '\(Debug\|Trace\)\(\.isOn\)\?("[^"]\+")' "$dir" | sed 's,.*\(Debug\|Trace\)\(\.isOn\)\?("\([^"]\+\)").*,\3,' | sort -u
-done | sort -u
-
diff --git a/contrib/depgraph b/contrib/depgraph
deleted file mode 100755
index b0e650f40..000000000
--- a/contrib/depgraph
+++ /dev/null
@@ -1,132 +0,0 @@
-#!/bin/sh
-#
-# depgraph
-# Morgan Deters, 27 October 2010
-#
-# Builds a graphviz graph of dependences between source and header files in CVC4.
-#
-
-progname=`basename "$0"`
-
-postproc='sort -u'
-mode=packages
-target=
-
-if [ $# -gt 0 ]; then
-  if [ "$1" = "-a" ]; then
-    postproc=cat
-    mode=headers
-    shift
-  fi
-  if [ $# -gt 0 -a "$1" != "-h" ]; then
-    target="$1"
-    shift
-  fi
-  if [ $# -gt 0 ]; then
-    echo "usage: $progname [-a] [target]"
-    echo "  -a ("all") produces _all_ headers in the source, with clusters for packages."
-    echo "    the default behavior produces just package dependence information."
-    echo "  with target, focus on dependences of that particular package (e.g. \"expr\")"
-    exit 1
-  fi
-fi
-
-cd "`dirname \"$0\"`/.."
-
-if ! [ -d src -a -d test/unit ]; then
-  echo "$progname: source directory malformed; is this CVC4 ?!" >&2
-  exit 1
-fi
-
-echo "digraph G {"
-
-paths=`find src -name '*.c' \
-             -o -name '*.cc' \
-             -o -name '*.cpp' \
-             -o -name '*.C' \
-             -o -name '*.h' \
-             -o -name '*.hh' \
-             -o -name '*.hpp' \
-             -o -name '*.H' \
-             -o -name '*.y' \
-             -o -name '*.yy' \
-             -o -name '*.ypp' \
-             -o -name '*.Y' \
-             -o -name '*.l' \
-             -o -name '*.ll' \
-             -o -name '*.lpp' \
-             -o -name '*.L' \
-             -o -name '*.g'`
-if [ "$mode" = headers ]; then
-  oldpackage=
-  for path in $paths; do
-    dir=`echo "$path" | sed 's,^\([^/]*\).*,\1,'`
-    file=`echo "$path" | sed 's,^[^/]*/,,'`
-    package=`echo "$file" | sed 's,^\(.*\)/.*,\1,'`
-    file=`echo "$file" | sed 's,^.*/,,'`
-    if [ -n "$target" -a "$target" != "$package" ]; then continue; fi
-    if [ -n "$oldpackage" -a "$package" != "$oldpackage" ]; then
-      echo '  }'
-    fi
-    if [ "$package" != "$oldpackage" ]; then
-      echo "  subgraph \"cluster$package\" {"
-      echo "    label=\"$package\";"
-      oldpackage="$package"
-    fi
-    echo "    \"$package/$file\"[label=\"$file\"];"
-  done
-  if [ -n "$oldpackage" ]; then
-    echo '  }'
-  fi
-fi
-for path in $paths; do
-    dir=`echo "$path" | sed 's,^\([^/]*\).*,\1,'`
-    file=`echo "$path" | sed 's,^[^/]*/,,'`
-    package=`echo "$file" | sed 's,^\(.*\)/.*,\1,'`
-    file=`echo "$file" | sed 's,^.*/,,'`
-    incs=`grep '^# *include *".*"' "$path" | sed 's,^# *include *"\(.*\)".*,\1,'`
-    if [ -n "$target" -a "$target" != "$package" ]; then continue; fi
-    for inc in $incs; do
-      case "$inc" in
-        expr/expr.h) inc=expr/expr_template.h ;;
-        expr/expr_manager.h) inc=expr/expr_manager_template.h ;;
-        expr/kind.h) inc=expr/kind_template.h ;;
-        expr/metakind.h) inc=expr/metakind_template.h ;;
-        theory/theoryof_table.h) inc=theory/theoryof_table_template.h ;;
-        util/integer.h) inc=util/integer.h.in ;;
-        util/rational.h) inc=util/rational.h.in ;;
-        cvc4autoconfig.h) inc=cvc4autoconfig.h.in ;;
-      esac
-      incpath=
-      dirpackageparent="$dir/`dirname "$package"`"
-      for incdir in "$dir" "$dir/include" "$dir/$package" . "$dirpackageparent"; do
-        if [ -e "$incdir/$inc" ]; then incpath="$incdir/$inc"; break; fi
-      done
-      if [ -z "$incpath" ]; then
-        echo "$progname: error: can't find include file '$inc' from source '$path'" >&2
-        exit 1
-      fi
-      incpath=`echo "$incpath" | sed 's,^\./,,'`
-      incpath=`echo "$incpath" | sed "s,^$dir/,,"`
-      incdir=`echo "$incpath" | sed 's,^\([^/]*\).*,\1,'`
-      incpackage=`echo "$incpath" | sed 's,^\(.*\)/.*,\1,'`
-      incfile=`echo "$incpath" | sed 's,^.*/,,'`
-      if [ "$mode" = packages ]; then
-        if [ "$package" != "$incpackage" ]; then
-          if [ -n "$target" ]; then
-            echo "  \"$package\" -> \"$incpackage\"[label=\"$incfile\"];"
-          else
-            echo "  \"$package\" -> \"$incpackage\";"
-          fi
-        fi
-      else
-        if [ -n "$target" ]; then
-          [ "$package" != "$incpackage" ] && echo "  \"$package/$file\" -> \"$incpackage\"[label=\"$incfile\"];"
-        else
-          echo "  \"$package/$file\" -> \"$incpath\";"
-        fi
-      fi
-    done
-  done | $postproc
-
-echo "}"
diff --git a/contrib/dimacs_to_smt.pl b/contrib/dimacs_to_smt.pl
deleted file mode 100755
index 701768119..000000000
--- a/contrib/dimacs_to_smt.pl
+++ /dev/null
@@ -1,37 +0,0 @@
-#!/usr/bin/perl -w
-# DIMACS to SMT
-# Morgan Deters
-# Copyright (c) 2009, 2010, 2011  The CVC4 Project
-
-use strict;
-
-my ($nvars, $nclauses);
-while(<>) {
-    next if /^c/;
-
-    if(/^p cnf (\d+) (\d+)/) {
-        ($nvars, $nclauses) = ($1, $2);
-        print "(benchmark b\n";
-        print ":status unknown\n";
-        print ":logic QF_UF\n";
-        for(my $i = 1; $i <= $nvars; ++$i) {
-            print ":extrapreds ((x$i))\n";
-        }
-        print ":formula (and\n";
-        next;
-    }
-
-    print "(or";
-    chomp;
-    @_ = split(/ /);
-    for(my $i = 0; $i < $#_; ++$i) {
-        if($_[$i] < 0) {
-            print " (not x" . -$_[$i] . ")";
-        } else {
-            print " x" . $_[$i];
-        }
-    }
-    print ")\n";
-}
-
-print "))\n";
diff --git a/contrib/get-abc b/contrib/get-abc
index 9f37a69e3..6f5987586 100755
--- a/contrib/get-abc
+++ b/contrib/get-abc
@@ -38,5 +38,5 @@ else
 fi
 
 echo
-echo ===================== Now configure CVC4 with =====================
+echo ===================== Now configure cvc5 with =====================
 echo ./configure.sh --abc
diff --git a/contrib/get-authors b/contrib/get-authors
index 6457569a5..3bec55130 100755
--- a/contrib/get-authors
+++ b/contrib/get-authors
@@ -1,7 +1,7 @@
 #!/bin/sh
 #
 # get-authors
-# Copyright (c) 2009-2020  The CVC4 Project
+# Copyright (c) 2009-2021  The cvc5 Project
 #
 # usage: get-authors [ files... ]
 #
diff --git a/contrib/get-drat2er b/contrib/get-drat2er
index 318de1b83..803add62f 100755
--- a/contrib/get-drat2er
+++ b/contrib/get-drat2er
@@ -16,5 +16,5 @@ cmake .. -DCMAKE_INSTALL_PREFIX="$INSTALL_DIR"
 make install -j$(nproc)
 
 echo
-echo ===================== Now configure CVC4 with =====================
+echo ===================== Now configure cvc5 with =====================
 echo ./configure.sh --drat2er
diff --git a/contrib/get-glpk-cut-log b/contrib/get-glpk-cut-log
index cf523dc5a..0a5747589 100755
--- a/contrib/get-glpk-cut-log
+++ b/contrib/get-glpk-cut-log
@@ -40,5 +40,5 @@ rename_installed_lib "libglpk.a" "libglpk-static.a"
 make install -j$(nproc)
 
 echo
-echo ===================== Now configure CVC4 with =====================
+echo ===================== Now configure cvc5 with =====================
 echo ./configure.sh --gpl --glpk
diff --git a/contrib/get-lfsc-checker b/contrib/get-lfsc-checker
index 45ae432f6..9a7292fc7 100755
--- a/contrib/get-lfsc-checker
+++ b/contrib/get-lfsc-checker
@@ -49,25 +49,25 @@ mkdir -p $BASE_DIR/share/lfsc
 cp -r $SIG_DIR/lfsc/new/signatures $BASE_DIR/share/lfsc
 
 # based on https://github.com/CVC4/signatures/blob/master/lfsc/new/scripts/cvc4_gen_and_check.sh
-cat << EOF > $BASE_DIR/bin/cvc4-lfsc-check.sh
+cat << EOF > $BASE_DIR/bin/cvc5-lfsc-check.sh
 #!/bin/bash
 
 echo "=== Generate proof: \$@" 
-$BASE_DIR/bin/cvc4-proof.sh \$@ > proof.plf
+$BASE_DIR/bin/cvc5-proof.sh \$@ > proof.plf
 
 echo "=== Check proof with LFSC" 
 $BASE_DIR/bin/lfsc-check.sh proof.plf
 EOF
-chmod +x $BASE_DIR/bin/cvc4-lfsc-check.sh
+chmod +x $BASE_DIR/bin/cvc5-lfsc-check.sh
 
 # based on https://github.com/CVC4/signatures/blob/master/lfsc/new/scripts/cvc4_gen.sh
-cat << EOF > $BASE_DIR/bin/cvc4-proof.sh
+cat << EOF > $BASE_DIR/bin/cvc5-proof.sh
 #!/bin/bash
 
-# call cvc4 and remove the first line of the output (should be "unsat")
+# call cvc5 and remove the first line of the output (should be "unsat")
 \$@ --dump-proofs --proof-format=lfsc | tail -n +2
 EOF
-chmod +x $BASE_DIR/bin/cvc4-proof.sh
+chmod +x $BASE_DIR/bin/cvc5-proof.sh
 
 # based on https://github.com/CVC4/signatures/blob/master/lfsc/new/scripts/lfsc_check.sh
 cat << EOF > $BASE_DIR/bin/lfsc-check.sh
@@ -107,9 +107,9 @@ popd
 
 echo ""
 echo "========== How to use LFSC =========="
-echo "Generate a LFSC proof with CVC4:"
-echo "  $CVC_DIR/deps/bin/cvc4-proof.sh cvc4 <options> <input file>"
+echo "Generate a LFSC proof with cvc5:"
+echo "  $CVC_DIR/deps/bin/cvc5-proof.sh cvc5 <options> <input file>"
 echo "Check a generated proof:"
 echo "  $CVC_DIR/deps/bin/lfsc-check.sh <proof file>"
-echo "Run CVC4 and check the generated proof:"
-echo "  $CVC_DIR/deps/bin/cvc4-lfsc-check.sh cvc4 <options> <input file>"
+echo "Run cvc5 and check the generated proof:"
+echo "  $CVC_DIR/deps/bin/cvc5-lfsc-check.sh cvc5 <options> <input file>"
diff --git a/contrib/get-script-header.sh b/contrib/get-script-header.sh
index 394669c68..5deaa00da 100644
--- a/contrib/get-script-header.sh
+++ b/contrib/get-script-header.sh
@@ -13,12 +13,12 @@ INSTALL_BIN_DIR="$INSTALL_DIR/bin"
 mkdir -p "$DEPS_DIR"
 
 if ! [ -e src/parser/cvc/Cvc.g ]; then
-  echo "$(basename $0): I expect to be in the contrib/ of a CVC4 source tree," >&2
+  echo "$(basename $0): I expect to be in the contrib/ of a cvc5 source tree," >&2
   echo "but apparently:" >&2
   echo >&2
   echo "  $(pwd)" >&2
   echo >&2
-  echo "is not a CVC4 source tree ?!" >&2
+  echo "is not a cvc5 source tree ?!" >&2
   exit 1
 fi
 
diff --git a/contrib/learn_resource_weights.py b/contrib/learn_resource_weights.py
index 8f5213ec2..76a7a043d 100755
--- a/contrib/learn_resource_weights.py
+++ b/contrib/learn_resource_weights.py
@@ -14,7 +14,7 @@ def parse_commandline():
     """Parse commandline arguments"""
     epilog = """
 This script can be used to compute good resource weights based on benchmark
-results. The resource weights are used by cvc4 to approximate the running time
+results. The resource weights are used by cvc5 to approximate the running time
 by the spent resources, multiplied with their weights.
 
 In the first stage ("parse") this script reads the output files of a benchmark
diff --git a/contrib/luby.c b/contrib/luby.c
deleted file mode 100644
index 71b07b665..000000000
--- a/contrib/luby.c
+++ /dev/null
@@ -1,69 +0,0 @@
-// luby.c - Luby sequence generator
-// Morgan Deters <mdeters@cs.nyu.edu> for the CVC4 project, 5 May 2011
-//
-// This program enumerates the Luby-based MiniSat 2 restart sequence.
-// MiniSat restarts after a number of conflicts determined by:
-//
-//    restart_base * luby(restart_inc, curr_restarts)
-//
-// By default, MiniSat has restart_base = 25, restart_inc = 3.0, and
-// curr_restarts is the number of restarts that have been done (so it
-// starts at 0).
-//
-// For the Luby paper, see:
-//   http://citeseer.ist.psu.edu/viewdoc/summary?doi=10.1.1.47.5558
-//
-// Compile luby.c with gcc -o luby luby.c -lm
-//
-
-#include <stdio.h>
-#include <stdlib.h>
-#include <string.h>
-#include <assert.h>
-#include <math.h>
-
-// luby() function copied from MiniSat 2
-// Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
-// Copyright (c) 2007-2010, Niklas Sorensson
-double luby(double y, int x){
-
-    // Find the finite subsequence that contains index 'x', and the
-    // size of that subsequence:
-    int size, seq;
-    for (size = 1, seq = 0; size < x+1; seq++, size = 2*size+1);
-
-    while (size-1 != x){
-        size = (size-1)>>1;
-        seq--;
-        x = x % size;
-    }
-
-    return pow(y, seq);
-}
-
-int main(int argc, char *argv[]) {
-  int N;
-  int base;
-  double inc;
-  int i;
-
-  if(argc != 4) {
-    fprintf(stderr, "usage: %s base inc N\n"
-            "In MiniSat 2, base==25 and inc==3 by default.\n"
-            "base is simply a multiplier after the sequence is computed.\n"
-            "N is the number to produce (-1 means run until CTRL-C)\n",
-            argv[0]);
-    exit(1);
-  }
-
-  base = atoi(argv[1]);
-  inc = strtod(argv[2], NULL);
-  N = atoi(argv[3]);
-
-  assert(base >= 1);
-  assert(inc >= 1.0);
-
-  for(i = 0; N < 0 || i < N; ++i) {
-    printf("%d %f\n", i, luby(inc, i) * base);
-  }
-}
diff --git a/contrib/mk_starexec b/contrib/mk_starexec
deleted file mode 100755
index aafe1f0c2..000000000
--- a/contrib/mk_starexec
+++ /dev/null
@@ -1,9 +0,0 @@
-#!/bin/bash
-# Run : mk_starexec [TEXT] 
-# Run from directory containing cvc4 binary and subdirectory starexec/ containing the starexec space, i.e. subdirectory bin/ with configuration files.
-# Generates file cvc4-[TEXT].tgz that can be uploaded to starexec.
-strip cvc4
-cp cvc4 ./starexec/bin/cvc4
-cd starexec
-tar -czf ../cvc4-$1.tgz .
-rm bin/cvc4
\ No newline at end of file
diff --git a/contrib/new-theory b/contrib/new-theory
deleted file mode 100755
index 9e4e92a71..000000000
--- a/contrib/new-theory
+++ /dev/null
@@ -1,206 +0,0 @@
-#!/bin/bash
-#
-# usage: new-theory [--alternate existing-theory] new-theory-dir-name
-#
-
-cd "`dirname "$0"`/.."
-
-if ! perl -v &>/dev/null; then
-  echo "ERROR: perl is required to run this script." >&2
-  exit 1
-fi
-
-if [ ! -e src/theory/theory_engine.h ]; then
-  echo "ERROR: This script doesn't appear to be the contrib/ subdirectory" >&2
-  echo "ERROR: of the CVC4 source tree." >&2
-  exit 1
-fi
-
-# Trailing whitespaces in src/Makefile.am mess with the regexps (and are
-# generally undesirable, so we throw an error instead of ignoring them).
-if grep -q '[[:blank:]]$' src/Makefile.am; then
-	echo "ERROR: trailing whitespaces in src/Makefile.am" >&2
-	exit 1
-fi
-
-if [ $# -ge 1 -a "$1" = --alternate ]; then
-  shift
-  alternate=true
-  alttheory="$1"
-  shift
-else
-  alternate=false
-fi
-
-if [ $# -ne 1 ]; then
-  echo "usage: new-theory [--alternate existing-theory] new-theory-dir-name" >&2
-  echo "e.g.:  new-theory arrays" >&2
-  echo "e.g.:  new-theory sets" >&2
-  echo "e.g.:  new-theory rewrite_rules" >&2
-  echo "e.g.:  new-theory --alternate arith difference-logic" >&2
-  echo >&2
-  echo "This tool will create a new src/theory/<new-theory-dir-name>" >&2
-  echo "directory and fill in some infrastructural files in that directory." >&2
-  echo "It also will incorporate that directory into the build process." >&2
-  echo "Please refer to the file README.WHATS-NEXT file created in that" >&2
-  echo "directory for tips on what to do next." >&2
-  echo >&2
-  echo "Theories with multiple words (e.g. \"rewrite_rules\") should have" >&2
-  echo "directories and namespaces separated by an underscore (_).  The" >&2
-  echo "resulting class names created by this script will be in CamelCase" >&2
-  echo "(e.g. RewriteRules) if that convention is followed." >&2
-  echo >&2
-  echo "With --alternate, create a new theory directory that is declared as" >&2
-  echo "an alternate implementation of an existing host theory.  Such" >&2
-  echo "\"alternates\" share preprocessing, typechecking, rewriting (i.e.," >&2
-  echo "normal form), and expression kinds with their host theories, but" >&2
-  echo "differ in decision procedure implementation.  They are selectable" >&2
-  echo "at runtime with --use-theory." >&2
-  exit 1
-fi
-
-dir="$1"
-
-if [ -e "src/theory/$dir" ]; then
-  echo "ERROR: Theory \"$dir\" already exists." >&2
-  echo "ERROR: Please choose a new directory name (or move that one aside)." >&2
-  echo "ERROR: Or, if you'd like to create an alternate implementation of" >&2
-  echo "ERROR: $dir, use this program this way:" >&2
-  echo "ERROR:     new-theory --alternate $dir new-implementation-name" >&2
-  exit 1
-fi
-
-if ! expr "$dir" : '[a-zA-Z][a-zA-Z0-9_]*$' &>/dev/null ||
-   expr "$dir" : '_$' &>/dev/null; then
-  echo "ERROR: \"$dir\" is not a valid theory name." >&2
-  echo "ERROR:" >&2
-  echo "ERROR: Theory names must start with a letter and be composed of" >&2
-  echo "ERROR: letters, numbers, and the underscore (_) character; an" >&2
-  echo "ERROR: underscore cannot be the final character." >&2
-  exit 1
-fi
-
-if $alternate; then
-  if ! [ -d "src/theory/$alttheory" -a -f "src/theory/$alttheory/kinds" ]; then
-    echo "ERROR: Theory \"$alttheory\" doesn't exist, or cannot read its kinds file." >&2
-    exit 1
-  fi
-  alt_id="$(
-    function theory() { echo $1 | sed 's,^THEORY_,,'; exit; }
-    source "src/theory/$alttheory/kinds"
-  )"
-fi
-
-id="`echo "$dir" | tr a-z A-Z`"
-# convoluted, but should be relatively portable and give a CamelCase
-# representation for a string.  (e.g. "foo_bar" becomes "FooBar")
-camel="`echo "$dir" | awk 'BEGIN { RS="_";ORS="";OFS="" } // {print toupper(substr($1,1,1)),substr($1,2,length($1))} END {print "\n"}'`"
-
-if ! mkdir "src/theory/$dir"; then
-  echo "ERROR: encountered an error creating directory src/theory/$dir" >&2
-  exit 1
-fi
-
-echo "Theory of $dir"
-echo "Theory directory: src/theory/$dir"
-echo "Theory id: THEORY_$id"
-$alternate && echo "Alternate for theory id: THEORY_$alt_id"
-echo "Theory class: CVC4::theory::$dir::Theory$camel"
-echo
-
-function copyskel {
-  src="$1"
-  dest="`echo "$src" | sed "s/DIR/$dir/g"`"
-  echo "Creating src/theory/$dir/$dest..."
-  sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g" \
-    contrib/theoryskel/$src \
-    > "src/theory/$dir/$dest"
-}
-
-function copyaltskel {
-  src="$1"
-  dest="`echo "$src" | sed "s/DIR/$dir/g"`"
-  echo "Creating src/theory/$dir/$dest..."
-  sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g;s/\$alt_id/$alt_id/g" \
-    contrib/alttheoryskel/$src \
-    > "src/theory/$dir/$dest"
-}
-
-function copyoptions {
-  src="$1"
-  dest="`echo "$src" | sed "s/DIR/$dir/g"`"
-  echo "Creating src/options/$dest..."
-  sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g;s/\$alt_id/$alt_id/g" \
-    contrib/optionsskel/$src \
-    > "src/options/$dest"
-}
-
-# copy files from the skeleton, with proper replacements
-if $alternate; then
-  alternate01=1
-  for file in `ls contrib/alttheoryskel`; do
-    copyaltskel "$file"
-  done
-else
-  alternate01=0
-  for file in `ls contrib/theoryskel`; do
-    copyskel "$file"
-  done
-fi
-# Copy the options file independently
-for file in `ls contrib/optionsskel`; do
-  copyoptions "$file"
-done
-
-
-echo
-echo "Adding $dir to THEORIES to src/Makefile.theories..."
-if grep -q '^THEORIES = .*[^a-zA-Z0-9_]'"$dir"'\([^a-zA-Z0-9_]\|$\)' src/Makefile.theories &>/dev/null; then
-  echo "NOTE: src/Makefile.theories already lists theory $dir"
-else
-  awk '/^THEORIES = / {print $0,"'"$dir"'"} !/^THEORIES = / {print$0}' src/Makefile.theories > src/Makefile.theories.new-theory
-  if ! cp -f src/Makefile.theories src/Makefile.theories~; then
-    echo "ERROR: cannot copy src/Makefile.theories !" >&2
-    exit 1
-  fi
-  if ! mv -f src/Makefile.theories.new-theory src/Makefile.theories; then
-    echo "ERROR: cannot replace src/Makefile.theories !" >&2
-    exit 1
-  fi
-fi
-
-echo "Adding sources to src/Makefile.am..."
-
-perl -e '
-  while(<>) { print; last if /^libcvc4_la_SOURCES = /; }
-  if('$alternate01') {
-    while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/theory_'"$dir"'.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'.cpp\n"; last; } else { print; } }
-  } else {
-    while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/theory_'"$dir"'.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'.cpp \\\n\ttheory/'"$dir"'/theory_'"$dir"'_rewriter.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'_type_rules.h\n"; last; } else { print; } }
-  }
-  while(<>) { print; last if /^EXTRA_DIST = /; }
-  while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/kinds\n"; last; } else { print; } }
-  while(<>) { print; }' src/Makefile.am > src/Makefile.am.new-theory
-if ! mv -f src/Makefile.am.new-theory src/Makefile.am; then
-  echo "ERROR: cannot replace src/Makefile.am !" >&2
-  exit 1
-fi
-
-echo "Adding ${dir}_options.toml to src/options/Makefile.am..."
-if grep -q '^	${dir}_options.toml' src/options/Makefile.am &>/dev/null; then
-  echo "NOTE: src/options/Makefile.am already seems to link to $dir option files"
-else
-  awk -v name="$dir" -f contrib/new-theory.awk src/options/Makefile.am > src/options/Makefile.am.new-theory
-  if ! cp -f src/options/Makefile.am src/options/Makefile.am~; then
-    echo "ERROR: cannot copy src/options/Makefile.am !" >&2
-    exit 1
-  fi
-  if ! mv -f src/options/Makefile.am.new-theory src/options/Makefile.am; then
-    echo "ERROR: cannot replace src/options/Makefile.am !" >&2
-    exit 1
-  fi
-fi
-
-echo
-echo "Rerunning autogen.sh..."
-./autogen.sh
diff --git a/contrib/new-theory.awk b/contrib/new-theory.awk
deleted file mode 100755
index 1adbb2f24..000000000
--- a/contrib/new-theory.awk
+++ /dev/null
@@ -1,7 +0,0 @@
-#!/bin/awk -v name=theory_new -f
-#
-
-# Keep non-matching lines unchanged
-!/^OPTIONS_CONFIG_FILES = \\/ {print$0}
-# Add *_options.toml to OPTIONS_CONFIG_FILES
-/^OPTIONS_CONFIG_FILES = \\/{print $0; printf "\t%s_options.toml \\\n", name;}
diff --git a/contrib/optionsskel/DIR_options.toml b/contrib/optionsskel/DIR_options.toml
deleted file mode 100644
index 09f44fde7..000000000
--- a/contrib/optionsskel/DIR_options.toml
+++ /dev/null
@@ -1,8 +0,0 @@
-#
-# Option specification file for CVC4
-# See src/options/README for a description of this file format
-#
-
-id     = "$id"
-name   = "$camel"
-header = "options/$dir_options.h"
diff --git a/contrib/spellcheck b/contrib/spellcheck
deleted file mode 100755
index 20cbd82d9..000000000
--- a/contrib/spellcheck
+++ /dev/null
@@ -1,22 +0,0 @@
-#!/bin/bash
-
-dir="$(dirname "$0")"
-
-find src \( -name '*.cpp' -o -name '*.h' \) \! -path 'src/prop/minisat/*' \! -path 'src/prop/bvminisat/*' \! -path 'src/parser/*/generated/*' |
-  while read f; do
-    misspelled_words=`
-    $dir/extract-strings-and-comments $f |
-      ispell -a -W 3 2>/dev/null |
-      tail -n +2 |
-        while read s; do
-          case "$s" in
-            \**|\+*|-*) ;;
-            \&*|\#*|\?*) echo "$s" | awk '{print$2}';;
-#           *) test -n "$s" && echo "UNKNOWN : $s";;
-          esac
-        done | sort -fu | sed 's,^,  ,'`
-    if [ -n "$misspelled_words" ]; then
-      echo "$f"
-      echo "$misspelled_words"
-    fi
-  done
diff --git a/contrib/sygus-v1-to-v2.sh b/contrib/sygus-v1-to-v2.sh
deleted file mode 100755
index 0d1ac17e4..000000000
--- a/contrib/sygus-v1-to-v2.sh
+++ /dev/null
@@ -1,21 +0,0 @@
-#!/bin/bash
-# This is a simple script for converting v1 sygus files to v2.
-
-# Show how to use the script
-if [[ "$#" < 3 || ! -f "$1" || ! -f "$2" ]]; then
-  echo "Usage: $0 [<path to cvc4>] [<path to sygus file>] [<path to output file>] [<additional cvc4 options>*]"
-  exit 1
-fi
-
-output=$("$1" "$2" --lang=sygus1 --dump-to="$3" --output-lang=sygus2 --dump=raw-benchmark --preprocess-only "${@:4}" 2>&1)
-
-exitCode=$?
-
-if [[ "$exitCode" == 0 ]]; then
-  # Remove incremental and produce-models options
-  sed -i '/(set-option :incremental false)/d' "$3"
-  sed -i '/(set-option :produce-models "true")/d' "$3"
-else
-  echo "$1 failed with exit code $exitCode:"
-  echo "$output"
-fi
diff --git a/contrib/test_install_headers.sh b/contrib/test_install_headers.sh
deleted file mode 100755
index 6f6855e31..000000000
--- a/contrib/test_install_headers.sh
+++ /dev/null
@@ -1,36 +0,0 @@
-#!/bin/bash
-# contrib/test_install_headers.sh
-# Tim King <taking@google.com> for the CVC4 project, 24 December 2015
-#
-# ./contrib/test_install_headers.sh <INSTALL>
-#
-# This files tests the completeness of the public headers for CVC4.
-# Any header marked by #include "cvc4_public.h" in either the builds/
-# or src/ directory is installed into the path INSTALL/include/cvc4 where
-# INSTALL is set using the --prefix=INSTALL flag at configure time.
-# This test uses find to attempt to include all of the headers in
-# INSTALL/include/cvc4 and compiles a simple cpp file.
-
-INSTALLATION=$1
-CXX=g++
-LDFLAGS=-lcln
-CXXFILE=test_cvc4_header_install.cpp
-OUTFILE=test_cvc4_header_install
-
-echo $INSTALLATION
-
-echo "Generating $CXXFILE"
-find $INSTALLATION/include/cvc4/ -name *.h -printf '%P\n' | \
-		 awk '{ print "#include <cvc4/" $0 ">"}' > $CXXFILE
-echo "int main() { return 0; }" >> $CXXFILE
-
-echo "Compiling $CXXFILE into $OUTFILE"
-echo "$CXX -I$INSTALLATION/include -L$INSTALLATION/lib $LDFLAGS -o $OUTFILE $CXXFILE"
-$CXX -I$INSTALLATION/include -L$INSTALLATION/lib $LDFLAGS -o $OUTFILE $CXXFILE
-
-read -p "Do you want to delete $CXXFILE and $OUTFILE? [y/n]" yn
-case $yn in
-		[Nn]* ) exit;;
-		[Yy]* ) rm "$OUTFILE" "$CXXFILE";;
-		* ) echo "Did not get a yes or no answer. Exiting."; exit;;
-esac
diff --git a/contrib/theoryskel/README.WHATS-NEXT b/contrib/theoryskel/README.WHATS-NEXT
deleted file mode 100644
index 213004d5b..000000000
--- a/contrib/theoryskel/README.WHATS-NEXT
+++ /dev/null
@@ -1,46 +0,0 @@
-Congratulations, you now have a new theory of $dir !
-
-Your next steps will likely be:
-
-* to specify theory constants, types, and operators in your \`kinds' file
-* to add typing rules to theory_$dir_type_rules.h for your operators
-  and constants
-* to write code in theory_$dir_rewriter.h to implement a normal form
-  for your theory's terms; in particular, you should ensure that you
-  rewrite (= X X) to "true" for terms X of your theory's sorts, and
-  evaluate any constant terms
-* for any new types that you have introduced, add "mk*Type()" functions to
-  the NodeManager and ExprManager in src/expr/node_manager.{h,cpp} and
-  src/expr/expr_manager_template.{h,cpp}.  You may also want "is*()" testers
-  in src/expr/type_node.h and a corresponding Type derived class in
-  src/expr/type.h.
-* to write parser rules in src/parser/cvc/Cvc.g to support the CVC input
-  language, src/parser/smt/Smt.g to support the (deprecated) SMT-LIBv1
-  language, and src/parser/smt2/Smt2.g to support SMT-LIBv2
-* to write printer code in
-src/printer/*/*_printer* to support printing
-  your theory terms and types in various output languages
-
-and finally:
-
-* to implement a decision procedure for your theory by implementing
-  Theory$camel::check() in theory_$dir.cpp. Before writing the actual
-  code, you will need :
-
-  * to determine which data structures are context dependent and use for
-    them context-dependent data structures (context/cd*.h)
-  * to choose which work will be done at QUICK_CHECK, STANDARD or at
-    FULL_EFFORT.
-
-You'll probably find the Developer's wiki useful:
-
-  http://cvc4.cs.stanford.edu/wiki/
-
-...and the Developer's Guide:
-
-  https://github.com/CVC4/CVC4/wiki/Developer-Guide
-
-which contains coding guidelines for the CVC4 project.
-
-Good luck, and please contact cvc4-devel@cs.stanford.edu for assistance
-should you need it!
diff --git a/contrib/theoryskel/kinds b/contrib/theoryskel/kinds
deleted file mode 100644
index 23e90c19a..000000000
--- a/contrib/theoryskel/kinds
+++ /dev/null
@@ -1,21 +0,0 @@
-# kinds                                                               -*- sh -*-
-#
-# For documentation on this file format, please refer to
-# src/theory/builtin/kinds.
-#
-
-theory THEORY_$id ::CVC4::theory::$dir::Theory$camel "theory/$dir/theory_$dir.h"
-typechecker "theory/$dir/theory_$dir_type_rules.h"
-rewriter ::CVC4::theory::$dir::Theory$camelRewriter "theory/$dir/theory_$dir_rewriter.h"
-
-properties check
-
-# Theory content goes here.
-
-# constants...
-
-# types...
-
-# operators...
-
-endtheory
diff --git a/contrib/theoryskel/theory_DIR.cpp b/contrib/theoryskel/theory_DIR.cpp
deleted file mode 100644
index 06307f4e7..000000000
--- a/contrib/theoryskel/theory_DIR.cpp
+++ /dev/null
@@ -1,46 +0,0 @@
-#include "theory/$dir/theory_$dir.h"
-
-using namespace std;
-
-namespace CVC4 {
-namespace theory {
-namespace $dir {
-
-/** Constructs a new instance of Theory$camel w.r.t. the provided contexts. */
-Theory$camel::Theory$camel(context::Context* c,
-                           context::UserContext* u,
-                           OutputChannel& out,
-                           Valuation valuation,
-                           const LogicInfo& logicInfo) :
-    Theory(THEORY_$id, c, u, out, valuation, logicInfo) {
-}/* Theory$camel::Theory$camel() */
-
-void Theory$camel::check(Effort level) {
-  if (done() && !fullEffort(level)) {
-    return;
-  }
-
-  TimerStat::CodeTimer checkTimer(d_checkTime);
-
-  while(!done()) {
-    // Get all the assertions
-    Assertion assertion = get();
-    TNode fact = assertion.assertion;
-
-    Debug("$dir") << "Theory$camel::check(): processing " << fact << std::endl;
-
-    // Do the work
-    switch(fact.getKind()) {
-
-    /* cases for all the theory's kinds go here... */
-
-    default:
-      Unhandled(fact.getKind());
-    }
-  }
-
-}/* Theory$camel::check() */
-
-}/* CVC4::theory::$dir namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/contrib/theoryskel/theory_DIR.h b/contrib/theoryskel/theory_DIR.h
deleted file mode 100644
index d8e652b7c..000000000
--- a/contrib/theoryskel/theory_DIR.h
+++ /dev/null
@@ -1,34 +0,0 @@
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__$id__THEORY_$id_H
-#define __CVC4__THEORY__$id__THEORY_$id_H
-
-#include "theory/theory.h"
-
-namespace CVC4 {
-namespace theory {
-namespace $dir {
-
-class Theory$camel : public Theory {
-public:
-
-  /** Constructs a new instance of Theory$camel w.r.t. the provided contexts. */
-  Theory$camel(context::Context* c,
-               context::UserContext* u,
-               OutputChannel& out,
-               Valuation valuation,
-               const LogicInfo& logicInfo);
-
-  void check(Effort);
-
-  std::string identify() const {
-    return "THEORY_$id";
-  }
-
-};/* class Theory$camel */
-
-}/* CVC4::theory::$dir namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__$id__THEORY_$id_H */
diff --git a/contrib/theoryskel/theory_DIR_rewriter.h b/contrib/theoryskel/theory_DIR_rewriter.h
deleted file mode 100644
index 16859bc23..000000000
--- a/contrib/theoryskel/theory_DIR_rewriter.h
+++ /dev/null
@@ -1,86 +0,0 @@
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__$id__THEORY_$id_REWRITER_H
-#define __CVC4__THEORY__$id__THEORY_$id_REWRITER_H
-
-#include "theory/rewriter.h"
-
-namespace CVC4 {
-namespace theory {
-namespace $dir {
-
-class Theory$camelRewriter {
-public:
-
-  /**
-   * Rewrite a node into the normal form for the theory of $dir.
-   * Called in post-order (really reverse-topological order) when
-   * traversing the expression DAG during rewriting.  This is the
-   * main function of the rewriter, and because of the ordering,
-   * it can assume its children are all rewritten already.
-   *
-   * This function can return one of three rewrite response codes
-   * along with the rewritten node:
-   *
-   *   REWRITE_DONE indicates that no more rewriting is needed.
-   *   REWRITE_AGAIN means that the top-level expression should be
-   *     rewritten again, but that its children are in final form.
-   *   REWRITE_AGAIN_FULL means that the entire returned expression
-   *     should be rewritten again (top-down with preRewrite(), then
-   *     bottom-up with postRewrite()).
-   *
-   * Even if this function returns REWRITE_DONE, if the returned
-   * expression belongs to a different theory, it will be fully
-   * rewritten by that theory's rewriter.
-   */
-  static RewriteResponse postRewrite(TNode node) {
-
-    // Implement me!
-
-    // This default implementation
-    return RewriteResponse(REWRITE_DONE, node);
-  }
-
-  /**
-   * Rewrite a node into the normal form for the theory of $dir
-   * in pre-order (really topological order)---meaning that the
-   * children may not be in the normal form.  This is an optimization
-   * for theories with cancelling terms (e.g., 0 * (big-nasty-expression)
-   * in arithmetic rewrites to 0 without the need to look at the big
-   * nasty expression).  Since it's only an optimization, the
-   * implementation here can do nothing.
-   */
-  static RewriteResponse preRewrite(TNode node) {
-    // do nothing
-    return RewriteResponse(REWRITE_DONE, node);
-  }
-
-  /**
-   * Rewrite an equality, in case special handling is required.
-   */
-  static Node rewriteEquality(TNode equality) {
-    // often this will suffice
-    return postRewrite(equality).node;
-  }
-
-  /**
-   * Initialize the rewriter.
-   */
-  static inline void init() {
-    // nothing to do
-  }
-
-  /**
-   * Shut down the rewriter.
-   */
-  static inline void shutdown() {
-    // nothing to do
-  }
-
-};/* class Theory$camelRewriter */
-
-}/* CVC4::theory::$dir namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__$id__THEORY_$id_REWRITER_H */
diff --git a/contrib/theoryskel/theory_DIR_type_rules.h b/contrib/theoryskel/theory_DIR_type_rules.h
deleted file mode 100644
index 29be55686..000000000
--- a/contrib/theoryskel/theory_DIR_type_rules.h
+++ /dev/null
@@ -1,35 +0,0 @@
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__$id__THEORY_$id_TYPE_RULES_H
-#define __CVC4__THEORY__$id__THEORY_$id_TYPE_RULES_H
-
-namespace CVC4 {
-namespace theory {
-namespace $dir {
-
-class $camelTypeRule {
-public:
-
-  /**
-   * Compute the type for (and optionally typecheck) a term belonging
-   * to the theory of $dir.
-   *
-   * @param check if true, the node's type should be checked as well
-   * as computed.
-   */
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
-                                     bool check)
-    throw (TypeCheckingExceptionPrivate) {
-
-    // TODO: implement me!
-    Unimplemented();
-
-  }
-
-};/* class $camelTypeRule */
-
-}/* CVC4::theory::$dir namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__$id__THEORY_$id_TYPE_RULES_H */
diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl
index 2ab350d24..a9bf1fe0b 100755
--- a/contrib/update-copyright.pl
+++ b/contrib/update-copyright.pl
@@ -110,7 +110,7 @@ if($#ARGV >= 0 && $ARGV[0] eq '-m') {
 
 my @searchdirs = ();
 if($#ARGV == -1) {
-  (chdir($dir."/..") && -f "src/include/cvc4_public.h") || die "can't find top-level source directory for cvc5";
+  (chdir($dir."/..") && -f "src/include/cvc5_public.h") || die "can't find top-level source directory for cvc5";
   my $pwd = `pwd`; chomp $pwd;
 
   print <<EOF;