Last active
May 4, 2016 01:56
-
-
Save nekketsuuu/267f4092fc6cf0e565b084acbcaa74d0 to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
z3$ python scripts/mk_make.py | |
New component: 'util' | |
New component: 'polynomial' | |
New component: 'sat' | |
New component: 'nlsat' | |
New component: 'hilbert' | |
New component: 'simplex' | |
New component: 'automata' | |
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: 'ackermannization' | |
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: 'bv_tactics' | |
New component: 'fuzzing' | |
New component: 'smt_tactic' | |
New component: 'sls_tactic' | |
New component: 'qe' | |
New component: 'duality' | |
New component: 'muz' | |
New component: 'dataflow' | |
New component: 'transforms' | |
New component: 'rel' | |
New component: 'pdr' | |
New component: 'clp' | |
New component: 'tab' | |
New component: 'bmc' | |
New component: 'ddnf' | |
New component: 'duality_intf' | |
New component: 'fp' | |
New component: 'nlsat_smt_tactic' | |
New component: 'ufbv_tactic' | |
New component: 'sat_solver' | |
New component: 'smtlogic_tactics' | |
New component: 'fpa_tactics' | |
New component: 'portfolio' | |
New component: 'smtparser' | |
New component: 'opt' | |
New component: 'api' | |
New component: 'shell' | |
New component: 'test' | |
New component: 'api_dll' | |
New component: 'dotnet' | |
New component: 'java' | |
New component: 'ml' | |
New component: 'cpp' | |
Python bindings directory was detected. | |
New component: 'python_install' | |
New component: 'cpp_example' | |
New component: 'z3_tptp' | |
New component: 'c_example' | |
New component: 'maxsat' | |
New component: 'dotnet_example' | |
New component: 'java_example' | |
New component: 'ml_example' | |
New component: 'py_example' | |
Generating src/util/version.h from src/util/version.h.in | |
Generated 'src/util/version.h' | |
Generating src/api/dotnet/Properties/AssemblyInfo.cs from src/api/dotnet/Properties/AssemblyInfo.cs.in | |
Generated 'src/nlsat/nlsat_params.hpp' | |
Generated 'src/opt/opt_params.hpp' | |
Generated 'src/parsers/util/parser_params.hpp' | |
Generated 'src/tactic/sls/sls_params.hpp' | |
Generated 'src/tactic/smtlogics/qfufbv_tactic_params.hpp' | |
Generated 'src/ackermannization/ackermannize_bv_tactic_params.hpp' | |
Generated 'src/ackermannization/ackermannization_params.hpp' | |
Generated 'src/smt/params/smt_params_helper.hpp' | |
Generated 'src/model/model_params.hpp' | |
Generated 'src/model/model_evaluator_params.hpp' | |
Generated 'src/ast/pp_params.hpp' | |
Generated 'src/ast/fpa/fpa2bv_rewriter_params.hpp' | |
Generated 'src/ast/pattern/pattern_inference_params_helper.hpp' | |
Generated 'src/ast/rewriter/rewriter_params.hpp' | |
Generated 'src/ast/rewriter/array_rewriter_params.hpp' | |
Generated 'src/ast/rewriter/fpa_rewriter_params.hpp' | |
Generated 'src/ast/rewriter/poly_rewriter_params.hpp' | |
Generated 'src/ast/rewriter/bv_rewriter_params.hpp' | |
Generated 'src/ast/rewriter/arith_rewriter_params.hpp' | |
Generated 'src/ast/rewriter/bool_rewriter_params.hpp' | |
Generated 'src/ast/normal_forms/nnf_params.hpp' | |
Generated 'src/ast/simplifier/arith_simplifier_params_helper.hpp' | |
Generated 'src/ast/simplifier/bv_simplifier_params_helper.hpp' | |
Generated 'src/ast/simplifier/array_simplifier_params_helper.hpp' | |
Generated 'src/solver/combined_solver_params.hpp' | |
Generated 'src/math/realclosure/rcf_params.hpp' | |
Generated 'src/math/polynomial/algebraic_params.hpp' | |
Generated 'src/sat/sat_scc_params.hpp' | |
Generated 'src/sat/sat_asymm_branch_params.hpp' | |
Generated 'src/sat/sat_params.hpp' | |
Generated 'src/sat/sat_simplifier_params.hpp' | |
Generated 'src/interp/interp_params.hpp' | |
Generated 'src/muz/base/fixedpoint_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/api_log_macros.h' | |
Generated 'src/api/api_log_macros.cpp' | |
Generated 'src/api/api_commands.cpp' | |
Generated 'src/api/python/z3core.py' | |
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 'z3core.py' | |
Copied 'z3.py' | |
Copied 'z3util.py' | |
Copied 'z3poly.py' | |
Copied 'z3consts.py' | |
Copied 'z3rcf.py' | |
Copied 'z3num.py' | |
Copied 'z3printer.py' | |
Copied 'z3test.py' | |
Copied 'z3types.py' | |
Generated 'z3rcf.cpython-35.pyc' | |
Generated 'z3num.cpython-35.pyc' | |
Generated 'z3core.cpython-35.pyc' | |
Generated 'z3types.cpython-35.pyc' | |
Generated 'z3poly.cpython-35.pyc' | |
Generated 'z3util.cpython-35.pyc' | |
Generated 'z3.cpython-35.pyc' | |
Generated 'z3printer.cpython-35.pyc' | |
Generated 'z3test.cpython-35.pyc' | |
Generated 'z3consts.cpython-35.pyc' | |
Testing ar... | |
Testing g++... | |
Testing gcc... | |
Testing floating point support... | |
Testing OpenMP... | |
Host platform: Linux | |
C++ Compiler: g++ | |
C Compiler : gcc | |
Archive Tool: ar | |
Arithmetic: internal | |
OpenMP: True | |
Prefix: /home/username/anaconda3 | |
64-bit: True | |
FP math: SSE2-GCC | |
Python pkg dir: /home/username/anaconda3/lib/python3.5/site-packages | |
Python version: 3.5 | |
Writing build/Makefile | |
Traceback (most recent call last): | |
File "scripts/mk_make.py", line 21, in <module> | |
mk_makefile() | |
File "/dir/to/z3/scripts/mk_util.py", line 2466, in mk_makefile | |
c.mk_makefile(out) | |
File "/dir/to/z3/scripts/mk_util.py", line 1047, in mk_makefile | |
Component.mk_makefile(self, out) | |
File "/dir/to/z3/scripts/mk_util.py", line 994, in mk_makefile | |
self.add_cpp_rules(out, include_defs, cppfile) | |
File "/dir/to/z3/scripts/mk_util.py", line 952, in add_cpp_rules | |
self.add_rule_for_each_include(out, cppfile) | |
File "/dir/to/z3/scripts/mk_util.py", line 929, in add_rule_for_each_include | |
includes = extract_c_includes(fullname) | |
File "/dir/to/z3/scripts/mk_util.py", line 743, in extract_c_includes | |
for line in f: | |
File "/dir/to/anaconda3/lib/python3.5/codecs.py", line 321, in decode | |
(result, consumed) = self._buffer_decode(data, self.errors, final) | |
UnicodeDecodeError: 'utf-8' codec can't decode byte 0x92 in position 73: invalid start byte | |
z3$ python --version | |
Python 3.5.1 :: Anaconda 4.0.0 (64-bit) | |
z3$ gcc --version | |
gcc (Ubuntu 4.8.4-2ubuntu1~14.04.1) 4.8.4 | |
Copyright (C) 2013 Free Software Foundation, Inc. | |
This is free software; see the source for copying conditions. There is NO | |
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. | |
z3$ |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment