[MSVC] Z3 build failed due to error C2666 and error C2512 under msvc x86 mode

[Zhaojun-Liu]

Issue description:
Hi,
Recently we updated the Z3 commit, it built failed due to error C2666 and C2512 under msvc x86 mode. Could you please take a look? Thanks.

Repro steps:

1. git clone https://github.com/Z3Prover/z3 F:\gitP\Z3Prover\z3
2. mkdir F:\gitP\Z3Prover\z3\build_x86 and cd F:\gitP\Z3Prover\z3\build_x86
3. cmake -G "Visual Studio 16 2019" -A Win32 -DCMAKE_SYSTEM_VERSION=10.0.18362.0 .. 2>&1
4. msbuild /m /p:Platform=Win32 /p:Configuration=Release Z3.sln /t:Rebuild /p:BuildInParallel=true 2>&1
5. msbuild /m /p:Platform=Win32 /p:Configuration=Release .\examples\c_example.vcxproj /t:Rebuild /p:BuildInParallel=true 2>&1
6. msbuild /m /p:Platform=Win32 /p:Configuration=Release .\examples\cpp_example.vcxproj /t:Rebuild /p:BuildInParallel=true 2>&1

Expected result:
build successfully.

Actual result:
example.cpp 1>F:\gitP\Z3Prover\z3\examples\c++\example.cpp(931,27): error C2666: 'z3::ast_vector_tpl<z3::func_decl>::operator []': 2 overloads have similar conversions [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example_build_dir\cpp_example.vcxproj] [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example.vcxproj] F:\gitP\Z3Prover\z3\src\api\c++\z3++.h(547,11): message : could be 'T z3::ast_vector_tpl<T>::operator [](unsigned int) const' [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example_build_dir\cpp_example.vcxproj] with [ T=z3::func_decl ] F:\gitP\Z3Prover\z3\examples\c++\example.cpp(931,27): message : or 'built-in C++ operator[](Z3_ast_vector, int)' [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example_build_dir\cpp_example.vcxproj] F:\gitP\Z3Prover\z3\examples\c++\example.cpp(931,27): message : while trying to match the argument list '(z3::func_decl_vector, int)' [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example_build_dir\cpp_example.vcxproj] 1>F:\gitP\Z3Prover\z3\examples\c++\example.cpp(931,12): error C2512: 'z3::expr': no appropriate default constructor available [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example_build_dir\cpp_example.vcxproj] [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example.vcxproj] F:\gitP\Z3Prover\z3\src\api\c++\z3++.h(756,11): message : see declaration of 'z3::expr' [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example_build_dir\cpp_example.vcxproj] 1>F:\gitP\Z3Prover\z3\examples\c++\example.cpp(932,27): error C2666: 'z3::ast_vector_tpl<z3::func_decl>::operator []': 2 overloads have similar conversions [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example_build_dir\cpp_example.vcxproj] [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example.vcxproj] F:\gitP\Z3Prover\z3\src\api\c++\z3++.h(547,11): message : could be 'T z3::ast_vector_tpl<T>::operator [](unsigned int) const' [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example_build_dir\cpp_example.vcxproj] with [ T=z3::func_decl ] F:\gitP\Z3Prover\z3\examples\c++\example.cpp(932,27): message : or 'built-in C++ operator[](Z3_ast_vector, int)' [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example_build_dir\cpp_example.vcxproj] F:\gitP\Z3Prover\z3\examples\c++\example.cpp(932,27): message : while trying to match the argument list '(z3::func_decl_vector, int)' [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example_build_dir\cpp_example.vcxproj] 1>F:\gitP\Z3Prover\z3\examples\c++\example.cpp(932,12): error C2512: 'z3::expr': no appropriate default constructor available [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example_build_dir\cpp_example.vcxproj] [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example.vcxproj] F:\gitP\Z3Prover\z3\src\api\c++\z3++.h(756,11): message : see declaration of 'z3::expr' [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example_build_dir\cpp_example.vcxproj] 1>C:\Program Files (x86)\Microsoft Visual Studio\2019\Enterprise\MSBuild\Microsoft\VC\v160\Microsoft.CppCommon.targets(241,5): error MSB8066: Custom build for 'F:\gitP\Z3Prover\z3\build_x86\CMakeFiles\4609bd6cd9cc5fb43033028daf6957b5\cpp_example-mkdir.rule;F:\gitP\Z3Prover\z3\build_x86\CMakeFiles\4609bd6cd9cc5fb43033028daf6957b5\cpp_example-download.rule;F:\gitP\Z3Prover\z3\build_x86\CMakeFiles\4609bd6cd9cc5fb43033028daf6957b5\cpp_example-update.rule;F:\gitP\Z3Prover\z3\build_x86\CMakeFiles\4609bd6cd9cc5fb43033028daf6957b5\cpp_example-patch.rule;F:\gitP\Z3Prover\z3\build_x86\CMakeFiles\4609bd6cd9cc5fb43033028daf6957b5\cpp_example-configure.rule;F:\gitP\Z3Prover\z3\build_x86\CMakeFiles\4609bd6cd9cc5fb43033028daf6957b5\cpp_example-build.rule;F:\gitP\Z3Prover\z3\build_x86\CMakeFiles\4609bd6cd9cc5fb43033028daf6957b5\cpp_example-install.rule;F:\gitP\Z3Prover\z3\build_x86\CMakeFiles\782db93e8c89b44bf5185765149ccfc7\cpp_example-complete.rule;F:\gitP\Z3Prover\z3\build_x86\CMakeFiles\7e1b667b19f6561c54638f80932b54dc\cpp_example.rule;F:\gitP\Z3Prover\z3\examples\CMakeLists.txt' exited with code 1. [F:\gitP\Z3Prover\z3\build_x86\examples\cpp_example.vcxproj]

Detailed log:
build.log

More info:
the commit we use is: 470bf27
and I tried the currently latest commit: 30165ed, the issue is persisting.
Windows version: Windows server 2019
VS version: VS2019 (VS16.11.11)

[NikolajBjorner]

I don't understand the error message. It doesn't occur on other platforms. File a bug against the piece that produces the message.
The error message appears malformed:

 C:\z36114\examples\c++\example.cpp(934,29): message : or       'built-in C++ operator[(Z3_ast_vector, int)' [C:\z36114\build\examples\cpp_example_build_dir\cpp_example
         .vcxproj]

The bracket '[' is not matched.

[Zhaojun-Liu]

Hi @NikolajBjorner , I didn't understand what you meant and your error message doesn't look the same as ours.

[NikolajBjorner]

You have

or 'built-in C++ operator[](Z3_ast_vector, int)'

My error message is slightly different with the right ] missing.
Either way, what is this built-in operator?
The other platforms don't throw this error. I don't see it in our own builds.
I can't debug the error because it doesn't make sense.
Figure out how to fix it or file a bug against the compiler.

[Zhaojun-Liu]

@NikolajBjorner Ok, I got it. Thanks for your reply.

[joemmett]

The error from the compiler is legitimate for the x86 MSVC compiler because ptrdiff_t is int on that platform and that type is important for the built-in [] operator for pointer arithmetic. I can get a similar errors from a reduced example using Clang and GCC with 32-bit targets: https://godbolt.org/z/7EcTGzsGr.

The ambiguity here is in resolving the overload between the operator[] of ast_vector_tpl (which involves converting the literal 0 to unsigned int) or instead using the implicit conversion operator to Z3_ast_vector and then using the built-in [] operator to do pointer arithmetic on it. You can get a similar error even on the 64-bit compilers by changing the argument from 0 to 0L.