=> Bootstrap dependency digest>=20010302: found digest-20160304 => Checksum SHA1 OK for z3-4.4.1.tar.gz => Checksum RMD160 OK for z3-4.4.1.tar.gz => Checksum SHA512 OK for z3-4.4.1.tar.gz => Checksum SHA1 OK for z3-jumbo-patch-20151123.gz => Checksum RMD160 OK for z3-jumbo-patch-20151123.gz => Checksum SHA512 OK for z3-jumbo-patch-20151123.gz ===> Installing dependencies for z3-4.4.1nb1 ========================================================================== 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.4.1nb1. 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/pkg/bin/bmake clean' after the changes. ========================================================================== => Full dependency ocaml>=4.03.0: found ocaml-4.03.0nb2 => Full dependency pth>=2.0.0nb2: found pth-2.0.7nb4 => Full dependency python27>=2.7.1nb2: found python27-2.7.12nb4 ===> Overriding tools for z3-4.4.1nb1 ===> Extracting for z3-4.4.1nb1 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.4.1nb1 => Applying distribution patches for z3-4.4.1nb1 => Applying pkgsrc patches for z3-4.4.1nb1 ===> Creating toolchain wrappers for z3-4.4.1nb1 ===> Configuring for z3-4.4.1nb1 opt = --destdir, arg = /usr/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: '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: 'ml_example' New component: 'py_example' Generated 'src/util/version.h' Updated 'src/api/dotnet/Properties/AssemblyInfo' 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/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' 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 'z3.py' Copied 'z3num.py' Copied 'z3poly.py' Copied 'z3printer.py' Copied 'z3rcf.py' Copied 'z3test.py' Copied 'z3types.py' Copied 'z3util.py' Copied 'z3consts.py' Copied 'z3core.py' Generated 'z3.pyc' Generated 'z3consts.pyc' Generated 'z3core.pyc' Generated 'z3num.pyc' Generated 'z3poly.pyc' Generated 'z3printer.pyc' Generated 'z3rcf.pyc' Generated 'z3test.pyc' Generated 'z3types.pyc' Generated 'z3util.pyc' Testing ocamlc... Testing ocamlopt... Finding OCAML_LIB... OCAML_LIB=/usr/pkg/lib/ocaml Testing ocamlfind... Generated "src/api/ml/z3enums.ml" Generated "src/api/ml/z3enums.mli" Testing ar... Testing c++... Testing cc... Testing floating point support... Testing OpenMP... Traceback (most recent call last): File "scripts/mk_make.py", line 20, in mk_makefile() File "/usr/pkgsrc/work/math/z3/work/z3-z3-4.4.1/scripts/mk_util.py", line 2022, in mk_makefile mk_config() File "/usr/pkgsrc/work/math/z3/work/z3-z3-4.4.1/scripts/mk_util.py", line 1920, in mk_config raise MKException('Unsupported platform: %s' % sysname) mk_exception.MKException: 'Unsupported platform: Minix' *** Error code 1 Stop. bmake[1]: stopped in /usr/pkgsrc/math/z3 *** Error code 1 Stop. bmake: stopped in /usr/pkgsrc/math/z3