Build from source error: ‘mod’ is not a member of ‘z3’

[Troublor]

Description

I tried to build solidity from source code with the latest version. I followed the instructions in Solidity Documentation, but I ran into an error when execute: cmake .. && make. The cmake error is as follows:

-- boost version: 106501
-- boost headers: /usr/include
-- boost lib   : /usr/lib/x86_64-linux-gnu/libboost_regex.a;/usr/lib/x86_64-linux-gnu/libboost_filesystem.a;/usr/lib/x86_64-linux-gnu/libboost_unit_test_framework.a;/usr/lib/x86_64-linux-gnu/libboost_program_options.a;/usr/lib/x86_64-linux-gnu/libboost_system.a

------------------------------------------------------------------------
-- Configuring solidity
------------------------------------------------------------------------
--                  CMake Version                            3.10.2
-- CMAKE_BUILD_TYPE Build type                               
-- TARGET_PLATFORM  Target platform                          Linux
--------------------------------------------------------------- features
-- COVERAGE         Coverage support                         OFF
------------------------------------------------------------- components
-- TESTS            Build tests                              ON
------------------------------------------------------------------------

Z3 SMT solver found. This enables optional SMT checking with Z3.
-- Configuring done
-- Generating done
-- Build files have been written to: /home/troublor/Softwares/solidity/build
[  0%] Built target solidity_BuildInfo.h
[  4%] Built target jsoncpp-project
[  8%] Built target devcore
[ 12%] Built target langutil
Scanning dependencies of target evmasm
[ 12%] Building CXX object libevmasm/CMakeFiles/evmasm.dir/Assembly.cpp.o
[ 12%] Building CXX object libevmasm/CMakeFiles/evmasm.dir/BlockDeduplicator.cpp.o
[ 13%] Building CXX object libevmasm/CMakeFiles/evmasm.dir/CommonSubexpressionEliminator.cpp.o
[ 13%] Building CXX object libevmasm/CMakeFiles/evmasm.dir/ControlFlowGraph.cpp.o
[ 14%] Building CXX object libevmasm/CMakeFiles/evmasm.dir/ExpressionClasses.cpp.o
[ 14%] Building CXX object libevmasm/CMakeFiles/evmasm.dir/GasMeter.cpp.o
[ 14%] Building CXX object libevmasm/CMakeFiles/evmasm.dir/KnownState.cpp.o
[ 14%] Building CXX object libevmasm/CMakeFiles/evmasm.dir/PathGasMeter.cpp.o
[ 15%] Building CXX object libevmasm/CMakeFiles/evmasm.dir/PeepholeOptimiser.cpp.o
[ 15%] Building CXX object libevmasm/CMakeFiles/evmasm.dir/SemanticInformation.cpp.o
[ 15%] Building CXX object libevmasm/CMakeFiles/evmasm.dir/SimplificationRules.cpp.o
[ 16%] Linking CXX static library libevmasm.a
[ 19%] Built target evmasm
Scanning dependencies of target yul
[ 20%] Building CXX object libyul/CMakeFiles/yul.dir/optimiser/DeadCodeEliminator.cpp.o
[ 21%] Building CXX object libyul/CMakeFiles/yul.dir/optimiser/Semantics.cpp.o
[ 21%] Building CXX object libyul/CMakeFiles/yul.dir/optimiser/SimplificationRules.cpp.o
[ 22%] Building CXX object libyul/CMakeFiles/yul.dir/optimiser/Suite.cpp.o
[ 23%] Linking CXX static library libyul.a
[ 41%] Built target yul
Scanning dependencies of target solidity
[ 41%] Building CXX object libsolidity/CMakeFiles/solidity.dir/analysis/ViewPureChecker.cpp.o
[ 41%] Building CXX object libsolidity/CMakeFiles/solidity.dir/interface/GasEstimator.cpp.o
[ 41%] Building CXX object libsolidity/CMakeFiles/solidity.dir/interface/Version.cpp.o
[ 42%] Building CXX object libsolidity/CMakeFiles/solidity.dir/formal/Z3Interface.cpp.o
/home/troublor/Softwares/solidity/libsolidity/formal/Z3Interface.cpp: In member function ‘z3::expr dev::solidity::smt::Z3Interface::toZ3Expr(const dev::solidity::smt::Expression&)’:
/home/troublor/Softwares/solidity/libsolidity/formal/Z3Interface.cpp:166:14: error: ‘mod’ is not a member of ‘z3’
   return z3::mod(arguments[0], arguments[1]);
              ^~~
