我尝试使用Visual Studio 2010编译器在Windows 7 64 Professional 64位上构建Z3定理证明器。我按照自述文件中的说明进行操作，直到进入“build”目录并点击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的理解英语足够好了，这整个废话只会让bug搜索变慢），但它大致如下所示："module machine type 'x64' conflicts with target machine type 'X86'"
我通过git clone https://git01.codeplex.com/z3得到了代码。有什么提示吗？
2条答案
按热度按时间eqqqjvef1#
如果尝试从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_x64x64 d）n制造
1.要构建32位以下的Z3：a）打开32位VS命令行窗口。b）使用命令脚本\mk_make. py-b release_x86配置构建环境。c）cd release_x86 d）nmake
s3fp2yjn2#
我只是有同样的问题（我的电脑是64bit），什么帮助是几件事的组合。一切尼古拉比约纳说，但此外，运行nmake作为：nmake CFG=释放ARCH=x64