[![License: BSD](
https://img.shields.io/badge/License-BSD%203--Clause-blue.svg)](
https://opensource.org/licenses/BSD-3-Clause)
-![CI](https://github.com/CVC4/CVC4/workflows/CI/badge.svg)
+![CI](https://github.com/cvc5/cvc5/workflows/CI/badge.svg)
[![Coverage](
- https://img.shields.io/endpoint?url=https://cvc4.cs.stanford.edu/downloads/builds/coverage/nightly-coverage.json)](
- https://cvc4.cs.stanford.edu/downloads/builds/coverage)
+ https://img.shields.io/endpoint?url=https://cvc5.stanford.edu/downloads/builds/coverage/nightly-coverage.json)](
+ https://cvc5.stanford.edu/downloads/builds/coverage)
-CVC4
+cvc5
===============================================================================
-CVC4 is a tool for determining the satisfiability of a first order formula
+cvc5 is a tool for determining the satisfiability of a first order formula
modulo a first order theory (or a combination of such theories). It is the
-fourth in the Cooperating Validity Checker family of tools (CVC, CVC Lite,
-CVC3) but does not directly incorporate code from any previous version.
+fifth in the Cooperating Validity Checker family of tools (CVC, CVC Lite,
+CVC3, CVC4) but does not directly incorporate code from any previous version
+prior to CVC4.
-If you are using CVC4 in your work, or incorporating it into software of your
+If you are using cvc5 in your work, or incorporating it into software of your
own, we invite you to send us a description and link to your
project/software, so that we can link it on our [Third Party
-Applications](https://cvc4.github.io/third-party-applications.html) page.
+Applications](https://cvc5.github.io/third-party-applications.html) page.
-CVC4 is intended to be an open and extensible SMT engine. It can be used as a
+cvc5 is intended to be an open and extensible SMT engine. It can be used as a
stand-alone tool or as a library. It has been designed to increase the
performance and reduce the memory overhead of its predecessors. It is written
entirely in C++ and is released under an open-source software license (see file
-[COPYING](https://github.com/CVC4/CVC4/blob/master/COPYING)).
+[COPYING](https://github.com/cvc5/cvc5/blob/master/COPYING)).
Website
-------------------------------------------------------------------------------
-CVC4's website is available at:
-http://cvc4.cs.stanford.edu/
+cvc5's website is available at:
+https://cvc5.github.io/
Documentation
-------------------------------------------------------------------------------
-Documentation for users of CVC4 is available at:
-http://cvc4.cs.stanford.edu/
+Documentation for users of cvc5 is available at:
+https://cvc5.github.io/docs/
Documentation for developers is available at:
-https://github.com/CVC4/CVC4/wiki/Developer-Guide
+https://github.com/cvc5/cvc5/wiki/Developer-Guide
Download
-------------------------------------------------------------------------------
-The latest version of CVC4 is available on GitHub:
-https://github.com/CVC4/CVC4
+The latest version of cvc5 is available on GitHub:
+https://github.com/cvc5/cvc5
-Source tar balls and binaries for releases and latest stable builds of the
-[master branch](https://github.com/CVC4/CVC4) on GitHub can be
-found [here](http://cvc4.cs.stanford.edu/downloads).
+Source tar balls and binaries for releases of the
+[master branch](https://github.com/cvc5/cvc5) can be
+found [here](https://github.com/cvc5/cvc5/releases).
+Nightly builds are available [here](https://cvc5.github.io/downloads).
Build and Dependencies
-------------------------------------------------------------------------------
-CVC4 can be built on Linux and macOS. For Windows, CVC4 can be cross-compiled
+cvc5 can be built on Linux and macOS. For Windows, cvc5 can be cross-compiled
using Mingw-w64.
For detailed build and installation instructions on these platforms,
-see file [INSTALL.md](https://github.com/CVC4/CVC4/blob/master/INSTALL.md).
+see file [INSTALL.rst](https://github.com/cvc5/cvc5/blob/master/INSTALL.rst).
Bug Reports
-------------------------------------------------------------------------------
-If you need to report a bug with CVC4, or make a feature request, please visit
-our bugtracker at our [GitHub issues](https://github.com/CVC4/CVC4/issues)
-page. We are very grateful for bug reports, as they help us improve CVC4.
+If you need to report a bug with cvc5, or make a feature request, please visit
+our bugtracker at our [GitHub issues](https://github.com/cvc5/cvc5/issues)
+page. We are very grateful for bug reports, as they help us improve cvc5.
Contributing
-------------------------------------------------------------------------------
For a full list of authors, please refer to the
-[AUTHORS](https://github.com/CVC4/CVC4/blob/master/AUTHORS) file.
+[AUTHORS](https://github.com/cvc5/cvc5/blob/master/AUTHORS) file.