=> Bootstrap dependency digest>=20010302: found digest-20160304 ===> Skipping vulnerability checks. WARNING: No /var/db/pkg/pkg-vulnerabilities file found. WARNING: To fix run: `/usr/sbin/pkg_admin -K /var/db/pkg fetch-pkg-vulnerabilities'. => Checksum SHA1 OK for z3-4.5.0.tar.gz => Checksum RMD160 OK for z3-4.5.0.tar.gz => Checksum SHA512 OK for z3-4.5.0.tar.gz ===> Installing dependencies for z3-4.5.0nb3 ========================================================================== The supported build options for z3 are: java ocaml The currently selected options are: ocaml You can select which build options to use by setting PKG_DEFAULT_OPTIONS or the following variable. Its current value is shown: PKG_OPTIONS.z3 (not defined) ========================================================================== ========================================================================== The following variables will affect the build process of this package, z3-4.5.0nb3. Their current value is shown below: * PYTHON_VERSION_DEFAULT = 27 Based on these variables, the following variables have been set: * PYPACKAGE = python27 * TERMCAP_TYPE = termcap You may want to abort the process now with CTRL-C and change their value before continuing. Be sure to run `/usr/bin/make clean' after the changes. ========================================================================== => Tool dependency checkperms>=1.1: found checkperms-1.12 => Build dependency cwrappers>=20150314: found cwrappers-20180325 => Full dependency python27>=2.7.1nb2: found python27-2.7.15nb1 => Full dependency ocaml-num>=1.1nb2: found ocaml-num-1.1nb2 => Full dependency ocaml>=4.07.0: found ocaml-4.07.0 ===> Overriding tools for z3-4.5.0nb3 ===> Extracting for z3-4.5.0nb3 tar: Global extended headers posix ustar archive. Extracting as plain files. Following files might be in the wrong directory or have wrong attributes. ===> Patching for z3-4.5.0nb3 => Applying pkgsrc patches for z3-4.5.0nb3 => Verifying /data/pkgsrc/math/z3/../../math/z3/patches/patch-configure => Applying pkgsrc patch /data/pkgsrc/math/z3/../../math/z3/patches/patch-configure Hmm... Looks like a unified diff to me... The text leading up to this was: -------------------------- |$NetBSD: patch-configure,v 1.1 2018/03/13 00:31:16 khorben Exp $ | |Fix parameter expansion when configuring Z3. | |--- configure.orig 2016-11-07 22:02:30.000000000 +0000 |+++ configure -------------------------- Patching file configure using Plan A... Hunk #1 succeeded at 14. done => Verifying /data/pkgsrc/math/z3/../../math/z3/patches/patch-scripts_mk__util.py => Applying pkgsrc patch /data/pkgsrc/math/z3/../../math/z3/patches/patch-scripts_mk__util.py Hmm... Looks like a unified diff to me... The text leading up to this was: -------------------------- |$NetBSD: patch-scripts_mk__util.py,v 1.4 2018/06/15 15:11:35 jperkin Exp $ | |--- scripts/mk_util.py.orig 2016-11-07 22:02:30.000000000 +0000 |+++ scripts/mk_util.py -------------------------- Patching file scripts/mk_util.py using Plan A... Hunk #1 succeeded at 69. Hunk #2 succeeded at 96. Hunk #3 succeeded at 141. Hunk #4 succeeded at 608. Hunk #5 succeeded at 630. Hunk #6 succeeded at 685. Hunk #7 succeeded at 735. Hunk #8 succeeded at 1218. Hunk #9 succeeded at 1237. Hunk #10 succeeded at 1391. Hunk #11 succeeded at 1413. Hunk #12 succeeded at 1711. Hunk #13 succeeded at 1786. Hunk #14 succeeded at 1839. Hunk #15 succeeded at 2449. Hunk #16 succeeded at 2463. Hunk #17 succeeded at 2505. Hunk #18 succeeded at 2540. Hunk #19 succeeded at 2601. Hunk #20 succeeded at 3307. done => Verifying /data/pkgsrc/math/z3/../../math/z3/patches/patch-src_util_scoped__timer.cpp => Applying pkgsrc patch /data/pkgsrc/math/z3/../../math/z3/patches/patch-src_util_scoped__timer.cpp Hmm... Looks like a unified diff to me... The text leading up to this was: -------------------------- |$NetBSD: patch-src_util_scoped__timer.cpp,v 1.1 2018/03/13 21:20:34 khorben Exp $ | |Add support for NetBSD. | |--- src/util/scoped_timer.cpp.orig 2016-11-07 22:02:30.000000000 +0000 |+++ src/util/scoped_timer.cpp -------------------------- Patching file src/util/scoped_timer.cpp using Plan A... Hunk #1 succeeded at 33. Hunk #2 succeeded at 66. Hunk #3 succeeded at 103. Hunk #4 succeeded at 166. Hunk #5 succeeded at 206. done => Verifying /data/pkgsrc/math/z3/../../math/z3/patches/patch-src_util_stopwatch.h => Applying pkgsrc patch /data/pkgsrc/math/z3/../../math/z3/patches/patch-src_util_stopwatch.h Hmm... Looks like a unified diff to me... The text leading up to this was: -------------------------- |$NetBSD: patch-src_util_stopwatch.h,v 1.1 2018/03/13 00:31:16 khorben Exp $ | |--- src/util/stopwatch.h.orig 2016-11-07 22:02:30.000000000 +0000 |+++ src/util/stopwatch.h -------------------------- Patching file src/util/stopwatch.h using Plan A... Hunk #1 succeeded at 130. done ===> Creating toolchain wrappers for z3-4.5.0nb3 ===> Configuring for z3-4.5.0nb3 => Checking for portability problems in extracted files opt = --destdir, arg = /data/scratch/math/z3/work/.destdir opt = --prefix, arg = /usr/pkg opt = --ml, arg = New component: 'util' New component: 'polynomial' New component: 'sat' New component: 'nlsat' New component: 'hilbert' New component: 'simplex' New component: 'automata' 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: 'ackermannization' 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: '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: 'ufbv_tactic' New component: 'sat_solver' New component: 'smtlogic_tactics' New component: 'fpa_tactics' 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: 'python' New component: 'python_install' New component: 'cpp_example' New component: 'z3_tptp' New component: 'c_example' New component: 'maxsat' New component: 'dotnet_example' New component: 'java_example' New component: 'ml_example' New component: 'py_example' Generating src/util/version.h from src/util/version.h.in Generated 'src/util/version.h' Generating src/api/dotnet/Properties/AssemblyInfo.cs from src/api/dotnet/Properties/AssemblyInfo.cs.in Generated 'src/ackermannization/ackermannization_params.hpp' Generated 'src/ackermannization/ackermannize_bv_tactic_params.hpp' Generated 'src/ast/pp_params.hpp' Generated 'src/ast/fpa/fpa2bv_rewriter_params.hpp' Generated 'src/ast/normal_forms/nnf_params.hpp' Generated 'src/ast/pattern/pattern_inference_params_helper.hpp' Generated 'src/ast/rewriter/arith_rewriter_params.hpp' Generated 'src/ast/rewriter/array_rewriter_params.hpp' Generated 'src/ast/rewriter/bool_rewriter_params.hpp' Generated 'src/ast/rewriter/bv_rewriter_params.hpp' Generated 'src/ast/rewriter/fpa_rewriter_params.hpp' Generated 'src/ast/rewriter/poly_rewriter_params.hpp' Generated 'src/ast/rewriter/rewriter_params.hpp' Generated 'src/ast/simplifier/arith_simplifier_params_helper.hpp' Generated 'src/ast/simplifier/array_simplifier_params_helper.hpp' Generated 'src/ast/simplifier/bv_simplifier_params_helper.hpp' Generated 'src/interp/interp_params.hpp' Generated 'src/math/polynomial/algebraic_params.hpp' Generated 'src/math/realclosure/rcf_params.hpp' Generated 'src/model/model_evaluator_params.hpp' Generated 'src/model/model_params.hpp' Generated 'src/muz/base/fixedpoint_params.hpp' Generated 'src/nlsat/nlsat_params.hpp' Generated 'src/opt/opt_params.hpp' Generated 'src/parsers/util/parser_params.hpp' Generated 'src/sat/sat_asymm_branch_params.hpp' Generated 'src/sat/sat_params.hpp' Generated 'src/sat/sat_scc_params.hpp' Generated 'src/sat/sat_simplifier_params.hpp' Generated 'src/smt/params/smt_params_helper.hpp' Generated 'src/solver/combined_solver_params.hpp' Generated 'src/tactic/sls/sls_params.hpp' Generated 'src/tactic/smtlogics/qfufbv_tactic_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/z3/z3consts.py Generated 'src/api/api_log_macros.h' Generated 'src/api/api_log_macros.cpp' Generated 'src/api/api_commands.cpp' Generated 'src/api/python/z3/z3core.py' Generated "src/api/ml/z3native.ml" Generated "src/api/ml/z3native_stubs.c" Listing src/api/python/z3 ... Compiling src/api/python/z3/__init__.py ... Compiling src/api/python/z3/z3.py ... Compiling src/api/python/z3/z3consts.py ... Compiling src/api/python/z3/z3core.py ... Compiling src/api/python/z3/z3num.py ... Compiling src/api/python/z3/z3poly.py ... Compiling src/api/python/z3/z3printer.py ... Compiling src/api/python/z3/z3rcf.py ... Compiling src/api/python/z3/z3types.py ... Compiling src/api/python/z3/z3util.py ... Generated python bytecode Copied '__init__.py' Copied 'z3.py' Copied 'z3num.py' Copied 'z3poly.py' Copied 'z3printer.py' Copied 'z3rcf.py' Copied 'z3types.py' Copied 'z3util.py' Copied 'z3consts.py' Copied 'z3core.py' Copied '__init__.pyc' Copied 'z3.pyc' Copied 'z3consts.pyc' Copied 'z3core.pyc' Copied 'z3num.pyc' Copied 'z3poly.pyc' Copied 'z3printer.pyc' Copied 'z3rcf.pyc' Copied 'z3types.pyc' Copied 'z3util.pyc' Testing ocamlc... Testing ocamlopt... Finding OCAML_LIB... OCAML_LIB=/usr/pkg/lib/ocaml Testing ocamlfind... Generated "src/api/ml/z3enums.ml" Testing ar... Testing clang++... Testing clang... Testing floating point support... Testing OpenMP... Host platform: NetBSD C++ Compiler: clang++ C Compiler : clang Archive Tool: ar Arithmetic: internal OpenMP: True Prefix: /usr/pkg Destdir: /data/scratch/math/z3/work/.destdir 64-bit: True FP math: SSE2-GCC Python pkg dir: /usr/pkg/lib/python2.7/site-packages Python version: 2.7 OCaml Compiler: ocamlc OCaml Find tool: ocamlfind OCaml Native: ocamlopt OCaml Library: /usr/pkg/lib/ocaml Writing build/Makefile Generating build/api/ml/META from src/api/ml/META.in Copied Z3Py example 'all_interval_series.py' to 'build/python' Copied Z3Py example 'example.py' to 'build/python' Copied Z3Py example 'socrates.py' to 'build/python' Copied Z3Py example 'visitor.py' to 'build/python' Makefile was successfully generated. compilation mode: Release Type 'cd build; make' to build Z3