I'm trying to build the Z3 theorem prover on Windows 7 64 Professional 64 bit using the Visual Studio 2010 compilers. I followed the README instructions up until I went into the "build" directory and hit nmake. After a while, I get the following:
cl /Fez3.exe /nologo /MD shell/datalog_frontend.obj shell/dimacs_frontend.obj shell/install_tactic.obj shell/main.obj shell/smtlib_frontend.ob
j shell/z3_log_frontend.obj api/api.lib parsers/smt/smtparser.lib tactic/portfolio/portfolio.lib tactic/ufbv/ufbv_tactic.lib tactic/smtlogics/smtlogic
_tactics.lib muz_qe/muz_qe.lib tactic/sls/sls_tactic.lib smt/tactic/smt_tactic.lib tactic/fpa/fpa.lib tactic/bv/bv_tactics.lib smt/user_plugin/user_pl
ugin.lib smt/smt.lib smt/proto_model/proto_model.lib ast/rewriter/bit_blaster/bit_blaster.lib ast/proof_checker/proof_checker.lib ast/macros/macros.li
b ast/pattern/pattern.lib parsers/smt2/smt2parser.lib cmd_context/extra_cmds/extra_cmds.lib cmd_context/cmd_context.lib solver/solver.lib tactic/aig/a
ig_tactic.lib math/subpaving/tactic/subpaving_tactic.lib nlsat/tactic/nlsat_tactic.lib tactic/arith/arith_tactics.lib sat/tactic/sat_tactic.lib tactic
/core/core_tactics.lib ast/normal_forms/normal_forms.lib ast/simplifier/simplifier.lib front_end_params/front_end_params.lib math/euclid/euclid.lib ma
th/grobner/grobner.lib parsers/util/parser_util.lib ast/substitution/substitution.lib tactic/tactic.lib model/model.lib ast/rewriter/rewriter.lib ast/
ast.lib math/subpaving/subpaving.lib math/interval/interval.lib nlsat/nlsat.lib sat/sat.lib math/polynomial/polynomial.lib util/util.lib /link /DEBUG
/MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT
shell/datalog_frontend.obj : fatal error LNK1112: Modul-Computertyp "x64" steht in Konflikt mit dem Zielcomputertyp "X86".
NMAKE : fatal error U1077: ""C:\Program Files (x86)\Microsoft Visual Studio 10.0\VC\BIN\amd64\cl.EXE"": Rückgabe-Code "0x2"
Stop.
The error message is in German, unfortunately, but it roughly says the following: "module machine type 'x64' conflicts with target machine type 'X86'"
I got the code by git clone https://git01.codeplex.com/z3. Any hints on what to do?
This error typically happens if you try to build x64 binary from a x86 command line environment.
Do one of the following:
To build Z3 under 64 bits: a) open a 64 bit Visual studio command line window. The VS distribution comes with some pre-configured shortcuts to command-line windows for either 32 or 64 bits. b) configure a build environment for Z3 using a command of the form scripts\mk_make.py --x64 -b release_x64. This creates a directory release_x64 where you can build a 64 bit version of Z3. c) cd release_x64 d) nmake
TO build Z3 under 32 bits: a) open a 32 bit VS command line window. b) configure a build environment using a command scripts\mk_make.py -b release_x86. c) cd release_x86 d) nmake