none
NMAKE : fatal error U1077 C:\Program Files (x86)\Microsoft Visual Studio\2017\BuildTools\VC\Tools\MSVC\14.16.27023\bin\HostX86\x86\cl.EXE; : return code 0x2; Stop. RRS feed

  • Question

  • Hi all

    I'm installing z3. I'm getting the below errors:

    z3.exe : fatal error LNK1120: 1 unresolved externals
    NMAKE : fatal error U1077: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\BuildTools\VC\Tools\MSVC\14.16.27023\bin\HostX86\x86\cl.EXE"' : return code '0x2'
    Stop.

    I'm using Visual Studio Build Tools 2017. 32bit one.

    OS : Windows 10 Pro

    Steps followed:

    Downloaded the z3 source code from https://github.com/Z3Prover/z3/releases

    Then extracted the zip file.

    Opened a Visual Studio Developer Command Prompt

    Went to the location of the downloaded & extracted folder

    Executed the command : 

    python scripts/mk_make.py

    After running the above command I got a path to execute the nmake

    Path : cd C:\Users\<username>\Downloads\z3-z3-4.8.4\build && nmake

    After getting lot of .cpp packages, it throwed errors. I tried some solutions regarding the same issue but no luck.

    Help me with this issue. Thanks in advance.

    Complete error as follows:

            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\pattern\pattern.lib ast\fpa\fpa.lib parsers\smt2\smt2parser.lib cmd_context\cmd_context.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 sat\tactic\sat_tactic.lib solver\solver.lib ast\proofs\proofs.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\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 /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT
    nlsat.lib(nlsat_solver.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    polynomial.lib(algebraic_numbers.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    rewriter.lib(bv_rewriter.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    rewriter.lib(arith_rewriter.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    rewriter.lib(fpa_rewriter.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    ast.lib(ast_smt2_pp.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt2parser.lib(smt2scanner.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    cmd_context.lib(basic_cmds.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    model.lib(model_evaluator.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    rewriter.lib(th_rewriter.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(theory_utvpi.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(smt_model_finder.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(smt_arith_value.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt2parser.lib(smt2parser.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(theory_seq.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(theory_fpa.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(theory_str.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(theory_jobscheduler.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(asserted_formulas.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(theory_array_full.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(theory_bv.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(theory_dl.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(theory_dense_diff_logic.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(theory_wmaxsat.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(expr_context_simplifier.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(smt_setup.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(theory_pb.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(theory_lra.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(theory_arith.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt.lib(theory_diff_logic.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    qe.lib(nlarith_util.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    sls_tactic.lib(sls_engine.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    smt_tactic.lib(ctx_solver_simplify_tactic.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    bv_tactics.lib(bv_bound_chk_tactic.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    qe.lib(qe_arith_plugin.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    qe.lib(qe_datatype_plugin.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    qe.lib(qe_dl_plugin.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    qe.lib(qe_array_plugin.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    qe.lib(qsat.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    qe.lib(qe.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    qe.lib(qe_bool_plugin.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    qe.lib(qe_bv_plugin.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    transforms.lib(dl_mk_karr_invariants.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    transforms.lib(dl_mk_scale.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    transforms.lib(dl_mk_loop_counter.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    sat_solver.lib(inc_sat_solver.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    rel.lib(dl_interval_relation.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    rel.lib(dl_bound_relation.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    rel.lib(karr_relation.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    rel.lib(udoc_relation.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    ddnf.lib(ddnf.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    spacer.lib(spacer_util.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    spacer.lib(spacer_qe_project.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    spacer.lib(spacer_quant_generalizer.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    opt.lib(wmax.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    opt.lib(sortmax.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    fp.lib(datalog_parser.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    bmc.lib(dl_bmc_engine.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    opt.lib(opt_solver.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    opt.lib(optsmt.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    opt.lib(maxsmt.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    opt.lib(maxres.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    api.lib(api_fpa.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    opt.lib(opt_context.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    opt.lib(opt_parse.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    opt.lib(opt_cmds.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    api.lib(api_numeral.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    api.lib(api_pb.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    api.lib(api_algebraic.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    api.lib(api_opt.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    api.lib(api_context.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    api.lib(api_ast.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    api.lib(api_arith.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    api.lib(api_bv.obj) : error LNK2001: unresolved external symbol "private: static class mpq_manager<0> * rational::g_mpq_manager" (?g_mpq_manager@rational@@0PAV?$mpq_manager@$0A@@@A)
    z3.exe : fatal error LNK1120: 1 unresolved externals
    NMAKE : fatal error U1077: '"C:\Program Files (x86)\Microsoft Visual Studio\2017\BuildTools\VC\Tools\MSVC\14.16.27023\bin\HostX86\x86\cl.EXE"' : return code '0x2'
    Stop.


    Thursday, December 27, 2018 11:32 AM

All replies

  • Hello Kalyan,

    Did you go past this error? I too am facing similar errors with cl.exe.

    Please share in case you found any resolution. Thank you!

    Best,

    Vishal

    Thursday, October 17, 2019 8:27 AM
  • Hello Vishal

    Did you go past this error? I too am facing similar errors with cl.exe.

    Please share in case you found any resolution. Thank you!

    yisun


    Sunday, October 27, 2019 8:03 AM