search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.43k stars 1.47k forks source link

Z3-4.12.1 doesn't build (OS X 13.2) : undefined symbol ast_smt2_pp #6555

Closed solas closed 1 year ago

solas commented 1 year ago

g++ -o z3 shell/lp_frontend.o ... util/util.a -lpthread Undefined symbols for architecture x86_64: "ast_smt2_pp(std::1::basic_ostream<char, std::__1::char_traits >&, func_decl, expr, smt2_pp_environment&, params_ref const&, unsigned int, char const*)", referenced from: model_converter::display_add(std::1::basic_ostream<char, std::1::char_traits >&, smt2_pp_environment&, ast_manager&, func_decl, expr) in tactic.a(model_converter.o) (maybe you meant: ast_smt2_pp(std::1::basic_ostream<char, std::__1::char_traits >&, func_decl, expr, smt2_pp_environment&, params_ref const&, unsigned int, char const*, bool)) ld: symbol(s) not found for architecture x86_64

Same result with clang++

NikolajBjorner commented 1 year ago

looks like a compiler issue around overload and default argument resolution. I have changed the signature of the function it complains about to work around it.