This archive contains Ultimate ReqCheck.
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>)
Vincent Langenfeld (<langenfv@informatik.uni-freiburg.de>)
Matthias Heizmann (<heizmann@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.15.4 - 64 bit build from master 745087e23 (2025-10-29)
  * Windows (z3.exe)
    Z3 version 4.15.4 - 64 bit build from master 745087e23 (2025-10-29)

* 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.17 (006e357b0a0e) (Jun  9 2026 17:21:08, gmp 6.2.0, gcc 9.4.0, 64-bit, reentrant)
  * Windows (mathsat.exe, gmp.dll, mathsat.dll)
    MathSAT5 version 5.6.17 (7c1b8284717f) (Jun  9 2026 17:44:03, gmp 6.3.0, msvc 19.50, 64-bit, reentrant)

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.

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

# Scripts to perform the complete analysis
This archive contains a script which can be used to analyze requirements or generate tests from them.
The script is named ``run_complete_analysis.py`` and requires Python 3.x.

The script should be run from the Ultimate ReqCheck directory, but can be configured to run from a different location.
Please consult the built-in help with ``python run_complete_analysis.py --help``

