2026-06-16 11:44.06: New job: build z3.4.16.0 (a34ae8d36229)
2026-06-16 11:44.06: Waiting for resource in pool day11-builds
2026-06-16 12:05.18: Got resource from pool day11-builds
2026-06-16 12:05.18: [profile full] build z3.4.16.0
2026-06-16 12:05.18: build z3.4.16.0 (a34ae8d36229)
=== DEPENDENCIES (9 transitive) ===
  conf-c++.1.0                                       87fef3e7fb4f
  conf-gmp.5                                         61e3c79e0ddf
  conf-pkg-config.5                                  64c6b37d622b
  conf-python-3.9.0.0                                9f0bbc328e53
  ocaml.4.14.4                                       cb826ea44eb2
  ocaml-base-compiler.4.14.4                         d2f775f983d7
  ocaml-config.2                                     669e0fcf9e4d
  ocamlfind.1.9.8                                    6025f4a8e98e
  zarith.1.14                                        cde7973b8292
=== STDOUT ===
Processing: [default: loading data]
[z3.4.16.0: dl]
[z3.4.16.0: extract]
[z3.4.16.0/gccstd-2a.patch: dl]
-> retrieved z3.4.16.0  (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.16.0)
- opt = --ml, arg = 
- Set Assembly Version (DEFAULT): 4 16 0 0
- New component: 'util'
- New component: 'polynomial'
- New component: 'interval'
- New component: 'dd'
- New component: 'simplex'
- New component: 'hilbert'
- New component: 'realclosure'
- New component: 'subpaving'
- New component: 'ast'
- New component: 'params'
- New component: 'parser_util'
- New component: 'grobner'
- New component: 'rewriter'
- New component: 'euf'
- New component: 'normal_forms'
- New component: 'macros'
- New component: 'model'
- New component: 'converters'
- New component: 'ast_sls'
- New component: 'sat'
- New component: 'nlsat'
- New component: 'lp'
- New component: 'bit_blaster'
- New component: 'substitution'
- New component: 'proofs'
- 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.16.0.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/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/smt_params_helper.hpp'
- Generated 'src/params/bv_rewriter_params.hpp'
- Generated 'src/params/sat_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/smt_parallel_params.hpp'
- Generated 'src/params/sls_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/lp/lp_params_helper.hpp'
- Generated 'src/math/realclosure/rcf_params.hpp'
- Generated 'src/math/polynomial/algebraic_params.hpp'
- Generated 'src/nlsat/nlsat_params.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 simplifiers
- Component euf
- Component ast
- Component util
- Component polynomial
- Component rewriter
- Component interval
- Component params
- Component normal_forms
- Component bit_blaster
- Component converters
- Component model
- Component macros
- Component substitution
- Component smtlogic_tactics
- Component ackermannization
- Component solver
- Component tactic
- 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 ast_sls
- 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 simplifiers
- Component euf
- Component ast
- Component util
- Component polynomial
- Component rewriter
- Component interval
- Component params
- Component normal_forms
- Component bit_blaster
- Component converters
- Component model
- Component macros
- Component substitution
- Component smtlogic_tactics
- Component ackermannization
- Component solver
- Component tactic
- 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 ast_sls
- 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 simplifiers
- Component euf
- Component ast
- Component util
- Component polynomial
- Component rewriter
- Component interval
- Component params
- Component normal_forms
- Component bit_blaster
- Component converters
- Component model
- Component macros
- Component substitution
- Component smtlogic_tactics
- Component ackermannization
- Component solver
- Component tactic
- 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 ast_sls
- 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'
- 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 'z3printer.cpython-311.pyc'
- Copied 'z3consts.cpython-311.pyc'
- Copied '__init__.cpython-311.pyc'
- Copied 'z3core.cpython-311.pyc'
- Copied 'z3util.cpython-311.pyc'
- Copied 'z3rcf.cpython-311.pyc'
- Copied 'z3poly.cpython-311.pyc'
- Copied 'z3types.cpython-311.pyc'
- Copied 'z3num.cpython-311.pyc'
- Copied 'z3.cpython-311.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
- libatomic:      not required
- Python pkg dir: /usr/local/lib/python3.11/dist-packages
- Python version: 3.11
- 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 'bincover.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.16.0)
- make: Entering directory '/home/opam/.opam/default/.opam-switch/build/z3.4.16.0/build'
- src/smt/smt_statistics.cpp
- src/math/lp/nla_throttle_example.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/z3_exception.cpp
- src/util/approx_set.cpp
- src/util/page.cpp
- src/util/timeout.cpp
- src/util/timeit.cpp
- src/util/bit_util.cpp
- src/util/stack.cpp
- src/util/util.cpp
- src/util/memory_manager.cpp
- src/shell/z3_log_frontend.cpp
- src/api/api_commands.cpp
- src/util/lbool.cpp
- src/util/mpn.cpp
- src/util/fixed_bit_vector.cpp
- src/util/hash.cpp
- src/api/z3_replayer.cpp
- ocamlfind ocamlc -package zarith  -I api/ml -o api/ml/z3enums.cmi -c api/ml/z3enums.mli
- src/solver/smt_logics.cpp
- src/util/symbol.cpp
- src/util/cmd_context_types.cpp
- src/util/warning.cpp
- src/util/min_cut.cpp
- src/util/state_graph.cpp
- ocamlfind ocamlc -package zarith  -I api/ml -o api/ml/z3enums.cmo -c ../src/api/ml/z3enums.ml
- src/util/prime_generator.cpp
- src/util/trace.cpp
- src/util/bit_vector.cpp
- src/util/rlimit.cpp
- src/util/smt2_util.cpp
- src/util/statistics.cpp
- src/util/scoped_timer.cpp
- src/util/small_object_allocator.cpp
- src/util/debug.cpp
- src/util/permutation.cpp
- src/util/region.cpp
- src/api/api_log_macros.cpp
- src/api/api_log.cpp
- src/math/simplex/bit_matrix.cpp
- src/util/mpz.cpp
- ocamlfind ocamlc -package zarith  -i -I api/ml -c ../src/api/ml/z3native.ml > api/ml/z3native.mli
- ocamlfind ocamlc -package zarith  -I api/ml -o api/ml/z3native.cmi -c api/ml/z3native.mli
- ocamlfind ocamlc -package zarith  -I api/ml -o api/ml/z3native.cmo -c ../src/api/ml/z3native.ml
- src/ast/sls/sat_ddfw.cpp
- src/params/pattern_inference_params.cpp
- src/math/realclosure/mpz_matrix.cpp
- src/math/interval/interval_mpq.cpp
- src/util/mpff.cpp
- src/util/mpfx.cpp
- src/util/scoped_ctrl_c.cpp
- src/util/env_params.cpp
- src/util/mpq_inf.cpp
- src/util/mpq.cpp
- cp ../src/api/ml/z3.mli api/ml/z3.mli
- ocamlfind ocamlc -package zarith  -I api/ml -o api/ml/z3.cmi -c api/ml/z3.mli
- src/shell/mem_initializer.cpp
- src/muz/spacer/spacer_matrix.cpp
- src/smt/old_interval.cpp
- ocamlfind ocamlc -package zarith  -I api/ml -o api/ml/z3.cmo -c ../src/api/ml/z3.ml
- src/ast/simplifiers/linear_equation.cpp
- src/sat/sat_config.cpp
- src/params/dyn_ack_params.cpp
- src/params/theory_bv_params.cpp
- src/params/qi_params.cpp
- src/params/theory_seq_params.cpp
- src/params/theory_arith_params.cpp
- src/params/theory_pb_params.cpp
- src/params/theory_array_params.cpp
- src/params/preprocessor_params.cpp
- src/math/realclosure/realclosure.cpp
- src/math/dd/dd_pdd.cpp
- src/math/interval/dep_intervals.cpp
- src/util/mpbq.cpp
- src/util/gparams.cpp
- src/util/inf_int_rational.cpp
- src/util/inf_rational.cpp
- src/util/hwf.cpp
- src/util/sexpr.cpp
- src/util/s_integer.cpp
- src/util/rational.cpp
- src/util/mpf.cpp
- src/util/params.cpp
- src/util/tbv.cpp
- src/api/dll/mem_initializer.cpp
- ocamlfind ocamlopt -package zarith  -I api/ml -o api/ml/z3enums.cmx -c ../src/api/ml/z3enums.ml
- src/ast/simplifiers/bound_propagator.cpp
- src/sat/sat_clause_set.cpp
- src/sat/sat_clause_use_list.cpp
- src/sat/sat_clause.cpp
- src/sat/sat_watched.cpp
- src/ast/sls/sls_bv_valuation.cpp
- src/params/context_params.cpp
- src/math/subpaving/subpaving.cpp
- src/math/subpaving/subpaving_mpff.cpp
- src/math/subpaving/subpaving_mpq.cpp
- src/math/subpaving/subpaving_hwf.cpp
- src/math/subpaving/subpaving_mpfx.cpp
- src/math/subpaving/subpaving_mpf.cpp
- src/math/hilbert/hilbert_basis.cpp
- src/math/simplex/simplex.cpp
- src/math/dd/dd_bdd.cpp
- src/util/zstring.cpp
- src/util/inf_s_integer.cpp
- ocamlfind ocamlopt -package zarith  -I api/ml -o api/ml/z3native.cmx -c ../src/api/ml/z3native.ml
- src/muz/spacer/spacer_arith_kernel.cpp
- src/math/lp/nla_throttle.cpp
- src/nlsat/nlsat_types.cpp
- src/ast/euf/euf_justification.cpp
- src/ast/rewriter/func_decl_replace.cpp
- src/math/grobner/pdd_solver.cpp
- src/math/grobner/pdd_simplifier.cpp
- src/ast/display_dimacs.cpp
- src/ast/quantifier_stat.cpp
- src/ast/for_each_ast.cpp
- src/ast/num_occurs.cpp
- src/ast/ast_lt.cpp
- src/ast/has_free_vars.cpp
- src/math/simplex/model_based_opt.cpp
- src/math/dd/dd_fdd.cpp
- src/math/polynomial/polynomial_cache.cpp
- ocamlfind ocamlopt -package zarith  -I api/ml -o api/ml/z3.cmx -c ../src/api/ml/z3.ml
- src/muz/base/bind_variables.cpp
- src/smt/smt_value_sort.cpp
- src/smt/uses_theory.cpp
- src/ackermannization/ackr_helper.cpp
- src/math/lp/lp_settings.cpp
- src/math/lp/nex_creator.cpp
- src/nlsat/nlsat_interval_set.cpp
- src/nlsat/nlsat_clause.cpp
- src/sat/sat_cleaner.cpp
- src/sat/sat_xor_finder.cpp
- src/sat/sat_parallel.cpp
- src/sat/sat_model_converter.cpp
- src/sat/sat_lookahead.cpp
- src/sat/sat_mus.cpp
- src/sat/sat_integrity_checker.cpp
- src/sat/sat_local_search.cpp
- src/sat/sat_drat.cpp
- src/sat/sat_gc.cpp
- src/sat/sat_probing.cpp
- src/sat/sat_bcd.cpp
- src/sat/sat_elim_eqs.cpp
- src/sat/sat_solver.cpp
- src/sat/sat_prob.cpp
- src/sat/sat_npn3_finder.cpp
- src/sat/sat_proof_trim.cpp
- src/sat/sat_asymm_branch.cpp
- src/sat/sat_aig_finder.cpp
- src/sat/dimacs.cpp
- src/sat/sat_big.cpp
- src/sat/sat_simplifier.cpp
- src/sat/sat_scc.cpp
- src/sat/sat_ddfw_wrapper.cpp
- src/ast/rewriter/mk_extract_proc.cpp
- src/ast/rewriter/char_rewriter.cpp
- src/ast/rewriter/datatype_rewriter.cpp
- src/ast/rewriter/dl_rewriter.cpp
- src/parsers/util/simple_parser.cpp
- src/parsers/util/cost_parser.cpp
- src/parsers/util/scanner.cpp
- src/ast/expr_map.cpp
- src/ast/used_vars.cpp
- src/ast/special_relations_decl_plugin.cpp
- src/ast/expr_stat.cpp
- src/ast/macro_substitution.cpp
- src/ast/pp.cpp
- src/ast/ast_ll_pp.cpp
- src/ast/cost_evaluator.cpp
- src/ast/for_each_expr.cpp
- src/ast/func_decl_dependencies.cpp
- src/ast/format.cpp
- src/ast/occurs.cpp
- src/ast/act_cache.cpp
- src/ast/array_peq.cpp
- src/math/polynomial/algebraic_numbers.cpp
- src/math/polynomial/polynomial.cpp
- src/math/polynomial/sexpr2upolynomial.cpp
- src/math/polynomial/rpolynomial.cpp
- src/api/dll/gparams_register_modules.cpp
- src/shell/main.cpp
- src/shell/drat_frontend.cpp
- src/shell/gparams_register_modules.cpp
- src/opt/totalizer.cpp
- src/smt/arith_eq_solver.cpp
- src/smt/smt_farkas_util.cpp
- src/smt/smt_literal.cpp
- src/math/subpaving/tactic/expr2subpaving.cpp
- src/cmd_context/pdecl.cpp
- src/solver/check_logic.cpp
- src/qe/mbp/mbp_solve_plugin.cpp
- src/ast/simplifiers/bound_manager.cpp
- src/math/lp/dense_matrix.cpp
- src/math/lp/indexed_vector.cpp
- src/nlsat/nlsat_evaluator.cpp
- src/nlsat/nlsat_variable_ordering_strategy.cpp
- src/nlsat/nlsat_simplify.cpp
- src/nlsat/nlsat_simple_checker.cpp
- src/sat/sat_anf_simplifier.cpp
- src/ast/converters/proof_converter.cpp
- src/ast/converters/equiv_proof_converter.cpp
- src/ast/converters/replace_proof_converter.cpp
- src/model/numeral_factory.cpp
- src/model/value_factory.cpp
- src/ast/normal_forms/elim_term_ite.cpp
- src/ast/normal_forms/name_exprs.cpp
- src/ast/euf/euf_enode.cpp
- src/ast/euf/euf_ac_plugin.cpp
- src/ast/euf/euf_egraph.cpp
- src/ast/euf/euf_arith_plugin.cpp
- src/ast/euf/euf_bv_plugin.cpp
- src/ast/euf/euf_plugin.cpp
- src/ast/euf/euf_specrel_plugin.cpp
- src/ast/euf/euf_etable.cpp
- src/ast/rewriter/arith_rewriter.cpp
- src/ast/rewriter/inj_axiom.cpp
- src/ast/rewriter/factor_rewriter.cpp
- src/ast/rewriter/pb_rewriter.cpp
- src/ast/rewriter/bv_rewriter.cpp
- src/ast/rewriter/mk_simplified_app.cpp
- src/ast/rewriter/label_rewriter.cpp
- src/ast/rewriter/dom_simplifier.cpp
- src/ast/rewriter/fpa_rewriter.cpp
- src/ast/rewriter/enum2bv_rewriter.cpp
- src/ast/rewriter/pb2bv_rewriter.cpp
- src/ast/rewriter/bv_bounds.cpp
- src/ast/rewriter/bool_rewriter.cpp
- src/ast/rewriter/factor_equivs.cpp
- src/ast/rewriter/bv2int_translator.cpp
- src/ast/rewriter/push_app_ite.cpp
- src/ast/rewriter/maximize_ac_sharing.cpp
- src/ast/rewriter/rewriter.cpp
- src/ast/rewriter/expr_replacer.cpp
- src/ast/rewriter/seq_skolem.cpp
- src/math/grobner/grobner.cpp
- src/parsers/util/pattern_validation.cpp
- src/ast/polymorphism_inst.cpp
- src/ast/arith_decl_plugin.cpp
- src/ast/pb_decl_plugin.cpp
- src/ast/reg_decl_plugins.cpp
- src/ast/char_decl_plugin.cpp
- src/ast/polymorphism_util.cpp
- src/ast/ast_pp_dot.cpp
- src/ast/well_sorted.cpp
- src/ast/expr2polynomial.cpp
- src/ast/fpa_decl_plugin.cpp
- src/ast/ast_util.cpp
- src/ast/shared_occs.cpp
- src/ast/dl_decl_plugin.cpp
- ../src/ast/dl_decl_plugin.cpp:20:9: fatal error: format: No such file or directory
-    20 | #include<format>
-       |         ^~~~~~~~
- compilation terminated.
- make: *** [Makefile:724: ast/dl_decl_plugin.o] Error 1
- make: *** Waiting for unfinished jobs....
- make: Leaving directory '/home/opam/.opam/default/.opam-switch/build/z3.4.16.0/build'
[ERROR] The compilation of z3.4.16.0 failed at "make -C build -j 39".
build failed... 

=== STDERR ===

2026-06-16 12:18.14: FAILED: build z3.4.16.0
2026-06-16 12:18.14: Job failed: build failed: z3.4.16.0