CODEWITHSUNDEEP
visual-studioz3
Lynn
Lynn

Reputation: 1

Z3 Build Error Using Visual Studio: fatal error LNK1112: module machine type 'x86' conflicts with target machine type 'x64'

I tried to build Z3 on Win10 64 Professional using Visual Studio 2019.I followed the README instructions up and hit nmake in the "build" directory. After that, I got the following:

 cl  /Fez3.exe /nologo /MD shell\datalog_frontend.obj shell\dimacs_frontend.obj shell\drat_frontend.obj shell\gparams_register_modules.obj shell\install_tactic.obj shell\main.obj shell\mem_initializer.obj shell\opt_frontend.obj shell\smtlib_frontend.obj shell\z3_log_frontend.obj api\api.lib cmd_context\extra_cmds\extra_cmds.lib opt\opt.lib tactic\portfolio\portfolio.lib tactic\fpa\fpa_tactics.lib tactic\ufbv\ufbv_tactic.lib tactic\smtlogics\smtlogic_tactics.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 nlsat\tactic\nlsat_tactic.lib sat\tactic\sat_tactic.lib sat\smt\sat_smt.lib smt\smt.lib smt\proto_model\proto_model.lib math\subpaving\tactic\subpaving_tactic.lib solver\assertions\solver_assertions.lib tactic\arith\arith_tactics.lib tactic\core\core_tactics.lib ast\fpa\fpa.lib ackermannization\ackermannization.lib tactic\aig\aig_tactic.lib ast\pattern\pattern.lib parsers\smt2\smt2parser.lib cmd_context\cmd_context.lib solver\solver.lib qe\lite\qe_lite.lib qe\mbp\mbp.lib tactic\tactic.lib ast\simplifiers\simplifiers.lib ast\converters\converters.lib model\model.lib ast\macros\macros.lib ast\proofs\proofs.lib ast\substitution\substitution.lib ast\normal_forms\normal_forms.lib ast\rewriter\bit_blaster\bit_blaster.lib ast\rewriter\rewriter.lib math\lp\lp.lib nlsat\nlsat.lib sat\sat.lib math\grobner\grobner.lib ast\euf\euf.lib parsers\util\parser_util.lib smt\params\smt_params.lib ast\ast.lib math\subpaving\subpaving.lib math\realclosure\realclosure.lib params\params.lib math\automata\automata.lib math\hilbert\hilbert.lib math\simplex\simplex.lib math\dd\dd.lib math\interval\interval.lib math\polynomial\polynomial.lib util\util.lib /link /profile /MACHINE:X64 /SUBSYSTEM:CONSOLE /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.29.30133\bin\HostX86\x86\cl.EXE"”: return code “0x2”

How to deal with this problem?

Upvotes: 0

Views: 85

Answers (1)

Axel Kemper
Axel Kemper

Reputation: 11322

Looking at the commandline, 83 files are to be linked to get a resulting executable:

shell\datalog_frontend.obj 
shell\dimacs_frontend.obj 
shell\drat_frontend.obj 
shell\gparams_register_modules.obj 
shell\install_tactic.obj 
shell\main.obj 
...
math\dd\dd.lib
math\interval\interval.lib
math\polynomial\polynomial.lib
util\util.lib

I would check three things:

  1. Was shell\datalog_frontend.obj actually compiled for CPUs with 64 bits? Make sure that all object files and all libraries are compiled for the same CPU bit-width.

  2. Is it correct that all these files are .lib library files rather than .obj files? They should probably be .obj files.

  3. Have you seen this related post? And this one?

It is not necessary to build Z3 on your own. You can just download precompiled binaries.

Upvotes: 0

Related Questions