Ld when compiling z3

When compiling z3, I met the following error. This seems to be a bug for ld. I wonder what I can do to compile it. This is a problem from the opt branch in git. I'm on iMac with OS X 10.9.2 (13C1021) I'm on xcode Version 5.1.1 (5B1008) with xcode-select tools installed on version 2333. I'm using a port with version 2.2.1 with ld installed. The problem seems to be related to the binding problem. I use the 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 
+2
linker ld z3
Apr 25 '14 at 10:25
source share
1 answer

This is because we used the port and installed gcc and ld and other packages.

Another possibility is that ld depended on llvm 3.3, and not on llvm 3.4. The problem was resolved after updating ld.

+1
Apr 25 '14 at 22:07
source share



All Articles