1

我正在尝试使用 Visual Studio 2010 编译器在 Windows 7 64 Professional 64 位上构建 Z3 定理证明器。我一直按照自述文件的说明进行操作，直到进入“构建”目录并点击nmake. 过了一会儿，我得到以下信息：

    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.

不幸的是，错误消息是德语的（爆炸 i18n，我对英语的理解足够好，这整个废话只会让寻找错误的速度变慢），但它大致说明了以下内容："module machine type 'x64' conflicts with target machine type 'X86'"

我得到了代码git clone https://git01.codeplex.com/z3。关于做什么的任何提示？

4

1 回答 1

5

如果您尝试从 x86 命令行环境构建 x64 二进制文件，通常会发生此错误。

执行以下操作之一：

  1. 要在 64 位下构建 Z3： a) 打开 64 位 Visual Studio 命令行窗口。VS 发行版带有一些预配置的 32 位或 64 位命令行窗口的快捷方式。b) 使用 scripts\mk_make.py --x64 -b release_x64 形式的命令为 Z3 配置构建环境。这将创建一个目录 release_x64，您可以在其中构建 64 位版本的 Z3。c) cd release_x64 d) nmake

  2. 在 32 位下构建 Z3： a) 打开 32 位 VS 命令行窗口。b) 使用命令 scripts\mk_make.py -b release_x86 配置构建环境。c) cd release_x86 d) nmake

于 2013-06-22T16:16:16.173 回答