This archive contains Ultimate.
Please direct any questions to one of the maintainers and/or consult the
websites.

Websites:
<https://github.com/ultimate-pa/ultimate>
<https://ultimate.informatik.uni-freiburg.de/>

Maintainers:
Daniel Dietsch (<dietsch@informatik.uni-freiburg.de>)
Matthias Heizmann (<heizmann@informatik.uni-freiburg.de>)
Dominik Klumpp (<klumpp@informatik.uni-freiburg.de>)
Frank Schüssele (<schuessf@informatik.uni-freiburg.de>)
Manuel Bentele (<bentele@informatik.uni-freiburg.de>)
Marcel Ebbinghaus (<ebbima@informatik.uni-freiburg.de>)

This archive also contains binaries for the following theorem provers.
* Z3 (<https://github.com/Z3Prover/z3>)
  * Linux (z3)
    Z3 version 4.13.4 - 64 bit build from master a8a50695c (2024-11-19)
  * Windows (z3.exe)
    Z3 version 4.13.4 - 64 bit build from master a8a50695c (2024-11-19)

* CVC4 (<http://cvc4.cs.nyu.edu/>)
  * Linux
    cvc4 is a release version,
    version 1.8 [git HEAD 52479010]
    compiled with GCC version 5.4.0 20160609
    on Aug 25 2020 00:35:00
  * Windows
    cvc4.exe is a release version,
    version 1.8
    compiled with GCC version 5.3.1 20160211
    on Aug 25 2020 08:27:39
    Note that this version does not output the git hash, but it should be
    the same as the Linux version.

* MathSAT5 (<http://mathsat.fbk.eu>)  
  * Linux (mathsat)
    MathSAT5 version 5.6.11 (1a1154baf0ab) (Aug  9 2024 08:45:22, gmp 6.2.0, gcc 7.5.0, 64-bit, reentrant)
  * Windows (mathsat.exe, mpir.dll, mathsat.dll)
    MathSAT5 version 5.6.11 (968f05bc5839) (Aug  9 2024 10:46:25, gmp 6.0.0/mpir 3.0.0, msvc 19.12, 64-bit)

For each of these theorem provers, a corresponding license file (z3-LICENSE,
cvc4-LICENSE, mathsat-LICENSE) can be found in our archive. Please consult
these files for additional restrictions regarding your application. If these
restrictions apply, you must delete the corresponding binaries. This might not
necessarily affect your application.

-------------------------------------------------------------------------------

1. Requirements
You require a working version of Python3.6 or higher. Its executable should be
present in your PATH variable.


2. Usage
This Ultimate tool should be called by the Python wrapper script Ultimate.py.
The wrapper script invokes a tool of the Ultimate family by selecting the
correct toolchain and settings file based on the given property file and the
files available in Ultimate's config/ directory. Depending on the concrete tool
you downloaded, the toolchain and the settings invoke very different
verification algorithms.

The script supports the input parameters that are used in the SV-COMP and
should be invoked as follows.

 $ ./Ultimate.py --spec <propfile> --file <inputfile> --architecture <architecture>

where
* <propfile> is a property file, usually with the ending *.prp,
* <inputfile> is a C program,
* <architecture> is either '32bit' or '64bit' (without quotes).

Additional information can be found by invoking
 $ ./Ultimate.py --help

The output of the Ultimate tool is written to the file "Ultimate.log" in the
current working directory and the result is written to stdout.

If the property specified in the property file does not hold, a human-readable
counterexample is written to UltimateCounterExample.errorpath.

Ultimate writes for many properties a violation or correctness witness to the
file witness.graphml.


3. Choosing the right parameters
3.1 Property files
You can use property files as defined by the latest SV-COMP
(e.g., for 2021, <https://sv-comp.sosy-lab.org/2021/rules.php> and
<https://github.com/sosy-lab/sv-benchmarks/releases/tag/svcomp21>).
* valid-memsafety.prp
   The result is 'TRUE' iff all pointer dereferences are valid,
   all deallocations are valid, and all allocated memory is eventually freed.
* no-overflow.prp
   The result is 'TRUE' iff no operations on signed integers results in an
   overflow. (Operations on unsigned integers are not checked as their
   behaviour is always defined by the C standard.)
* unreach-call.prp
   The result is 'TRUE' iff the program does not contain an execution that
   calls the SV-COMP error function __VERIFIER_error().
* termination.prp
   The result is 'TRUE' iff every program execution reaches the end of the
   program, i.e., iff all program executions are finite.
* no-data-race.prp
   The result is 'TRUE' iff there is no data race. Please refer to
   <https://en.cppreference.com/w/c/language/memory_model#Threads_and_data_races>
   for a definition of data race.
* valid-memcleanup.prp
   All allocated memory is deallocated before the program terminates and there
   exists no finite execution of the program on which the program terminates
   but still points to allocated memory.
For most of these property files (except termination.prp) Ultimate also checks
if all ACSL specifications (e.g., "//@ assert x > 0") are valid.


3.2 Architecture
The architecture parameter specifies whether the program is written for an
ILP32 (32bit) or an LP64 (64bit) architecture.


4. Results
The wrapper script provides output to stdout that indicates whether the checked
property is violated or not. The output can be one of the following:
* TRUE
  The property holds.
* FALSE(P)
  Generally means that the property is violated. P specifies which property is
  violated.
* UNKNOWN: MSG
  Ultimate is not able to decide whether the property is satisfied or not. MSG
  usually describes, why it is not able to decide.
* ERROR: MSG
  Indicates an abnormal termination of Ultimate due to some error. MSG usually
  describes the error.
