# Changelog

veriT follows Calendar Versioning. Version numbers are of the form
YYYY.0M.MICRO i.e. year, zero-padded month, and patch level.
Compatibility is only assured between versions with the same year and
month. The performance on individual benchmarks might even fluctuate
between patch levels.

## [2021.06.1] - 2021-11-03

### Changes

- veriT now always returns with an error code 14 in case of a timeout and
  24 in case of a CPU timeout (when available).  This is independent of
  the operating system.

## [2021.06] - 2021-06-29

This release corresponds mostly to veriT as submitted to SMT-COMP 2021.
The timeout support for Windows and the proof format change were done
after the submission, but they should not affect solving performance.

### Proof Incompatibilities
- The contexts provided in anchors are now sorted.  Every variable of
  the substitution is printed with its sort.  The syntax corresponds
  to the SMT-LIB syntax used in variable lists, such as for `forall`.
  For example, instead of `(anchor :step t3 :args (x) (:= y x)))`, now
  `(anchor :step t3 :args ((x S) (:= (y S) x)))` is printed.

### Additions
- New preprocessing method: quantifier simplification by unification.
  It can be deactivated with `--disable-qsimp` and fine tuned with:
  `--qsimp-delete`, `--qsimp-eager`, `--qsimp-solitary`.
  For now, this method is not proof producing.
- Support `define-fun` when not in proof production mode.
- Support setting  a wallclock time limit on Windows using `--max-time`.
  Uses Timer Queues and forces a hard exit.  Hence, e.g, statistics will
  not be printed.
- Support setting a CPU time limit on systems with `setitimer` via
  `--max-virtual-time`.
- Recognize QF_LIRA.

### Bugfixes
- Fix compilation with -fno-common, the default in gcc10.

## [2020.10] - 2020-10-14

This release is motivated by the inclusion of veriT as a backend for proof
reconstruction in Isabelle.  It is the first release since 2016. Since
the last stable release of veriT, the solver has seen many changes. The
changes mainly affect quantifier instantiation and proof production.