Build:
- 0
2026-07-26 10:56.01: New job: build z3.4.12.2 (4fb962ffedc7)
2026-07-26 10:56.01: Waiting for resource in pool day11-builds
2026-07-26 11:33.16: Got resource from pool day11-builds
2026-07-26 11:33.16: [profile full] build z3.4.12.2
2026-07-26 11:33.16: build z3.4.12.2 (4fb962ffedc7)
=== DEPENDENCIES (10 transitive) ===
compiler-cloning.enabled 22a431860256
conf-c++.1.0 93639c2e939b
conf-gmp.5 be8168159001
conf-pkg-config.5 2c611009363a
conf-python-3.9.0.0 10e92bdeecd9
ocaml.5.5.0 af24caade1d3
ocaml-base-compiler.5.5.0 5f93989ce6d7
ocaml-compiler.5.5.0 15edcf5138e5
ocamlfind.1.9.9~preview c75d6f48ab10
zarith.1.14 ace7f2650d27
=== STDOUT ===
Processing: [default: loading data]
[WARNING] These additional system packages are required, but not available on your system: python3-distutils
[z3.4.12.2: dl]
[z3.4.12.2: extract]
-> retrieved z3.4.12.2 (https://opam.ocaml.org/cache)
[z3: python3]
+ /usr/bin/python3 "scripts/mk_make.py" "--ml" (CWD=/home/opam/.opam/default/.opam-switch/build/z3.4.12.2)
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_util.py:398: SyntaxWarning: invalid escape sequence '\['
- open_pat = re.compile("\[search path for class files: (.*)\]")
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_util.py:816: SyntaxWarning: invalid escape sequence '\<'
- system_inc_pat = re.compile("[ \t]*#include[ \t]*\<.*\>[ \t]*")
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_util.py:1747: SyntaxWarning: invalid escape sequence '\%'
- <Compile Include="..\%s\*.cs;*.cs" Exclude="bin\**;obj\**;**\*.xproj;packages\**" />
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_util.py:2256: SyntaxWarning: invalid escape sequence '\%'
- <Compile Include="..\%s/*.cs" />
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_util.py:3165: SyntaxWarning: invalid escape sequence '\M'
- f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.Default.props" />\n')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_util.py:3176: SyntaxWarning: invalid escape sequence '\M'
- f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.props" />\n')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_util.py:3179: SyntaxWarning: invalid escape sequence '\M'
- f.write(' <Import Project="$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props" Condition="exists(\'$(UserRootDir)\Microsoft.Cpp.$(Platform).user.props\')" Label="LocalAppDataPlatform" /> </ImportGroup>\n')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_util.py:3182: SyntaxWarning: invalid escape sequence '\$'
- f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Debug|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_util.py:3185: SyntaxWarning: invalid escape sequence '\$'
- f.write(' <OutDir Condition="\'$(Configuration)|$(Platform)\'==\'Release|Win32\'">$(SolutionDir)\$(ProjectName)\$(Configuration)\</OutDir>\n')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_util.py:3190: SyntaxWarning: invalid escape sequence '\$'
- f.write(' <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_util.py:3193: SyntaxWarning: invalid escape sequence '\$'
- f.write(' <IntDir>$(ProjectName)\$(Configuration)\</IntDir>\n')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_util.py:3270: SyntaxWarning: invalid escape sequence '\M'
- f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_util.py:3311: SyntaxWarning: invalid escape sequence '\M'
- f.write(' <Import Project="$(VCTargetsPath)\Microsoft.Cpp.targets" />\n')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_genfile_common.py:142: SyntaxWarning: invalid escape sequence '\-'
- words = re.split('[^\-a-zA-Z0-9_]+', line)
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_genfile_common.py:230: SyntaxWarning: invalid escape sequence '\-'
- words = re.split('[^\-a-zA-Z0-9_]+', line)
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_genfile_common.py:318: SyntaxWarning: invalid escape sequence '\-'
- words = re.split('[^\-a-zA-Z0-9_]+', line)
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_genfile_common.py:444: SyntaxWarning: invalid escape sequence '\-'
- words = re.split('[^\-a-zA-Z0-9_]+', line)
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_genfile_common.py:577: SyntaxWarning: invalid escape sequence '\W'
- words = re.split('\W+', line)
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_genfile_common.py:621: SyntaxWarning: invalid escape sequence '\('
- reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_genfile_common.py:622: SyntaxWarning: invalid escape sequence '\('
- reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_genfile_common.py:623: SyntaxWarning: invalid escape sequence '\('
- reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_genfile_common.py:701: SyntaxWarning: invalid escape sequence '\('
- tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_genfile_common.py:702: SyntaxWarning: invalid escape sequence '\('
- probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_genfile_common.py:703: SyntaxWarning: invalid escape sequence '\('
- simplifier_pat = re.compile('[ \t]*ADD_SIMPLIFIER\(.*\)')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_genfile_common.py:783: SyntaxWarning: invalid escape sequence '\('
- initializer_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_genfile_common.py:785: SyntaxWarning: invalid escape sequence '\('
- initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)')
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/mk_genfile_common.py:786: SyntaxWarning: invalid escape sequence '\('
- finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)')
- opt = --ml, arg =
- Set Assembly Version (DEFAULT): 4 12 2 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.2.0"
- Generating src/util/z3_version.h from src/util/z3_version.h.in
- Generated 'src/util/z3_version.h'
- Generated 'src/tactic/smtlogics/qfufbv_tactic_params.hpp'
- Generated 'src/tactic/sls/sls_params.hpp'
- Generated 'src/sat/sat_params.hpp'
- Generated 'src/sat/sat_asymm_branch_params.hpp'
- Generated 'src/sat/sat_scc_params.hpp'
- Generated 'src/sat/sat_simplifier_params.hpp'
- Generated 'src/ast/pp_params.hpp'
- Generated 'src/ast/normal_forms/nnf_params.hpp'
- Generated 'src/muz/base/fp_params.hpp'
- Generated 'src/model/model_evaluator_params.hpp'
- Generated 'src/model/model_params.hpp'
- Generated 'src/solver/parallel_params.hpp'
- Generated 'src/solver/combined_solver_params.hpp'
- Generated 'src/params/fpa_rewriter_params.hpp'
- Generated 'src/params/bool_rewriter_params.hpp'
- Generated 'src/params/poly_rewriter_params.hpp'
- Generated 'src/params/bv_rewriter_params.hpp'
- Generated 'src/params/fpa2bv_rewriter_params.hpp'
- Generated 'src/params/rewriter_params.hpp'
- Generated 'src/params/seq_rewriter_params.hpp'
- Generated 'src/params/arith_rewriter_params.hpp'
- Generated 'src/params/solver_params.hpp'
- Generated 'src/params/pattern_inference_params_helper.hpp'
- Generated 'src/params/tactic_params.hpp'
- Generated 'src/params/array_rewriter_params.hpp'
- Generated 'src/ackermannization/ackermannization_params.hpp'
- Generated 'src/ackermannization/ackermannize_bv_tactic_params.hpp'
- Generated 'src/math/realclosure/rcf_params.hpp'
- Generated 'src/math/polynomial/algebraic_params.hpp'
- Generated 'src/nlsat/nlsat_params.hpp'
- Generated 'src/smt/params/smt_params_helper.hpp'
- Generated 'src/parsers/util/parser_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'
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/update_api.py:119: SyntaxWarning: invalid escape sequence '\('
- pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*")
- /home/opam/.opam/default/.opam-switch/build/z3.4.12.2/scripts/update_api.py:120: SyntaxWarning: invalid escape sequence '\('
- pat2 = re.compile("Z3_DECLARE_CLOSURE\((.*),(.*), \((.*)\)\)")
-
- 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 'z3consts.py'
- Copied 'z3core.py'
- Copied 'z3types.py'
- Copied 'z3printer.py'
- Copied 'z3.py'
- Copied '__init__.py'
- Copied 'z3poly.py'
- Copied 'z3num.py'
- Copied 'z3rcf.py'
- Copied 'z3util.py'
- Copied 'z3core.cpython-313.pyc'
- Copied 'z3consts.cpython-313.pyc'
- Copied 'z3rcf.cpython-313.pyc'
- Copied 'z3num.cpython-313.pyc'
- Copied 'z3poly.cpython-313.pyc'
- Copied 'z3util.cpython-313.pyc'
- Copied 'z3printer.cpython-313.pyc'
- Copied '__init__.cpython-313.pyc'
- Copied 'z3types.cpython-313.pyc'
- Copied 'z3.cpython-313.pyc'
- Testing ocamlc...
- Testing ocamlopt...
- Finding OCAML_LIB...
- OCAML_LIB=/home/opam/.opam/default/lib/ocaml
- Testing ocamlfind...
- Generated "src/api/ml/z3enums.ml"
- Testing ar...
- Testing g++...
- Testing gcc...
- Testing floating point support...
- Host platform: Linux
- C++ Compiler: g++
- C Compiler : gcc
- Archive Tool: ar
- Arithmetic: internal
- Prefix: /usr
- 64-bit: True
- FP math: SSE2-GCC
- Python pkg dir: /usr/local/lib/python3.13/dist-packages
- Python version: 3.13
- OCaml Compiler: ocamlc
- OCaml Find tool: ocamlfind
- OCaml Native: ocamlopt
- OCaml Library: /home/opam/.opam/default/lib/ocaml
- Writing build/Makefile
- Generating build/api/ml/META from src/api/ml/META.in
- Copied Z3Py example 'proofreplay.py' to 'build/python'
- Copied Z3Py example 'hs.py' to 'build/python'
- Copied Z3Py example 'mini_quip.py' to 'build/python'
- Copied Z3Py example 'visitor.py' to 'build/python'
- Copied Z3Py example 'parallel.py' to 'build/python'
- Copied Z3Py example 'trafficjam.py' to 'build/python'
- Copied Z3Py example 'efsmt.py' to 'build/python'
- Copied Z3Py example 'socrates.py' to 'build/python'
- Copied Z3Py example 'example.py' to 'build/python'
- Copied Z3Py example 'union_sort.py' to 'build/python'
- Copied Z3Py example 'mini_ic3.py' to 'build/python'
- Copied Z3Py example 'all_interval_series.py' to 'build/python'
- Copied Z3Py example 'simplify_formula.py' to 'build/python'
- Copied Z3Py example 'prooflogs.py' to 'build/python'
- Copied Z3Py example 'rc2.py' to 'build/python'
- Makefile was successfully generated.
- compilation mode: Release
- Type 'cd build; make' to build Z3
[z3: make build]
+ /usr/bin/make "-C" "build" "-j" "39" (CWD=/home/opam/.opam/default/.opam-switch/build/z3.4.12.2)
- make: Entering directory '/home/opam/.opam/default/.opam-switch/build/z3.4.12.2/build'
- src/smt/smt_statistics.cpp
- src/util/luby.cpp
- src/util/approx_nat.cpp
- src/util/common_msgs.cpp
- ocamlfind ocamlc -package zarith -i -I api/ml -c ../src/api/ml/z3enums.ml > api/ml/z3enums.mli
- src/api/dll/dll.cpp
- src/util/approx_set.cpp
- src/util/z3_exception.cpp
- src/util/page.cpp
- src/util/memory_manager.cpp
- ocamlfind ocamlc -package zarith -I api/ml -o api/ml/z3enums.cmi -c api/ml/z3enums.mli
- src/api/api_commands.cpp
- ocamlfind ocamlc -package zarith -I api/ml -o api/ml/z3enums.cmo -c ../src/api/ml/z3enums.ml
- src/util/timeout.cpp
- src/util/lbool.cpp
- src/util/timeit.cpp
- src/util/bit_util.cpp
- src/util/stack.cpp
- src/util/util.cpp
- src/util/scoped_ctrl_c.cpp
- src/util/scoped_timer.cpp
- src/shell/z3_log_frontend.cpp
- src/solver/smt_logics.cpp
- src/util/warning.cpp
- src/util/cmd_context_types.cpp
- src/util/mpn.cpp
- src/util/smt2_util.cpp
- src/util/fixed_bit_vector.cpp
- src/util/small_object_allocator.cpp
- src/util/hash.cpp
- src/util/permutation.cpp
- src/api/z3_replayer.cpp
- src/api/api_log.cpp
- src/api/api_log_macros.cpp
- src/math/automata/automaton.cpp
- src/sat/sat_cutset.cpp
- src/util/symbol.cpp
- src/util/bit_vector.cpp
- src/util/min_cut.cpp
- src/util/state_graph.cpp
- src/util/prime_generator.cpp
- src/util/trace.cpp
- src/util/statistics.cpp
- src/util/debug.cpp
- src/util/rlimit.cpp
- src/util/region.cpp
- In file included from ../src/util/region.cpp:53:
- ../src/util/region.cpp: In member function 'void* region::allocate(size_t)':
- ../src/util/tptr.h:29:62: error: 'uintptr_t' does not name a type
- 29 | #define ALIGN(T, PTR) reinterpret_cast<T>(((reinterpret_cast<uintptr_t>(PTR) >> PTR_ALIGNMENT) + \
- | ^~~~~~~~~
- ../src/util/region.cpp:82:22: note: in expansion of macro 'ALIGN'
- 82 | m_curr_ptr = ALIGN(char *, new_curr_ptr);
- | ^~~~~
- ../src/util/region.cpp:57:1: note: 'uintptr_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
- 56 | #include "util/page.h"
- +++ |+#include <cstdint>
- 57 |
- ../src/util/tptr.h:30:38: error: 'uintptr_t' does not name a type
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/region.cpp:82:22: note: in expansion of macro 'ALIGN'
- 82 | m_curr_ptr = ALIGN(char *, new_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:30:38: note: 'uintptr_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/region.cpp:82:22: note: in expansion of macro 'ALIGN'
- 82 | m_curr_ptr = ALIGN(char *, new_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:30:67: error: 'uintptr_t' does not name a type
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/region.cpp:82:22: note: in expansion of macro 'ALIGN'
- 82 | m_curr_ptr = ALIGN(char *, new_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:30:67: note: 'uintptr_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/region.cpp:82:22: note: in expansion of macro 'ALIGN'
- 82 | m_curr_ptr = ALIGN(char *, new_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:29:62: error: 'uintptr_t' does not name a type
- 29 | #define ALIGN(T, PTR) reinterpret_cast<T>(((reinterpret_cast<uintptr_t>(PTR) >> PTR_ALIGNMENT) + \
- | ^~~~~~~~~
- ../src/util/region.cpp:89:22: note: in expansion of macro 'ALIGN'
- 89 | m_curr_ptr = ALIGN(char *, m_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:29:62: note: 'uintptr_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
- 29 | #define ALIGN(T, PTR) reinterpret_cast<T>(((reinterpret_cast<uintptr_t>(PTR) >> PTR_ALIGNMENT) + \
- | ^~~~~~~~~
- ../src/util/region.cpp:89:22: note: in expansion of macro 'ALIGN'
- 89 | m_curr_ptr = ALIGN(char *, m_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:30:38: error: 'uintptr_t' does not name a type
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/region.cpp:89:22: note: in expansion of macro 'ALIGN'
- 89 | m_curr_ptr = ALIGN(char *, m_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:30:38: note: 'uintptr_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/region.cpp:89:22: note: in expansion of macro 'ALIGN'
- 89 | m_curr_ptr = ALIGN(char *, m_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:30:67: error: 'uintptr_t' does not name a type
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/region.cpp:89:22: note: in expansion of macro 'ALIGN'
- 89 | m_curr_ptr = ALIGN(char *, m_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:30:67: note: 'uintptr_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/region.cpp:89:22: note: in expansion of macro 'ALIGN'
- 89 | m_curr_ptr = ALIGN(char *, m_curr_ptr);
- | ^~~~~
- ocamlfind ocamlc -package zarith -i -I api/ml -c ../src/api/ml/z3native.ml > api/ml/z3native.mli
- make: *** [Makefile:315: util/region.o] Error 1
- make: *** Waiting for unfinished jobs....
- ocamlfind ocamlc -package zarith -I api/ml -o api/ml/z3native.cmi -c api/ml/z3native.mli
- In file included from ../src/util/stack.cpp:20:
- ../src/util/stack.cpp: In member function 'void* stack::allocate_small(size_t, bool)':
- ../src/util/tptr.h:29:62: error: 'uintptr_t' does not name a type
- 29 | #define ALIGN(T, PTR) reinterpret_cast<T>(((reinterpret_cast<uintptr_t>(PTR) >> PTR_ALIGNMENT) + \
- | ^~~~~~~~~
- ../src/util/stack.cpp:99:22: note: in expansion of macro 'ALIGN'
- 99 | m_curr_ptr = ALIGN(char *, new_curr_ptr);
- | ^~~~~
- ../src/util/stack.cpp:21:1: note: 'uintptr_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
- 20 | #include "util/tptr.h"
- +++ |+#include <cstdint>
- 21 |
- ../src/util/tptr.h:30:38: error: 'uintptr_t' does not name a type
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/stack.cpp:99:22: note: in expansion of macro 'ALIGN'
- 99 | m_curr_ptr = ALIGN(char *, new_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:30:38: note: 'uintptr_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/stack.cpp:99:22: note: in expansion of macro 'ALIGN'
- 99 | m_curr_ptr = ALIGN(char *, new_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:30:67: error: 'uintptr_t' does not name a type
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/stack.cpp:99:22: note: in expansion of macro 'ALIGN'
- 99 | m_curr_ptr = ALIGN(char *, new_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:30:67: note: 'uintptr_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/stack.cpp:99:22: note: in expansion of macro 'ALIGN'
- 99 | m_curr_ptr = ALIGN(char *, new_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:29:62: error: 'uintptr_t' does not name a type
- 29 | #define ALIGN(T, PTR) reinterpret_cast<T>(((reinterpret_cast<uintptr_t>(PTR) >> PTR_ALIGNMENT) + \
- | ^~~~~~~~~
- ../src/util/stack.cpp:105:22: note: in expansion of macro 'ALIGN'
- 105 | m_curr_ptr = ALIGN(char *, m_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:29:62: note: 'uintptr_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
- 29 | #define ALIGN(T, PTR) reinterpret_cast<T>(((reinterpret_cast<uintptr_t>(PTR) >> PTR_ALIGNMENT) + \
- | ^~~~~~~~~
- ../src/util/stack.cpp:105:22: note: in expansion of macro 'ALIGN'
- 105 | m_curr_ptr = ALIGN(char *, m_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:30:38: error: 'uintptr_t' does not name a type
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/stack.cpp:105:22: note: in expansion of macro 'ALIGN'
- 105 | m_curr_ptr = ALIGN(char *, m_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:30:38: note: 'uintptr_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/stack.cpp:105:22: note: in expansion of macro 'ALIGN'
- 105 | m_curr_ptr = ALIGN(char *, m_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:30:67: error: 'uintptr_t' does not name a type
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/stack.cpp:105:22: note: in expansion of macro 'ALIGN'
- 105 | m_curr_ptr = ALIGN(char *, m_curr_ptr);
- | ^~~~~
- ../src/util/tptr.h:30:67: note: 'uintptr_t' is defined in header '<cstdint>'; this is probably fixable by adding '#include <cstdint>'
- 30 | static_cast<uintptr_t>((reinterpret_cast<uintptr_t>(PTR) & TAG_MASK) != 0)) << PTR_ALIGNMENT)
- | ^~~~~~~~~
- ../src/util/stack.cpp:105:22: note: in expansion of macro 'ALIGN'
- 105 | m_curr_ptr = ALIGN(char *, m_curr_ptr);
- | ^~~~~
- ocamlfind ocamlc -package zarith -I api/ml -o api/ml/z3native.cmo -c ../src/api/ml/z3native.ml
- make: *** [Makefile:162: util/stack.o] Error 1
[ERROR] The compilation of z3.4.12.2 failed at "make -C build -j 39".
- make: Leaving directory '/home/opam/.opam/default/.opam-switch/build/z3.4.12.2/build'
build failed...
=== STDERR ===
2026-07-26 11:36.10: FAILED: build z3.4.12.2
2026-07-26 11:36.10: Job failed: build failed: z3.4.12.2