===============================================================================
                         The veriT SMT solver
                         General informations
===============================================================================

About
=====

The veriT solver provides a complete satisfiability procedure for
quantifier-free formulas with uninterpreted functions and linear arithmetics on
real numbers. It also comes with incomplete procedures for formulas with
non-linear rational arithmetics [1], linear integer arithmetics and
quantifiers. For some logics, veriT has the capability to build proofs which
may then be reused or checked by external tools.

veriT is available under the BSD license.  It has a front-end for the SMTLIB-2
language (documented at http://www.smtlib.org), but does not support
sophisticated interactions through the SMT command language.

[1] Support for non-linear rational arithmetics is provided through interaction
with Redlog (http://www.redlog.eu).  To enable this support, Redlog must be
installed in the sub-directory extern/reduce.


Installation
============

Compilation and installation instructions are in the INSTALL file.

Documentation is available in man, html and latex formats in the directories
doc/user/verit and doc/user/librv.

Usage
=====

The following command prints a list of the available options and a short
description of each option:

  % verit --help

Please notice that symbol names beginning with veriT__ are reserved.


Source organization
===================

Here is a small description of what you will find under each subdirectory:
- src: veriT's source code
- extern: third-party software source and binaries
- doc: veriT's user documentation
