z3.rs
z3.rs copied to clipboard
z3-sys fails to build on Windows?
Hey there! I'm trying to play around with this crate on Windows, and z3-sys is failing to build when I try to do a static build. I'm super new to this and I don't really understand the build errors. Does anyone have any idea what I can do to get this working?
Error output
error: failed to run custom build command for `z3-sys v0.6.2`Caused by: process didn't exit successfully:
C:\Users\zkat\src\orogene\target\release\build\z3-sys-6bf7b8d11a33477d\build-script-build
(exit code: 101) --- stdout running: "cmake" "C:\Users\zkat\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.6.2\z3" "-G" "Visual Studio 16 2019" "-Thost=x64" "-Ax64" "-DZ3_BUILD_LIBZ3_SHARED=false" "-DZ3_BUILD_EXECUTABLE=false" "-DZ3_BUILD_TEST_EXECUTABLES=false" "-DCMAKE_INSTALL_PREFIX=C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out" "-DCMAKE_C_FLAGS= -nologo -MT -Brepro" "-DCMAKE_C_FLAGS_RELEASE= -nologo -MT -Brepro" "-DCMAKE_CXX_FLAGS= -DWIN32 -D_WINDOWS -nologo -MT -Brepro" "-DCMAKE_CXX_FLAGS_RELEASE= -DWIN32 -D_WINDOWS -nologo -MT -Brepro" "-DCMAKE_ASM_FLAGS= -nologo -MT -Brepro" "-DCMAKE_ASM_FLAGS_RELEASE= -nologo -MT -Brepro" "-DCMAKE_BUILD_TYPE=Release" -- Selecting Windows SDK version 10.0.18362.0 to target Windows 10.0.19041. -- The CXX compiler identification is MSVC 19.25.28614.0 -- Check for working CXX compiler: C:/Program Files (x86)/Microsoft Visual Studio/2019/BuildTools/VC/Tools/MSVC/14.25.28610/bin/Hostx64/x64/cl.exe -- Check for working CXX compiler: C:/Program Files (x86)/Microsoft Visual Studio/2019/BuildTools/VC/Tools/MSVC/14.25.28610/bin/Hostx64/x64/cl.exe - works -- Detecting CXX compiler ABI info -- Detecting CXX compiler ABI info - done -- Detecting CXX compile features -- Detecting CXX compile features - done -- Z3 version 4.8.8.0 -- Failed to find git directory. -- CMake generator: Visual Studio 16 2019 -- Available configurations: Debug;Release;MinSizeRel;RelWithDebInfo -- Found PythonInterp: C:/Program Files/WindowsApps/PythonSoftwareFoundation.Python.3.8_3.8.752.0_x64__qbz5n2kfra8p0/python3.8.exe -- PYTHON_EXECUTABLE: C:/Program Files/WindowsApps/PythonSoftwareFoundation.Python.3.8_3.8.752.0_x64__qbz5n2kfra8p0/python3.8.exe -- Detected target architecture: x86_64 -- Platform: Windows -- Not using libgmp -- Not using Z3_API_LOG_SYNC -- Thread-safe build -- Performing Test HAS_SSE2 -- Performing Test HAS_SSE2 - Failed -- Looking for C++ include pthread.h -- Looking for C++ include pthread.h - not found -- Found Threads: TRUE -- Performing Test HAS__W3 -- Performing Test HAS__W3 - Success -- C++ compiler supports /W3 -- Treating only serious compiler warnings as errors -- LTO disabled -- Performing Test HAS_MSVC_NO_OMIT_FRAME_POINTER -- Performing Test HAS_MSVC_NO_OMIT_FRAME_POINTER - Success -- Performing Test HAS__Gd -- Performing Test HAS__Gd - Success -- C++ compiler supports /Gd -- Performing Test HAS__EHsc -- Performing Test HAS__EHsc - Success -- C++ compiler supports /EHsc -- CMAKE_CXX_FLAGS: " -DWIN32 -D_WINDOWS -nologo -MT -Brepro" -- CMAKE_EXE_LINKER_FLAGS: "/machine:x64 /STACK:8388608 /RELEASE" -- CMAKE_STATIC_LINKER_FLAGS: "/machine:x64" -- CMAKE_SHARED_LINKER_FLAGS: "/machine:x64 /SUBSYSTEM:WINDOWS /RELEASE" -- CMAKE_CXX_FLAGS_DEBUG: "/MDd /Zi /Ob0 /Od /RTC1" -- CMAKE_EXE_LINKER_FLAGS_DEBUG: "/debug /INCREMENTAL:NO /OPT:REF /OPT:ICF /TLBID:1 /NXCOMPAT" -- CMAKE_SHARED_LINKER_FLAGS_DEBUG: "/debug /INCREMENTAL:NO /OPT:REF /OPT:ICF /TLBID:1" -- CMAKE_STATIC_LINKER_FLAGS_DEBUG: " /INCREMENTAL:NO" -- CMAKE_CXX_FLAGS_RELEASE: " -DWIN32 -D_WINDOWS -nologo -MT -Brepro" -- CMAKE_EXE_LINKER_FLAGS_RELEASE: "/INCREMENTAL:NO" -- CMAKE_SHARED_LINKER_FLAGS_RELEASE: "/INCREMENTAL:NO" -- CMAKE_STATIC_LINKER_FLAGS_RELEASE: " /INCREMENTAL:NO" -- CMAKE_CXX_FLAGS_RELWITHDEBINFO: "/MD /Zi /O2 /Ob1 /DNDEBUG" -- CMAKE_EXE_LINKER_FLAGS_RELWITHDEBINFO: "/debug /INCREMENTAL:NO " -- CMAKE_SHARED_LINKER_FLAGS_RELWITHDEBINFO: "/debug /INCREMENTAL:NO " -- CMAKE_STATIC_LINKER_FLAGS_RELWITHDEBINFO: " /INCREMENTAL:NO" -- CMAKE_CXX_FLAGS_MINSIZEREL: "/MD /O1 /Ob1 /DNDEBUG" -- CMAKE_EXE_LINKER_FLAGS_MINSIZEREL: "/INCREMENTAL:NO /OPT:REF /OPT:ICF /TLBID:1 /NXCOMPAT" -- CMAKE_SHARED_LINKER_FLAGS_MINSIZEREL: "/INCREMENTAL:NO /OPT:REF /OPT:ICF /TLBID:1" -- CMAKE_STATIC_LINKER_FLAGS_MINSIZEREL: " /INCREMENTAL:NO" -- Z3_COMPONENT_CXX_DEFINES: $<$CONFIG:Debug:Z3DEBUG>;$<$CONFIG:Release:_EXTERNAL_RELEASE>;$<$CONFIG:RelWithDebInfo:_EXTERNAL_RELEASE>;-D_WINDOWS;-D_MP_INTERNAL;$<$CONFIG:Debug:_TRACE>;UNICODE;_UNICODE -- Z3_COMPONENT_CXX_FLAGS: /W3;$<$CONFIG:Debug:/Oy->;$<$CONFIG:MinSizeRel:/Oy->;/Gd;/EHsc -- Z3_DEPENDENT_LIBS: -- Z3_COMPONENT_EXTRA_INCLUDE_DIRS: C:/Users/zkat/src/orogene/target/release/build/z3-sys-efa3561d0d5a5b66/out/build/src;C:/Users/zkat/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.6.2/z3/src -- Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS: -- CMAKE_INSTALL_LIBDIR: "lib" -- CMAKE_INSTALL_BINDIR: "bin" -- CMAKE_INSTALL_INCLUDEDIR: "include" -- CMAKE_INSTALL_PKGCONFIGDIR: "lib/pkgconfig" -- CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: "lib/cmake/z3" -- Adding component util -- Adding component polynomial -- Adding rule to generate "algebraic_params.hpp" -- Adding component dd -- Adding component hilbert -- Adding component simplex -- Adding component automata -- Adding component interval -- Adding component realclosure -- Adding rule to generate "rcf_params.hpp" -- Adding component subpaving -- Adding component ast -- Adding rule to generate "pp_params.hpp" -- Adding component rewriter -- Adding rule to generate "arith_rewriter_params.hpp" -- Adding rule to generate "array_rewriter_params.hpp" -- Adding rule to generate "bool_rewriter_params.hpp" -- Adding rule to generate "bv_rewriter_params.hpp" -- Adding rule to generate "fpa_rewriter_params.hpp" -- Adding rule to generate "poly_rewriter_params.hpp" -- Adding rule to generate "rewriter_params.hpp" -- Adding rule to generate "seq_rewriter_params.hpp" -- Adding component normal_forms -- Adding rule to generate "nnf_params.hpp" -- Adding component model -- Adding rule to generate "model_evaluator_params.hpp" -- Adding rule to generate "model_params.hpp" -- Adding component tactic -- Adding rule to generate "tactic_params.hpp" -- Adding component substitution -- Adding component parser_util -- Adding rule to generate "parser_params.hpp" -- Adding component grobner -- Adding component sat -- Adding rule to generate "sat_asymm_branch_params.hpp" -- Adding rule to generate "sat_params.hpp" -- Adding rule to generate "sat_scc_params.hpp" -- Adding rule to generate "sat_simplifier_params.hpp" -- Adding component nlsat -- Adding rule to generate "nlsat_params.hpp" -- Adding component lp -- Adding component core_tactics -- Adding component subpaving_tactic -- Adding component aig_tactic -- Adding component solver -- Adding rule to generate "combined_solver_params.hpp" -- Adding rule to generate "parallel_params.hpp" -- Adding rule to generate "solver_params.hpp" -- Adding component sat_tactic -- Adding component arith_tactics -- Adding component nlsat_tactic -- Adding component ackermannization -- Adding rule to generate "ackermannization_params.hpp" -- Adding rule to generate "ackermannize_bv_tactic_params.hpp" -- Adding component cmd_context -- Adding component extra_cmds -- Adding component smt2parser -- Adding component proofs -- Adding component fpa -- Adding rule to generate "fpa2bv_rewriter_params.hpp" -- Adding component macros -- Adding component pattern -- Adding rule to generate "pattern_inference_params_helper.hpp" -- Adding component bit_blaster -- Adding component smt_params -- Adding rule to generate "smt_params_helper.hpp" -- Adding component proto_model -- Adding component smt -- Adding component bv_tactics -- Adding component smt_tactic -- Adding component sls_tactic -- Adding rule to generate "sls_params.hpp" -- Adding component qe -- Adding component muz -- Adding rule to generate "fp_params.hpp" -- Adding component dataflow -- Adding component transforms -- Adding component rel -- Adding component clp -- Adding component tab -- Adding component bmc -- Adding component ddnf -- Adding component spacer -- Adding component fp -- Adding component ufbv_tactic -- Adding component sat_solver -- Adding component smtlogic_tactics -- Adding rule to generate "qfufbv_tactic_params.hpp" -- Adding component fpa_tactics -- Adding component fd_solver -- Adding component portfolio -- Adding component opt -- Adding rule to generate "opt_params.hpp" -- Adding component api -- Adding component api_dll -- Building documentation disabled -- Configuring done -- Generating done -- Build files have been written to: C:/Users/zkat/src/orogene/target/release/build/z3-sys-efa3561d0d5a5b66/out/build running: "cmake" "--build" "." "--target" "install" "--config" "Release" "--" Microsoft (R) Build Engine version 16.5.0+d4cbfca49 for .NET Framework Copyright (C) Microsoft Corporation. All rights reserved.Checking Build System Building Custom Rule C:/Users/zkat/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.6.2/z3/src/util/CMakeLists.txt approx_nat.cpp approx_set.cpp bit_util.cpp bit_vector.cpp cmd_context_types.cpp common_msgs.cpp debug.cpp env_params.cpp fixed_bit_vector.cpp gparams.cpp hash.cpp hwf.cpp inf_int_rational.cpp inf_rational.cpp inf_s_integer.cpp lbool.cpp luby.cpp memory_manager.cpp min_cut.cpp mpbq.cpp Generating Code... Compiling... mpf.cpp mpff.cpp mpfx.cpp mpn.cpp mpq.cpp mpq_inf.cpp mpz.cpp page.cpp params.cpp permutation.cpp prime_generator.cpp rational.cpp region.cpp rlimit.cpp scoped_ctrl_c.cpp scoped_timer.cpp sexpr.cpp s_integer.cpp small_object_allocator.cpp smt2_util.cpp Generating Code... Compiling... stack.cpp statistics.cpp symbol.cpp timeit.cpp timeout.cpp trace.cpp util.cpp warning.cpp z3_exception.cpp Generating Code... LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\util\util.vcxproj] util.vcxproj -> C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\util\util.dir\Release\util.lib Generating "C:/Users/zkat/src/orogene/target/release/build/z3-sys-efa3561d0d5a5b66/out/build/src/math/polynomial/algebraic_params.hpp" from "algebraic_params.pyg" Access is denied. C:\Program Files (x86)\Microsoft Visual Studio\2019\BuildTools\MSBuild\Microsoft\VC\v160\Microsoft.CppCommon.targets(231,5): error MSB6006: "cmd.exe" exited with code 5. [C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\math\polynomial\polynomial.vcxproj] Building Custom Rule C:/Users/zkat/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.6.2/z3/src/math/automata/CMakeLists.txt automaton.cpp LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\math\automata\automata.vcxproj] automata.vcxproj -> C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\math\automata\automata.dir\Release\automata.lib Building Custom Rule C:/Users/zkat/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.6.2/z3/src/math/dd/CMakeLists.txt dd_bdd.cpp dd_pdd.cpp Generating Code... LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\math\dd\dd.vcxproj] dd.vcxproj -> C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\math\dd\dd.dir\Release\dd.lib Building Custom Rule C:/Users/zkat/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.6.2/z3/src/math/simplex/CMakeLists.txt simplex.cpp model_based_opt.cpp bit_matrix.cpp Generating Code... LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\math\simplex\simplex.vcxproj] simplex.vcxproj -> C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\math\simplex\simplex.dir\Release\simplex.lib Building Custom Rule C:/Users/zkat/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.6.2/z3/src/math/hilbert/CMakeLists.txt hilbert_basis.cpp LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\math\hilbert\hilbert.vcxproj] hilbert.vcxproj -> C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\math\hilbert\hilbert.dir\Release\hilbert.lib Building Custom Rule C:/Users/zkat/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.6.2/z3/src/math/interval/CMakeLists.txt interval_mpq.cpp dep_intervals.cpp Generating Code... LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\math\interval\interval.vcxproj] interval.vcxproj -> C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\math\interval\interval.dir\Release\interval.lib Building Custom Rule C:/Users/zkat/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.6.2/z3/src/math/subpaving/CMakeLists.txt subpaving.cpp subpaving_hwf.cpp subpaving_mpf.cpp subpaving_mpff.cpp subpaving_mpfx.cpp subpaving_mpq.cpp Generating Code... LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\math\subpaving\subpaving.vcxproj] subpaving.vcxproj -> C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\math\subpaving\subpaving.dir\Release\subpaving.lib Generating "C:/Users/zkat/src/orogene/target/release/build/z3-sys-efa3561d0d5a5b66/out/build/src/math/realclosure/rcf_params.hpp" from "rcf_params.pyg" Access is denied. C:\Program Files (x86)\Microsoft Visual Studio\2019\BuildTools\MSBuild\Microsoft\VC\v160\Microsoft.CppCommon.targets(231,5): error MSB6006: "cmd.exe" exited with code 5. [C:\Users\zkat\src\orogene\target\release\build\z3-sys-efa3561d0d5a5b66\out\build\src\math\realclosure\realclosure.vcxproj]
--- stderr CMake Warning at CMakeLists.txt:60 (message): Disabling Z3_INCLUDE_GIT_DESCRIBE Call Stack (most recent call first): CMakeLists.txt:109 (disable_git_describe)
CMake Warning at CMakeLists.txt:64 (message): Disabling Z3_INCLUDE_GIT_HASH Call Stack (most recent call first): CMakeLists.txt:110 (disable_git_hash)
CMake Warning (dev) at cmake/msvc_legacy_quirks.cmake:160 (message): Skipping legacy linker MSVC options for x86_64 RELEASE Call Stack (most recent call first): CMakeLists.txt:429 (include) This warning is for project developers. Use -Wno-dev to suppress it.
CMake Warning (dev) at cmake/msvc_legacy_quirks.cmake:160 (message): Skipping legacy linker MSVC options for x86_64 RELWITHDEBINFO Call Stack (most recent call first): CMakeLists.txt:429 (include) This warning is for project developers. Use -Wno-dev to suppress it.
CMake Warning at examples/CMakeLists.txt:24 (message): Cannot set built type of external project when building with a multi-configuration generator
CMake Warning: Manually-specified variables were not used by the project:
CMAKE_ASM_FLAGS CMAKE_ASM_FLAGS_RELEASE CMAKE_BUILD_TYPE CMAKE_C_FLAGS CMAKE_C_FLAGS_RELEASE
thread 'main' panicked at ' command did not execute successfully, got: exit code: 1
build script failed, must exit now', C:\Users\zkat.cargo\registry\src\github.com-1ecc6299db9ec823\cmake-0.1.44\src\lib.rs:885:5 note: run with
RUST_BACKTRACE=1
environment variable to display a backtracewarning: build failed, waiting for other jobs to finish... error: build failed
Thanks for filing an issue.
I have to admit that I'm not super familiar with either windows or cmake. I basically have just done enough to get it building in CI, and that pushed me to the limits of my windows/cmake knowledge.
I do see an "Access is denied." message in there, maybe it is a directory permissions thing?
If you or anyone else can help resolve this, that would be very appreciated!
If it's not a permission problem, then maybe another process has an open handle to the file? I usually use something like handle or procmon to track down issues like this.
I don't even get this far. Here's my error, also while trying to do a static build:
Build error
cargo build
Compiling z3-sys v0.7.1
error: failed to run custom build command for `z3-sys v0.7.1`
Caused by:
process didn't exit successfully: `C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d7090e311c4ee3cf\build-script-build` (exit code: 101)
--- stdout
CMAKE_TOOLCHAIN_FILE_x86_64-pc-windows-msvc = None
CMAKE_TOOLCHAIN_FILE_x86_64_pc_windows_msvc = None
HOST_CMAKE_TOOLCHAIN_FILE = None
CMAKE_TOOLCHAIN_FILE = None
CMAKE_GENERATOR_x86_64-pc-windows-msvc = None
CMAKE_GENERATOR_x86_64_pc_windows_msvc = None
HOST_CMAKE_GENERATOR = None
CMAKE_GENERATOR = None
CMAKE_PREFIX_PATH_x86_64-pc-windows-msvc = None
CMAKE_PREFIX_PATH_x86_64_pc_windows_msvc = None
HOST_CMAKE_PREFIX_PATH = None
CMAKE_PREFIX_PATH = None
CMAKE_x86_64-pc-windows-msvc = None
CMAKE_x86_64_pc_windows_msvc = None
HOST_CMAKE = None
CMAKE = None
running: "cmake" "C:\\Users\\ahelwer\\.cargo\\registry\\src\\github.com-1ecc6299db9ec823\\z3-sys-0.7.1\\z3" "-G" "Visual Studio 16 2019" "-Thost=x64" "-Ax64" "-DZ3_BUILD_LIBZ3_SHARED=false" "-DZ3_BUILD_EXECUTABLE=false" "-DZ3_BUILD_TEST_EXECUTABLES=false" "-DCMAKE_INSTALL_PREFIX=C:\\Users\\ahelwer\\source\\teleport-z3\\target\\debug\\build\\z3-sys-d974b02077215d28\\out" "-DCMAKE_C_FLAGS= -nologo -MD -Brepro" "-DCMAKE_C_FLAGS_DEBUG= -nologo -MD -Brepro" "-DCMAKE_CXX_FLAGS= -MP -DWIN32 -D_WINDOWS -nologo -MD -Brepro" "-DCMAKE_CXX_FLAGS_DEBUG= -MP -DWIN32 -D_WINDOWS -nologo -MD -Brepro" "-DCMAKE_ASM_FLAGS= -nologo -MD -Brepro" "-DCMAKE_ASM_FLAGS_DEBUG= -nologo -MD -Brepro" "-DCMAKE_BUILD_TYPE=Debug"
--- stderr
CMake Error: Could not create named generator Visual Studio 16 2019
Generators
* Unix Makefiles = Generates standard UNIX makefiles.
Ninja = Generates build.ninja files.
Ninja Multi-Config = Generates build-<Config>.ninja files.
CodeBlocks - Ninja = Generates CodeBlocks project files.
CodeBlocks - Unix Makefiles = Generates CodeBlocks project files.
CodeLite - Ninja = Generates CodeLite project files.
CodeLite - Unix Makefiles = Generates CodeLite project files.
Eclipse CDT4 - Ninja = Generates Eclipse CDT 4.0 project files.
Eclipse CDT4 - Unix Makefiles= Generates Eclipse CDT 4.0 project files.
Kate - Ninja = Generates Kate project files.
Kate - Unix Makefiles = Generates Kate project files.
Sublime Text 2 - Ninja = Generates Sublime Text 2 project files.
Sublime Text 2 - Unix Makefiles
= Generates Sublime Text 2 project files.
thread 'main' panicked at '
command did not execute successfully, got: exit code: 1
build script failed, must exit now', C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\cmake-0.1.46\src\lib.rs:974:5
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
This is while running it in the x64 Native Tools Command Prompt for VS 2019, so cc
is definitely in the path:
cc
cc: fatal error: no input files
compilation terminated.
I believe this is because I have MSYS2 installed and it's using that version of cmake. I will uninstall it and then see what happens.
I uninstalled MSYS2 and installed cmake from chocolatey; got significantly further, ending in the following error:
thread 'main' panicked at 'Unable to find libclang: "couldn't find any valid shared libraries matching: ['clang.dll', 'libclang.dll'], set the
LIBCLANG_PATH
environment variable to a path where one of these files can be found (invalid: [])"', C:\Users\ahelwer.cargo\registry\src\github.com-1ecc6299db9ec823\bindgen-0.58.1\src/lib.rs:2057:31
Full build output
cargo build
Compiling z3-sys v0.7.1
error: failed to run custom build command for `z3-sys v0.7.1`
Caused by:
process didn't exit successfully: `C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d7090e311c4ee3cf\build-script-build` (exit code: 101)
--- stdout
CMAKE_TOOLCHAIN_FILE_x86_64-pc-windows-msvc = None
CMAKE_TOOLCHAIN_FILE_x86_64_pc_windows_msvc = None
HOST_CMAKE_TOOLCHAIN_FILE = None
CMAKE_TOOLCHAIN_FILE = None
CMAKE_GENERATOR_x86_64-pc-windows-msvc = None
CMAKE_GENERATOR_x86_64_pc_windows_msvc = None
HOST_CMAKE_GENERATOR = None
CMAKE_GENERATOR = None
CMAKE_PREFIX_PATH_x86_64-pc-windows-msvc = None
CMAKE_PREFIX_PATH_x86_64_pc_windows_msvc = None
HOST_CMAKE_PREFIX_PATH = None
CMAKE_PREFIX_PATH = None
CMAKE_x86_64-pc-windows-msvc = None
CMAKE_x86_64_pc_windows_msvc = None
HOST_CMAKE = None
CMAKE = None
running: "cmake" "C:\\Users\\ahelwer\\.cargo\\registry\\src\\github.com-1ecc6299db9ec823\\z3-sys-0.7.1\\z3" "-G" "Visual Studio 16 2019" "-Thost=x64" "-Ax64" "-DZ3_BUILD_LIBZ3_SHARED=false" "-DZ3_BUILD_EXECUTABLE=false" "-DZ3_BUILD_TEST_EXECUTABLES=false" "-DCMAKE_INSTALL_PREFIX=C:\\Users\\ahelwer\\source\\teleport-z3\\target\\debug\\build\\z3-sys-d974b02077215d28\\out" "-DCMAKE_C_FLAGS= -nologo -MD -Brepro" "-DCMAKE_C_FLAGS_DEBUG= -nologo -MD -Brepro" "-DCMAKE_CXX_FLAGS= -MP -DWIN32 -D_WINDOWS -nologo -MD -Brepro" "-DCMAKE_CXX_FLAGS_DEBUG= -MP -DWIN32 -D_WINDOWS -nologo -MD -Brepro" "-DCMAKE_ASM_FLAGS= -nologo -MD -Brepro" "-DCMAKE_ASM_FLAGS_DEBUG= -nologo -MD -Brepro" "-DCMAKE_BUILD_TYPE=Debug"
-- Selecting Windows SDK version 10.0.18362.0 to target Windows 10.0.19042.
-- The CXX compiler identification is MSVC 19.29.30133.0
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Check for working CXX compiler: C:/Program Files (x86)/Microsoft Visual Studio/2019/Community/VC/Tools/MSVC/14.29.30133/bin/Hostx64/x64/cl.exe - skipped
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Z3 version 4.8.12.0
-- Failed to find git directory.
-- CMake generator: Visual Studio 16 2019
-- Available configurations: Debug;Release;MinSizeRel;RelWithDebInfo
-- Found PythonInterp: C:/Python39/python.exe (found version "3.9.6")
-- PYTHON_EXECUTABLE: C:/Python39/python.exe
-- Detected target architecture: x86_64
-- Platform: Windows
-- Not using libgmp
-- Not using Z3_API_LOG_SYNC
-- Thread-safe build
-- Performing Test HAS_SSE2
-- Performing Test HAS_SSE2 - Failed
-- Looking for C++ include pthread.h
-- Looking for C++ include pthread.h - not found
-- Found Threads: TRUE
-- Performing Test HAS__W3
-- Performing Test HAS__W3 - Success
-- C++ compiler supports /W3
-- Treating only serious compiler warnings as errors
-- LTO disabled
-- Performing Test HAS_MSVC_NO_OMIT_FRAME_POINTER
-- Performing Test HAS_MSVC_NO_OMIT_FRAME_POINTER - Success
-- Performing Test HAS__Gd
-- Performing Test HAS__Gd - Success
-- C++ compiler supports /Gd
-- Performing Test HAS__EHsc
-- Performing Test HAS__EHsc - Success
-- C++ compiler supports /EHsc
-- CMAKE_CXX_FLAGS: " -MP -DWIN32 -D_WINDOWS -nologo -MD -Brepro"
-- CMAKE_EXE_LINKER_FLAGS: "/machine:x64 /STACK:8388608 /RELEASE"
-- CMAKE_STATIC_LINKER_FLAGS: "/machine:x64"
-- CMAKE_SHARED_LINKER_FLAGS: "/machine:x64 /SUBSYSTEM:WINDOWS /RELEASE"
-- CMAKE_CXX_FLAGS_DEBUG: " -MP -DWIN32 -D_WINDOWS -nologo -MD -Brepro"
-- CMAKE_EXE_LINKER_FLAGS_DEBUG: "/debug /INCREMENTAL:NO /OPT:REF /OPT:ICF /TLBID:1 /NXCOMPAT"
-- CMAKE_SHARED_LINKER_FLAGS_DEBUG: "/debug /INCREMENTAL:NO /OPT:REF /OPT:ICF /TLBID:1"
-- CMAKE_STATIC_LINKER_FLAGS_DEBUG: " /INCREMENTAL:NO"
-- CMAKE_CXX_FLAGS_RELEASE: "/MD /O2 /Ob2 /DNDEBUG"
-- CMAKE_EXE_LINKER_FLAGS_RELEASE: "/INCREMENTAL:NO"
-- CMAKE_SHARED_LINKER_FLAGS_RELEASE: "/INCREMENTAL:NO"
-- CMAKE_STATIC_LINKER_FLAGS_RELEASE: " /INCREMENTAL:NO"
-- CMAKE_CXX_FLAGS_RELWITHDEBINFO: "/MD /Zi /O2 /Ob1 /DNDEBUG"
-- CMAKE_EXE_LINKER_FLAGS_RELWITHDEBINFO: "/debug /INCREMENTAL:NO "
-- CMAKE_SHARED_LINKER_FLAGS_RELWITHDEBINFO: "/debug /INCREMENTAL:NO "
-- CMAKE_STATIC_LINKER_FLAGS_RELWITHDEBINFO: " /INCREMENTAL:NO"
-- CMAKE_CXX_FLAGS_MINSIZEREL: "/MD /O1 /Ob1 /DNDEBUG"
-- CMAKE_EXE_LINKER_FLAGS_MINSIZEREL: "/INCREMENTAL:NO /OPT:REF /OPT:ICF /TLBID:1 /NXCOMPAT"
-- CMAKE_SHARED_LINKER_FLAGS_MINSIZEREL: "/INCREMENTAL:NO /OPT:REF /OPT:ICF /TLBID:1"
-- CMAKE_STATIC_LINKER_FLAGS_MINSIZEREL: " /INCREMENTAL:NO"
-- Z3_COMPONENT_CXX_DEFINES: $<$<CONFIG:Debug>:Z3DEBUG>;$<$<CONFIG:Release>:_EXTERNAL_RELEASE>;$<$<CONFIG:RelWithDebInfo>:_EXTERNAL_RELEASE>;-D_WINDOWS;-D_MP_INTERNAL;$<$<CONFIG:Debug>:_TRACE>;UNICODE;_UNICODE
-- Z3_COMPONENT_CXX_FLAGS: /W3;$<$<CONFIG:Debug>:/Oy->;$<$<CONFIG:MinSizeRel>:/Oy->;/Gd;/EHsc
-- Z3_DEPENDENT_LIBS: Threads::Threads
-- Z3_COMPONENT_EXTRA_INCLUDE_DIRS: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src;C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src
-- Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS:
-- CMAKE_INSTALL_LIBDIR: "lib"
-- CMAKE_INSTALL_BINDIR: "bin"
-- CMAKE_INSTALL_INCLUDEDIR: "include"
-- CMAKE_INSTALL_PKGCONFIGDIR: "lib/pkgconfig"
-- CMAKE_INSTALL_Z3_CMAKE_PACKAGE_DIR: "lib/cmake/z3"
-- Adding component util
-- Adding component polynomial
-- Adding rule to generate "algebraic_params.hpp"
-- Adding component dd
-- Adding component hilbert
-- Adding component simplex
-- Adding component automata
-- Adding component interval
-- Adding component realclosure
-- Adding rule to generate "rcf_params.hpp"
-- Adding component subpaving
-- Adding component ast
-- Adding rule to generate "pp_params.hpp"
-- Adding component params
-- Adding rule to generate "arith_rewriter_params.hpp"
-- Adding rule to generate "array_rewriter_params.hpp"
-- Adding rule to generate "bool_rewriter_params.hpp"
-- Adding rule to generate "bv_rewriter_params.hpp"
-- Adding rule to generate "fpa_rewriter_params.hpp"
-- Adding rule to generate "fpa2bv_rewriter_params.hpp"
-- Adding rule to generate "pattern_inference_params_helper.hpp"
-- Adding rule to generate "poly_rewriter_params.hpp"
-- Adding rule to generate "rewriter_params.hpp"
-- Adding rule to generate "seq_rewriter_params.hpp"
-- Adding component rewriter
-- Adding component normal_forms
-- Adding rule to generate "nnf_params.hpp"
-- Adding component macros
-- Adding component model
-- Adding rule to generate "model_evaluator_params.hpp"
-- Adding rule to generate "model_params.hpp"
-- Adding component tactic
-- Adding rule to generate "tactic_params.hpp"
-- Adding component substitution
-- Adding component euf
-- Adding component smt_params
-- Adding rule to generate "smt_params_helper.hpp"
-- Adding component parser_util
-- Adding rule to generate "parser_params.hpp"
-- Adding component grobner
-- Adding component sat
-- Adding rule to generate "sat_asymm_branch_params.hpp"
-- Adding rule to generate "sat_params.hpp"
-- Adding rule to generate "sat_scc_params.hpp"
-- Adding rule to generate "sat_simplifier_params.hpp"
-- Adding component nlsat
-- Adding rule to generate "nlsat_params.hpp"
-- Adding component core_tactics
-- Adding component subpaving_tactic
-- Adding component aig_tactic
-- Adding component arith_tactics
-- Adding component solver
-- Adding rule to generate "combined_solver_params.hpp"
-- Adding rule to generate "parallel_params.hpp"
-- Adding rule to generate "solver_params.hpp"
-- Adding component cmd_context
-- Adding component extra_cmds
-- Adding component smt2parser
-- Adding component solver_assertions
-- Adding component pattern
-- Adding component bit_blaster
-- Adding component lp
-- Adding component mbp
-- Adding component sat_smt
-- Adding component sat_tactic
-- Adding component nlsat_tactic
-- Adding component ackermannization
-- Adding rule to generate "ackermannization_params.hpp"
-- Adding rule to generate "ackermannize_bv_tactic_params.hpp"
-- Adding component proofs
-- Adding component fpa
-- Adding component proto_model
-- Adding component smt
-- Adding component bv_tactics
-- Adding component smt_tactic
-- Adding component sls_tactic
-- Adding rule to generate "sls_params.hpp"
-- Adding component qe
-- Adding component muz
-- Adding rule to generate "fp_params.hpp"
-- Adding component dataflow
-- Adding component transforms
-- Adding component rel
-- Adding component clp
-- Adding component tab
-- Adding component bmc
-- Adding component ddnf
-- Adding component spacer
-- Adding component fp
-- Adding component ufbv_tactic
-- Adding component sat_solver
-- Adding component smtlogic_tactics
-- Adding rule to generate "qfufbv_tactic_params.hpp"
-- Adding component fpa_tactics
-- Adding component fd_solver
-- Adding component portfolio
-- Adding component opt
-- Adding rule to generate "opt_params.hpp"
-- Adding component api
-- Adding component api_dll
-- Building documentation disabled
-- Configuring done
-- Generating done
-- Build files have been written to: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build
running: "cmake" "--build" "." "--target" "install" "--config" "Debug" "--parallel" "8" "--" "-m"
Microsoft (R) Build Engine version 16.11.0+0538acc04 for .NET Framework
Copyright (C) Microsoft Corporation. All rights reserved.
Checking Build System
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/util/CMakeLists.txt
approx_nat.cpp
approx_set.cpp
bit_util.cpp
bit_vector.cpp
cmd_context_types.cpp
common_msgs.cpp
debug.cpp
env_params.cpp
fixed_bit_vector.cpp
gparams.cpp
hash.cpp
hwf.cpp
inf_int_rational.cpp
inf_rational.cpp
inf_s_integer.cpp
lbool.cpp
luby.cpp
memory_manager.cpp
min_cut.cpp
mpbq.cpp
Generating Code...
Compiling...
mpf.cpp
mpff.cpp
mpfx.cpp
mpn.cpp
mpq.cpp
mpq_inf.cpp
mpz.cpp
page.cpp
params.cpp
permutation.cpp
prime_generator.cpp
rational.cpp
region.cpp
rlimit.cpp
scoped_ctrl_c.cpp
scoped_timer.cpp
sexpr.cpp
s_integer.cpp
small_object_allocator.cpp
smt2_util.cpp
Generating Code...
Compiling...
stack.cpp
state_graph.cpp
statistics.cpp
symbol.cpp
timeit.cpp
timeout.cpp
trace.cpp
util.cpp
warning.cpp
z3_exception.cpp
zstring.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\util\util.vcxproj]
util.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\util\util.dir\Debug\util.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/math/simplex/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/math/automata/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/math/dd/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/math/interval/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/math/hilbert/CMakeLists.txt
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/params/arith_rewriter_params.hpp" from "arith_rewriter_params.pyg"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/math/polynomial/algebraic_params.hpp" from "algebraic_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\math\polynomial\algebraic_params.pyg
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\params\arith_rewriter_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\polynomial\algebraic_params.hpp"
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\params\arith_rewriter_params.hpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/params/array_rewriter_params.hpp" from "array_rewriter_params.pyg"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/math/polynomial/CMakeLists.txt
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\params\array_rewriter_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\params\array_rewriter_params.hpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/params/bool_rewriter_params.hpp" from "bool_rewriter_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\params\bool_rewriter_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\params\bool_rewriter_params.hpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/params/bv_rewriter_params.hpp" from "bv_rewriter_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\params\bv_rewriter_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\params\bv_rewriter_params.hpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/params/fpa_rewriter_params.hpp" from "fpa_rewriter_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\params\fpa_rewriter_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\params\fpa_rewriter_params.hpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/params/fpa2bv_rewriter_params.hpp" from "fpa2bv_rewriter_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\params\fpa2bv_rewriter_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\params\fpa2bv_rewriter_params.hpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/params/pattern_inference_params_helper.hpp" from "pattern_inference_params_helper.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\params\pattern_inference_params_helper.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\params\pattern_inference_params_helper.hpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/params/poly_rewriter_params.hpp" from "poly_rewriter_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\params\poly_rewriter_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\params\poly_rewriter_params.hpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/params/rewriter_params.hpp" from "rewriter_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\params\rewriter_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\params\rewriter_params.hpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/params/seq_rewriter_params.hpp" from "seq_rewriter_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\params\seq_rewriter_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\params\seq_rewriter_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/params/CMakeLists.txt
pattern_inference_params.cpp
simplex.cpp
hilbert_basis.cpp
automaton.cpp
interval_mpq.cpp
algebraic_numbers.cpp
dd_bdd.cpp
context_params.cpp
dep_intervals.cpp
dd_pdd.cpp
model_based_opt.cpp
polynomial_cache.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\automata\automata.vcxproj]
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\params\params.vcxproj]
automata.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\automata\automata.dir\Debug\automata.lib
params.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\params\params.dir\Debug\params.lib
Generating Code...
Generating Code...
bit_matrix.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\hilbert\hilbert.vcxproj]
hilbert.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\hilbert\hilbert.dir\Debug\hilbert.lib
polynomial.cpp
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/smt/params/smt_params_helper.hpp" from "smt_params_helper.pyg"
Generating Code...
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\smt\params\smt_params_helper.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\smt\params\smt_params_helper.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/smt/params/CMakeLists.txt
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\interval\interval.vcxproj]
interval.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\interval\interval.dir\Debug\interval.lib
dyn_ack_params.cpp
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/math/subpaving/CMakeLists.txt
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/math/realclosure/rcf_params.hpp" from "rcf_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\math\realclosure\rcf_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\realclosure\rcf_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/math/realclosure/CMakeLists.txt
subpaving.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\dd\dd.vcxproj]
mpz_matrix.cpp
rpolynomial.cpp
dd.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\dd\dd.dir\Debug\dd.lib
preprocessor_params.cpp
realclosure.cpp
subpaving_hwf.cpp
sexpr2upolynomial.cpp
qi_params.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\simplex\simplex.vcxproj]
simplex.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\simplex\simplex.dir\Debug\simplex.lib
smt_params.cpp
upolynomial.cpp
Generating Code...
subpaving_mpf.cpp
theory_arith_params.cpp
upolynomial_factorization.cpp
theory_array_params.cpp
subpaving_mpff.cpp
theory_bv_params.cpp
Generating Code...
theory_pb_params.cpp
subpaving_mpfx.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\realclosure\realclosure.vcxproj]
theory_seq_params.cpp
realclosure.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\realclosure\realclosure.dir\Debug\realclosure.lib
theory_str_params.cpp
subpaving_mpq.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\smt\params\smt_params.vcxproj]
smt_params.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\smt\params\smt_params.dir\Debug\smt_params.lib
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\polynomial\polynomial.vcxproj]
polynomial.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\polynomial\polynomial.dir\Debug\polynomial.lib
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/ast/pp_params.hpp" from "pp_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\ast\pp_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\pp_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/ast/CMakeLists.txt
act_cache.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\subpaving\subpaving.vcxproj]
subpaving.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\subpaving\subpaving.dir\Debug\subpaving.lib
arith_decl_plugin.cpp
array_decl_plugin.cpp
ast.cpp
ast_ll_pp.cpp
ast_lt.cpp
ast_pp_util.cpp
ast_printer.cpp
ast_smt2_pp.cpp
ast_smt_pp.cpp
ast_pp_dot.cpp
ast_translation.cpp
ast_util.cpp
bv_decl_plugin.cpp
char_decl_plugin.cpp
cost_evaluator.cpp
datatype_decl_plugin.cpp
decl_collector.cpp
display_dimacs.cpp
dl_decl_plugin.cpp
Generating Code...
Compiling...
expr2polynomial.cpp
expr2var.cpp
expr_abstract.cpp
expr_functors.cpp
expr_map.cpp
expr_stat.cpp
expr_substitution.cpp
for_each_ast.cpp
for_each_expr.cpp
format.cpp
fpa_decl_plugin.cpp
func_decl_dependencies.cpp
has_free_vars.cpp
macro_substitution.cpp
num_occurs.cpp
occurs.cpp
pb_decl_plugin.cpp
pp.cpp
quantifier_stat.cpp
recfun_decl_plugin.cpp
Generating Code...
Compiling...
reg_decl_plugins.cpp
seq_decl_plugin.cpp
shared_occs.cpp
special_relations_decl_plugin.cpp
static_features.cpp
used_vars.cpp
value_generator.cpp
well_sorted.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\ast.vcxproj]
ast.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\ast.dir\Debug\ast.lib
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/parsers/util/parser_params.hpp" from "parser_params.pyg"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/ast/euf/CMakeLists.txt
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\parsers\util\parser_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\parsers\util\parser_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/parsers/util/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/math/grobner/CMakeLists.txt
euf_enode.cpp
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/ast/rewriter/CMakeLists.txt
cost_parser.cpp
grobner.cpp
arith_rewriter.cpp
pattern_validation.cpp
euf_etable.cpp
pdd_simplifier.cpp
array_rewriter.cpp
scanner.cpp
euf_egraph.cpp
pdd_solver.cpp
ast_counter.cpp
Generating Code...
simple_parser.cpp
Generating Code...
bit2int.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\grobner\grobner.vcxproj]
grobner.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\grobner\grobner.dir\Debug\grobner.lib
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/sat/sat_asymm_branch_params.hpp" from "sat_asymm_branch_params.pyg"
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\euf\euf.vcxproj]
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\sat\sat_asymm_branch_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\sat\sat_asymm_branch_params.hpp"
euf.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\euf\euf.dir\Debug\euf.lib
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/sat/sat_params.hpp" from "sat_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\sat\sat_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\sat\sat_params.hpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/sat/sat_scc_params.hpp" from "sat_scc_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\sat\sat_scc_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\sat\sat_scc_params.hpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/sat/sat_simplifier_params.hpp" from "sat_simplifier_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\sat\sat_simplifier_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\sat\sat_simplifier_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/sat/CMakeLists.txt
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\parsers\util\parser_util.vcxproj]
parser_util.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\parsers\util\parser_util.dir\Debug\parser_util.lib
bool_rewriter.cpp
dimacs.cpp
sat_aig_cuts.cpp
bv_bounds.cpp
sat_aig_finder.cpp
bv_elim.cpp
sat_anf_simplifier.cpp
bv_rewriter.cpp
sat_asymm_branch.cpp
sat_bcd.cpp
cached_var_subst.cpp
sat_big.cpp
datatype_rewriter.cpp
sat_binspr.cpp
der.cpp
sat_clause.cpp
sat_clause_set.cpp
distribute_forall.cpp
sat_clause_use_list.cpp
dl_rewriter.cpp
sat_cleaner.cpp
elim_bounds.cpp
sat_config.cpp
sat_cut_simplifier.cpp
enum2bv_rewriter.cpp
sat_cutset.cpp
sat_ddfw.cpp
expr_replacer.cpp
sat_drat.cpp
expr_safe_replace.cpp
sat_elim_eqs.cpp
factor_equivs.cpp
sat_elim_vars.cpp
sat_gc.cpp
factor_rewriter.cpp
Generating Code...
fpa_rewriter.cpp
Generating Code...
Compiling...
sat_integrity_checker.cpp
sat_local_search.cpp
sat_lookahead.cpp
Compiling...
func_decl_replace.cpp
sat_lut_finder.cpp
hoist_rewriter.cpp
sat_model_converter.cpp
sat_mus.cpp
inj_axiom.cpp
sat_npn3_finder.cpp
label_rewriter.cpp
sat_parallel.cpp
maximize_ac_sharing.cpp
sat_prob.cpp
mk_simplified_app.cpp
sat_probing.cpp
sat_scc.cpp
pb_rewriter.cpp
sat_simplifier.cpp
pb2bv_rewriter.cpp
sat_solver.cpp
push_app_ite.cpp
sat_watched.cpp
quant_hoist.cpp
sat_xor_finder.cpp
Generating Code...
recfun_rewriter.cpp
rewriter.cpp
seq_axioms.cpp
seq_eq_solver.cpp
seq_rewriter.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\sat\sat.vcxproj]
sat.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\sat\sat.dir\Debug\sat.lib
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/nlsat/nlsat_params.hpp" from "nlsat_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\nlsat\nlsat_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\nlsat\nlsat_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/nlsat/CMakeLists.txt
nlsat_clause.cpp
seq_skolem.cpp
nlsat_evaluator.cpp
th_rewriter.cpp
nlsat_explain.cpp
nlsat_interval_set.cpp
value_sweep.cpp
nlsat_solver.cpp
var_subst.cpp
nlsat_types.cpp
mk_extract_proc.cpp
Generating Code...
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\nlsat\nlsat.vcxproj]
nlsat.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\nlsat\nlsat.dir\Debug\nlsat.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/math/lp/CMakeLists.txt
binary_heap_priority_queue.cpp
binary_heap_upair_queue.cpp
core_solver_pretty_printer.cpp
dense_matrix.cpp
eta_matrix.cpp
emonics.cpp
factorization.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\rewriter\rewriter.vcxproj]
factorization_factory_imp.cpp
rewriter.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\rewriter\rewriter.dir\Debug\rewriter.lib
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/ast/normal_forms/nnf_params.hpp" from "nnf_params.pyg"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/ast/macros/CMakeLists.txt
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\ast\normal_forms\nnf_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\normal_forms\nnf_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/ast/normal_forms/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/ast/proofs/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/ast/rewriter/bit_blaster/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/ast/substitution/CMakeLists.txt
proof_checker.cpp
matcher.cpp
macro_finder.cpp
defined_names.cpp
bit_blaster.cpp
substitution.cpp
elim_term_ite.cpp
gomory.cpp
macro_manager.cpp
proof_utils.cpp
bit_blaster_rewriter.cpp
name_exprs.cpp
substitution_tree.cpp
Generating Code...
hnf_cutter.cpp
quantifier_macro_info.cpp
Generating Code...
unifier.cpp
nnf.cpp
macro_util.cpp
horner.cpp
Generating Code...
pull_quant.cpp
quasi_macros.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\rewriter\bit_blaster\bit_blaster.vcxproj]
bit_blaster.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\rewriter\bit_blaster\bit_blaster.dir\Debug\bit_blaster.lib
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\proofs\proofs.vcxproj]
proofs.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\proofs\proofs.dir\Debug\proofs.lib
indexed_vector.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\substitution\substitution.vcxproj]
substitution.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\substitution\substitution.dir\Debug\substitution.lib
Generating Code...
Generating Code...
int_branch.cpp
int_cube.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\normal_forms\normal_forms.vcxproj]
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\macros\macros.vcxproj]
normal_forms.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\normal_forms\normal_forms.dir\Debug\normal_forms.lib
macros.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\macros\macros.dir\Debug\macros.lib
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/model/model_evaluator_params.hpp" from "model_evaluator_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\model\model_evaluator_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\model\model_evaluator_params.hpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/model/model_params.hpp" from "model_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\model\model_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\model\model_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/model/CMakeLists.txt
array_factory.cpp
int_gcd_test.cpp
datatype_factory.cpp
int_solver.cpp
func_interp.cpp
lar_solver.cpp
model2expr.cpp
model_core.cpp
lar_core_solver.cpp
model.cpp
lp_core_solver_base.cpp
model_evaluator.cpp
lp_dual_core_solver.cpp
Generating Code...
model_implicant.cpp
model_macro_solver.cpp
model_pp.cpp
model_smt2_pp.cpp
model_v2_pp.cpp
numeral_factory.cpp
struct_factory.cpp
value_factory.cpp
Compiling...
lp_dual_simplex.cpp
Generating Code...
lp_primal_core_solver.cpp
lp_primal_simplex.cpp
lp_settings.cpp
lp_solver.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\model\model.vcxproj]
model.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\model\model.dir\Debug\model.lib
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/tactic/tactic_params.hpp" from "tactic_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\tactic\tactic_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\tactic_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/smt/proto_model/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/tactic/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/ast/fpa/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/qe/mbp/CMakeLists.txt
lu.cpp
mbp_arith.cpp
bv2fpa_converter.cpp
dependency_converter.cpp
proto_model.cpp
lp_utils.cpp
equiv_proof_converter.cpp
fpa2bv_converter.cpp
mbp_arrays.cpp
matrix.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\smt\proto_model\proto_model.vcxproj]
proto_model.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\smt\proto_model\proto_model.dir\Debug\proto_model.lib
generic_model_converter.cpp
mon_eq.cpp
fpa2bv_rewriter.cpp
mbp_datatypes.cpp
goal.cpp
monomial_bounds.cpp
mbp_plugin.cpp
Generating Code...
goal_num_occurs.cpp
mbp_solve_plugin.cpp
nex_creator.cpp
goal_shared_occs.cpp
mbp_term_graph.cpp
nla_basics_lemmas.cpp
goal_util.cpp
Generating Code...
horn_subsume_model_converter.cpp
nla_common.cpp
model_converter.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\fpa\fpa.vcxproj]
fpa.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\fpa\fpa.dir\Debug\fpa.lib
nla_core.cpp
probe.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\qe\mbp\mbp.vcxproj]
mbp.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\qe\mbp\mbp.dir\Debug\mbp.lib
proof_converter.cpp
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/sat/smt/CMakeLists.txt
arith_axioms.cpp
nla_intervals.cpp
replace_proof_converter.cpp
sine_filter.cpp
nla_monotone_lemmas.cpp
arith_diagnostics.cpp
tactical.cpp
nla_order_lemmas.cpp
tactic.cpp
arith_internalize.cpp
Generating Code...
nla_solver.cpp
nla_tangent_lemmas.cpp
arith_solver.cpp
nra_solver.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\tactic.vcxproj]
tactic.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\tactic.dir\Debug\tactic.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/tactic/aig/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/tactic/core/CMakeLists.txt
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/solver/combined_solver_params.hpp" from "combined_solver_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\solver\combined_solver_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\solver\combined_solver_params.hpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/solver/parallel_params.hpp" from "parallel_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\solver\parallel_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\solver\parallel_params.hpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/solver/solver_params.hpp" from "solver_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\solver\solver_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\solver\solver_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/solver/CMakeLists.txt
aig.cpp
check_sat_result.cpp
blast_term_ite_tactic.cpp
Generating Code...
array_axioms.cpp
check_logic.cpp
aig_tactic.cpp
cofactor_elim_term_ite.cpp
combined_solver.cpp
Generating Code...
array_diagnostics.cpp
cofactor_term_ite_tactic.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\aig\aig_tactic.vcxproj]
aig_tactic.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\aig\aig_tactic.dir\Debug\aig_tactic.lib
mus.cpp
collect_statistics_tactic.cpp
array_internalize.cpp
parallel_tactic.cpp
ctx_simplify_tactic.cpp
array_model.cpp
smt_logics.cpp
solver.cpp
der_tactic.cpp
array_solver.cpp
solver_na2as.cpp
distribute_forall_tactic.cpp
solver_pool.cpp
dom_simplify_tactic.cpp
atom2bool_var.cpp
Compiling...
permutation_matrix.cpp
solver2tactic.cpp
random_updater.cpp
elim_term_ite_tactic.cpp
bv_ackerman.cpp
tactic2solver.cpp
row_eta_matrix.cpp
elim_uncnstr_tactic.cpp
bv_delay_internalize.cpp
scaler.cpp
Generating Code...
square_dense_submatrix.cpp
injectivity_tactic.cpp
bv_internalize.cpp
square_sparse_matrix.cpp
nnf_tactic.cpp
static_matrix.cpp
bv_invariant.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\solver\solver.vcxproj]
solver.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\solver\solver.dir\Debug\solver.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/cmd_context/CMakeLists.txt
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/ackermannization/ackermannization_params.hpp" from "ackermannization_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\ackermannization\ackermannization_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ackermannization\ackermannization_params.hpp"
occf_tactic.cpp
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/ackermannization/ackermannize_bv_tactic_params.hpp" from "ackermannize_bv_tactic_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\ackermannization\ackermannize_bv_tactic_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ackermannization\ackermannize_bv_tactic_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/ackermannization/CMakeLists.txt
ackermannize_bv_model_converter.cpp
basic_cmds.cpp
Generating Code...
bv_solver.cpp
pb_preprocess_tactic.cpp
ackermannize_bv_tactic.cpp
cmd_context.cpp
propagate_values_tactic.cpp
ackr_bound_probe.cpp
dt_solver.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\lp\lp.vcxproj]
cmd_context_to_goal.cpp
lp.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\lp\lp.dir\Debug\lp.lib
reduce_args_tactic.cpp
ackr_helper.cpp
euf_ackerman.cpp
cmd_util.cpp
ackr_model_converter.cpp
reduce_invertible_tactic.cpp
echo_tactic.cpp
lackr.cpp
euf_internalize.cpp
simplify_tactic.cpp
lackr_model_constructor.cpp
eval_cmd.cpp
solve_eqs_tactic.cpp
euf_invariant.cpp
lackr_model_converter_lazy.cpp
parametric_cmd.cpp
special_relations_tactic.cpp
euf_model.cpp
Generating Code...
pdecl.cpp
Generating Code...
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ackermannization\ackermannization.vcxproj]
ackermannization.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ackermannization\ackermannization.dir\Debug\ackermannization.lib
simplify_cmd.cpp
tactic_cmds.cpp
tactic_manager.cpp
Generating Code...
Compiling...
euf_proof.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\cmd_context\cmd_context.vcxproj]
cmd_context.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\cmd_context\cmd_context.dir\Debug\cmd_context.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/parsers/smt2/CMakeLists.txt
marshal.cpp
euf_relevancy.cpp
smt2parser.cpp
Compiling...
split_clause_tactic.cpp
euf_solver.cpp
symmetry_reduce_tactic.cpp
smt2scanner.cpp
tseitin_cnf_tactic.cpp
Generating Code...
collect_occs.cpp
fpa_solver.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\parsers\smt2\smt2parser.vcxproj]
smt2parser.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\parsers\smt2\smt2parser.dir\Debug\smt2parser.lib
Generating "database.h"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/solver/assertions/CMakeLists.txt
INFO:root:Generated "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/ast/pattern/database.h"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/ast/pattern/CMakeLists.txt
expr_pattern_match.cpp
asserted_formulas.cpp
Generating Code...
pb_card.cpp
pattern_inference.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\core\core_tactics.vcxproj]
pb_constraint.cpp
core_tactics.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\core\core_tactics.dir\Debug\core_tactics.lib
Generating Code...
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/math/subpaving/tactic/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/tactic/bv/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/tactic/arith/CMakeLists.txt
expr2subpaving.cpp
bit_blaster_model_converter.cpp
add_bounds_tactic.cpp
pb_internalize.cpp
subpaving_tactic.cpp
bit_blaster_tactic.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\pattern\pattern.vcxproj]
arith_bounds_tactic.cpp
pattern.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\ast\pattern\pattern.dir\Debug\pattern.lib
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\solver\assertions\solver_assertions.vcxproj]
solver_assertions.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\solver\assertions\solver_assertions.dir\Debug\solver_assertions.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/smt/CMakeLists.txt
arith_eq_adapter.cpp
Generating Code...
bv1_blaster_tactic.cpp
bound_manager.cpp
pb_pb.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\subpaving\tactic\subpaving_tactic.vcxproj]
subpaving_tactic.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\math\subpaving\tactic\subpaving_tactic.dir\Debug\subpaving_tactic.lib
bound_propagator.cpp
arith_eq_solver.cpp
pb_solver.cpp
bvarray2uf_rewriter.cpp
bv2int_rewriter.cpp
dyn_ack.cpp
bvarray2uf_tactic.cpp
q_clause.cpp
bv2real_rewriter.cpp
expr_context_simplifier.cpp
bv_bound_chk_tactic.cpp
q_ematch.cpp
card2bv_tactic.cpp
fingerprints.cpp
bv_bounds_tactic.cpp
degree_shift_tactic.cpp
mam.cpp
bv_size_reduction_tactic.cpp
q_eval.cpp
diff_neq_tactic.cpp
dt2bv_tactic.cpp
old_interval.cpp
eq2bv_tactic.cpp
q_mam.cpp
elim_small_bv_tactic.cpp
qi_queue.cpp
factor_tactic.cpp
max_bv_sharing_tactic.cpp
q_mbi.cpp
seq_axioms.cpp
fix_dl_var_tactic.cpp
Generating Code...
seq_eq_solver.cpp
fm_tactic.cpp
q_model_fixer.cpp
lia2card_tactic.cpp
q_queue.cpp
seq_ne_solver.cpp
lia2pb_tactic.cpp
q_solver.cpp
seq_offset_eq.cpp
linear_equation.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\bv\bv_tactics.vcxproj]
bv_tactics.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\bv\bv_tactics.dir\Debug\bv_tactics.lib
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/tactic/sls/sls_params.hpp" from "sls_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\tactic\sls\sls_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\sls\sls_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/tactic/sls/CMakeLists.txt
bvsls_opt_engine.cpp
nla2bv_tactic.cpp
recfun_solver.cpp
seq_regex.cpp
sls_engine.cpp
normalize_bounds_tactic.cpp
sat_dual_solver.cpp
pb2bv_model_converter.cpp
sls_tactic.cpp
smt_almost_cg_table.cpp
sat_th.cpp
pb2bv_tactic.cpp
smt_arith_value.cpp
Generating Code...
Generating Code...
Generating Code...
smt_case_split_queue.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\sls\sls_tactic.vcxproj]
sls_tactic.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\sls\sls_tactic.dir\Debug\sls_tactic.lib
smt_cg_table.cpp
smt_checker.cpp
smt_clause.cpp
smt_clause_proof.cpp
Compiling...
user_solver.cpp
Generating Code...
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\sat\smt\sat_smt.vcxproj]
sat_smt.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\sat\smt\sat_smt.dir\Debug\sat_smt.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/sat/tactic/CMakeLists.txt
goal2sat.cpp
Compiling...
probe_arith.cpp
propagate_ineqs_tactic.cpp
sat_tactic.cpp
purify_arith_tactic.cpp
Generating Code...
recover_01_tactic.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\sat\tactic\sat_tactic.vcxproj]
sat_tactic.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\sat\tactic\sat_tactic.dir\Debug\sat_tactic.lib
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\arith\arith_tactics.vcxproj]
arith_tactics.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\arith\arith_tactics.dir\Debug\arith_tactics.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/nlsat/tactic/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/cmd_context/extra_cmds/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/sat/sat_solver/CMakeLists.txt
dbg_cmds.cpp
goal2nlsat.cpp
inc_sat_solver.cpp
nlsat_tactic.cpp
polynomial_cmds.cpp
Compiling...
smt_conflict_resolution.cpp
qfnra_nlsat_tactic.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\sat\sat_solver\sat_solver.vcxproj]
sat_solver.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\sat\sat_solver\sat_solver.dir\Debug\sat_solver.lib
subpaving_cmds.cpp
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/tactic/fd_solver/CMakeLists.txt
bounded_int2bv_solver.cpp
smt_consequences.cpp
Generating Code...
Generating Code...
enum2bv_solver.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\nlsat\tactic\nlsat_tactic.vcxproj]
nlsat_tactic.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\nlsat\tactic\nlsat_tactic.dir\Debug\nlsat_tactic.lib
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\cmd_context\extra_cmds\extra_cmds.vcxproj]
extra_cmds.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\cmd_context\extra_cmds\extra_cmds.dir\Debug\extra_cmds.lib
smt_context.cpp
fd_solver.cpp
pb2bv_solver.cpp
smt_context_inv.cpp
smtfd_solver.cpp
smt_context_pp.cpp
Generating Code...
smt_context_stat.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\fd_solver\fd_solver.vcxproj]
fd_solver.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\fd_solver\fd_solver.dir\Debug\fd_solver.lib
smt_enode.cpp
smt_farkas_util.cpp
smt_for_each_relevant_expr.cpp
smt_implied_equalities.cpp
smt_induction.cpp
smt_internalizer.cpp
smt_justification.cpp
smt_kernel.cpp
smt_literal.cpp
smt_lookahead.cpp
smt_model_checker.cpp
smt_model_finder.cpp
smt_model_generator.cpp
smt_parallel.cpp
Generating Code...
Compiling...
smt_quantifier.cpp
smt_quick_checker.cpp
smt_relevancy.cpp
smt_setup.cpp
smt_solver.cpp
smt_statistics.cpp
smt_theory.cpp
smt_value_sort.cpp
smt2_extra_cmds.cpp
theory_arith.cpp
theory_array_bapa.cpp
theory_array_base.cpp
theory_array.cpp
theory_array_full.cpp
theory_bv.cpp
theory_char.cpp
theory_datatype.cpp
theory_dense_diff_logic.cpp
theory_diff_logic.cpp
theory_dl.cpp
Generating Code...
Compiling...
theory_dummy.cpp
theory_fpa.cpp
theory_lra.cpp
theory_opt.cpp
theory_pb.cpp
theory_recfun.cpp
theory_seq.cpp
theory_special_relations.cpp
theory_str.cpp
theory_str_mc.cpp
theory_str_regex.cpp
theory_utvpi.cpp
theory_wmaxsat.cpp
user_propagator.cpp
uses_theory.cpp
watch_list.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\smt\smt.vcxproj]
smt.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\smt\smt.dir\Debug\smt.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/qe/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/smt/tactic/CMakeLists.txt
ctx_solver_simplify_tactic.cpp
nlarith_util.cpp
smt_tactic_core.cpp
nlqsat.cpp
unit_subsumption_tactic.cpp
qe_arith_plugin.cpp
Generating Code...
qe_array_plugin.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\smt\tactic\smt_tactic.vcxproj]
smt_tactic.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\smt\tactic\smt_tactic.dir\Debug\smt_tactic.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/tactic/ufbv/CMakeLists.txt
macro_finder_tactic.cpp
qe_bool_plugin.cpp
quasi_macros_tactic.cpp
qe_bv_plugin.cpp
qe_cmd.cpp
ufbv_rewriter.cpp
ufbv_rewriter_tactic.cpp
qe.cpp
ufbv_tactic.cpp
Generating Code...
qe_datatype_plugin.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\ufbv\ufbv_tactic.vcxproj]
ufbv_tactic.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\ufbv\ufbv_tactic.dir\Debug\ufbv_tactic.lib
qe_dl_plugin.cpp
qe_lite.cpp
qe_mbi.cpp
qe_mbp.cpp
qe_tactic.cpp
qsat.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\qe\qe.vcxproj]
qe.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\qe\qe.dir\Debug\qe.lib
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/muz/base/fp_params.hpp" from "fp_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\muz\base\fp_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\base\fp_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/muz/base/CMakeLists.txt
bind_variables.cpp
dl_boogie_proof.cpp
dl_context.cpp
dl_costs.cpp
dl_rule.cpp
dl_rule_set.cpp
dl_rule_subsumption_index.cpp
dl_rule_transformer.cpp
dl_util.cpp
hnf.cpp
rule_properties.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\base\muz.vcxproj]
muz.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\base\muz.dir\Debug\muz.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/muz/dataflow/CMakeLists.txt
dataflow.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\dataflow\dataflow.vcxproj]
dataflow.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\dataflow\dataflow.dir\Debug\dataflow.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/muz/transforms/CMakeLists.txt
dl_mk_array_blast.cpp
dl_mk_backwards.cpp
dl_mk_bit_blast.cpp
dl_mk_coalesce.cpp
dl_mk_coi_filter.cpp
dl_mk_filter_rules.cpp
dl_mk_interp_tail_simplifier.cpp
dl_mk_karr_invariants.cpp
dl_mk_loop_counter.cpp
dl_mk_magic_sets.cpp
dl_mk_magic_symbolic.cpp
dl_mk_quantifier_abstraction.cpp
dl_mk_quantifier_instantiation.cpp
dl_mk_rule_inliner.cpp
dl_mk_scale.cpp
dl_mk_separate_negated_tails.cpp
dl_mk_slice.cpp
dl_mk_subsumption_checker.cpp
dl_mk_unbound_compressor.cpp
dl_mk_unfold.cpp
Generating Code...
Compiling...
dl_transforms.cpp
dl_mk_array_eq_rewrite.cpp
dl_mk_array_instantiation.cpp
dl_mk_elim_term_ite.cpp
dl_mk_synchronize.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\transforms\transforms.vcxproj]
transforms.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\transforms\transforms.dir\Debug\transforms.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/muz/tab/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/muz/rel/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/muz/bmc/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/muz/spacer/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/muz/clp/CMakeLists.txt
dl_bmc_engine.cpp
tab_context.cpp
spacer_legacy_mev.cpp
clp_context.cpp
aig_exporter.cpp
spacer_legacy_frames.cpp
check_relation.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\clp\clp.vcxproj]
clp.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\clp\clp.dir\Debug\clp.lib
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\tab\tab.vcxproj]
tab.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\tab\tab.dir\Debug\tab.lib
dl_base.cpp
spacer_context.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\bmc\bmc.vcxproj]
bmc.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\bmc\bmc.dir\Debug\bmc.lib
dl_bound_relation.cpp
spacer_dl_interface.cpp
dl_check_table.cpp
spacer_farkas_learner.cpp
dl_compiler.cpp
spacer_generalizers.cpp
dl_external_relation.cpp
spacer_manager.cpp
dl_finite_product_relation.cpp
spacer_prop_solver.cpp
dl_instruction.cpp
spacer_sym_mux.cpp
dl_interval_relation.cpp
spacer_util.cpp
dl_lazy_table.cpp
spacer_iuc_solver.cpp
dl_mk_explanations.cpp
spacer_legacy_mbp.cpp
dl_mk_similarity_compressor.cpp
spacer_proof_utils.cpp
dl_mk_simple_joins.cpp
spacer_unsat_core_learner.cpp
dl_product_relation.cpp
spacer_unsat_core_plugin.cpp
dl_relation_manager.cpp
spacer_matrix.cpp
spacer_antiunify.cpp
dl_sieve_relation.cpp
spacer_mev_array.cpp
dl_sparse_table.cpp
spacer_qe_project.cpp
dl_table.cpp
spacer_sem_matcher.cpp
dl_table_relation.cpp
Generating Code...
Generating Code...
Compiling...
doc.cpp
karr_relation.cpp
Compiling...
spacer_quant_generalizer.cpp
rel_context.cpp
spacer_arith_generalizers.cpp
tbv.cpp
spacer_callback.cpp
udoc_relation.cpp
spacer_json.cpp
Generating Code...
spacer_iuc_proof.cpp
spacer_mbc.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\rel\rel.vcxproj]
rel.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\rel\rel.dir\Debug\rel.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/muz/ddnf/CMakeLists.txt
ddnf.cpp
spacer_pdr.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\ddnf\ddnf.vcxproj]
ddnf.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\ddnf\ddnf.dir\Debug\ddnf.lib
spacer_sat_answer.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\spacer\spacer.vcxproj]
spacer.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\spacer\spacer.dir\Debug\spacer.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/muz/fp/CMakeLists.txt
datalog_parser.cpp
dl_cmds.cpp
dl_register_engine.cpp
horn_tactic.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\fp\fp.vcxproj]
fp.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\muz\fp\fp.dir\Debug\fp.lib
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/tactic/smtlogics/qfufbv_tactic_params.hpp" from "qfufbv_tactic_params.pyg"
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\tactic\smtlogics\qfufbv_tactic_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\smtlogics\qfufbv_tactic_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/tactic/smtlogics/CMakeLists.txt
nra_tactic.cpp
qfaufbv_tactic.cpp
qfauflia_tactic.cpp
qfbv_tactic.cpp
qfidl_tactic.cpp
qflia_tactic.cpp
qflra_tactic.cpp
qfnia_tactic.cpp
qfnra_tactic.cpp
qfufbv_ackr_model_converter.cpp
qfufbv_tactic.cpp
qfuf_tactic.cpp
quant_tactics.cpp
smt_tactic.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\smtlogics\smtlogic_tactics.vcxproj]
smtlogic_tactics.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\smtlogics\smtlogic_tactics.dir\Debug\smtlogic_tactics.lib
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/opt/opt_params.hpp" from "opt_params.pyg"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/tactic/fpa/CMakeLists.txt
INFO:root:Using C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\z3-sys-0.7.1\z3\src\opt\opt_params.pyg
INFO:root:Generated "C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\opt\opt_params.hpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/opt/CMakeLists.txt
fpa2bv_model_converter.cpp
maxlex.cpp
fpa2bv_tactic.cpp
maxres.cpp
qffp_tactic.cpp
qffplra_tactic.cpp
maxsmt.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\fpa\fpa_tactics.vcxproj]
fpa_tactics.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\fpa\fpa_tactics.dir\Debug\fpa_tactics.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/tactic/portfolio/CMakeLists.txt
opt_cmds.cpp
default_tactic.cpp
smt_strategic_solver.cpp
opt_context.cpp
solver2lookahead.cpp
Generating Code...
opt_lns.cpp
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\portfolio\portfolio.vcxproj]
portfolio.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\tactic\portfolio\portfolio.dir\Debug\portfolio.lib
opt_pareto.cpp
opt_parse.cpp
optsmt.cpp
opt_solver.cpp
pb_sls.cpp
sortmax.cpp
wmax.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\opt\opt.vcxproj]
opt.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\opt\opt.dir\Debug\opt.lib
Generating api_commands.cpp;api_log_macros.cpp;api_log_macros.h
Faking emission of 'z3\z3core.py'
Generated 'C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/api\api_log_macros.h'
Generated 'C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/api\api_log_macros.cpp'
Generated 'C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/api\api_commands.cpp'
Generated 'C:\Users\ahelwer\AppData\Local\Temp\tmpzd5v3sx0'
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/api/CMakeLists.txt
api_algebraic.cpp
api_arith.cpp
api_array.cpp
api_ast.cpp
api_ast_map.cpp
api_ast_vector.cpp
api_bv.cpp
api_config_params.cpp
api_context.cpp
api_datalog.cpp
api_datatype.cpp
api_fpa.cpp
api_goal.cpp
api_log.cpp
api_model.cpp
api_numeral.cpp
api_opt.cpp
api_params.cpp
api_parsers.cpp
api_pb.cpp
Generating Code...
Compiling...
api_polynomial.cpp
api_qe.cpp
api_quant.cpp
api_rcf.cpp
api_seq.cpp
api_solver.cpp
api_special_relations.cpp
api_stats.cpp
api_tactic.cpp
z3_replayer.cpp
api_commands.cpp
api_log_macros.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\api\api.vcxproj]
api.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\api\api.dir\Debug\api.lib
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/api/dll/gparams_register_modules.cpp"
INFO:root:Generated "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/api/dll\gparams_register_modules.cpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/api/dll/install_tactic.cpp"
INFO:root:Generated "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/api/dll\install_tactic.cpp"
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/api/dll/mem_initializer.cpp"
INFO:root:Generated "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/api/dll\mem_initializer.cpp"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/api/dll/CMakeLists.txt
dll.cpp
gparams_register_modules.cpp
install_tactic.cpp
mem_initializer.cpp
Generating Code...
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\api\dll\api_dll.vcxproj]
api_dll.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\api\dll\api_dll.dir\Debug\api_dll.lib
Generating "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/api_dll.def"
INFO:root:Generated "C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/build/src/api_dll.def"
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/CMakeLists.txt
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/src/CMakeLists.txt
LINK : warning LNK4044: unrecognized option '/INCREMENTAL:NO'; ignored [C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\src\libz3.vcxproj]
libz3.vcxproj -> C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\build\Debug\libz3.lib
Building Custom Rule C:/Users/ahelwer/.cargo/registry/src/github.com-1ecc6299db9ec823/z3-sys-0.7.1/z3/CMakeLists.txt
-- Install configuration: "Debug"
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/lib/cmake/z3/Z3Targets.cmake
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/lib/cmake/z3/Z3Targets-debug.cmake
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/lib/cmake/z3/Z3Config.cmake
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/lib/cmake/z3/Z3ConfigVersion.cmake
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/lib/pkgconfig/z3.pc
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/lib/libz3.lib
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/include/z3_algebraic.h
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/include/z3_api.h
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/include/z3_ast_containers.h
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/include/z3_fixedpoint.h
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/include/z3_fpa.h
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/include/z3.h
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/include/z3++.h
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/include/z3_macros.h
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/include/z3_optimization.h
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/include/z3_polynomial.h
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/include/z3_rcf.h
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/include/z3_v1.h
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/include/z3_spacer.h
-- Installing: C:/Users/ahelwer/source/teleport-z3/target/debug/build/z3-sys-d974b02077215d28/out/include/z3_version.h
cargo:root=C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out
cargo:rustc-link-search=native=C:\Users\ahelwer\source\teleport-z3\target\debug\build\z3-sys-d974b02077215d28\out\lib
cargo:rustc-link-lib=static=libz3
cargo:rerun-if-changed=build.rs
cargo:rerun-if-changed=z3/src/api/z3.h
--- stderr
CMake Warning at CMakeLists.txt:51 (message):
Disabling Z3_INCLUDE_GIT_DESCRIBE
Call Stack (most recent call first):
CMakeLists.txt:100 (disable_git_describe)
CMake Warning at CMakeLists.txt:55 (message):
Disabling Z3_INCLUDE_GIT_HASH
Call Stack (most recent call first):
CMakeLists.txt:101 (disable_git_hash)
CMake Warning (dev) at cmake/msvc_legacy_quirks.cmake:160 (message):
Skipping legacy linker MSVC options for x86_64 RELEASE
Call Stack (most recent call first):
CMakeLists.txt:423 (include)
This warning is for project developers. Use -Wno-dev to suppress it.
CMake Warning (dev) at cmake/msvc_legacy_quirks.cmake:160 (message):
Skipping legacy linker MSVC options for x86_64 RELWITHDEBINFO
Call Stack (most recent call first):
CMakeLists.txt:423 (include)
This warning is for project developers. Use -Wno-dev to suppress it.
CMake Warning at examples/CMakeLists.txt:24 (message):
Cannot set built type of external project when building with a
multi-configuration generator
CMake Warning:
Manually-specified variables were not used by the project:
CMAKE_ASM_FLAGS
CMAKE_ASM_FLAGS_DEBUG
CMAKE_BUILD_TYPE
CMAKE_C_FLAGS
CMAKE_C_FLAGS_DEBUG
thread 'main' panicked at 'Unable to find libclang: "couldn\'t find any valid shared libraries matching: [\'clang.dll\', \'libclang.dll\'], set the `LIBCLANG_PATH` environment variable to a path where one of these files can be found (invalid: [])"', C:\Users\ahelwer\.cargo\registry\src\github.com-1ecc6299db9ec823\bindgen-0.58.1\src/lib.rs:2057:31
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
Not sure why it's looking for clang instead of using MSVC. Upon looking at the github actions workflow in this repo it seems clang is required though, so I'll install it then try again.
After installing llvm from chocolatey the build now succeeds! Unfortunately was not able to reproduce the OP's issue; would be nice to have the build dependencies documented somewhere, or linked to from the project's or package's README.
Not sure why it's looking for clang instead of using MSVC.
z3-sys uses bindgen in the build process to re-generate the ffi, and bindgen depends on libclang. Imo bindgen shouldn't be part of the regular build process, the dependency hell that is unleashed on consuming crates is horrible :|