Skip to content

Instantly share code, notes, and snippets.

@nekketsuuu
Last active May 4, 2016 01:56
Show Gist options
  • Save nekketsuuu/267f4092fc6cf0e565b084acbcaa74d0 to your computer and use it in GitHub Desktop.
Save nekketsuuu/267f4092fc6cf0e565b084acbcaa74d0 to your computer and use it in GitHub Desktop.
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