I met the following error while compiling z3. It seems to be an error for ld. I wonder what I can do to make it compile. It is a problem from the opt branch in git. I am on iMac with OS X 10.9.2 (13C1021) I am with xcode Version 5.1.1 (5B1008) with xcode-select tools installed to version 2333. I use port with version 2.2.1 with ld installed. The problem seems to be a linking problem. I am using link loader as: ld64 @136_2+llvm33 (active) My gcc is gcc (MacPorts gcc48 4.8.2_0) 4.8.2
Thank you very much!
g++ -o z3 shell/datalog_frontend.o shell/dimacs_frontend.o
shell/gparams_register_modules.o shell/install_tactic.o shell/main.o
shell/mem_initializer.o shell/smtlib_frontend.o shell/z3_log_frontend.o api/api.a opt/opt.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 smt/tactic/smt_tactic.a tactic/fpa/fpa.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/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/simplex/simplex.a math/hilbert/hilbert.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a -lpthread -fopenmp
0 0x1079c1a68 __assert_rtn + 144
1 0x107a3bccd mach_o::relocatable::Parser<x86_64>::parse(mach_o::relocatable::ParserOptions const&) + 1039
2 0x107a2b899 mach_o::relocatable::Parser<x86_64>::parse(unsigned char const*, unsigned long long, char const*, long, ld::File::Ordinal, mach_o::relocatable::ParserOptions const&) + 313
3 0x107a290f0 mach_o::relocatable::parse(unsigned char const*, unsigned long long, char const*, long, ld::File::Ordinal, mach_o::relocatable::ParserOptions const&) + 208
4 0x107a18797 archive::File<x86_64>::makeObjectFileForMember(archive::File<x86_64>::Entry const*) const + 795
5 0x107a182b3 archive::File<x86_64>::justInTimeforEachAtom(char const*, ld::File::AtomHandler&) const + 139
6 0x1079c5d46 ld::tool::InputFiles::searchLibraries(char const*, bool, bool, bool, ld::File::AtomHandler&) const + 210
7 0x107a0b772 ld::tool::Resolver::resolveUndefines() + 200
8 0x107a0d6e1 ld::tool::Resolver::resolve() + 75
9 0x1079c1d44 main + 370
A linker snapshot was created at:
/tmp/z3-2014-03-25-110931.ld-snapshot
ld: Assertion failed: (cfiStartsArray[i] != cfiStartsArray[i-1]), function parse, file src/ld/parsers/macho_relocatable_file.cpp, line 1555.
collect2: error: ld returned 1 exit status
make: *** [z3] Error 1
It is because we used port and installed gcc and ld and other packages.
Another possibility is that ld was depend on llvm 3.3 rather than llvm 3.4. The problem was solved after updating ld.