z3.rs z3-sys fails to build on Windows?

z3-sys fails to build on Windows?

Open zkat opened this issue 4 years ago • 6 comments

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 backtrace
warning: build failed, waiting for other jobs to finish...
error: build failed

Aug 01 '20 23:08 zkat

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!

Aug 03 '20 15:08 fitzgen

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.

Sep 15 '20 06:09 lzybkr

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.

Oct 18 '21 14:10 ahelwer

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.

Oct 18 '21 15:10 ahelwer

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.

Oct 18 '21 15:10 ahelwer

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 :|

May 10 '22 09:05 Trolldemorted

z3.rs z3.rs copied to clipboard

z3-sys fails to build on Windows?

z3.rs
z3.rs copied to clipboard