Build error with GCC 12.2.0 - need help with Undefined symbols

[Jerry1144]

Hello, I'm trying to build LLVM which depends on Z3 which needs modern C++ features so my ancient Apple-supplied clang won't work, and I use gcc-12 instead. Yet the build fails.

First with CMake build (which is what Homebrew's script uses), and now with manual Python build, the problem is the same - in the final stages of the build, some symbols with alien-looking names cannot be found. I see nothing resembling __ZN20pattern_inference_rwD1Ev in the offending sat_smt.h or q_solver.cpp and am totally confused.

bash-3.2$ python scripts/mk_make.py --prefix=/usr/local/Cellar/z3/4.12.1
opt = --prefix, arg = /usr/local/Cellar/z3/4.12.1
Set Assembly Version (DEFAULT): 4 12 1 0
New component: 'util'
New component: 'polynomial'
(snip)
Host platform:  Darwin
C++ Compiler:   g++-12
C Compiler  :   gcc-12
Archive Tool:   ar
Arithmetic:     internal
Prefix:         /usr/local/Cellar/z3/4.12.1
64-bit:         True
FP math:        SSE2-GCC
Python pkg dir: /usr/local/lib/python3.11/site-packages
Python version: 3.11
Writing build/Makefile
(snip)

bash-3.2$ cd build;make
(snip)
(snip)
(snip)
src/sat/smt/arith_solver.cpp
src/sat/smt/arith_axioms.cpp
g++-12  -o z3  shell/lp_frontend.o shell/dimacs_frontend.o shell/z3_log_frontend.o shell/install_tactic.o shell/mem_initializer.o shell/datalog_frontend.o shell/gparams_register_modules.o shell/opt_frontend.o shell/smtlib_frontend.o shell/main.o shell/drat_frontend.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 qe/lite/qe_lite.a qe/mbp/mbp.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 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 
g++-12 -o libz3.dylib -dynamiclib api/dll/install_tactic.o api/dll/mem_initializer.o api/dll/gparams_register_modules.o api/dll/dll.o api/api_array.o api/api_fpa.o api/api_arith.o api/api_datatype.o api/z3_replayer.o api/api_model.o api/api_log_macros.o api/api_ast_map.o api/api_datalog.o api/api_ast_vector.o api/api_commands.o api/api_opt.o api/api_special_relations.o api/api_algebraic.o api/api_tactic.o api/api_ast.o api/api_context.o api/api_qe.o api/api_log.o api/api_pb.o api/api_polynomial.o api/api_goal.o api/api_rcf.o api/api_seq.o api/api_bv.o api/api_stats.o api/api_config_params.o api/api_solver.o api/api_quant.o api/api_params.o api/api_numeral.o api/api_parsers.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 qe/lite/qe_lite.a qe/mbp/mbp.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 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 
Undefined symbols for architecture x86_64:
  "__ZN12rewriter_tplI21pattern_inference_cfgED2Ev", referenced from:
Undefined symbols for architecture x86_64:
  "__ZN12rewriter_tplI21pattern_inference_cfgED2Ev", referenced from:
      __ZN20pattern_inference_rwD1Ev in sat_smt.a(q_solver.o)
      __ZN20pattern_inference_rwD1Ev in sat_smt.a(q_solver.o)
ld: symbol(s) not found for architecture x86_64
ld: symbol(s) not found for architecture x86_64
collect2: error: ld returned 1 exit status
make: *** [libz3.dylib] Error 1
make: *** Waiting for unfinished jobs....
collect2: error: ld returned 1 exit status
make: *** [z3] Error 1

I can open a fresh shell and g++-12 -o z3 blahblah myself and get the same error, so it's unlikely that Homebrew's superenv caused this. Any idea how I may resolve this on my side? Thanks in advance.

[Jerry1144]

After tedious work to compile a llvm version 12, I successfully built z3 with llvm_clang. Hmmm.
What's so special with my particular copy of gcc 12 and 11? Like, those Linux builds are all built with GCC so it should not have been problematic.

[NikolajBjorner]

maybe a template dependency issue?
I tend to #include "ast/rewriter/rewriter_def.h" in files that fail to compile on some platforms to resolve. It pops up somewhat arbitrarily.

[tcely]

It's not popping up arbitrarily. See #6764 for the explanation.