This file contains a summary of important user-visible changes.

cvc5 1.3.2
==========

## Changes

- Fixes a bug related to variable elimination for quantified formulas that have
  variable shadowing.
- We now use a more efficient version of resolution by default in CPC proofs
  (proof rule `CHAIN_M_RESOLUTION`) for representing SAT proofs from Minisat.
- CPC proofs now have no mixed arithmetic by default.
- Updates to the linear and non-linear arithmetic solver, including a new
  lemma schema for multiplication (`--nl-ext-flatten-mon`), as well as
  minor improvements to the Diophantine Equation solver.
- Minor updates and fixes to the CPC proof signature. The current CPC proofs are
  checkable by Ethos 0.2.2 (`./contrib/get-ethos-checker`).

cvc5 1.3.1
==========

## Changes

- **API**
  * The C++ methods `Term TermManager::mkString(const std::wstring& s)` and
    `std::wstring Term::getStringValue()` are now deprecated in favor of
    the new methods `Term TermManager::mkString(const std::u32string& s)` and
    `std::u32string Term::getU32StringValue()` which use `std::u32string`
    to represent Unicode strings instead of `std::wstring`.
    Unlike `std::wstring`, whose character type `wchar_t` is 16 bits on
    Windows and 32 bits on Linux and macOS, the character type of
    `std::u32string`, `char32_t`, is guaranteed to be at least 32 bits on
    all platforms.
    Similarly, the C API functions `cvc5_mk_string_from_wchar` and
    `cvc5_term_get_string_value` are now deprecated in favor of
    the new functions `cvc5_mk_string_from_char32` and
    `cvc5_term_get_u32string_value`.
- A build configuration `stable-mode` is available via our configure script.
  Similar to the build configuration `safe-mode`, this configuration guards
  against all cvc5 features that are not robust, but in constrast it does not
  guarantee full proof and model support.
- Minor updates to the CPC proof signature. The current CPC proofs are checkable
  by Ethos 0.2.1 (`./contrib/get-ethos-checker`).

cvc5 1.3.0
==========

## New Features

- A build configuration `safe-mode` is available via our configure script
  which guards all cvc5 features that are either not robust or do not have
  full proof and model support. It is also possible to guard against these
  features using the command line option `--safe-mode=safe`. The definition
  of what is allowable in safe mode coincides with our fuzzing guidelines,
  see https://github.com/cvc5/cvc5/wiki/Fuzzing-cvc5.
- We have significantly increased coverage of proofs in the Cooperating Proof
  Calculus (CPC) proof format. In particular, we expect that CPC proofs are
  complete for *all* theories and features allowed in safe mode. These proofs
  may be obtained by the `(get-proof)` SMT-LIB command, or via the API using
  the method `Solver::getProof`, and are checkable by Ethos 0.2.0
  (`./contrib/get-ethos-checker`).
- We now support the SMT-LIB version 2.7 standard syntax for arithmetic
  bit-vector conversion functions whose smt2 syntax is `int_to_bv`, `ubv_to_int`
  and `sbv_to_int`. The first maps to the existing kind `Kind::INT_TO_BITVECTOR`.
  The kinds `Kind::BITVECTOR_UBV_TO_INT` and `Kind::BITVECTOR_SBV_TO_INT`
  are added to the API for the latter two. Note the syntax `int2bv` and `bv2nat`
  as well as the kind `Kind::BITVECTOR_TO_NAT` are now deprecated.

## Changes

- Bumped CaDiCaL to version 2.1.3.
- The proof granularity is now `dsl-rewrite` by default. The regression test
  `make regress-dsl-proof` is deleted and is now equivalent to
  `make regress-proof`.
- Following the SMT-LIB standard, we now print parentheses around all proof
  outputs.
- The option `--safe-options` is renamed to `--safe-mode=safe`. We additionally
  support the option `--safe-mode=stable`, which disables experimental
  features but does not insist on complete proofs or models.
- The quantifier instatiation strategy `--mbqi-fast-sygus` has been renamed to
  `--mbqi-enum`.
