=> Bootstrap dependency digest>=20010302: found digest-20160304 => 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.0nb2 ========================================================================== 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.0nb2. Their current value is shown below: * PYTHON_VERSION_DEFAULT = 27 Based on these variables, the following variables have been set: * PYPACKAGE = python27 * TERMCAP_TYPE = tinfo You may want to abort the process now with CTRL-C and change their value before continuing. Be sure to run `/usr/pkg/bin/bmake clean' after the changes. ========================================================================== => Tool dependency nbpatch-[0-9]*: found nbpatch-20151107 => Build dependency cwrappers>=20150314: found cwrappers-20180325 => Full dependency python27>=2.7.1nb2: found python27-2.7.15nb1 => Full dependency ocaml-num>=1.1: found ocaml-num-1.1nb1 => Full dependency ocaml>=4.06.1: found ocaml-4.06.1 ===> Overriding tools for z3-4.5.0nb2 ===> Extracting for z3-4.5.0nb2 ===> Patching for z3-4.5.0nb2 => Applying pkgsrc patches for z3-4.5.0nb2 ===> Creating toolchain wrappers for z3-4.5.0nb2 ===> Configuring for z3-4.5.0nb2 opt = --destdir, arg = /var/pkgsrc/work/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: FreeBSD C++ Compiler: clang++ C Compiler : clang Archive Tool: ar Arithmetic: internal OpenMP: False Prefix: /usr/pkg Destdir: /var/pkgsrc/work/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