Source: z3 Version: 4.4.1-0.2 Severity: serious Justification: fails to build from source User: reproducible-bui...@lists.alioth.debian.org Usertags: ftbfs X-Debbugs-Cc: reproducible-bui...@lists.alioth.debian.org
Dear Maintainer,
z3 fails to build from source in unstable/amd64:
[..]
dh_ocamlinit -O--parallel
debian/rules override_dh_auto_configure
make[1]: Entering directory
'/home/lamby/temp/cdt.20160828113355.M8pdxROBix.db.z3/z3-4.4.1'
if [ yes = yes ]; then \
sed -i 's/^DOTNET_ENABLED=.*/DOTNET_ENABLED=True/' scripts/mk_util.py; \
else \
sed -i 's/^DOTNET_ENABLED=.*/DOTNET_ENABLED=False/' scripts/mk_util.py;
\
fi
if [ yes = yes ]; then \
python scripts/mk_make.py --java --ml
--prefix=/home/lamby/temp/cdt.20160828113355.M8pdxROBix.db.z3/z3-4.4.1/debian/tmp/usr;
\
else \
python scripts/mk_make.py --ml
--prefix=/home/lamby/temp/cdt.20160828113355.M8pdxROBix.db.z3/z3-4.4.1/debian/tmp/usr;
\
fi
opt = --java, arg =
opt = --ml, arg =
opt = --prefix, arg =
/home/lamby/temp/cdt.20160828113355.M8pdxROBix.db.z3/z3-4.4.1/debian/tmp/usr
New component: 'util'
New component: 'polynomial'
New component: 'sat'
New component: 'nlsat'
New component: 'hilbert'
New component: 'simplex'
New component: 'interval'
New component: 'realclosure'
New component: 'subpaving'
New component: 'ast'
New component: 'rewriter'
New component: 'normal_forms'
New component: 'model'
New component: 'tactic'
New component: 'substitution'
New component: 'parser_util'
New component: 'grobner'
New component: 'euclid'
New component: 'core_tactics'
New component: 'sat_tactic'
New component: 'arith_tactics'
New component: 'nlsat_tactic'
New component: 'subpaving_tactic'
New component: 'aig_tactic'
New component: 'solver'
New component: 'interp'
New component: 'cmd_context'
New component: 'extra_cmds'
New component: 'smt2parser'
New component: 'proof_checker'
New component: 'simplifier'
New component: 'fpa'
New component: 'macros'
New component: 'pattern'
New component: 'bit_blaster'
New component: 'smt_params'
New component: 'proto_model'
New component: 'smt'
New component: 'user_plugin'
New component: 'bv_tactics'
New component: 'fuzzing'
New component: 'smt_tactic'
New component: 'sls_tactic'
New component: 'qe'
New component: 'duality'
New component: 'muz'
New component: 'dataflow'
New component: 'transforms'
New component: 'rel'
New component: 'pdr'
New component: 'clp'
New component: 'tab'
New component: 'bmc'
New component: 'ddnf'
New component: 'duality_intf'
New component: 'fp'
New component: 'nlsat_smt_tactic'
New component: 'smtlogic_tactics'
New component: 'fpa_tactics'
New component: 'ufbv_tactic'
New component: 'sat_solver'
New component: 'portfolio'
New component: 'smtparser'
New component: 'opt'
New component: 'api'
New component: 'shell'
New component: 'test'
New component: 'api_dll'
New component: 'dotnet'
New component: 'java'
New component: 'ml'
New component: 'cpp'
Python bindings directory was detected.
New component: 'cpp_example'
New component: 'iz3'
New component: 'z3_tptp'
New component: 'c_example'
New component: 'maxsat'
New component: 'dotnet_example'
New component: 'java_example'
New component: 'py_example'
Generated 'src/util/version.h'
Updated 'src/api/dotnet/Properties/AssemblyInfo'
Generated 'src/nlsat/nlsat_params.hpp'
Generated 'src/tactic/sls/sls_params.hpp'
Generated 'src/math/realclosure/rcf_params.hpp'
Generated 'src/math/polynomial/algebraic_params.hpp'
Generated 'src/muz/base/fixedpoint_params.hpp'
Generated 'src/ast/pp_params.hpp'
Generated 'src/ast/fpa/fpa2bv_rewriter_params.hpp'
Generated 'src/ast/simplifier/bv_simplifier_params_helper.hpp'
Generated 'src/ast/simplifier/arith_simplifier_params_helper.hpp'
Generated 'src/ast/simplifier/array_simplifier_params_helper.hpp'
Generated 'src/ast/normal_forms/nnf_params.hpp'
Generated 'src/ast/rewriter/rewriter_params.hpp'
Generated 'src/ast/rewriter/bv_rewriter_params.hpp'
Generated 'src/ast/rewriter/bool_rewriter_params.hpp'
Generated 'src/ast/rewriter/arith_rewriter_params.hpp'
Generated 'src/ast/rewriter/fpa_rewriter_params.hpp'
Generated 'src/ast/rewriter/array_rewriter_params.hpp'
Generated 'src/ast/rewriter/poly_rewriter_params.hpp'
Generated 'src/ast/pattern/pattern_inference_params_helper.hpp'
Generated 'src/opt/opt_params.hpp'
Generated 'src/sat/sat_scc_params.hpp'
Generated 'src/sat/sat_simplifier_params.hpp'
Generated 'src/sat/sat_asymm_branch_params.hpp'
Generated 'src/sat/sat_params.hpp'
Generated 'src/solver/combined_solver_params.hpp'
Generated 'src/interp/interp_params.hpp'
Generated 'src/model/model_params.hpp'
Generated 'src/model/model_evaluator_params.hpp'
Generated 'src/smt/params/smt_params_helper.hpp'
Generated 'src/parsers/util/parser_params.hpp'
Generated 'src/ast/pattern/database.h'
Generated 'src/shell/install_tactic.cpp'
Generated 'src/test/install_tactic.cpp'
Generated 'src/api/dll/install_tactic.cpp'
Generated 'src/shell/mem_initializer.cpp'
Generated 'src/test/mem_initializer.cpp'
Generated 'src/api/dll/mem_initializer.cpp'
Generated 'src/shell/gparams_register_modules.cpp'
Generated 'src/test/gparams_register_modules.cpp'
Generated 'src/api/dll/gparams_register_modules.cpp'
Generated 'src/api/python/z3consts.py'
Generated 'src/api/dotnet/Enumerations.cs'
Finding javac ...
Finding jar ...
Testing /usr/bin/javac...
Finding jni.h...
Generated 'src/api/java/enumerations'
Generated 'src/api/java/Native.java'
Generated "src/api/ml/z3native.ml"
Generated 'src/api/api_log_macros.h'
Generated 'src/api/api_log_macros.cpp'
Generated 'src/api/api_commands.cpp'
Generated 'src/api/python/z3core.py'
Generated 'src/api/dotnet/Native.cs'
Listing src/api/python ...
Compiling src/api/python/z3.py ...
Compiling src/api/python/z3consts.py ...
Compiling src/api/python/z3core.py ...
Compiling src/api/python/z3num.py ...
Compiling src/api/python/z3poly.py ...
Compiling src/api/python/z3printer.py ...
Compiling src/api/python/z3rcf.py ...
Compiling src/api/python/z3test.py ...
Compiling src/api/python/z3types.py ...
Compiling src/api/python/z3util.py ...
Copied 'z3printer.py'
Copied 'z3num.py'
Copied 'z3util.py'
Copied 'z3poly.py'
Copied 'z3test.py'
Copied 'z3consts.py'
Copied 'z3core.py'
Copied 'z3types.py'
Copied 'z3rcf.py'
Copied 'z3.py'
Generated 'z3poly.pyc'
Generated 'z3test.pyc'
Generated 'z3types.pyc'
Generated 'z3printer.pyc'
Generated 'z3.pyc'
Generated 'z3util.pyc'
Generated 'z3consts.pyc'
Generated 'z3num.pyc'
Generated 'z3core.pyc'
Generated 'z3rcf.pyc'
Testing ocamlc...
Finding OCAML_LIB...
OCAML_LIB=/usr/lib/ocaml
Testing ocamlfind...
Generated "src/api/ml/z3enums.ml"
Generated "src/api/ml/z3enums.mli"
Testing ar...
Testing g++...
Testing gcc...
Testing floating point support...
Testing OpenMP...
Host platform: Linux
C++ Compiler: g++
C Compiler : gcc
Arithmetic: internal
OpenMP: True
Prefix:
/home/lamby/temp/cdt.20160828113355.M8pdxROBix.db.z3/z3-4.4.1/debian/tmp/usr
64-bit: True
FP math: SSE2-GCC
Python version: 2.7
JNI Bindings: /usr/lib/jvm/java-8-openjdk-amd64/include
Java Compiler: /usr/bin/javac
OCaml Compiler: ocamlc
OCaml Native: true
OCaml Library: /usr/lib/ocaml
Writing build/Makefile
Updated 'build/api/ml/META'
Copied Z3Py example 'example.py' to 'build'
Makefile was successfully generated.
python packages dir:
/home/lamby/temp/cdt.20160828113355.M8pdxROBix.db.z3/z3-4.4.1/debian/tmp/usr/lib/python2.7/dist-packages
compilation mode: Release
Type 'cd build; make' to build Z3
sed -i 's/^SLINK_FLAGS=.*/SLINK_FLAGS=-fPIE -pie -Wl,-z,relro -Wl,-z,now
-Wl,-soname,libz3.so.4 -fPIC -shared/' build/config.mk
sed -i 's/^CXXFLAGS=/CXXFLAGS=-fPIC /' build/config.mk
printf '%%:\n\t$(MAKE) -C build $@\n' > Makefile
printf '\nall:\n\t$(MAKE) -C build $@\n' >> Makefile
ln -s libz3.so build/libz3.dll
# from T2 README, with fixes
printf '<configuration>\n <dllmap dll="libz3.dll"
target="/usr/lib/x86_64-linux-gnu/libz3.so" os="linux"/>\n</configuration>\n' >
build/Microsoft.Z3.dll.config
make[1]: Leaving directory
'/home/lamby/temp/cdt.20160828113355.M8pdxROBix.db.z3/z3-4.4.1'
jh_linkjars -O--parallel
dh_auto_build -O--parallel
make -j9
make[1]: Entering directory
'/home/lamby/temp/cdt.20160828113355.M8pdxROBix.db.z3/z3-4.4.1'
make -C build all
make[2]: Entering directory
'/home/lamby/temp/cdt.20160828113355.M8pdxROBix.db.z3/z3-4.4.1/build'
src/smt/smt_statistics.cpp
src/interp/iz3profiling.cpp
src/util/approx_nat.cpp
src/util/luby.cpp
src/util/common_msgs.cpp
src/util/scoped_ctrl_c.cpp
src/api/dll/dll.cpp
cp ../src/api/ml/z3enums.mli api/ml/z3enums.mli
cp ../src/api/ml/z3native.mli api/ml/z3native.mli
cp ../src/api/ml/z3.mli api/ml/z3.mli
cp ../src/api/ml/z3enums.ml api/ml/z3enums.ml
cp ../src/api/ml/z3native.ml api/ml/z3native.ml
cp ../src/api/ml/z3.ml api/ml/z3.ml
cp ../src/api/ml/z3native_stubs.c api/ml/z3native_stubs.c
src/util/approx_set.cpp
src/util/memory_manager.cpp
src/util/z3_exception.cpp
src/util/cooperate.cpp
src/util/timeit.cpp
ocamlc -I api/ml -c api/ml/z3enums.mli
src/api/api_commands.cpp
src/util/scoped_timer.cpp
src/util/util.cpp
src/util/lbool.cpp
src/util/page.cpp
src/util/stack.cpp
src/util/timer.cpp
src/util/mpn.cpp
src/util/bit_util.cpp
src/util/timeout.cpp
ocamlc -I api/ml -c api/ml/z3native.mli
ocamlc -a -o api/ml/z3enums.ml -o api/ml/z3enums.cma
src/shell/z3_log_frontend.cpp
src/api/api_log.cpp
src/util/hash.cpp
src/util/fixed_bit_vector.cpp
ocamlc -I api/ml -c api/ml/z3.mli
ocamlc -a -o api/ml/z3native.ml -o api/ml/z3native.cma
src/api/z3_replayer.cpp
src/util/symbol.cpp
src/util/region.cpp
src/util/prime_generator.cpp
src/util/small_object_allocator.cpp
src/util/warning.cpp
src/util/rlimit.cpp
src/util/smt2_util.cpp
src/util/trace.cpp
src/util/cmd_context_types.cpp
src/util/bit_vector.cpp
src/util/permutation.cpp
src/util/debug.cpp
ocamlc -a -o api/ml/z3.ml -o api/ml/z3.cma
src/api/api_log_macros.cpp
src/smt/params/qi_params.cpp
src/smt/params/theory_arith_params.cpp
src/smt/params/theory_bv_params.cpp
../src/util/debug.cpp: In function 'void invoke_gdb()':
../src/util/debug.cpp:79:38: error: cannot convert 'std::basic_istream<char>'
to 'bool' in initialization
bool ok = (std::cin >> result);
^
Makefile:289: recipe for target 'util/debug.o' failed
make[2]: *** [util/debug.o] Error 1
make[2]: *** Waiting for unfinished jobs....
make[2]: Leaving directory
'/home/lamby/temp/cdt.20160828113355.M8pdxROBix.db.z3/z3-4.4.1/build'
Makefile:5: recipe for target 'all' failed
make[1]: *** [all] Error 2
make[1]: Leaving directory
'/home/lamby/temp/cdt.20160828113355.M8pdxROBix.db.z3/z3-4.4.1'
dh_auto_build: make -j9 returned exit code 2
debian/rules:23: recipe for target 'build' failed
make: *** [build] Error 2
[..]
The full build log is attached.
Regards,
--
,''`.
: :' : Chris Lamb
`. `'` la...@debian.org / chris-lamb.co.uk
`-
z3.4.4.1-0.2.unstable.amd64.log.txt.gz
Description: Binary data