- **API**
  + Added support for multiple `TermManager` instances within the same thread and
    across threads. Previously, all `TermManager` objects in a thread shared
    a single memory reference and could not be shared across threads.
    Instances can now be shared across threads, but they are not thread-safe and
    must be protected from concurrent access.


cvc5 1.2.1
==========

## New Features

- Updates to the `cpc` proof signature. The 0.1.1 release of Ethos can check
  proofs generated by this version of cvc5 (`./contrib/get-ethos-checker`).

- Increased coverage for proofs, in particular for theories allowed by
  `--safe-options`.

- Added support for `SymbolManager::getNamedTerms()` to retrieve the set of
  terms that have been given names by the SMT-LIB attribute `:named`.

- Added option `--parsing-mode` to allow configuration of both more strict but
  also more lenient parsing than default. Already existing option
  `--strict-parsing` is an alias `--parsing-mode=strict`.
  Parsing symbols that start with `.` or `@` (used for internally freshly
  introduced symbols) in lenient parsing mode (`--parsing-mode=lenient`).

## Changes

- The option `--safe-options` now **disables experimental** theories and their
  extensions in cvc5. This includes the theory of bags, the theory of finite
  fields, the theory of separation logic, higher-order extensions to the theory
  of equality, as well as extensions of the theory of arithmetic for
  transcendental functions, integer-and, and power functions, and the theory of
  arrays for constant arrays. These theories are still enabled by default and
  further more can be used in combination with safe options by the options e.g.
  `--arith-exp` **prior** to setting `--safe-options`.

- Renamed the flag `--sets-ext` to `--sets-exp`, which enables non-standard
  extensions of the sets theory.

- Fixed a soundness bug in the solver for `set.filter`.

- When printing with tags `-o pre-asserts` or `-o post-asserts`, by default we
  now ensure that declarations are printed in a deterministic order.

- Bumped CaDiCaL to version 2.0.0.


cvc5 1.2.0
==========

## New Features

- New **C API**, implemented as a thin wrapper around the C++ API.
   - Documentation: https://cvc5.github.io/docs-ci/docs-main/api/c/c.html
   - Examples: https://github.com/cvc5/cvc5/tree/main/examples/api/c

