search

Z3Prover / z3

The Z3 Theorem Prover
Other
10.29k stars 1.48k forks source link

module machine conflicts with target machine" build error #2320

Closed d-vyd closed 5 years ago

d-vyd commented 5 years ago

I followed the instructions to build in a developer command prompt (VS 2019) and received an error and return code '0x2'. I'm running Windows 10 64-bit on an i7. I issued these commands:

D:\projects\Programming\z3\build>python scripts/mkmake.py -x D:\projects\Programming\z3\build>cd build D:\projects\Programming\z3\build>nmake

Everything worked fine until this "module machine conflicts with target machine" error:

... timeit.cpp timeout.cpp trace.cpp util.cpp warning.cpp z3_exception.cpp cl /Fez3.exe /nologo /MD shell\datalog_frontend.obj shell\dimacs_frontend.obj shell\gparams_register_modules.obj shell\install_tactic.obj shell\lp_frontend.obj shell\main.obj shell\mem_initializer.obj shell\opt_frontend.obj shell\smtlib_frontend.obj shell\z3_log_frontend.obj cmd_context\extra_cmds\extra_cmds.lib api\api.lib opt\opt.lib tactic\portfolio\portfolio.lib tactic\fpa\fpa_tactics.lib tactic\smtlogics\smtlogic_tactics.lib tactic\ufbv\ufbv_tactic.lib muz\fp\fp.lib muz\bmc\bmc.lib muz\ddnf\ddnf.lib muz\tab\tab.lib muz\clp\clp.lib muz\spacer\spacer.lib muz\rel\rel.lib muz\transforms\transforms.lib muz\dataflow\dataflow.lib muz\base\muz.lib tactic\fd_solver\fd_solver.lib sat\sat_solver\sat_solver.lib qe\qe.lib tactic\sls\sls_tactic.lib smt\tactic\smt_tactic.lib tactic\bv\bv_tactics.lib smt\smt.lib smt\proto_model\proto_model.lib smt\params\smt_params.lib ast\rewriter\bit_blaster\bit_blaster.lib ast\fpa\fpa.lib ackermannization\ackermannization.lib tactic\aig\aig_tactic.lib math\subpaving\tactic\subpaving_tactic.lib nlsat\tactic\nlsat_tactic.lib tactic\arith\arith_tactics.lib tactic\core\core_tactics.lib ast\pattern\pattern.lib parsers\smt2\smt2parser.lib sat\tactic\sat_tactic.lib cmd_context\cmd_context.lib solver\solver.lib ast\proofs\proofs.lib math\euclid\euclid.lib math\grobner\grobner.lib parsers\util\parser_util.lib ast\substitution\substitution.lib tactic\tactic.lib model\model.lib ast\normal_forms\normal_forms.lib ast\macros\macros.lib ast\rewriter\rewriter.lib ast\ast.lib math\subpaving\subpaving.lib math\realclosure\realclosure.lib math\interval\interval.lib math\automata\automata.lib math\simplex\simplex.lib math\hilbert\hilbert.lib util\lp\lp.lib nlsat\nlsat.lib sat\sat.lib math\polynomial\polynomial.lib util\util.lib /link /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 shell\datalog_frontend.obj : fatal error LNK1112: module machine type 'x86' conflicts with target machine type 'x64' NMAKE : fatal error U1077: '"C:\Program Files (x86)\Microsoft Visual Studio\2019\Community\VC\Tools\MSVC\14.21.27702\bin\HostX86\x86\cl.EXE"' : return code '0x2' Stop.

wintersteiger commented 5 years ago

Make sure you use the correct Visual Studio Command Prompt - there are 32 and 64 bit versions and only use -x if you're building in a 64 bit Command Prompt. Also, make sure you delete and regenerate the build directory so that no old 32-bit object files are around.

d-vyd commented 5 years ago

Thank you. It compiled!

On Jun 5, 2019 12:49 PM, "Christoph M. Wintersteiger" notifications@github.com wrote:

Closed #2320https://github.com/Z3Prover/z3/issues/2320.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHubhttps://github.com/Z3Prover/z3/issues/2320?email_source=notifications&email_token=AGJMWF2WK2TWLOZMSIECGDTPY6D3JA5CNFSM4HTP3TFKYY3PNVWWK3TUL52HS4DFWZEXG43VMVCXMZLOORHG65DJMZUWGYLUNFXW5KTDN5WW2ZLOORPWSZGORZ7P3KI#event-2390687145, or mute the threadhttps://github.com/notifications/unsubscribe-auth/AGJMWFZFRNAV7DWJ2BXYFADPY6D3JANCNFSM4HTP3TFA.