debug build fails

[ice-phoenix]

When trying to compile z3 (unstable branch) with mk_make.py -d, it fails with:

g++ -o z3  shell/main.o shell/dimacs_frontend.o shell/z3_log_frontend.o shell/mem_initializer.o shell/datalog_frontend.o shell/smtlib_frontend.o shell/install_tactic.o shell/gparams_register_modules.o api/api.a parsers/smt/smtparser.a tactic/portfolio/portfolio.a tactic/ufbv/ufbv_tactic.a tactic/smtlogics/smtlogic_tactics.a muz/fp/fp.a muz/duality/duality_intf.a muz/bmc/bmc.a muz/tab/tab.a muz/clp/clp.a muz/pdr/pdr.a muz/rel/rel.a muz/transforms/transforms.a muz/base/muz.a duality/duality.a qe/qe.a tactic/sls/sls_tactic.a tactic/fpa/fpa_tactics.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a smt/user_plugin/user_plugin.a smt/smt.a smt/proto_model/proto_model.a smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/pattern/pattern.a ast/macros/macros.a ast/fpa/fpa.a ast/simplifier/simplifier.a ast/proof_checker/proof_checker.a parsers/smt2/smt2parser.a cmd_context/extra_cmds/extra_cmds.a cmd_context/cmd_context.a interp/interp.a solver/solver.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a sat/tactic/sat_tactic.a tactic/core/core_tactics.a math/euclid/euclid.a math/grobner/grobner.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/rewriter/rewriter.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a math/hilbert/hilbert.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a  -lpthread -Wl,-O1,--sort-common,--as-needed,-z,relro -fopenmp -lrt
parsers/smt/smtparser.a(smtparser.o): In function `proto_region::~proto_region()':
smtparser.cpp:(.text._ZN12proto_regionD2Ev[_ZN12proto_regionD5Ev]+0x12a): undefined reference to `region::reset()'
parsers/smt/smtparser.a(smtparser.o): In function `smtparser::make_expression(symbol_table<idbuilder*>&, proto_expr*, obj_ref<expr, ast_manager>&)':
smtparser.cpp:(.text._ZN9smtparser15make_expressionER12symbol_tableIP9idbuilderEP10proto_exprR7obj_refI4expr11ast_managerE[_ZN9smtparser15make_expressionER12symbol_tableIP9idbuilderEP10proto_exprR7obj_refI4expr11ast_managerE]+0x50): undefined reference to `region::region()'
parsers/smt/smtparser.a(smtparser.o): In function `smtparser::read_patterns(unsigned int, symbol_table<idbuilder*>&, proto_expr* const*&, ref_buffer<expr, ast_manager, 16u>&, ref_buffer<expr, ast_manager, 16u>&, int&, symbol&, symbol&)':
smtparser.cpp:(.text._ZN9smtparser13read_patternsEjR12symbol_tableIP9idbuilderERPKP10proto_exprR10ref_bufferI4expr11ast_managerLj16EESE_RiR6symbolSH_[_ZN9smtparser13read_patternsEjR12symbol_tableIP9idbuilderERPKP10proto_exprR10ref_bufferI4expr11ast_managerLj16EESE_RiR6symbolSH_]+0x8e): undefined reference to `region::region()'
parsers/smt/smtparser.a(smtparser.o): In function `smtparser::parse_string(char const*)':
smtparser.cpp:(.text._ZN9smtparser12parse_stringEPKc[_ZN9smtparser12parse_stringEPKc]+0x1f0): undefined reference to `region::region()'
parsers/smt/smtparser.a(smtparser.o): In function `smtparser::parse_stream(std::istream&)':
smtparser.cpp:(.text._ZN9smtparser12parse_streamERSi[_ZN9smtparser12parse_streamERSi]+0x42): undefined reference to `region::region()'
collect2: error: ld returned 1 exit status
Makefile:3216: recipe for target 'z3' failed
make: *** [z3] Error 1

[wintersteiger]

This looks like you might have some stale object files in the build directory. Can you please retry with a completely fresh build directory? Also, what's your system configuration, OS and g++ version, etc.

[ice-phoenix]

[ice-phoenix@niobium ~]$ uname -a
Linux niobium.local 3.19.2-1-ARCH #1 SMP PREEMPT Wed Mar 18 16:21:02 CET 2015 x86_64 GNU/Linux
[ice-phoenix@niobium ~]$ g++ --version
g++ (GCC) 4.9.2 20150304 (prerelease)

[wintersteiger]

This looks like a linker bug to me. The function region::reset() is an inline function in region.h:42 which is where it should be. Potentially also a misconfiguration problem when enabling -d because in debug mode this function is inline, while in release mode it's defined in region.cpp.

[ice-phoenix]

After trying with a clean build directory, everything compiled successfully. It does look like some of the libs were left from the previous compilation and were not recompiled with -d. Cheers!