- Exposed creation and maintenance of **Skolem functions** to the API. Skolem
  functions are symbols that are internally introduced by cvc5 during solving.
  They are formalized via an identifier (see
  https://cvc5.github.io/docs-ci/docs-main/skolem-ids.html for details) as well
  as a (possibly empty) set of indices.
  + The **API** methods `Term::isSkolem()`, `Term::getSkolemId()`, and
    `Term::getSkolemIndices()`may now be used to identify terms corresponding
    to skolems.

- We now export kinds `BITVECTOR_FROM_BOOLS`, `BITVECTOR_BIT`, `DIVISION_TOTAL`,
  `INTS_DIVISION_TOTAL`, `INTS_MODULUS_TOTAL` which may appear in terms
  resulting from simplification or terms appearing in proofs.

- Proof rules corresponding to rewrite rules are now exported in the API via
  the enum `ProofRewriteRule`.

- A new `Plugin` class is available in our API. This class allows a user
  to be notified when SAT clauses or theory lemmas are learned internally
  by cvc5. The plugin class also contains a callback for the user to introduce
  new learned clauses into the state of cvc5 during solving.

- Added a new strategy `--mbqi-fast-sygus` (disabled by default) for **quantifier
  instantiation** which uses SyGuS enumeration to augment instantiations from
  model-based quantifier instantiation.

## Changes

- We now require CMake >= 3.16.

- **API**
  All APIs have been refactored to expose a TermManager to the API. A term
  manager manages creation and maintenance of all terms and sorts (across
  potentially several solver instances within a thread).
  Corresponding functions that were previously associated with a solver
  instance and are now associated with a term manager are now deprecated
  and will be removed in a future release.
  * Python:
    - Constructor `SymbolManager(Solver)` is now deprecated and replaced
      by `SymbolManager(TermManager)`.
  * Pythonic:
    - Unsat cores and proofs are now available via the `Solver` methods
      `unsat_core()` and `proof()`, respectively.

- The default proof format of cvc5 has been renamed to the
  **Cooperating Proof Calculus (CPC) proof format**. This proof format coincides
  with proof objects in our API.
  * **API**
    + The option `--proof-format=cpc` prints proofs in the CPC format.
      This option is now enabled by default.
  * The **Ethos** proof checker is available, which can check proofs in this
    format. In particular, the 0.1.0 release of Ethos can check proofs generated
    by this version of cvc5. This checker is the second generation of the
    AletheLF checker (`alfc`). Ethos inherits the code base of alfc and is based
    on a logical framework called **Eunoia** (formerly called AletheLF).
    See https://github.com/cvc5/ethos for more details. Note that the
    development version of Ethos is available for download via the script
    `./contrib/get-ethos-checker`, which will be kept in sync with further
    development versions of cvc5.
  * The rules of this format have been formalized in Eunoia and are available
    in the cvc5 repository under the directory `./proofs/eo/cpc/`.

- The semantics of `SQRT` was changed to assume the result is positive.

- Fixed a bug involving how sequence terms are printed in model values.


cvc5 1.1.2
==========

## New Features

- Added support for **nullable** sorts and lift operator to the theory of
  **datatypes**.

- Added a new strategy `--sub-cbqi` (disabled by default) for **quantifier
  instantiation** which uses subsolvers to compute unsat cores of instantiations
  that are used in proofs of unsatisfiability.

- Add support for the kind `BITVECTOR_NEGO` corresponding to bitvector
  negation overflow detection.

## Changes

- SAT clauses are no longer marked as removable in MiniSat. This change
  **improves performance** overall on quantifier-free logics with arithmetic and
  strings.
- **API**
  * Functions `kindToString(Kind)` and `sortKindToString(SortKind)` are now
    deprecated and replaced by `std::to_string(Kind)` and
    `std::to_string(SortKind)`. They will be removed in the next minor release.
- Minor changes to the output format for proofs. Proofs in the AletheLF
  proof format generated by cvc5 now correspond directly to their representation
  in proof objects obtained in via the API (the `Proof` class). Moreover,
  proofs now use SMT-LIB compliant syntax for quantified formulas and unary
  arithmetic negation.
- The option `--safe-options` now disallows cases where more than one regular
  option is used.
- Fixes the parsing of `define-fun-rec` and `define-funs-rec` in interactive
  mode.
- Renamed `bag.duplicate_removal` to `bag.setof`.
- Improvements to handling of constant production rules (`Constant`) in SyGuS
  grammars.

cvc5 1.1.1
==========

## New Features

- Added support for **forward declarations** (feature `:fwd-decls`) in **SyGuS**
  inputs. This allows functions-to-synthesize to include previous
  functions-to-synthesize in their grammars. This feature is enabled by default
  for all SyGuS inputs.

## Changes

- Fixed a bug when piping input from stdin, which caused cvc5 to have degraded
  performance. This bug could also cause cvc5 to throw spurious parser errors.


cvc5 1.1.0
==========

## New Features

- **API**
  * The **signature** of functions `Solver::mkFiniteFieldSort(const std::string&)`
    and `Solver::mkFiniteFieldElem(const std::string&, const Sort&)` is now
    extended with an additional (optional) parameter to
    `Solver::mkFiniteFieldSort(const std::string& size, uint32_t base)` and
    `Solver::mkFiniteFieldElem(const string& value, const Sort& sort, uint32_t base)`
    to configure the base of the string representation of the given string
    parameters.
  * A **new API for proofs** is available. The new `Proof` class represents a node
    of the proof tree. Function
    `Solver::getProof(modes::ProofComponent c = modes::ProofComponent::FULL)`
    returns the root proof nodes of a proof component as a vector. Function
    `Solver::proofToString(std::vector<Proof> proof, modes::ProofFormat format, modes::ProofComponent component)`
    can be used to print proof components to a string with a specified proof
    format.
  * Added support for **parsing** inputs from file, string, or input stream. We
    provide an `InputParser`, `SymbolManager`, and `Command` class for reading
    inputs (see `include/cvc5_parser.h`). Example use cases of these classes
    are available at https://cvc5.github.io/docs/cvc5-1.1.1/examples/parser.html
    and https://cvc5.github.io/docs/cvc5-1.1.1/examples/parser_sym_manager.html.
    These interfaces are also available in the Java and Python APIs.
  * Added a variant of **timeout cores** that accepts a set of assumptions. This
    is available via the API method `Solver::getTimeoutCoreAssuming` or the
    SMT-LIB command `get-timeout-core-assuming`, which accept a list of
    formulas to assume, while all current assertions are implicitly included
    in the core.
  * Added new method `Solver::getUnsatCoreLemmas` which returns the set of
    theory lemmas that were relevant to showing the last query was
    unsatisfiable. This is also avialable via the SMT-LIB command
    `get-unsat-core-lemmas`.

- Support for the **AletheLF (ALF) proof format**. This format combines the
  strengths of the Alethe and LFSC proof formats, namely it borrows much of the
  syntax of Alethe, while being based on a logical framework like LFSC.
  * **API**
    + The option `--proof-format=alf` prints proofs in the AletheLF format.
      This option is enabled by default.
  * The ALF proof checker (alfc) is available for download via the script
    `./contrib/get-alf-checker`.

- **CaDiCaL** is now integrated via the IPASIR-UP interface as **CDCL(T) SAT
  solver**. The CDCL(T) SAT solver can be configured via option `--sat-solver`.
  Currently, MiniSat is still default. Note that CaDiCaL cannot be used as the
  CDCL(T) SAT engine when proof production is enabled. In that case, option
  `--sat-solver` will default back to MiniSat.

## Changes

- Various bug fixes.


cvc5 1.0.9
==========

Note: This is a pre-release version for the upcoming version 1.1.0.

## New Features

- **API**
  + Added the ability to query the logic that has been set in the solver via
    `Solver::isLogicSet` and `Solver::getLogic`.

## Changes

- **SMT-LIB**
  * The syntax for 0-ary tuples has been changed for the purposes of
    disambiguation. The new syntax for 0-ary tuple sort is `UnitTuple` whose
    0-ary constructor is `tuple.unit` (the previous syntax had overloaded
    `Tuple` and `tuple`, with no arguments).


cvc5 1.0.8
==========

Note: This is a pre-release version for the upcoming version 1.1.0.

## Changes

- **API**
  + C++ enums are now enum classes
  + Added argument `fresh` to `Solver::declareFun` which distinguishes whether
    the solver should construct a new term or (when applicable) return a
    term constructed with the same name and sort. An analogous flag is added
    to `Solver::declareSort`. The option `--fresh-declarations` determines
    whether the parser constructs fresh terms and sorts for each declaration
    (true by default, which matches the previous behavior).


cvc5 1.0.7
==========

## Changes

- Various bug fixes

cvc5 1.0.6
==========

## New Features

- **API**
  + New API function `Solver::mkFloatingPoint(const Term& sign, const Term& exp, const Term& sig)`,
  returns a floating-point value from the three IEEE-754 bit-vector value.
  + Added support for querying the values of real algebraic numbers in the API.
    In particular, the methods
    `Term::isRealAlgebraicNumber()`,
    `Term::getRealAlgebraicNumberDefiningPolynomial()`,
    `Term::getRealAlgebraicNumberLowerBound()`, and
    `Term::getRealAlgebraicNumberUpperBound()` may now be used to query the
    contents of terms corresponding to real algebraic numbers.

- Support for timeout cores
  * **API**
    + New API function `Solver::getTimeoutCore()` when applicable returns a
      subset of the current assertions that cause the solver to timeout without
      a provided timeout (option `--timeout-core-timeout`).
  * **SMT-LIB**
    + New command `(get-timeout-core)` which invokes the above method.

- Support for new interfaces to the SyGuS solver.
  * **API**
    + New API function `Solver::findSynth` which takes an identifier specifying
      a target term to synthesize and (optionally) a grammar. This method can
      be used to directly enumerate terms in a provided grammar
      (`FindSynthTarget::ENUM`), or as a way of finding other terms of interest,
      e.g,. a rewrite rule that is applicable to the current set of assertions
      (`FindSynthTarget::REWRITE_INPUT`).
    + New API function `Solver::findSynthNext` which gets the next term in the
      enumeration.
  * **SMT-LIB**
    + New commands `find-synth` and `find-synth-next` which invoke the above
      methods.

## Changes

- Removed support for the ANTLR parser and parsing for the TPTP language.
      components.
- **API**
  + Simplified the `Solver::mkTuple` method. The sorts of the elements no longer
    need to be provided.
  + Option `--print-unsat-cores-full` has been renamed to `--print-cores-full`.
    Setting this option to true will print all assertions in the unsat core,
    regardless of whether they are named. This option also impacts how timeout
    cores are printed.
  + Removed API support for the deprecated SyGuS 2.0 command `Solver::synthInv`.
    This method is equivalent to `Solver::synthFun` with a Boolean range sort.


cvc5 1.0.5
==========

## New Features

- A new (hand-written) parser is available and enabled by default.
  * **Note**: the previous parser can be enabled using command line options
    `--no-flex-parser --no-stdin-input-per-line`. These options will be
    available until version 1.1 is released.


cvc5 1.0.4
==========

## New Features

- Support for the theory of (prime-order) **finite fields**:
  * Sorts are created with
    * C++: `Solver::makeFiniteFieldSort`
    * SMT-LIB: `(_ FiniteField P)` for prime order `P`
  * Constants are created with
    * C++: `Solver::makeFiniteFieldElem`
    * SMT-LIB: `(as ffN F)` for integer `N` and field sort `F`
  * The operators are multiplication, addition and negation
    * C++: kinds `FF_MUL`, `FF_ADD`, and `FF_NEG`
    * SMT-LIB: operators `ff.mul`, `ff.add`, and `ff.neg`
  * The only predicate is equality


cvc5 1.0.3
==========

## New Features

- **API**
  * New API function `Solver::getVersion()`, returns a string representation
    of the solver version.
- Support for **bit-vector overflow** detection operators:
  * `BITVECTOR_UADDO` unsigned addition overflow detection
  * `BITVECTOR_SADDO` signed addition overflow detection
  * `BITVECTOR_UMULO` unsigned multiplication overflow detection
  * `BITVECTOR_SMULO` signed multiplication overflow detection
  * `BITVECTOR_USUBO` unsigned subtraction overflow detection
  * `BITVECTOR_SSUBO` signed subtraction overflow detection
  * `BITVECTOR_SDIVO` signed division overflow detection
- Support for **Web Assembly** compilation using Emscripten.

## Changes

- The (non-standard) operators `BITVECTOR_TO_NAT` and `INT_TO_BITVECTOR` now
  belong to the UF theory. A logic that includes UF is required to use them.
- The sort for (non-standard) bit-vector operators `BITVECTOR_REDAND` and
  `BITVECTOR_REDOR` is now `(_ BitVec 1)` (was Boolean), following the
  definition of reduction operators in Verilog (their origin).
- Reenable functionality that allows `(get-model)` commands after answering
  `unknown` when `:produce-models` is set to `true`. Note that there is no
  guarantee that building a model succeeds in this case.


cvc5 1.0.2
==========

## Changes

- **API**
  * Previously, it was not possible to share Sort, Term, Op, Grammar and
    datatype objects between Solver instances. This is now allowed for solvers
    that belong to the same thread.


cvc5 1.0.1
==========

## New Features

- Support for cross-compiling an **ARM** binary of cvc5 on x86 macOS.
- Support for declaring **oracle functions** in the API via the method
  `declareOracleFun`. This allows users to declare functions whose semantics
  are associated with a provided executable implementation.

## Changes

- Removed support for non-standard `declare-funs`, `declare-consts`, and
  `declare-sorts` commands.
- The kind for integer constants is now `CONST_INTEGER`, while real constants
  continue to have kind `CONST_RATIONAL`.
- Type rules for (dis)equality and if-then-else no longer allow mixing
  integers and reals. Type rules for other operators like `APPLY_UF` now
  require their arguments to match the type of the function being applied, and
  do not assume integer/real subtyping.
- The API method `mkTuple` no longer supports casting integers to reals when
  constructing tuples.


cvc5 1.0
=========

## Website

https://cvc5.github.io

## Documentation

https://cvc5.github.io/docs

## System Description
**cvc5: A Versatile and Industrial-Strength SMT Solver.**  
Barbosa H., Barrett C., Brain M., Kremer G., Lachnitt H., Mann M., Mohamed A.,
Mohamed M., Niemetz A., Nötzli A., Ozdemir A., Preiner M., Reynolds A., Sheng
Y., Tinelli C., and Zohar Y., TACAS 2022.
[http://dx.doi.org/10.1007/978-3-030-99524-9_24](http://dx.doi.org/10.1007/978-3-030-99524-9_24)

## New Features

### Streamlined C++ API

Documentation: https://cvc5.github.io/docs/latest/api/cpp/cpp.html

### Two new Python language bindings

- Base module: Feature complete with C++ API
- Pythonic module: A pythonic wrapper around the base module
- Documentation: https://cvc5.github.io/docs/latest/api/python/python.html

### New Java language bindings

Documentation: https://cvc5.github.io/docs/latest/api/java/java.html

### Theory of Bags (Multisets)

A new theory of bags, which are collections that allow duplicates. It
supports basic operators like union disjoint, union max, intersection,
difference subtract, difference remove, duplicate removal, and multiplicity
of an element in a bag.

### Theory of Sequences
- A new parametric theory of sequences whose syntax is compatible with the
  syntax for sequences used by Z3.
- A new array-inspired procedure (option `--seq-array`).

### Arithmetic

Nonlinear real arithmetic is now solved using a new solver based on
cylindrical algebraic coverings. Includes full support for non-rational
models and a number of options `--nl-cov-*` for, e.g., different projection
operators, Lazard's lifting or variable elimination.
The new solver requires the libpoly library, and Lazard's lifting
additionally requires CoCoALib.

### Arrays

Added support for an `eqrange` predicate. `(eqrange a b i j)` is true
if arrays `a` and `b` are equal on all indices within indices `i` and `j`.

### Bit-vectors
- New bit-vector solver with CaDiCaL as default SAT back-end.
- New approach for solving bit-vectors as integers (option `--solve-bv-as-int`).

### Datatypes
Support for generic datatype updaters `((_ update s) t u)` which replaces
the field specified by selector `s` of `t` by the value `u`.

### Integers

- Support for an integer operator `(_ iand n)` that returns the bitwise `and`
  of two integers, seen as integers modulo n.
- Support for an integer operator `int.pow2`, used as `(int.pow2 x)` which
  represents 2 to the power of x.

### Quantifiers
- Improved support for enumerative instantiation (option `--enum-inst`).
- SyGuS-based quantifier instantiation (option `--sygus-inst`).

### Strings

- Improved performance using new techniques, including model-based
  reductions, eager context-dependent simplification, and equality-based
  conflict finding.
- Support for `str.indexof_re(s, r, n)`, which returns the index of the first
  occurrence of a regular expression `r` in a string `s` after index `n` or
  -1 if `r` does not match a substring after `n`.

### Proofs

- Documentation available at:
  https://cvc5.github.io/docs/latest/proofs/proofs.html
- When used after an unsatisfiable response to `checkSat`, `getProof`
  returns a representation of the refutation proof for the current set of
  assertions (get-proof in SMT-LIB).
- Preliminary support for translations to external proof formats LFSC and Alethe.

### Difficulty Estimation

The API method `getDifficulty` returns a map from asserted formulas to
integers which estimates how much that formula contributed to the
difficulty of the overall problem (`get-difficulty` in SMT-LIB).

### Learned Literals

The API method `getLearnedLiterals` gets a list of literals that are
entailed by the current set of assertions that were learned during solving
(`get-learned-literals` in SMT-LIB).

### Abduction and Interpolation

- The API method `getAbduct` can be used to find an abduct for the current set
  of assertions and provided goal (get-abduct in SMT-LIB). Optionally, a
  SyGuS grammar can be provided to restrict the shape of possible abducts.
  If using the text inferace, the grammar may be provided using the same
  syntax for grammars as in SyGuS IF format.
- The API method `getInterpolant` can be used to find an interpolant for the
  current set of assertions and provided goal (get-interpolant in SMT-LIB).
  Like abduction, grammars may be provided to restrict the shape of
  interpolants.

### Support for Incremental Synthesis Queries

- The core SyGuS solver now supports getting multiple solutions for a
  synthesis conjecture via the API. The method `checkSynthNext` finds the
  next SyGuS solution to the current set of SyGuS constraints
  (`check-synth-next` in SyGuS IF).
- `getAbductNext` finds the next abduct for the current set of
  assertions and provided goal (`get-abduct-next` in SMT-LIB).
- `getInterpolantNext` finds the next interpolant for the current set of
  assertions and provided goal (`get-interpolant-next` in SMT-LIB).

### Pool-based Quantifier Instantiation

- The API method `declarePool` declares symbol sets of terms called pools
  (`declare-pool` in SMT-LIB).
- Pools can be used in annotations of quantified formulas for fine grained
  control over quantifier instantiations (`:inst-pool`, `:inst-add-to-pool`,
  `:skolem-add-to-pool` in SMT-LIB).

### Diagnostic Outputs

The option `-o TAG` can be used to enable a class of useful diagnostic
information, such as the state of the input formula before and after
pre-preprocessing, quantifier instantiations, literals learned
during solving, among others. For SyGuS problems, it can be used to
show candidate solutions and grammars that the solver has generated.

### Unsat cores
- Production modes based on the new proof infrastructure
  (`--unsat-cores-mode=sat-proof`) and on the solving-under-assumption
  feature of Minisat (`--unsat-cores-mode=assumptions`). The mode based on
  SAT assumptions + preprocessing proofs is the new default.
- Computing minimal unsat cores (option `--minimal-unsat-cores`).

### Blocking Models
- The API method `blockModels` can be used to block the current model using
  various policies for how to exclude the values of terms (`block-model` in
  SMT-LIB).
- The API method `blockModelValues` can be used to block the current model
  for a provided set of terms (`block-model-values` in SMT-LIB).

### Model Cores
- The API method `isModelCoreSymbol` can be used to query whether the value
  for a symbol was critical to whether the model satisfies the current set of
  assertions.
- Models can be limited to show only model core symbols (option `--model-cores`).

## Changes

* CaDiCaL and SymFPU are now required dependencies. CaDiCaL 1.4.1 is now the
  version used by default.
* Options have been extensively refactored, please refer to the cvc5
  documentation for further information.
* Removed support for the CVC language.
* SyGuS: Removed support for SyGuS-IF 1.0.
* Removed support for the (non-standard) `define` command.
* Removed the legacy API along with the Java and Python bindings for it.
* Interactive shell: the GPL-licensed Readline library has been replaced the
  BSD-licensed Editline. Compiling with `--best` now enables Editline, instead
  of Readline. Without selecting optional GPL components, Editline-enabled cvc5
  builds will be BSD licensed.
* The `competition` build type includes the dependencies used for SMT-COMP by
  default. Note that this makes this build type produce GPL-licensed binaries.
* Bit-vector operator `bvxnor` was previously mistakenly marked as
  left-assoicative in SMT-LIB. This has recently been corrected in SMT-LIB. We
  now restrict `bvxnor` to only allow two operands in order to avoid confusion
  about the semantics, since the behavior of n-ary operands to `bvxnor` is now
  undefined in SMT-LIB.
* SMT-LIB output for `get-model` command now conforms with the standard,
  and does *not* begin with the keyword `model`. The output
  is the same as before, only with this word removed from the beginning.
* Building with Python 2 is now deprecated.
* The SMT-LIB syntax for some extensions has been changed. Notably, set
  operators are now prefixed by `set.`, and relations by `rel.`. For example,
  `union` is now written `set.union`.
* Removed support for redundant logics `ALL_SUPPORTED` and `QF_ALL_SUPPORTED`,
  use `ALL` and `QF_ALL` instead.