z3-src 503.2.2

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47


set
echo "Build"
call "C:\Program Files (x86)\Microsoft Visual Studio 12.0\VC\vcvarsall.bat" amd64
cmake -G "NMake Makefiles" -S . -B build -DZ3_BUILD_DOTNET_BINDINGS=True -DZ3_BUILD_JAVA_BINDINGS=True -DZ3_BUILD_PYTHON_BINDINGS=True
cd build
nmake
if ERRORLEVEL 1 exit 1

rem echo "Test python bindings"
rem pushd python
rem python z3test.py z3
rem if ERRORLEVEL 1 exit 1
rem python z3test.py z3num
rem if ERRORLEVEL 1 exit 1
rem popd

echo "Build and run examples"
nmake cpp_example
examples\cpp_example_build_dir\cpp_example.exe
if ERRORLEVEL 1 exit 1

nmake c_example
examples\c_example_build_dir\c_example.exe
if ERRORLEVEL 1 exit 1

rem nmake java_example
rem java_example.exe
if ERRORLEVEL 1 exit 1

rem nmake dotnet_example
rem dotnet_example.exe
if ERRORLEVEL 1 exit 1

echo "Build and run unit tests"
nmake test-z3
rem TBD: test error level
rem test-z3.exe -a


cd ..
echo "Run regression tests"
git clone https://github.com/z3prover/z3test z3test
echo "test-benchmarks"
python z3test\scripts\test_benchmarks.py build\z3.exe z3test\regressions\smt2
if ERRORLEVEL 1 exit 1
echo "benchmarks tested"