=> Bootstrap dependency digest>=20211023: found digest-20220214
=> Checksum BLAKE2s OK for z3-4.8.3.tar.gz
=> Checksum SHA512 OK for z3-4.8.3.tar.gz
===> Installing dependencies for z3-4.8.3nb2
==========================================================================
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.8.3nb2.  Their current value is shown below:

        * PYTHON_VERSION_DEFAULT = 39

Based on these variables, the following variables have been set:

        * PYPACKAGE = python39
        * TERMCAP_TYPE = termcap

You may want to abort the process now with CTRL-C and change the value
of variables in the first group 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 python39>=3.9.0: found python39-3.9.12
=> Full dependency ocaml-num>=1.4: found ocaml-num-1.4
=> Full dependency ocaml>=4.11.2: found ocaml-4.11.2nb1
===> 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'.
===> Overriding tools for z3-4.8.3nb2
===> Extracting for z3-4.8.3nb2
===> Patching for z3-4.8.3nb2
=> Applying pkgsrc patches for z3-4.8.3nb2
=> Verifying /usr/pkgsrc/math/z3/../../math/z3/patches/patch-scripts_mk__genfile__common.py
=> Applying pkgsrc patch /usr/pkgsrc/math/z3/../../math/z3/patches/patch-scripts_mk__genfile__common.py
Hmm...  Looks like a unified diff to me...
The text leading up to this was:
--------------------------
|$NetBSD: patch-scripts_mk__genfile__common.py,v 1.1 2020/05/31 20:49:34 joerg Exp $
|
|--- scripts/mk_genfile_common.py.orig	2018-11-19 20:21:17.000000000 +0000
|+++ scripts/mk_genfile_common.py
--------------------------
Patching file scripts/mk_genfile_common.py using Plan A...
Hunk #1 succeeded at 622.
Hunk #2 succeeded at 697.
Hunk #3 succeeded at 766.
Hunk #4 succeeded at 809.
done
=> Verifying /usr/pkgsrc/math/z3/../../math/z3/patches/patch-scripts_mk__util.py
=> Applying pkgsrc patch /usr/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.6 2020/05/31 20:49:34 joerg Exp $
|
|--- scripts/mk_util.py.orig	2018-11-19 20:21:17.000000000 +0000
|+++ scripts/mk_util.py
--------------------------
Patching file scripts/mk_util.py using Plan A...
Hunk #1 succeeded at 803.
Hunk #2 succeeded at 2002.
Hunk #3 succeeded at 2695.
Hunk #4 succeeded at 2824.
done
===> Creating toolchain wrappers for z3-4.8.3nb2
===> Configuring for z3-4.8.3nb2
=> Checking for portability problems in extracted files
opt = --ml, arg = 
New component: 'util'
New component: 'polynomial'
New component: 'sat'
New component: 'nlsat'
New component: 'lp'
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: 'macros'
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: 'proofs'
New component: 'solver'
New component: 'sat_tactic'
New component: 'arith_tactics'
New component: 'nlsat_tactic'
New component: 'subpaving_tactic'
New component: 'aig_tactic'
New component: 'ackermannization'
New component: 'cmd_context'
New component: 'smt2parser'
New component: 'fpa'
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: 'sat_solver'
New component: 'fd_solver'
New component: 'muz'
New component: 'dataflow'
New component: 'transforms'
New component: 'rel'
New component: 'spacer'
New component: 'clp'
New component: 'tab'
New component: 'ddnf'
New component: 'bmc'
New component: 'fp'
New component: 'ufbv_tactic'
New component: 'smtlogic_tactics'
New component: 'fpa_tactics'
New component: 'portfolio'
New component: 'opt'
New component: 'api'
New component: 'extra_cmds'
New component: 'shell'
New component: 'test'
New component: 'api_dll'
New component: 'dotnet'
New component: 'dotnetcore'
New component: 'java'
New component: 'ml'
New component: 'cpp'
Python bindings directory was detected.
New component: 'python'
New component: 'python_install'
New component: 'js'
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/z3_version.h from src/util/z3_version.h.in
Generated 'src/util/z3_version.h'
Generating src/api/dotnet/Properties/AssemblyInfo.cs from src/api/dotnet/Properties/AssemblyInfo.cs.in
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/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/fp_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/solver/parallel_params.hpp'
Generated 'src/tactic/sls/sls_params.hpp'
Generated 'src/tactic/smtlogics/qfufbv_tactic_params.hpp'
Generated 'src/util/lp/lp_params.hpp'
Generated 'src/ast/pattern/database.h'
Component api
Component portfolio
Component smtlogic_tactics
Component ackermannization
Component model
Component rewriter
Component ast
Component util
Component polynomial
Component automata
Component solver
Component tactic
Component proofs
Component sat_solver
Component core_tactics
Component macros
Component normal_forms
Component aig_tactic
Component bv_tactics
Component bit_blaster
Component arith_tactics
Component sat
Component sat_tactic
Component nlsat_tactic
Component nlsat
Component smt_tactic
Component smt
Component cmd_context
Component proto_model
Component smt_params
Component pattern
Component smt2parser
Component parser_util
Component substitution
Component grobner
Component euclid
Component simplex
Component fpa
Component lp
Component fp
Component muz
Component qe
Component clp
Component transforms
Component hilbert
Component dataflow
Component tab
Component rel
Component bmc
Component fd_solver
Component ddnf
Component spacer
Component ufbv_tactic
Component fpa_tactics
Component sls_tactic
Component subpaving_tactic
Component subpaving
Component interval
Component realclosure
Component opt
Component extra_cmds
Component shell
Generated 'src/shell/install_tactic.cpp'
Component api
Component portfolio
Component smtlogic_tactics
Component ackermannization
Component model
Component rewriter
Component ast
Component util
Component polynomial
Component automata
Component solver
Component tactic
Component proofs
Component sat_solver
Component core_tactics
Component macros
Component normal_forms
Component aig_tactic
Component bv_tactics
Component bit_blaster
Component arith_tactics
Component sat
Component sat_tactic
Component nlsat_tactic
Component nlsat
Component smt_tactic
Component smt
Component cmd_context
Component proto_model
Component smt_params
Component pattern
Component smt2parser
Component parser_util
Component substitution
Component grobner
Component euclid
Component simplex
Component fpa
Component lp
Component fp
Component muz
Component qe
Component clp
Component transforms
Component hilbert
Component dataflow
Component tab
Component rel
Component bmc
Component fd_solver
Component ddnf
Component spacer
Component ufbv_tactic
Component fpa_tactics
Component sls_tactic
Component subpaving_tactic
Component subpaving
Component interval
Component realclosure
Component opt
Component fuzzing
Component test
Generated 'src/test/install_tactic.cpp'
Component api
Component portfolio
Component smtlogic_tactics
Component ackermannization
Component model
Component rewriter
Component ast
Component util
Component polynomial
Component automata
Component solver
Component tactic
Component proofs
Component sat_solver
Component core_tactics
Component macros
Component normal_forms
Component aig_tactic
Component bv_tactics
Component bit_blaster
Component arith_tactics
Component sat
Component sat_tactic
Component nlsat_tactic
Component nlsat
Component smt_tactic
Component smt
Component cmd_context
Component proto_model
Component smt_params
Component pattern
Component smt2parser
Component parser_util
Component substitution
Component grobner
Component euclid
Component simplex
Component fpa
Component lp
Component fp
Component muz
Component qe
Component clp
Component transforms
Component hilbert
Component dataflow
Component tab
Component rel
Component bmc
Component fd_solver
Component ddnf
Component spacer
Component ufbv_tactic
Component fpa_tactics
Component sls_tactic
Component subpaving_tactic
Component subpaving
Component interval
Component realclosure
Component opt
Component extra_cmds
Component api_dll
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__.cpython-39.pyc'
Copied 'z3.cpython-39.pyc'
Copied 'z3consts.cpython-39.pyc'
Copied 'z3core.cpython-39.pyc'
Copied 'z3num.cpython-39.pyc'
Copied 'z3poly.cpython-39.pyc'
Copied 'z3printer.cpython-39.pyc'
Copied 'z3rcf.cpython-39.pyc'
Copied 'z3types.cpython-39.pyc'
Copied 'z3util.cpython-39.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 c++...
Testing gcc...
Testing floating point support...
Testing OpenMP...
Host platform:  NetBSD
C++ Compiler:   c++
C Compiler  :   gcc
Archive Tool:   ar
Arithmetic:     internal
OpenMP:         True
Prefix:         /usr/pkg
64-bit:         False
FP math:        UNKNOWN
Python pkg dir: /usr/pkg/lib/python3.9/site-packages
Python version: 3.9
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 'mini_ic3.py' to 'build/python'
Copied Z3Py example 'parallel.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