Compilation Error

[gpfarina]

Hi I can't compile Z3. These are the last lines of compilation:
g++ -o z3 shell/mem_initializer.o shell/datalog_frontend.o shell/lp_frontend.o shell/gparams_register_modules.o shell/z3_log_frontend.o shell/main.o shell/opt_frontend.o shell/install_tactic.o shell/smtlib_frontend.o shell/dimacs_frontend.o api/api.a opt/opt.a parsers/smt/smtparser.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a sat/sat_solver/sat_solver.a tactic/ufbv/ufbv_tactic.a tactic/nlsat_smt/nlsat_smt_tactic.a muz/fp/fp.a muz/duality/duality_intf.a muz/ddnf/ddnf.a muz/bmc/bmc.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/pdr/pdr.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a duality/duality.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a smt/smt.a smt/proto_model/proto_model.a smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/pattern/pattern.a ast/fpa/fpa.a ast/proof_checker/proof_checker.a parsers/smt2/smt2parser.a cmd_context/extra_cmds/extra_cmds.a cmd_context/cmd_context.a interp/interp.a ackermannization/ackermannization.a solver/solver.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a sat/tactic/sat_tactic.a tactic/core/core_tactics.a math/euclid/euclid.a math/grobner/grobner.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/macros/macros.a ast/rewriter/rewriter.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a math/automata/automata.a math/simplex/simplex.a math/hilbert/hilbert.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/lp/lp.a util/util.a -lpthread -fopenmp -lrt
tactic/core/core_tactics.a(dom_simplify_tactic.o):(.data.rel.ro._ZTI28expr_substitution_simplifier[_ZTI28expr_substitution_simplifier]+0x10): undefined reference to `typeinfo for dom_simplify_tactic::simplifier'
collect2: error: ld returned 1 exit status
Makefile:4041: recipe for target 'z3' failed
make: *** [z3] Error 1

some info:
Linux balerion 4.10.0-35-generic #39-Ubuntu SMP Wed Sep 13 07:46:59 UTC 2017 x86_64 x86_64 x86_64 GNU/Linux

g++ -v
Using built-in specs.
COLLECT_GCC=g++
COLLECT_LTO_WRAPPER=/usr/lib/gcc/x86_64-linux-gnu/6/lto-wrapper
Target: x86_64-linux-gnu
Configured with: ../src/configure -v --with-pkgversion='Ubuntu 6.3.0-12ubuntu2' --with-bugurl=file:///usr/share/doc/gcc-6/README.Bugs --enable-languages=c,ada,c++,java,go,d,fortran,objc,obj-c++ --prefix=/usr --program-suffix=-6 --program-prefix=x86_64-linux-gnu- --enable-shared --enable-linker-build-id --libexecdir=/usr/lib --without-included-gettext --enable-threads=posix --libdir=/usr/lib --enable-nls --with-sysroot=/ --enable-clocale=gnu --enable-libstdcxx-debug --enable-libstdcxx-time=yes --with-default-libstdcxx-abi=new --enable-gnu-unique-object --disable-vtable-verify --enable-libmpx --enable-plugin --enable-default-pie --with-system-zlib --disable-browser-plugin --enable-java-awt=gtk --enable-gtk-cairo --with-java-home=/usr/lib/jvm/java-1.5.0-gcj-6-amd64/jre --enable-java-home --with-jvm-root-dir=/usr/lib/jvm/java-1.5.0-gcj-6-amd64 --with-jvm-jar-dir=/usr/lib/jvm-exports/java-1.5.0-gcj-6-amd64 --with-arch-directory=amd64 --with-ecj-jar=/usr/share/java/eclipse-ecj.jar --with-target-system-zlib --enable-objc-gc=auto --enable-multiarch --disable-werror --with-arch-32=i686 --with-abi=m64 --with-multilib-list=m32,m64,mx32 --enable-multilib --with-tune=generic --enable-checking=release --build=x86_64-linux-gnu --host=x86_64-linux-gnu --target=x86_64-linux-gnu
Thread model: posix
gcc version 6.3.0 20170406 (Ubuntu 6.3.0-12ubuntu2)

[wintersteiger]

Yes, the master branch currently doesn't build; fix in progress.

[oferst]

The problem I see now to compile is different:
/bin/sh: interp../smt/smt_solver.h.node: No such file or directory
make: *** [Makefile:1299: interp../smt/smt_solver.h.node] Error 1

this is with typing make in the build directory. That file is actually there so it seems just a matter of where is it looking for it. Am I missing some env. variable ?

[wintersteiger]

Could you try re-running mk_make.py to update the build directory in case any files changed since your last upgrade?

[oferst]

I tried now several paths:

1. I tried to download the pre-compiled executable from github, but apparently it requires certain permissions which I do not have.

2. I downloaded the executable from codeplax, but apparently it is an older version (specifically, it does not support assert-soft, which I need).

3. I cloned the sources and tried to compile via the VS 2017 command prompt. The python stage seems to work fine. Then with nmake I am getting:

c:\z3\build>nmake

Microsoft (R) Program Maintenance Utility Version 14.12.25831.0
Copyright (C) Microsoft Corporation. All rights reserved.

datalog_frontend.cpp
C:\Program Files (x86)\Windows Kits\10\include\10.0.16299.0\um\winnt.h(21998): error C3861: '__readfsdword': identifier not found
C:\Program Files (x86)\Windows Kits\10\include\10.0.16299.0\um\winbase.h(9189): error C2065: 'InterlockedIncrement64': undeclared identifier
C:\Program Files (x86)\Windows Kits\10\include\10.0.16299.0\um\winbase.h(9221): error C2065: 'InterlockedDecrement64': undeclared identifier
C:\Program Files (x86)\Windows Kits\10\include\10.0.16299.0\um\winbase.h(9257): error C3861: 'InterlockedExchange64': identifier not found
C:\Program Files (x86)\Windows Kits\10\include\10.0.16299.0\um\winbase.h(9311): error C3861: 'InterlockedExchangeAdd64': identifier not found
C:\Program Files (x86)\Windows Kits\10\include\10.0.16299.0\um\winbase.h(9321): error C3861: 'InterlockedExchangeAdd64': identifier not found
C:\Program Files (x86)\Windows Kits\10\include\10.0.16299.0\um\winbase.h(9368): error C3861: 'InterlockedAnd64': identifier not found
C:\Program Files (x86)\Windows Kits\10\include\10.0.16299.0\um\winbase.h(9378): error C3861: 'InterlockedOr64': identifier not found
C:\Program Files (x86)\Windows Kits\10\include\10.0.16299.0\um\winbase.h(9388): error C3861: 'InterlockedXor64': identifier not found
NMAKE : fatal error U1077: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\Enterprise\VC\Tools\MSVC\14.12.25827\bin\HostX86\x86\cl.EXE"' : return code '0x2'
Stop.

4. The make route: python stage seems fine. Inside bash I get errors related to mingw, apparently:
   STAFF+ofers@strichman-ofer /cygdrive/c/z3/build
   $ make
   src/shell/datalog_frontend.cpp
   In file included from c:\mingw\lib\gcc\mingw32\4.9.3\include\c++\cmath:44:0,
   from c:\mingw\lib\gcc\mingw32\4.9.3\include\c++\random:38,
   from c:\mingw\lib\gcc\mingw32\4.9.3\include\c++\bits\stl_algo.h:66,
   from c:\mingw\lib\gcc\mingw32\4.9.3\include\c++\algorithm:62,
   from ../src/util/vector.h:28,
   from ../src/ast/ast.h:22,
   from ../src/smt/params/smt_params.h:22,
   from ../src/shell/datalog_frontend.cpp:28:
   c:\mingw\include\math.h: In function 'float hypotf(float, float)':
   c:\mingw\include\math.h:635:30: error: '_hypot' was not declared in this scope
   { return (float)(_hypot (x, y)); }
   ^
   make: *** [Makefile:3986: shell/datalog_frontend.o] Error 1