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

## Unreleased

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

### Proof Incompatibilities
- The printing of sorts in the contexts was simplified.  Every fixed
  variable is printed with its sort, but the sort of proper substitution
  in the context must be inferred from the right hand side.  For example,
  instead of `(anchor :step t3 :args ((x S) (:= (y S) x)))`, now
  `(anchor :step t3 :args ((x S) (:= y x)))` is printed.  The sort of
  `y` is equivalent to the sort of `x`.

### Bugfixes
- Fix a portability issue by ensuring that our own sorting implementation
  is used everywhere.  Otherwise, the behaviour of veriT could depend on
  how equal values are ordered during sorting.
- Fix compilation of the tarball after invoking `make clean`.  During cleanup
  some generated files (such as the lexer) are deleted.  We now ship the source
  file for those generated files to allow recompilation.

## [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 fixed variable
  is printed with its sort.  The sort of proper substitution in the
  context can be inferred from the right hand side. 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 x)))` is printed.  The sort of
  `y` is equivalent to the sort of `x`.

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