/home/troublor/Softwares/solidity/libsolidity/formal/Z3Interface.cpp:166:14: note: suggested alternative: ‘cond’
   return z3::mod(arguments[0], arguments[1]);
              ^~~
              cond
libsolidity/CMakeFiles/solidity.dir/build.make:1166: recipe for target 'libsolidity/CMakeFiles/solidity.dir/formal/Z3Interface.cpp.o' failed
make[2]: *** [libsolidity/CMakeFiles/solidity.dir/formal/Z3Interface.cpp.o] Error 1
CMakeFiles/Makefile2:389: recipe for target 'libsolidity/CMakeFiles/solidity.dir/all' failed
make[1]: *** [libsolidity/CMakeFiles/solidity.dir/all] Error 2
Makefile:129: recipe for target 'all' failed
make: *** [all] Error 2

My Z3 version is 4.8.0 - 64 bit and I'm using Ubuntu 18.04 I also tried to build with the solidity_0.5.7.tar.gz in the release page and it's the same problem.

[leonardoalt]

That is weird. If cmake said it found Z3 than the version should be correct. I also have 4.8.0 - 64 bit on Linux. I'm guessing you installed Z3 4.8.0 manually, since Ubuntu still distributes Z3 4.4. Can you please open CMakeCache.txt and check variables Z3_EXECUTABLE, Z3_INCLUDE_DIR and Z3_LIBRARY? It could be that you have multiple versions installed and there's some confusion going on the cmake side.

[Troublor]

@leonardoalt Thanks for your help!
I did install Z3 4.8.0 manually. Z3_INCLUDE_DIR does have a problem. After I move head files in z3/include to /usr/include, it works. Thank you.

//Path to a program.
Z3_EXECUTABLE:FILEPATH=/my/path/to/z3-4.8.4.d6df51951f4c-x64-ubuntu-16.04/bin/z3

//Path to a file.
Z3_INCLUDE_DIR:PATH=/usr/include

//Path to a library.
Z3_LIBRARY:FILEPATH=/my/path/to/z3-4.8.4.d6df51951f4c-x64-ubuntu-16.04/bin/libz3.so

[anurag-git]

I am facing same issue. I just pulled new changes and didn't install anything.

My CMakeCache.txt says

//Path to a program.
Z3_EXECUTABLE:FILEPATH=Z3_EXECUTABLE-NOTFOUND

//Path to a file.
Z3_INCLUDE_DIR:PATH=/usr/include

//Path to a library.
[Z3_LIBRARY:FILEPATH=/usr/lib/x86_64-linux-gnu/libz3.so`]

@leonardoalt , any idea?

[leonardoalt]

@anurag-git The build system also needs the z3 executable in this case, in order to check the version. It looks like in your case it couldn't find it. This is indeed a new requirement that wasn't there before. Could you please check that you have the executable installed?

[zerjioang]

I do have the same misconfiguration problem when using Ubuntu 18 on ARM (armv7l) device. Is there a final solution to this issue?

[leonardoalt]

@zerjioang so far we've encountered no issues on the build system side. In @anurag-git 's case it looks like the executable is not installed. Can you please open CMakeCache.txt and check variables Z3_EXECUTABLE, Z3_INCLUDE_DIR and Z3_LIBRARY?

[zerjioang]

@leonardoalt my Z3 installer was missing, I just install it with apt and everything was fine. I thought it was automatically installed after running install_deps script

[leonardoalt]

Ok, good! I'll close the issue then. @anurag-git please re-open if it still doesn't work for you after installing the executable.