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)

* Bitwuzla (<https://github.com/bitwuzla/bitwuzla>)
  * Linux (bitwuzla)
    Bitwuzla version 0.9.1
  * Windows (bitwuzla.exe)
    Bitwuzla version 0.9.1

* 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)

* CVC5 (<https://github.com/cvc5/cvc5>)
  * Linux (cvc5)
    cvc5 1.4.1 [git 2b2e844 on branch HEAD]
  * Windows (cvc5.exe)
    cvc5 1.4.1 [git 2b2e844 on branch HEAD]

For each of these theorem provers, a corresponding license file (z3-LICENSE,
bitwuzla-LICENSE, mathsat-LICENSE, cvc5-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``

