AMD64 Windows build failure

[mlr-msft]

I'm attempting to build the latest Z3 for Windows on a 64-bit platform. After invoking NMAKE, the build fails giving the following message:

    cl /Fez3.exe /nologo /MD shell\datalog_frontend.obj shell\dimacs_frontend.obj shell\gparams_register_modules.obj shell\install_tactic.obj shell\main.obj shell\mem_initializer.obj shell\smtlib_frontend.obj 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\fp\fp.lib muz\duality\duality_intf.lib muz\bmc\bmc.lib muz\tab\tab.lib muz\clp\clp.lib muz\pdr\pdr.lib muz\rel\rel.lib muz\transforms\transforms.lib muz\base\muz.lib duality\duality.lib qe\qe.lib tactic\sls\sls_tactic.lib tactic\fpa\fpa_tactics.lib smt\tactic\smt_tactic.lib tactic\bv\bv_tactics.lib smt\user_plugin\user_plugin.lib smt\smt.lib smt\proto_model\proto_model.lib smt\params\smt_params.lib ast\rewriter\bit_blaster\bit_blaster.lib ast\pattern\pattern.lib ast\macros\macros.lib ast\fpa\fpa.lib ast\simplifier\simplifier.lib ast\proof_checker\proof_checker.lib parsers\smt2\smt2parser.lib cmd_context\extra_cmds\extra_cmds.lib cmd_context\cmd_context.lib interp\interp.lib solver\solver.lib tactic\aig\aig_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 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\rewriter\rewriter.lib ast\ast.lib math\subpaving\subpaving.lib math\realclosure\realclosure.lib math\interval\interval.lib math\hilbert\hilbert.lib nlsat\nlsat.lib sat\sat.lib math\polynomial\polynomial.lib util\util.lib  /link /LTCG /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT
shell\datalog_frontend.obj : fatal error LNK1112: module machine type 'x64' conflicts with target machine type 'X86'

Thanks in advance.

[NikolajBjorner]

I tend to get these error messages if I recycle the build directory from a 32 bit build or use the wrong VS command-shell (there are separate command shells one can invoke from the VS distribution depending on target platforms). My own x64 build seems fine.

[mlr-msft]

That doesn't appear to be the case in my situation. I am using a fresh pull of the Z3 repository and I've confirmed that I'm both generating and building from within a 64-bit VS command shell.

As far as I can tell, the reason is related to the VS_X64 flag not being set before line 1765 of mk_util.py is reached when generating makefiles. Forcing a 64-bit build with the -x argument to mk_make.py works around the problem for me and eliminates recurring platform mismatch warnings.

Could it be that the Python scripts are not detecting the 64-bit compiler correctly? I have noticed that I am using a 32-bit Python. If the script is querying which Python interpreter is running to determine the value of VS_X64, rather than checking the output of cl.exe, a problem of the sort that I am describing would manifest.

[NikolajBjorner]

You have to explicitly set the make files to x64 using -x. The default sets the make files for 32 bit.