=>> Building math/z3 build started at Fri Mar 29 00:36:24 GMT 2024 port directory: /usr/ports/math/z3 package name: z3-4.12.4 building for: FreeBSD pkg-builder.dan.net.uk 13.2-RELEASE-p10 FreeBSD 13.2-RELEASE-p10 amd64 maintained by: arrowd@FreeBSD.org Makefile datestamp: -rw-r--r-- 1 root wheel 1072 Mar 2 16:12 /usr/ports/math/z3/Makefile Ports top last git commit: c2c35d895e Ports top unclean checkout: yes Port dir last git commit: 43251ef42e Port dir unclean checkout: no Poudriere version: poudriere-git-3.4.99.20240122_1 Host OSVERSION: 1400097 Jail OSVERSION: 1302001 Job Id: 19 ---Begin Environment--- SHELL=/bin/csh OSVERSION=1302001 UNAME_v=FreeBSD 13.2-RELEASE-p10 UNAME_r=13.2-RELEASE-p10 BLOCKSIZE=K MAIL=/var/mail/root MM_CHARSET=UTF-8 LANG=C.UTF-8 STATUS=1 HOME=/root PATH=/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin:/root/bin MAKE_OBJDIR_CHECK_WRITABLE=0 LOCALBASE=/usr/local USER=root POUDRIERE_NAME=poudriere-git LIBEXECPREFIX=/usr/local/libexec/poudriere POUDRIERE_VERSION=3.4.99.20240122_1 MASTERMNT=/usr/local/poudriere/data/.m/13-amd64-default-dan/ref LC_COLLATE=C POUDRIERE_BUILD_TYPE=bulk PACKAGE_BUILDING=yes SAVED_TERM=screen OUTPUT_REDIRECTED_STDERR=4 OUTPUT_REDIRECTED=1 PWD=/usr/local/poudriere/data/.m/13-amd64-default-dan/19/.p OUTPUT_REDIRECTED_STDOUT=3 P_PORTS_FEATURES=FLAVORS SUBPACKAGES SELECTED_OPTIONS MASTERNAME=13-amd64-default-dan SCRIPTPREFIX=/usr/local/share/poudriere SCRIPTNAME=bulk.sh OLDPWD=/usr/local/poudriere/data/.m/13-amd64-default-dan/ref/.p/pool POUDRIERE_PKGNAME=poudriere-git-3.4.99.20240122_1 SCRIPTPATH=/usr/local/share/poudriere/bulk.sh POUDRIEREPATH=/usr/local/bin/poudriere ---End Environment--- ---Begin Poudriere Port Flags/Env--- PORT_FLAGS= PKGENV= FLAVOR= MAKE_ARGS= ---End Poudriere Port Flags/Env--- ---Begin OPTIONS List--- ===> The following configuration options are available for z3-4.12.4: DEBUG=off: Build with debugging support GMP=off: Use GMP library for AP arithmetic STATIC=off: Build static z3 library ===> Use 'make config' to modify these settings ---End OPTIONS List--- --MAINTAINER-- arrowd@FreeBSD.org --End MAINTAINER-- --CONFIGURE_ARGS-- --prefix=/usr/local --End CONFIGURE_ARGS-- --CONFIGURE_ENV-- PYTHON="/usr/local/bin/python3.9" XDG_DATA_HOME=/wrkdirs/usr/ports/math/z3/work XDG_CONFIG_HOME=/wrkdirs/usr/ports/math/z3/work XDG_CACHE_HOME=/wrkdirs/usr/ports/math/z3/work/.cache HOME=/wrkdirs/usr/ports/math/z3/work TMPDIR="/tmp" PATH=/ccache/libexec/ccache:/wrkdirs/usr/ports/math/z3/work/.bin:/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin:/root/bin PKG_CONFIG_LIBDIR=/wrkdirs/usr/ports/math/z3/work/.pkgconfig:/usr/local/libdata/pkgconfig:/usr/local/share/pkgconfig:/usr/libdata/pkgconfig SHELL=/bin/sh CONFIG_SHELL=/bin/sh CCACHE_DIR="/root/.ccache" --End CONFIGURE_ENV-- --MAKE_ENV-- XDG_DATA_HOME=/wrkdirs/usr/ports/math/z3/work XDG_CONFIG_HOME=/wrkdirs/usr/ports/math/z3/work XDG_CACHE_HOME=/wrkdirs/usr/ports/math/z3/work/.cache HOME=/wrkdirs/usr/ports/math/z3/work TMPDIR="/tmp" PATH=/ccache/libexec/ccache:/wrkdirs/usr/ports/math/z3/work/.bin:/sbin:/bin:/usr/sbin:/usr/bin:/usr/local/sbin:/usr/local/bin:/root/bin PKG_CONFIG_LIBDIR=/wrkdirs/usr/ports/math/z3/work/.pkgconfig:/usr/local/libdata/pkgconfig:/usr/local/share/pkgconfig:/usr/libdata/pkgconfig MK_DEBUG_FILES=no MK_KERNEL_SYMBOLS=no SHELL=/bin/sh NO_LINT=YES PREFIX=/usr/local LOCALBASE=/usr/local CC="cc" CFLAGS="-O2 -pipe -fstack-protector-strong -fno-strict-aliasing " CPP="cpp" CPPFLAGS="" LDFLAGS=" -fstack-protector-strong " LIBS="" CXX="c++" CXXFLAGS="-O2 -pipe -fstack-protector-strong -fno-strict-aliasing " CCACHE_DIR="/root/.ccache" BSD_INSTALL_PROGRAM="install -s -m 555" BSD_INSTALL_LIB="install -s -m 0644" BSD_INSTALL_SCRIPT="install -m 555" BSD_INSTALL_DATA="install -m 0644" BSD_INSTALL_MAN="install -m 444" --End MAKE_ENV-- --PLIST_SUB-- DEBUG="@comment " NO_DEBUG="" GMP="@comment " NO_GMP="" STATIC="@comment " NO_STATIC="" PYTHON_INCLUDEDIR=include/python3.9 PYTHON_LIBDIR=lib/python3.9 PYTHON_PLATFORM=freebsd13 PYTHON_SITELIBDIR=lib/python3.9/site-packages PYTHON_SUFFIX=39 PYTHON_EXT_SUFFIX=.cpython-39 PYTHON_VER=3.9 PYTHON_VERSION=python3.9 PYTHON2="@comment " PYTHON3="" OSREL=13.2 PREFIX=%D LOCALBASE=/usr/local RESETPREFIX=/usr/local LIB32DIR=lib DOCSDIR="share/doc/z3" EXAMPLESDIR="share/examples/z3" DATADIR="share/z3" WWWDIR="www/z3" ETCDIR="etc/z3" --End PLIST_SUB-- --SUB_LIST-- DEBUG="@comment " NO_DEBUG="" GMP="@comment " NO_GMP="" STATIC="@comment " NO_STATIC="" PYTHON_INCLUDEDIR=/usr/local/include/python3.9 PYTHON_LIBDIR=/usr/local/lib/python3.9 PYTHON_PLATFORM=freebsd13 PYTHON_SITELIBDIR=/usr/local/lib/python3.9/site-packages PYTHON_SUFFIX=39 PYTHON_EXT_SUFFIX=.cpython-39 PYTHON_VER=3.9 PYTHON_VERSION=python3.9 PYTHON2="@comment " PYTHON3="" PREFIX=/usr/local LOCALBASE=/usr/local DATADIR=/usr/local/share/z3 DOCSDIR=/usr/local/share/doc/z3 EXAMPLESDIR=/usr/local/share/examples/z3 WWWDIR=/usr/local/www/z3 ETCDIR=/usr/local/etc/z3 --End SUB_LIST-- ---Begin make.conf--- USE_PACKAGE_DEPENDS=yes BATCH=yes WRKDIRPREFIX=/wrkdirs PORTSDIR=/usr/ports PACKAGES=/packages DISTDIR=/distfiles FORCE_PACKAGE=yes PACKAGE_BUILDING=yes PACKAGE_BUILDING_FLAVORS=yes #### #### CCACHE_CPP2=1 WITH_SSP_PORTS=yes WITH_SSP=yes #WITH_LTO=yes DISABLE_LICENSES=yes LICENSES_ACCEPTED=AGPLv3 APACHE10 APACHE11 APACHE20 ART10 ARTPERL10 ART20 BSD BSD2CLAUSE BSD3CLAUSE BSD4CLAUSE BSL CC0-1.0 CDDL ClArtistic EPL GFDL GMGPL GPLv1 GPLv2 GPLv3 GPLv3RLE ISCL LGPL20 LGPL21 LGPL3 LPPL10 LPPL11 LPPL12 LPPL13 LPPL13a LPPL13b LPPL13c MIT MPL OpenSSL OFL10 OFL11 OWL PostgreSQL PHP202 PHP30 PHP301 PSFL RUBY ZLIB ZPL21 SVM-Light EULA ALASIR Microsoft-exFAT SIMIAN UDEVGAME unknown MTA COMMERCIAL teamspeak NO_LICENSES_DIALOGS=yes #### #### NO_IGNORE=yes DEFAULT_VERSIONS+=ssl=openssl mysql=8.0 imagemagick=7 samba=4.13 java=18 WITH_SETID_MODE=force PHP_ZTS=enabled OPTIONS_UNSET+=OPENJPEG OPTIONS_UNSET+=GSSAPI_BASE OPTIONS_SET+=ZTS OPTIONS_SET+=GSSAPI_NONE WITH_CCACHE_BUILD=yes CCACHE_DIR=/root/.ccache NO_CCACHE_DEPEND=1 CCACHE_WRAPPER_PATH= /ccache/libexec/ccache #### Misc Poudriere #### .include "/etc/make.conf.ports_env" GID=0 UID=0 DISABLE_MAKE_JOBS=poudriere ---End make.conf--- --Resource limits-- cpu time (seconds, -t) unlimited file size (512-blocks, -f) unlimited data seg size (kbytes, -d) 33554432 stack size (kbytes, -s) 524288 core file size (512-blocks, -c) unlimited max memory size (kbytes, -m) unlimited locked memory (kbytes, -l) unlimited max user processes (-u) 89999 open files (-n) 8192 virtual mem size (kbytes, -v) unlimited swap limit (kbytes, -w) unlimited socket buffer size (bytes, -b) unlimited pseudo-terminals (-p) unlimited kqueues (-k) unlimited umtx shared locks (-o) unlimited --End resource limits-- =================================================== ===== env: NO_DEPENDS=yes USER=root UID=0 GID=0 =========================================================================== =================================================== ===== env: USE_PACKAGE_DEPENDS_ONLY=1 USER=root UID=0 GID=0 ===> z3-4.12.4 depends on file: /usr/local/sbin/pkg - not found ===> Installing existing package /packages/All/pkg-1.20.9_1.pkg [pkg-builder.dan.net.uk] Installing pkg-1.20.9_1... [pkg-builder.dan.net.uk] Extracting pkg-1.20.9_1: .......... done ===> z3-4.12.4 depends on file: /usr/local/sbin/pkg - found ===> Returning to build of z3-4.12.4 =========================================================================== =================================================== ===== env: USE_PACKAGE_DEPENDS_ONLY=1 USER=root UID=0 GID=0 =========================================================================== =================================================== ===== env: NO_DEPENDS=yes USER=root UID=0 GID=0 ===> Fetching all distfiles required by z3-4.12.4 for building =========================================================================== =================================================== ===== env: NO_DEPENDS=yes USER=root UID=0 GID=0 ===> Fetching all distfiles required by z3-4.12.4 for building => SHA256 Checksum OK for Z3Prover-z3-z3-4.12.4_GH0.tar.gz. =========================================================================== =================================================== ===== env: USE_PACKAGE_DEPENDS_ONLY=1 USER=root UID=0 GID=0 =========================================================================== =================================================== ===== env: NO_DEPENDS=yes USER=root UID=0 GID=0 ===> Fetching all distfiles required by z3-4.12.4 for building ===> Extracting for z3-4.12.4 => SHA256 Checksum OK for Z3Prover-z3-z3-4.12.4_GH0.tar.gz. =========================================================================== =================================================== ===== env: USE_PACKAGE_DEPENDS_ONLY=1 USER=root UID=0 GID=0 =========================================================================== =================================================== ===== env: NO_DEPENDS=yes USER=root UID=0 GID=0 ===> Patching for z3-4.12.4 ===> Applying FreeBSD patches for z3-4.12.4 from /usr/ports/math/z3/files =========================================================================== =================================================== ===== env: USE_PACKAGE_DEPENDS_ONLY=1 USER=root UID=0 GID=0 ===> z3-4.12.4 depends on file: /usr/local/bin/python3.9 - not found ===> Installing existing package /packages/All/python39-3.9.18_1.pkg [pkg-builder.dan.net.uk] Installing python39-3.9.18_1... [pkg-builder.dan.net.uk] `-- Installing gettext-runtime-0.22.3_1... [pkg-builder.dan.net.uk] | `-- Installing indexinfo-0.3.1... [pkg-builder.dan.net.uk] | `-- Extracting indexinfo-0.3.1: . done [pkg-builder.dan.net.uk] `-- Extracting gettext-runtime-0.22.3_1: .......... done [pkg-builder.dan.net.uk] `-- Installing libffi-3.4.4_1... [pkg-builder.dan.net.uk] `-- Extracting libffi-3.4.4_1: .......... done [pkg-builder.dan.net.uk] `-- Installing mpdecimal-2.5.1... [pkg-builder.dan.net.uk] `-- Extracting mpdecimal-2.5.1: .......... done [pkg-builder.dan.net.uk] `-- Installing openssl-3.0.13_1,1... [pkg-builder.dan.net.uk] `-- Extracting openssl-3.0.13_1,1: .......... done [pkg-builder.dan.net.uk] `-- Installing readline-8.2.10... [pkg-builder.dan.net.uk] `-- Extracting readline-8.2.10: .......... done [pkg-builder.dan.net.uk] Extracting python39-3.9.18_1: .......... done ===== Message from python39-3.9.18_1: -- Note that some standard Python modules are provided as separate ports as they require additional dependencies. They are available as: py39-gdbm databases/py-gdbm@py39 py39-sqlite3 databases/py-sqlite3@py39 py39-tkinter x11-toolkits/py-tkinter@py39 ===> z3-4.12.4 depends on file: /usr/local/bin/python3.9 - found ===> Returning to build of z3-4.12.4 =========================================================================== =================================================== ===== env: USE_PACKAGE_DEPENDS_ONLY=1 USER=root UID=0 GID=0 =========================================================================== =================================================== ===== env: NO_DEPENDS=yes USER=root UID=0 GID=0 ===> Configuring for z3-4.12.4 opt = --prefix, arg = /usr/local Set Assembly Version (DEFAULT): 4 12 4 0 New component: 'util' New component: 'polynomial' New component: 'interval' New component: 'dd' New component: 'simplex' New component: 'hilbert' New component: 'automata' New component: 'params' New component: 'realclosure' New component: 'subpaving' New component: 'ast' New component: 'smt_params' New component: 'parser_util' New component: 'euf' New component: 'grobner' New component: 'sat' New component: 'nlsat' New component: 'lp' New component: 'rewriter' New component: 'bit_blaster' New component: 'normal_forms' New component: 'substitution' New component: 'proofs' New component: 'macros' New component: 'model' New component: 'converters' New component: 'simplifiers' New component: 'tactic' New component: 'mbp' New component: 'qe_lite' New component: 'solver' New component: 'cmd_context' New component: 'smt2parser' New component: 'pattern' New component: 'aig_tactic' New component: 'ackermannization' New component: 'fpa' New component: 'core_tactics' New component: 'arith_tactics' New component: 'solver_assertions' New component: 'subpaving_tactic' New component: 'proto_model' New component: 'smt' New component: 'sat_smt' New component: 'sat_tactic' New component: 'nlsat_tactic' 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: 'smtlogic_tactics' New component: 'ufbv_tactic' New component: 'fpa_tactics' New component: 'portfolio' New component: 'opt' New component: 'extra_cmds' 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: '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' UpdateVersion: "Z3 4.12.4.0" Generating src/util/z3_version.h from src/util/z3_version.h.in Generated 'src/util/z3_version.h' Generated 'src/ast/pp_params.hpp' Generated 'src/ast/normal_forms/nnf_params.hpp' Generated 'src/sat/sat_params.hpp' Generated 'src/sat/sat_scc_params.hpp' Generated 'src/sat/sat_asymm_branch_params.hpp' Generated 'src/sat/sat_simplifier_params.hpp' Generated 'src/muz/base/fp_params.hpp' Generated 'src/nlsat/nlsat_params.hpp' Generated 'src/smt/params/smt_params_helper.hpp' Generated 'src/params/solver_params.hpp' Generated 'src/params/array_rewriter_params.hpp' Generated 'src/params/pattern_inference_params_helper.hpp' Generated 'src/params/bv_rewriter_params.hpp' Generated 'src/params/poly_rewriter_params.hpp' Generated 'src/params/bool_rewriter_params.hpp' Generated 'src/params/fpa_rewriter_params.hpp' Generated 'src/params/arith_rewriter_params.hpp' Generated 'src/params/seq_rewriter_params.hpp' Generated 'src/params/fpa2bv_rewriter_params.hpp' Generated 'src/params/rewriter_params.hpp' Generated 'src/params/tactic_params.hpp' Generated 'src/tactic/sls/sls_params.hpp' Generated 'src/tactic/smtlogics/qfufbv_tactic_params.hpp' Generated 'src/ackermannization/ackermannize_bv_tactic_params.hpp' Generated 'src/ackermannization/ackermannization_params.hpp' Generated 'src/parsers/util/parser_params.hpp' Generated 'src/solver/combined_solver_params.hpp' Generated 'src/solver/parallel_params.hpp' Generated 'src/model/model_params.hpp' Generated 'src/model/model_evaluator_params.hpp' Generated 'src/math/polynomial/algebraic_params.hpp' Generated 'src/math/realclosure/rcf_params.hpp' Generated 'src/opt/opt_params.hpp' Generated 'src/ast/pattern/database.h' Component api Component portfolio Component smtlogic_tactics Component ackermannization Component model Component macros Component rewriter Component ast Component util Component polynomial Component interval Component automata Component params Component solver Component smt_params Component tactic Component simplifiers Component euf Component normal_forms Component bit_blaster Component converters Component substitution Component qe_lite Component mbp Component simplex Component proofs Component sat_solver Component core_tactics Component pattern Component smt2parser Component cmd_context Component parser_util Component aig_tactic Component bv_tactics Component arith_tactics Component sat Component dd Component grobner Component sat_tactic Component sat_smt Component smt Component proto_model Component solver_assertions Component fpa Component lp Component nlsat Component nlsat_tactic Component smt_tactic 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 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 macros Component rewriter Component ast Component util Component polynomial Component interval Component automata Component params Component solver Component smt_params Component tactic Component simplifiers Component euf Component normal_forms Component bit_blaster Component converters Component substitution Component qe_lite Component mbp Component simplex Component proofs Component sat_solver Component core_tactics Component pattern Component smt2parser Component cmd_context Component parser_util Component aig_tactic Component bv_tactics Component arith_tactics Component sat Component dd Component grobner Component sat_tactic Component sat_smt Component smt Component proto_model Component solver_assertions Component fpa Component lp Component nlsat Component nlsat_tactic Component smt_tactic 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 realclosure Component opt Component extra_cmds Component fuzzing Component test Generated 'src/test/install_tactic.cpp' Component api Component portfolio Component smtlogic_tactics Component ackermannization Component model Component macros Component rewriter Component ast Component util Component polynomial Component interval Component automata Component params Component solver Component smt_params Component tactic Component simplifiers Component euf Component normal_forms Component bit_blaster Component converters Component substitution Component qe_lite Component mbp Component simplex Component proofs Component sat_solver Component core_tactics Component pattern Component smt2parser Component cmd_context Component parser_util Component aig_tactic Component bv_tactics Component arith_tactics Component sat Component dd Component grobner Component sat_tactic Component sat_smt Component smt Component proto_model Component solver_assertions Component fpa Component lp Component nlsat Component nlsat_tactic Component smt_tactic 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 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' 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 'z3printer.py' Copied '__init__.py' Copied 'z3util.py' Copied 'z3rcf.py' Copied 'z3num.py' Copied 'z3consts.py' Copied 'z3types.py' Copied 'z3core.py' Copied 'z3.py' Copied 'z3poly.py' Copied 'z3util.cpython-39.pyc' Copied 'z3printer.cpython-39.pyc' Copied 'z3core.cpython-39.pyc' Copied 'z3poly.cpython-39.pyc' Copied 'z3types.cpython-39.pyc' Copied 'z3num.cpython-39.pyc' Copied 'z3consts.cpython-39.pyc' Copied 'z3.cpython-39.pyc' Copied '__init__.cpython-39.pyc' Copied 'z3rcf.cpython-39.pyc' Testing ar... Testing c++... Testing cc... Testing floating point support... Host platform: FreeBSD C++ Compiler: c++ C Compiler : cc Archive Tool: ar Arithmetic: internal Prefix: /usr/local 64-bit: True FP math: SSE2-GCC Python pkg dir: /usr/local/lib/python3.9/site-packages Python version: 3.9 Writing build/Makefile Copied Z3Py example 'visitor.py' to 'build/python' Copied Z3Py example 'all_interval_series.py' to 'build/python' Copied Z3Py example 'socrates.py' to 'build/python' Copied Z3Py example 'trafficjam.py' to 'build/python' Copied Z3Py example 'simplify_formula.py' to 'build/python' Copied Z3Py example 'rc2.py' to 'build/python' Copied Z3Py example 'example.py' to 'build/python' Copied Z3Py example 'parallel.py' to 'build/python' Copied Z3Py example 'proofreplay.py' to 'build/python' Copied Z3Py example 'prooflogs.py' to 'build/python' Copied Z3Py example 'hs.py' to 'build/python' Copied Z3Py example 'efsmt.py' to 'build/python' Copied Z3Py example 'mini_ic3.py' to 'build/python' Copied Z3Py example 'union_sort.py' to 'build/python' Copied Z3Py example 'mini_quip.py' to 'build/python' Makefile was successfully generated. compilation mode: Release Type 'cd build; make' to build Z3 =========================================================================== =================================================== ===== env: NO_DEPENDS=yes USER=root UID=0 GID=0 ===> Building for z3-4.12.4 src/shell/drat_frontend.cpp src/shell/main.cpp src/shell/z3_log_frontend.cpp src/shell/gparams_register_modules.cpp src/shell/smtlib_frontend.cpp src/shell/mem_initializer.cpp src/shell/dimacs_frontend.cpp src/shell/datalog_frontend.cpp src/shell/opt_frontend.cpp src/shell/install_tactic.cpp src/api/api_numeral.cpp src/api/api_bv.cpp src/api/api_rcf.cpp src/api/api_array.cpp src/api/api_seq.cpp src/api/api_goal.cpp src/api/api_solver.cpp src/api/api_quant.cpp src/api/api_fpa.cpp src/api/api_ast.cpp src/api/api_pb.cpp src/api/api_special_relations.cpp src/api/z3_replayer.cpp src/api/api_log_macros.cpp src/api/api_commands.cpp src/api/api_ast_vector.cpp src/api/api_stats.cpp src/api/api_tactic.cpp src/api/api_params.cpp src/api/api_log.cpp src/api/api_polynomial.cpp src/api/api_context.cpp src/api/api_model.cpp src/api/api_config_params.cpp src/api/api_datatype.cpp src/api/api_ast_map.cpp src/api/api_parsers.cpp src/api/api_opt.cpp src/api/api_datalog.cpp src/api/api_algebraic.cpp src/api/api_qe.cpp src/api/api_arith.cpp src/cmd_context/extra_cmds/subpaving_cmds.cpp src/cmd_context/extra_cmds/proof_cmds.cpp src/cmd_context/extra_cmds/polynomial_cmds.cpp src/cmd_context/extra_cmds/dbg_cmds.cpp src/opt/opt_parse.cpp src/opt/maxcore.cpp src/opt/opt_solver.cpp src/opt/opt_lns.cpp src/opt/opt_pareto.cpp src/opt/opt_cmds.cpp src/opt/optsmt.cpp src/opt/opt_preprocess.cpp src/opt/maxsmt.cpp src/opt/wmax.cpp src/opt/maxlex.cpp src/opt/opt_context.cpp src/opt/pb_sls.cpp src/opt/sortmax.cpp src/opt/opt_cores.cpp src/opt/totalizer.cpp src/tactic/portfolio/smt_strategic_solver.cpp src/tactic/portfolio/default_tactic.cpp src/tactic/portfolio/solver_subsumption_tactic.cpp src/tactic/portfolio/solver2lookahead.cpp src/tactic/fpa/qffplra_tactic.cpp src/tactic/fpa/qffp_tactic.cpp src/tactic/fpa/fpa2bv_tactic.cpp src/tactic/fpa/fpa2bv_model_converter.cpp src/tactic/ufbv/macro_finder_tactic.cpp src/tactic/ufbv/ufbv_tactic.cpp src/tactic/ufbv/quasi_macros_tactic.cpp src/tactic/ufbv/ufbv_rewriter_tactic.cpp src/tactic/smtlogics/nra_tactic.cpp src/tactic/smtlogics/qfidl_tactic.cpp src/tactic/smtlogics/qfaufbv_tactic.cpp src/tactic/smtlogics/quant_tactics.cpp src/tactic/smtlogics/qfnra_tactic.cpp src/tactic/smtlogics/qfauflia_tactic.cpp src/tactic/smtlogics/qfnia_tactic.cpp src/tactic/smtlogics/qflia_tactic.cpp src/tactic/smtlogics/smt_tactic.cpp src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp src/tactic/smtlogics/qfbv_tactic.cpp src/tactic/smtlogics/qfufbv_tactic.cpp src/tactic/smtlogics/qflra_tactic.cpp src/tactic/smtlogics/qfuf_tactic.cpp src/muz/fp/datalog_parser.cpp src/muz/fp/dl_cmds.cpp src/muz/fp/dl_register_engine.cpp src/muz/fp/horn_tactic.cpp src/muz/bmc/dl_bmc_engine.cpp src/muz/ddnf/ddnf.cpp src/muz/tab/tab_context.cpp src/muz/clp/clp_context.cpp src/muz/spacer/spacer_expand_bnd_generalizer.cpp src/muz/spacer/spacer_conjecture.cpp src/muz/spacer/spacer_quant_generalizer.cpp src/muz/spacer/spacer_unsat_core_plugin.cpp src/muz/spacer/spacer_matrix.cpp src/muz/spacer/spacer_prop_solver.cpp src/muz/spacer/spacer_arith_kernel.cpp src/muz/spacer/spacer_farkas_learner.cpp src/muz/spacer/spacer_sym_mux.cpp src/muz/spacer/spacer_legacy_mbp.cpp src/muz/spacer/spacer_cluster.cpp src/muz/spacer/spacer_iuc_solver.cpp src/muz/spacer/spacer_callback.cpp src/muz/spacer/spacer_sem_matcher.cpp src/muz/spacer/spacer_antiunify.cpp src/muz/spacer/spacer_global_generalizer.cpp src/muz/spacer/spacer_concretize.cpp src/muz/spacer/spacer_ind_lemma_generalizer.cpp src/muz/spacer/spacer_legacy_frames.cpp src/muz/spacer/spacer_context.cpp src/muz/spacer/spacer_arith_generalizers.cpp src/muz/spacer/spacer_manager.cpp src/muz/spacer/spacer_cluster_util.cpp src/muz/spacer/spacer_dl_interface.cpp src/muz/spacer/spacer_generalizers.cpp src/muz/spacer/spacer_iuc_proof.cpp src/muz/spacer/spacer_util.cpp src/muz/spacer/spacer_unsat_core_learner.cpp src/muz/spacer/spacer_qe_project.cpp src/muz/spacer/spacer_proof_utils.cpp src/muz/spacer/spacer_pdr.cpp src/muz/spacer/spacer_mev_array.cpp src/muz/spacer/spacer_sat_answer.cpp src/muz/spacer/spacer_mbc.cpp src/muz/spacer/spacer_convex_closure.cpp src/muz/spacer/spacer_legacy_mev.cpp src/muz/rel/udoc_relation.cpp src/muz/rel/dl_check_table.cpp src/muz/rel/dl_compiler.cpp src/muz/rel/dl_relation_manager.cpp src/muz/rel/dl_mk_similarity_compressor.cpp src/muz/rel/dl_mk_simple_joins.cpp src/muz/rel/dl_table_relation.cpp src/muz/rel/dl_sparse_table.cpp src/muz/rel/check_relation.cpp src/muz/rel/aig_exporter.cpp src/muz/rel/dl_instruction.cpp src/muz/rel/dl_bound_relation.cpp src/muz/rel/dl_product_relation.cpp src/muz/rel/dl_mk_explanations.cpp src/muz/rel/karr_relation.cpp src/muz/rel/dl_base.cpp src/muz/rel/dl_external_relation.cpp src/muz/rel/dl_sieve_relation.cpp src/muz/rel/dl_table.cpp src/muz/rel/dl_finite_product_relation.cpp src/muz/rel/dl_interval_relation.cpp src/muz/rel/dl_lazy_table.cpp src/muz/rel/doc.cpp src/muz/rel/rel_context.cpp src/muz/transforms/dl_mk_unfold.cpp src/muz/transforms/dl_transforms.cpp src/muz/transforms/dl_mk_quantifier_abstraction.cpp src/muz/transforms/dl_mk_array_instantiation.cpp src/muz/transforms/dl_mk_loop_counter.cpp src/muz/transforms/dl_mk_array_eq_rewrite.cpp src/muz/transforms/dl_mk_quantifier_instantiation.cpp src/muz/transforms/dl_mk_scale.cpp src/muz/transforms/dl_mk_separate_negated_tails.cpp src/muz/transforms/dl_mk_unbound_compressor.cpp src/muz/transforms/dl_mk_coalesce.cpp src/muz/transforms/dl_mk_coi_filter.cpp src/muz/transforms/dl_mk_backwards.cpp src/muz/transforms/dl_mk_magic_symbolic.cpp src/muz/transforms/dl_mk_slice.cpp src/muz/transforms/dl_mk_synchronize.cpp src/muz/transforms/dl_mk_magic_sets.cpp src/muz/transforms/dl_mk_subsumption_checker.cpp src/muz/transforms/dl_mk_interp_tail_simplifier.cpp src/muz/transforms/dl_mk_bit_blast.cpp src/muz/transforms/dl_mk_array_blast.cpp src/muz/transforms/dl_mk_rule_inliner.cpp src/muz/transforms/dl_mk_filter_rules.cpp src/muz/transforms/dl_mk_karr_invariants.cpp src/muz/transforms/dl_mk_elim_term_ite.cpp src/muz/dataflow/dataflow.cpp src/muz/base/dl_rule.cpp src/muz/base/hnf.cpp src/muz/base/dl_rule_set.cpp src/muz/base/dl_costs.cpp src/muz/base/bind_variables.cpp src/muz/base/dl_rule_transformer.cpp src/muz/base/dl_util.cpp src/muz/base/dl_boogie_proof.cpp src/muz/base/rule_properties.cpp src/muz/base/dl_context.cpp src/muz/base/dl_rule_subsumption_index.cpp src/tactic/fd_solver/fd_solver.cpp src/tactic/fd_solver/bounded_int2bv_solver.cpp src/tactic/fd_solver/enum2bv_solver.cpp src/tactic/fd_solver/pb2bv_solver.cpp src/tactic/fd_solver/smtfd_solver.cpp src/sat/sat_solver/inc_sat_solver.cpp src/sat/sat_solver/sat_smt_solver.cpp src/qe/qe_array_plugin.cpp src/qe/qe.cpp src/qe/qe_bv_plugin.cpp src/qe/qe_bool_plugin.cpp src/qe/nlqsat.cpp src/qe/nlarith_util.cpp src/qe/qe_arith_plugin.cpp src/qe/qe_tactic.cpp src/qe/qe_mbp.cpp src/qe/qe_datatype_plugin.cpp src/qe/qsat.cpp src/qe/qe_cmd.cpp src/qe/qe_mbi.cpp src/qe/qe_dl_plugin.cpp src/tactic/sls/sls_tactic.cpp src/tactic/sls/sls_engine.cpp src/tactic/sls/bvsls_opt_engine.cpp src/smt/tactic/unit_subsumption_tactic.cpp src/smt/tactic/ctx_solver_simplify_tactic.cpp src/smt/tactic/smt_tactic_core.cpp src/tactic/bv/bvarray2uf_tactic.cpp src/tactic/bv/dt2bv_tactic.cpp src/tactic/bv/bvarray2uf_rewriter.cpp src/tactic/bv/elim_small_bv_tactic.cpp src/tactic/bv/bit_blaster_model_converter.cpp src/tactic/bv/bv_size_reduction_tactic.cpp src/tactic/bv/bv1_blaster_tactic.cpp src/tactic/bv/bv_bounds_tactic.cpp src/tactic/bv/bv_bound_chk_tactic.cpp src/tactic/bv/bit_blaster_tactic.cpp src/nlsat/tactic/qfnra_nlsat_tactic.cpp src/nlsat/tactic/goal2nlsat.cpp src/nlsat/tactic/nlsat_tactic.cpp src/sat/tactic/sat_tactic.cpp src/sat/tactic/sat2goal.cpp src/sat/tactic/goal2sat.cpp src/sat/smt/tseitin_theory_checker.cpp src/sat/smt/q_mbi.cpp src/sat/smt/pb_pb.cpp src/sat/smt/euf_solver.cpp src/sat/smt/pb_solver.cpp src/sat/smt/array_model.cpp src/sat/smt/recfun_solver.cpp src/sat/smt/array_diagnostics.cpp src/sat/smt/q_queue.cpp src/sat/smt/xor_solver.cpp src/sat/smt/euf_proof.cpp src/sat/smt/arith_diagnostics.cpp src/sat/smt/euf_invariant.cpp src/sat/smt/q_solver.cpp src/sat/smt/dt_solver.cpp src/sat/smt/bv_internalize.cpp src/sat/smt/bv_solver.cpp src/sat/smt/bv_theory_checker.cpp src/sat/smt/array_axioms.cpp src/sat/smt/arith_solver.cpp src/sat/smt/euf_local_search.cpp src/sat/smt/q_eval.cpp src/sat/smt/pb_constraint.cpp src/sat/smt/pb_internalize.cpp src/sat/smt/q_model_fixer.cpp src/sat/smt/q_theory_checker.cpp src/sat/smt/arith_internalize.cpp src/sat/smt/specrel_solver.cpp src/sat/smt/euf_model.cpp src/sat/smt/q_mam.cpp src/sat/smt/arith_sls.cpp src/sat/smt/fpa_solver.cpp src/sat/smt/euf_ackerman.cpp src/sat/smt/pb_card.cpp src/sat/smt/array_internalize.cpp src/sat/smt/euf_internalize.cpp src/sat/smt/euf_relevancy.cpp src/sat/smt/user_solver.cpp src/sat/smt/sat_th.cpp src/sat/smt/bv_ackerman.cpp src/sat/smt/q_ematch.cpp src/sat/smt/bv_delay_internalize.cpp src/sat/smt/q_clause.cpp src/sat/smt/array_solver.cpp src/sat/smt/atom2bool_var.cpp src/sat/smt/euf_proof_checker.cpp src/sat/smt/arith_axioms.cpp src/sat/smt/bv_invariant.cpp src/smt/smt_value_sort.cpp src/smt/theory_seq.cpp src/smt/smt_relevancy.cpp src/smt/old_interval.cpp src/smt/seq_regex.cpp src/smt/uses_theory.cpp src/smt/theory_user_propagator.cpp src/smt/smt_enode.cpp src/smt/smt_case_split_queue.cpp src/smt/smt_cg_table.cpp src/smt/smt_context_pp.cpp src/smt/arith_eq_solver.cpp src/smt/smt_arith_value.cpp src/smt/smt_implied_equalities.cpp src/smt/theory_datatype.cpp src/smt/theory_recfun.cpp src/smt/smt_clause.cpp src/smt/smt_model_checker.cpp src/smt/theory_arith.cpp src/smt/dyn_ack.cpp src/smt/theory_str_regex.cpp src/smt/theory_wmaxsat.cpp src/smt/smt_context_stat.cpp src/smt/seq_offset_eq.cpp src/smt/smt_context.cpp src/smt/theory_dummy.cpp src/smt/fingerprints.cpp src/smt/smt_model_generator.cpp src/smt/smt_for_each_relevant_expr.cpp src/smt/smt_justification.cpp src/smt/smt_conflict_resolution.cpp src/smt/theory_dl.cpp src/smt/theory_special_relations.cpp src/smt/smt_internalizer.cpp src/smt/theory_lra.cpp src/smt/smt_model_finder.cpp src/smt/theory_pb.cpp src/smt/theory_array.cpp src/smt/smt_literal.cpp src/smt/smt_quick_checker.cpp src/smt/watch_list.cpp src/smt/theory_utvpi.cpp src/smt/seq_eq_solver.cpp src/smt/smt_clause_proof.cpp src/smt/theory_fpa.cpp src/smt/smt_farkas_util.cpp src/smt/theory_diff_logic.cpp src/smt/smt_quantifier.cpp src/smt/smt_parallel.cpp src/smt/smt_consequences.cpp src/smt/smt_solver.cpp src/smt/theory_str_mc.cpp src/smt/theory_array_full.cpp src/smt/theory_char.cpp src/smt/theory_str.cpp src/smt/theory_array_base.cpp src/smt/mam.cpp src/smt/smt_almost_cg_table.cpp src/smt/smt_statistics.cpp src/smt/smt_kernel.cpp src/smt/qi_queue.cpp src/smt/expr_context_simplifier.cpp src/smt/smt2_extra_cmds.cpp src/smt/smt_checker.cpp src/smt/seq_axioms.cpp src/smt/theory_dense_diff_logic.cpp src/smt/arith_eq_adapter.cpp src/smt/smt_theory.cpp src/smt/theory_array_bapa.cpp src/smt/theory_opt.cpp src/smt/theory_bv.cpp src/smt/smt_context_inv.cpp src/smt/seq_ne_solver.cpp src/smt/smt_lookahead.cpp src/smt/smt_setup.cpp src/smt/proto_model/proto_model.cpp src/math/subpaving/tactic/expr2subpaving.cpp src/math/subpaving/tactic/subpaving_tactic.cpp src/solver/assertions/asserted_formulas.cpp src/tactic/arith/pb2bv_model_converter.cpp src/tactic/arith/lia2pb_tactic.cpp src/tactic/arith/nla2bv_tactic.cpp src/tactic/arith/normalize_bounds_tactic.cpp src/tactic/arith/add_bounds_tactic.cpp src/tactic/arith/bv2real_rewriter.cpp src/tactic/arith/eq2bv_tactic.cpp src/tactic/arith/fm_tactic.cpp src/tactic/arith/bv2int_rewriter.cpp src/tactic/arith/degree_shift_tactic.cpp src/tactic/arith/pb2bv_tactic.cpp src/tactic/arith/diff_neq_tactic.cpp src/tactic/arith/factor_tactic.cpp src/tactic/arith/arith_bounds_tactic.cpp src/tactic/arith/purify_arith_tactic.cpp src/tactic/arith/lia2card_tactic.cpp src/tactic/arith/recover_01_tactic.cpp src/tactic/arith/fix_dl_var_tactic.cpp src/tactic/arith/probe_arith.cpp src/tactic/core/injectivity_tactic.cpp src/tactic/core/propagate_values_tactic.cpp src/tactic/core/blast_term_ite_tactic.cpp src/tactic/core/euf_completion_tactic.cpp src/tactic/core/special_relations_tactic.cpp src/tactic/core/simplify_tactic.cpp src/tactic/core/cofactor_term_ite_tactic.cpp src/tactic/core/symmetry_reduce_tactic.cpp src/tactic/core/collect_occs.cpp src/tactic/core/split_clause_tactic.cpp src/tactic/core/tseitin_cnf_tactic.cpp src/tactic/core/pb_preprocess_tactic.cpp src/tactic/core/ctx_simplify_tactic.cpp src/tactic/core/elim_uncnstr_tactic.cpp src/tactic/core/nnf_tactic.cpp src/tactic/core/der_tactic.cpp src/tactic/core/occf_tactic.cpp src/tactic/core/collect_statistics_tactic.cpp src/tactic/core/reduce_args_tactic.cpp src/tactic/core/elim_term_ite_tactic.cpp src/tactic/core/cofactor_elim_term_ite.cpp src/ast/fpa/fpa2bv_converter.cpp src/ast/fpa/fpa2bv_rewriter.cpp src/ast/fpa/bv2fpa_converter.cpp src/ackermannization/ackr_bound_probe.cpp src/ackermannization/ackermannize_bv_tactic.cpp src/ackermannization/ackr_helper.cpp src/ackermannization/lackr_model_converter_lazy.cpp src/ackermannization/ackermannize_bv_model_converter.cpp src/ackermannization/lackr.cpp src/ackermannization/lackr_model_constructor.cpp src/ackermannization/ackr_model_converter.cpp src/tactic/aig/aig.cpp src/tactic/aig/aig_tactic.cpp src/ast/pattern/expr_pattern_match.cpp src/ast/pattern/pattern_inference.cpp src/parsers/smt2/smt2scanner.cpp src/parsers/smt2/marshal.cpp src/parsers/smt2/smt2parser.cpp src/cmd_context/cmd_context.cpp src/cmd_context/cmd_util.cpp src/cmd_context/simplifier_cmds.cpp src/cmd_context/parametric_cmd.cpp src/cmd_context/simplify_cmd.cpp src/cmd_context/echo_tactic.cpp src/cmd_context/tactic_manager.cpp src/cmd_context/pdecl.cpp src/cmd_context/tactic_cmds.cpp src/cmd_context/cmd_context_to_goal.cpp src/cmd_context/basic_cmds.cpp src/cmd_context/eval_cmd.cpp src/solver/smt_logics.cpp src/solver/mus.cpp src/solver/solver2tactic.cpp src/solver/simplifier_solver.cpp src/solver/combined_solver.cpp src/solver/solver_preprocess.cpp src/solver/tactic2solver.cpp src/solver/check_logic.cpp src/solver/solver.cpp src/solver/parallel_tactical.cpp src/solver/check_sat_result.cpp src/solver/solver_pool.cpp src/solver/solver_na2as.cpp src/qe/lite/qe_lite_tactic.cpp src/qe/lite/qel.cpp src/qe/mbp/mbp_arith.cpp src/qe/mbp/mbp_plugin.cpp src/qe/mbp/mbp_arrays_tg.cpp src/qe/mbp/mbp_qel_util.cpp src/qe/mbp/mbp_term_graph.cpp src/qe/mbp/mbp_solve_plugin.cpp src/qe/mbp/mbp_dt_tg.cpp src/qe/mbp/mbp_datatypes.cpp src/qe/mbp/mbp_qel.cpp src/qe/mbp/mbp_arrays.cpp src/qe/mbp/mbp_basic_tg.cpp src/tactic/goal_shared_occs.cpp src/tactic/goal_num_occurs.cpp src/tactic/goal.cpp src/tactic/dependency_converter.cpp src/tactic/tactic.cpp src/tactic/probe.cpp src/tactic/tactical.cpp src/tactic/goal_util.cpp src/ast/simplifiers/extract_eqs.cpp src/ast/simplifiers/bound_simplifier.cpp src/ast/simplifiers/card2bv.cpp src/ast/simplifiers/bound_manager.cpp src/ast/simplifiers/elim_unconstrained.cpp src/ast/simplifiers/dependent_expr_state.cpp src/ast/simplifiers/dominator_simplifier.cpp src/ast/simplifiers/linear_equation.cpp src/ast/simplifiers/model_reconstruction_trail.cpp src/ast/simplifiers/euf_completion.cpp src/ast/simplifiers/distribute_forall.cpp src/ast/simplifiers/bound_propagator.cpp src/ast/simplifiers/demodulator_simplifier.cpp src/ast/simplifiers/eliminate_predicates.cpp src/ast/simplifiers/bv_bounds_simplifier.cpp src/ast/simplifiers/solve_context_eqs.cpp src/ast/simplifiers/solve_eqs.cpp src/ast/simplifiers/bv_slice.cpp src/ast/simplifiers/propagate_values.cpp src/ast/simplifiers/max_bv_sharing.cpp src/ast/simplifiers/reduce_args_simplifier.cpp src/ast/simplifiers/bit_blaster.cpp src/ast/converters/generic_model_converter.cpp src/ast/converters/replace_proof_converter.cpp src/ast/converters/equiv_proof_converter.cpp src/ast/converters/proof_converter.cpp src/ast/converters/horn_subsume_model_converter.cpp src/ast/converters/expr_inverter.cpp src/ast/converters/model_converter.cpp src/model/value_factory.cpp src/model/model_smt2_pp.cpp src/model/struct_factory.cpp src/model/func_interp.cpp src/model/model2expr.cpp src/model/model_v2_pp.cpp src/model/numeral_factory.cpp src/model/model_macro_solver.cpp src/model/model.cpp src/model/model_pp.cpp src/model/model_core.cpp src/model/model_implicant.cpp src/model/array_factory.cpp src/model/datatype_factory.cpp src/model/model_evaluator.cpp src/ast/macros/quasi_macros.cpp src/ast/macros/macro_util.cpp src/ast/macros/quantifier_macro_info.cpp src/ast/macros/macro_manager.cpp src/ast/macros/macro_finder.cpp src/ast/proofs/proof_checker.cpp src/ast/proofs/proof_utils.cpp src/ast/substitution/unifier.cpp src/ast/substitution/demodulator_rewriter.cpp src/ast/substitution/substitution.cpp src/ast/substitution/substitution_tree.cpp src/ast/substitution/matcher.cpp src/ast/normal_forms/pull_quant.cpp src/ast/normal_forms/elim_term_ite.cpp src/ast/normal_forms/name_exprs.cpp src/ast/normal_forms/nnf.cpp src/ast/normal_forms/defined_names.cpp src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp src/ast/rewriter/bit_blaster/bit_blaster.cpp src/ast/rewriter/inj_axiom.cpp src/ast/rewriter/seq_rewriter.cpp src/ast/rewriter/elim_bounds.cpp src/ast/rewriter/maximize_ac_sharing.cpp src/ast/rewriter/mk_extract_proc.cpp src/ast/rewriter/cached_var_subst.cpp src/ast/rewriter/seq_skolem.cpp src/ast/rewriter/enum2bv_rewriter.cpp src/ast/rewriter/bit2int.cpp src/ast/rewriter/fpa_rewriter.cpp src/ast/rewriter/recfun_rewriter.cpp src/ast/rewriter/value_sweep.cpp src/ast/rewriter/mk_simplified_app.cpp src/ast/rewriter/expr_replacer.cpp src/ast/rewriter/arith_rewriter.cpp src/ast/rewriter/expr_safe_replace.cpp src/ast/rewriter/ast_counter.cpp src/ast/rewriter/pb2bv_rewriter.cpp src/ast/rewriter/var_subst.cpp src/ast/rewriter/distribute_forall.cpp src/ast/rewriter/th_rewriter.cpp src/ast/rewriter/bv_bounds.cpp src/ast/rewriter/dl_rewriter.cpp src/ast/rewriter/seq_eq_solver.cpp src/ast/rewriter/bv_rewriter.cpp src/ast/rewriter/pb_rewriter.cpp src/ast/rewriter/datatype_rewriter.cpp src/ast/rewriter/label_rewriter.cpp src/ast/rewriter/array_rewriter.cpp src/ast/rewriter/factor_rewriter.cpp src/ast/rewriter/bool_rewriter.cpp src/ast/rewriter/der.cpp src/ast/rewriter/char_rewriter.cpp src/ast/rewriter/bv_elim.cpp src/ast/rewriter/seq_axioms.cpp src/ast/rewriter/factor_equivs.cpp src/ast/rewriter/rewriter.cpp src/ast/rewriter/dom_simplifier.cpp src/ast/rewriter/push_app_ite.cpp src/ast/rewriter/func_decl_replace.cpp src/ast/rewriter/macro_replacer.cpp src/ast/rewriter/quant_hoist.cpp src/math/lp/nla_divisions.cpp src/math/lp/int_cube.cpp src/math/lp/dense_matrix.cpp src/math/lp/matrix.cpp src/math/lp/nla_grobner.cpp src/math/lp/indexed_vector.cpp src/math/lp/lp_settings.cpp src/math/lp/mon_eq.cpp src/math/lp/static_matrix.cpp src/math/lp/int_gcd_test.cpp src/math/lp/factorization.cpp src/math/lp/nla_order_lemmas.cpp src/math/lp/monomial_bounds.cpp src/math/lp/nla_common.cpp src/math/lp/lp_core_solver_base.cpp src/math/lp/nra_solver.cpp src/math/lp/emonics.cpp src/math/lp/lar_solver.cpp src/math/lp/int_branch.cpp src/math/lp/gomory.cpp src/math/lp/nla_core.cpp src/math/lp/nla_tangent_lemmas.cpp src/math/lp/nla_monotone_lemmas.cpp src/math/lp/horner.cpp src/math/lp/core_solver_pretty_printer.cpp src/math/lp/nla_intervals.cpp src/math/lp/lar_core_solver.cpp src/math/lp/factorization_factory_imp.cpp src/math/lp/nla_powers.cpp src/math/lp/int_solver.cpp src/math/lp/hnf_cutter.cpp src/math/lp/nla_solver.cpp src/math/lp/permutation_matrix.cpp src/math/lp/nex_creator.cpp src/math/lp/random_updater.cpp src/math/lp/nla_basics_lemmas.cpp src/math/lp/lp_primal_core_solver.cpp src/nlsat/nlsat_clause.cpp src/nlsat/nlsat_solver.cpp src/nlsat/nlsat_types.cpp src/nlsat/nlsat_evaluator.cpp src/nlsat/nlsat_interval_set.cpp src/nlsat/nlsat_explain.cpp src/sat/sat_lookahead.cpp src/sat/sat_probing.cpp src/sat/sat_drat.cpp src/sat/sat_watched.cpp src/sat/sat_local_search.cpp src/sat/sat_prob.cpp src/sat/sat_aig_cuts.cpp src/sat/sat_elim_vars.cpp src/sat/sat_xor_finder.cpp src/sat/sat_big.cpp src/sat/sat_gc.cpp src/sat/sat_ddfw.cpp src/sat/sat_cut_simplifier.cpp src/sat/sat_clause_use_list.cpp src/sat/sat_cleaner.cpp src/sat/sat_solver.cpp src/sat/sat_clause_set.cpp src/sat/sat_integrity_checker.cpp src/sat/sat_clause.cpp src/sat/sat_asymm_branch.cpp src/sat/dimacs.cpp src/sat/sat_bcd.cpp src/sat/sat_npn3_finder.cpp src/sat/sat_cutset.cpp src/sat/sat_mus.cpp src/sat/sat_binspr.cpp src/sat/sat_simplifier.cpp src/sat/sat_anf_simplifier.cpp src/sat/sat_proof_trim.cpp src/sat/sat_aig_finder.cpp src/sat/sat_config.cpp src/sat/sat_elim_eqs.cpp src/sat/sat_model_converter.cpp src/sat/sat_lut_finder.cpp src/sat/sat_parallel.cpp src/sat/sat_scc.cpp src/math/grobner/pdd_simplifier.cpp src/math/grobner/grobner.cpp src/math/grobner/pdd_solver.cpp src/ast/euf/euf_etable.cpp src/ast/euf/euf_ac_plugin.cpp src/ast/euf/euf_enode.cpp src/ast/euf/euf_specrel_plugin.cpp src/ast/euf/euf_egraph.cpp src/ast/euf/euf_bv_plugin.cpp src/ast/euf/euf_plugin.cpp src/ast/euf/euf_justification.cpp src/ast/euf/euf_arith_plugin.cpp src/parsers/util/simple_parser.cpp src/parsers/util/cost_parser.cpp src/parsers/util/pattern_validation.cpp src/parsers/util/scanner.cpp src/smt/params/theory_seq_params.cpp src/smt/params/qi_params.cpp src/smt/params/smt_params.cpp src/smt/params/theory_str_params.cpp src/smt/params/theory_pb_params.cpp src/smt/params/dyn_ack_params.cpp src/smt/params/theory_array_params.cpp src/smt/params/theory_bv_params.cpp src/smt/params/preprocessor_params.cpp src/smt/params/theory_arith_params.cpp src/ast/static_features.cpp src/ast/polymorphism_util.cpp src/ast/ast.cpp src/ast/for_each_expr.cpp src/ast/value_generator.cpp src/ast/cost_evaluator.cpp src/ast/bv_decl_plugin.cpp src/ast/expr_map.cpp src/ast/array_peq.cpp src/ast/expr_functors.cpp src/ast/ast_smt2_pp.cpp src/ast/special_relations_decl_plugin.cpp src/ast/has_free_vars.cpp src/ast/char_decl_plugin.cpp src/ast/for_each_ast.cpp src/ast/polymorphism_inst.cpp src/ast/macro_substitution.cpp src/ast/dl_decl_plugin.cpp src/ast/expr2var.cpp src/ast/expr_substitution.cpp src/ast/datatype_decl_plugin.cpp src/ast/num_occurs.cpp src/ast/ast_ll_pp.cpp src/ast/array_decl_plugin.cpp src/ast/quantifier_stat.cpp src/ast/shared_occs.cpp src/ast/expr2polynomial.cpp src/ast/ast_util.cpp src/ast/format.cpp src/ast/ast_printer.cpp src/ast/display_dimacs.cpp src/ast/used_vars.cpp src/ast/well_sorted.cpp src/ast/func_decl_dependencies.cpp src/ast/pb_decl_plugin.cpp src/ast/ast_lt.cpp src/ast/occurs.cpp src/ast/reg_decl_plugins.cpp src/ast/act_cache.cpp src/ast/expr_stat.cpp src/ast/decl_collector.cpp src/ast/expr_abstract.cpp src/ast/ast_translation.cpp src/ast/ast_pp_dot.cpp src/ast/seq_decl_plugin.cpp src/ast/recfun_decl_plugin.cpp src/ast/ast_smt_pp.cpp src/ast/ast_pp_util.cpp src/ast/arith_decl_plugin.cpp src/ast/fpa_decl_plugin.cpp src/ast/pp.cpp src/math/subpaving/subpaving_mpq.cpp src/math/subpaving/subpaving.cpp src/math/subpaving/subpaving_mpfx.cpp src/math/subpaving/subpaving_mpff.cpp src/math/subpaving/subpaving_hwf.cpp src/math/subpaving/subpaving_mpf.cpp src/math/realclosure/realclosure.cpp src/math/realclosure/mpz_matrix.cpp src/params/context_params.cpp src/params/pattern_inference_params.cpp src/math/automata/automaton.cpp src/math/hilbert/hilbert_basis.cpp src/math/simplex/model_based_opt.cpp src/math/simplex/simplex.cpp src/math/simplex/bit_matrix.cpp src/math/dd/dd_pdd.cpp src/math/dd/dd_bdd.cpp src/math/dd/dd_fdd.cpp src/math/interval/dep_intervals.cpp src/math/interval/interval_mpq.cpp src/math/polynomial/rpolynomial.cpp src/math/polynomial/algebraic_numbers.cpp src/math/polynomial/polynomial.cpp src/math/polynomial/upolynomial_factorization.cpp src/math/polynomial/sexpr2upolynomial.cpp src/math/polynomial/upolynomial.cpp src/math/polynomial/polynomial_cache.cpp src/util/trace.cpp src/util/hash.cpp src/util/timeit.cpp src/util/z3_exception.cpp src/util/hwf.cpp src/util/timeout.cpp src/util/approx_nat.cpp src/util/s_integer.cpp src/util/prime_generator.cpp src/util/params.cpp src/util/mpf.cpp src/util/common_msgs.cpp src/util/permutation.cpp src/util/inf_int_rational.cpp src/util/mpn.cpp src/util/inf_rational.cpp src/util/min_cut.cpp src/util/scoped_ctrl_c.cpp src/util/stack.cpp src/util/scoped_timer.cpp src/util/mpz.cpp src/util/bit_util.cpp src/util/gparams.cpp src/util/cmd_context_types.cpp src/util/sexpr.cpp src/util/region.cpp src/util/smt2_util.cpp src/util/fixed_bit_vector.cpp src/util/tbv.cpp src/util/mpq_inf.cpp src/util/mpbq.cpp src/util/inf_s_integer.cpp src/util/lbool.cpp src/util/memory_manager.cpp src/util/small_object_allocator.cpp src/util/mpff.cpp src/util/rational.cpp src/util/mpq.cpp src/util/util.cpp src/util/state_graph.cpp src/util/debug.cpp src/util/page.cpp src/util/approx_set.cpp src/util/mpfx.cpp src/util/warning.cpp src/util/rlimit.cpp src/util/env_params.cpp src/util/luby.cpp src/util/zstring.cpp src/util/statistics.cpp src/util/symbol.cpp src/util/bit_vector.cpp c++ -oz3 shell/drat_frontend.o shell/main.o shell/z3_log_frontend.o shell/gparams_register_modules.o shell/smtlib_frontend.o shell/mem_initializer.o shell/dimacs_frontend.o shell/datalog_frontend.o shell/opt_frontend.o shell/install_tactic.o api/api.a cmd_context/extra_cmds/extra_cmds.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/ufbv/ufbv_tactic.a tactic/smtlogics/smtlogic_tactics.a muz/fp/fp.a muz/bmc/bmc.a muz/ddnf/ddnf.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a tactic/fd_solver/fd_solver.a sat/sat_solver/sat_solver.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a nlsat/tactic/nlsat_tactic.a sat/tactic/sat_tactic.a sat/smt/sat_smt.a smt/smt.a smt/proto_model/proto_model.a math/subpaving/tactic/subpaving_tactic.a solver/assertions/solver_assertions.a tactic/arith/arith_tactics.a tactic/core/core_tactics.a ast/fpa/fpa.a ackermannization/ackermannization.a tactic/aig/aig_tactic.a ast/pattern/pattern.a parsers/smt2/smt2parser.a cmd_context/cmd_context.a solver/solver.a qe/lite/qe_lite.a qe/mbp/mbp.a tactic/tactic.a ast/simplifiers/simplifiers.a ast/converters/converters.a model/model.a ast/macros/macros.a ast/proofs/proofs.a ast/substitution/substitution.a ast/normal_forms/normal_forms.a ast/rewriter/bit_blaster/bit_blaster.a ast/rewriter/rewriter.a math/lp/lp.a nlsat/nlsat.a sat/sat.a math/grobner/grobner.a ast/euf/euf.a parsers/util/parser_util.a smt/params/smt_params.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a params/params.a math/automata/automata.a math/hilbert/hilbert.a math/simplex/simplex.a math/dd/dd.a math/interval/interval.a math/polynomial/polynomial.a util/util.a -lpthread -fstack-protector-strong src/api/dll/gparams_register_modules.cpp src/api/dll/mem_initializer.cpp src/api/dll/dll.cpp src/api/dll/install_tactic.cpp c++ -olibz3.so -shared api/dll/gparams_register_modules.o api/dll/mem_initializer.o api/dll/dll.o api/dll/install_tactic.o api/api_numeral.o api/api_bv.o api/api_rcf.o api/api_array.o api/api_seq.o api/api_goal.o api/api_solver.o api/api_quant.o api/api_fpa.o api/api_ast.o api/api_pb.o api/api_special_relations.o api/z3_replayer.o api/api_log_macros.o api/api_commands.o api/api_ast_vector.o api/api_stats.o api/api_tactic.o api/api_params.o api/api_log.o api/api_polynomial.o api/api_context.o api/api_model.o api/api_config_params.o api/api_datatype.o api/api_ast_map.o api/api_parsers.o api/api_opt.o api/api_datalog.o api/api_algebraic.o api/api_qe.o api/api_arith.o cmd_context/extra_cmds/extra_cmds.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/ufbv/ufbv_tactic.a tactic/smtlogics/smtlogic_tactics.a muz/fp/fp.a muz/bmc/bmc.a muz/ddnf/ddnf.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a tactic/fd_solver/fd_solver.a sat/sat_solver/sat_solver.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a nlsat/tactic/nlsat_tactic.a sat/tactic/sat_tactic.a sat/smt/sat_smt.a smt/smt.a smt/proto_model/proto_model.a math/subpaving/tactic/subpaving_tactic.a solver/assertions/solver_assertions.a tactic/arith/arith_tactics.a tactic/core/core_tactics.a ast/fpa/fpa.a ackermannization/ackermannization.a tactic/aig/aig_tactic.a ast/pattern/pattern.a parsers/smt2/smt2parser.a cmd_context/cmd_context.a solver/solver.a qe/lite/qe_lite.a qe/mbp/mbp.a tactic/tactic.a ast/simplifiers/simplifiers.a ast/converters/converters.a model/model.a ast/macros/macros.a ast/proofs/proofs.a ast/substitution/substitution.a ast/normal_forms/normal_forms.a ast/rewriter/bit_blaster/bit_blaster.a ast/rewriter/rewriter.a math/lp/lp.a nlsat/nlsat.a sat/sat.a math/grobner/grobner.a ast/euf/euf.a parsers/util/parser_util.a smt/params/smt_params.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a params/params.a math/automata/automata.a math/hilbert/hilbert.a math/simplex/simplex.a math/dd/dd.a math/interval/interval.a math/polynomial/polynomial.a util/util.a -lpthread -fstack-protector-strong -Wl,-soname,libz3.so.0 -Wl,-soname,libz3.so ln -f -s ../libz3.so python Z3 was successfully built. Z3Py scripts can already be executed in the 'build/python' directory. Z3Py scripts stored in arbitrary directories can be executed if the 'build/python' directory is added to the PYTHONPATH environment variable and the 'build' directory is added to the LD_LIBRARY_PATH environment variable. Use the following command to install Z3 at prefix /usr/local. sudo make install =========================================================================== =================================================== ===== env: USE_PACKAGE_DEPENDS_ONLY=1 USER=root UID=0 GID=0 =========================================================================== =================================================== ===== env: NO_DEPENDS=yes USER=root UID=0 GID=0 ===> Staging for z3-4.12.4 ===> Generating temporary packing list Z3 was successfully installed. /usr/bin/strip /wrkdirs/usr/ports/math/z3/work/stage/usr/local/bin/z3 /usr/bin/strip /wrkdirs/usr/ports/math/z3/work/stage/usr/local/lib/libz3.so /bin/ln -s libz3.so /wrkdirs/usr/ports/math/z3/work/stage/usr/local/lib/libz3.so.0 ====> Compressing man pages (compress-man) =========================================================================== =================================================== ===== env: 'PKG_NOTES=build_timestamp ports_top_git_hash ports_top_checkout_unclean port_git_hash port_checkout_unclean built_by' 'PKG_NOTE_build_timestamp=2024-03-29T00:36:24+0000' 'PKG_NOTE_ports_top_git_hash=c2c35d895e' 'PKG_NOTE_ports_top_checkout_unclean=yes' 'PKG_NOTE_port_git_hash=43251ef42e' 'PKG_NOTE_port_checkout_unclean=no' 'PKG_NOTE_built_by=poudriere-git-3.4.99.20240122_1' NO_DEPENDS=yes USER=root UID=0 GID=0 ===> Building packages for z3-4.12.4 ===> Building z3-4.12.4 =========================================================================== =>> Cleaning up wrkdir ===> Cleaning for z3-4.12.4 build of math/z3 | z3-4.12.4 ended at Fri Mar 29 09:06:12 GMT 2024 build time: 08:29:50