Comments (3)
You seem to use Visual Studio 2008?
I am seeing the same on 64 bit edition:
(Took sources revision ac21ffe)
d:\z3-master>python scripts/mk_make.py
New component: 'util'
New component: 'polynomial'
New component: 'sat'
New component: 'nlsat'
New component: 'hilbert'
New component: 'interval'
New component: 'realclosure'
New component: 'subpaving'
New component: 'ast'
New component: 'rewriter'
New component: 'normal_forms'
New component: 'model'
New component: 'tactic'
New component: 'substitution'
New component: 'parser_util'
New component: 'grobner'
New component: 'euclid'
New component: 'core_tactics'
New component: 'sat_tactic'
New component: 'arith_tactics'
New component: 'nlsat_tactic'
New component: 'subpaving_tactic'
New component: 'aig_tactic'
New component: 'solver'
New component: 'interp'
New component: 'cmd_context'
New component: 'extra_cmds'
New component: 'smt2parser'
New component: 'proof_checker'
New component: 'simplifier'
New component: 'fpa'
New component: 'macros'
New component: 'pattern'
New component: 'bit_blaster'
New component: 'smt_params'
New component: 'proto_model'
New component: 'smt'
New component: 'user_plugin'
New component: 'bv_tactics'
New component: 'fuzzing'
New component: 'fpa_tactics'
New component: 'smt_tactic'
New component: 'sls_tactic'
New component: 'qe'
New component: 'duality'
New component: 'muz'
New component: 'transforms'
New component: 'rel'
New component: 'pdr'
New component: 'clp'
New component: 'tab'
New component: 'bmc'
New component: 'duality_intf'
New component: 'fp'
New component: 'smtlogic_tactics'
New component: 'ufbv_tactic'
New component: 'portfolio'
New component: 'smtparser'
New component: 'api'
New component: 'shell'
New component: 'test'
New component: 'api_dll'
New component: 'dotnet'
New component: 'java'
New component: 'cpp'
Python bindings directory was detected.
New component: 'cpp_example'
New component: 'iz3'
New component: 'z3_tptp'
New component: 'c_example'
New component: 'maxsat'
New component: 'dotnet_example'
New component: 'java_example'
New component: 'py_example'
Generated 'src\util\version.h'
Updated 'src\api\dotnet\Properties\AssemblyInfo'
Generated 'src\api\dll\api_dll.def'
Generated 'src\ast\pp_params.hpp'
Generated 'src\ast\normal_forms\nnf_params.hpp'
Generated 'src\ast\pattern\pattern_inference_params_helper.hpp'
Generated 'src\ast\rewriter\arith_rewriter_params.hpp'
Generated 'src\ast\rewriter\array_rewriter_params.hpp'
Generated 'src\ast\rewriter\bool_rewriter_params.hpp'
Generated 'src\ast\rewriter\bv_rewriter_params.hpp'
Generated 'src\ast\rewriter\poly_rewriter_params.hpp'
Generated 'src\ast\rewriter\rewriter_params.hpp'
Generated 'src\ast\simplifier\arith_simplifier_params_helper.hpp'
Generated 'src\ast\simplifier\array_simplifier_params_helper.hpp'
Generated 'src\ast\simplifier\bv_simplifier_params_helper.hpp'
Generated 'src\interp\interp_params.hpp'
Generated 'src\math\polynomial\algebraic_params.hpp'
Generated 'src\math\realclosure\rcf_params.hpp'
Generated 'src\model\model_evaluator_params.hpp'
Generated 'src\model\model_params.hpp'
Generated 'src\muz\base\fixedpoint_params.hpp'
Generated 'src\nlsat\nlsat_params.hpp'
Generated 'src\parsers\util\parser_params.hpp'
Generated 'src\sat\sat_asymm_branch_params.hpp'
Generated 'src\sat\sat_params.hpp'
Generated 'src\sat\sat_scc_params.hpp'
Generated 'src\sat\sat_simplifier_params.hpp'
Generated 'src\smt\params\smt_params_helper.hpp'
Generated 'src\solver\combined_solver_params.hpp'
Generated 'src\tactic\sls\sls_params.hpp'
Generated 'src\ast\pattern\database.h'
Generated 'src\shell\install_tactic.cpp'
Generated 'src\test\install_tactic.cpp'
Generated 'src\api\dll\install_tactic.cpp'
Generated 'src\shell\mem_initializer.cpp'
Generated 'src\test\mem_initializer.cpp'
Generated 'src\api\dll\mem_initializer.cpp'
Generated 'src\shell\gparams_register_modules.cpp'
Generated 'src\test\gparams_register_modules.cpp'
Generated 'src\api\dll\gparams_register_modules.cpp'
Generated 'src\api\python\z3consts.py'
Generated 'src\api\dotnet\Enumerations.cs'
Generated 'src\api\api_log_macros.h'
Generated 'src\api\api_log_macros.cpp'
Generated 'src\api\api_commands.cpp'
Generated 'src\api\python\z3core.py'
Generated 'src\api\dotnet\Native.cs'
Listing src\api\python ...
Compiling src\api\python\z3.py ...
Compiling src\api\python\z3consts.py ...
Compiling src\api\python\z3core.py ...
Compiling src\api\python\z3num.py ...
Compiling src\api\python\z3poly.py ...
Compiling src\api\python\z3printer.py ...
Compiling src\api\python\z3rcf.py ...
Compiling src\api\python\z3test.py ...
Compiling src\api\python\z3types.py ...
Compiling src\api\python\z3util.py ...
Copied 'z3.py'
Copied 'z3consts.py'
Copied 'z3core.py'
Copied 'z3num.py'
Copied 'z3poly.py'
Copied 'z3printer.py'
Copied 'z3rcf.py'
Copied 'z3test.py'
Copied 'z3types.py'
Copied 'z3util.py'
Generated 'z3.pyc'
Generated 'z3consts.pyc'
Generated 'z3core.pyc'
Generated 'z3num.pyc'
Generated 'z3poly.pyc'
Generated 'z3printer.pyc'
Generated 'z3rcf.pyc'
Generated 'z3test.pyc'
Generated 'z3types.pyc'
Generated 'z3util.pyc'
64-bit: True
Writing build\Makefile
Copied Z3Py example 'example.py' to 'build'
Makefile was successfully generated.
compilation mode: Release
platform: x86
To build Z3, open a [Visual Studio Command Prompt], then
type 'cd d:\z3-master\build && nmake'
Remark: to open a Visual Studio Command Prompt, go to: "Start > All Programs > Visual Studio > Visual Studio Tools"
d:\z3-master>cd d:\z3-master\build && nmake
Microsoft (R) Program Maintenance Utility Version 9.00.21022.08
Copyright (C) Microsoft Corporation. All rights reserved.
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
gparams_register_modules.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
install_tactic.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
main.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
mem_initializer.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
api_algebraic.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
api_arith.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
api_array.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
api_ast.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
api_ast_map.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
api_ast_vector.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
api_bv.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
api_commands.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
api_config_params.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
api_context.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
api_datalog.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
api_datatype.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
api_goal.cpp
cl : Command line warning D9002 : ignoring unknown option '/arch:SSE2'
api_interp.cpp
d:\z3-master\src\interp\iz3mgr.h(133) : error C2143: syntax error : missing ';' before '<'
d:\z3-master\src\interp\iz3mgr.h(133) : error C2913: explicit specialization; 'std::less' is not a specialization of a class
template
d:\z3-master\src\interp\iz3mgr.h(133) : error C2059: syntax error : '<'
d:\z3-master\src\interp\iz3mgr.h(133) : error C2143: syntax error : missing ';' before '{'
d:\z3-master\src\interp\iz3mgr.h(133) : error C2447: '{' : missing function header (old-style formal list?)
NMAKE : fatal error U1077: '"C:\Program Files (x86)\Microsoft Visual Studio 9.0\VC\BIN\amd64\cl.EXE"' : return code '0x2'
Stop.
d:\z3-master\build>
from z3.
No message was added here, but I think this was solved by the fix by this. Could you check whether the problem still exists?
from z3.
The build is now successful. Thank you.
from z3.
Related Issues (20)
- Make bug HOT 4
- Issue with tactic HOT 5
- Segfault on NIRA
- heap-use-after-free at src/util/rlimit.cpp:90
- invalid model on an incremental QF_UFLIA instance HOT 1
- Optimization issue HOT 1
- Segmentation fault when testing smt2 on linux HOT 1
- kernel support? HOT 1
- need help for formal verifiaction of picorv32
- Issue with tactic HOT 1
- refutation unsoundness issue on an incremental QF_NRA instance
- ASSERTION VIOLATION, File: ../src/qe/mbp/mbp_basic_tg.cpp, Line: 139 HOT 1
- Dead code in nla_basics_lemmas.cpp HOT 1
- Redundant checks in rpolynomial.cpp
- Support constant rotating in bit-blast HOT 2
- Assertion Violation at ../src/qe/qsat.cpp:580
- Assertion Violation at ../src/smt/smt_internalizer.cpp:1112
- z3-solver Z3.String() is not a function angular implementation HOT 2
- Rust Z3. How can I convert Float to f32/f64? HOT 1
- Is it possible to always get rational solutions for NRA? HOT 2
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from z3.