Created temporary directory: /tmp/pip-ephem-wheel-cache-s5wqamls Created temporary directory: /tmp/pip-req-tracker-c0ln70ql Created requirements tracker '/tmp/pip-req-tracker-c0ln70ql' Created temporary directory: /tmp/pip-wheel-cy5479rh Collecting z3-solver-mythril==4.8.4.1 1 location(s) to search for versions of z3-solver-mythril: * https://pypi.org/simple/z3-solver-mythril/ Getting page https://pypi.org/simple/z3-solver-mythril/ Analyzing links from page https://pypi.org/simple/z3-solver-mythril/ Found link https://files.pythonhosted.org/packages/3c/f7/d7e22110f59de19ed69d6fe8fdb06f697927d41de192aefae8bf76022566/z3-solver-mythril-4.8.4.1.tar.gz#sha256=16986cb10e18da3d70ba0e9694b037eeea43524ac725d10cf4cdc6387164b8b4 (from https://pypi.org/simple/z3-solver-mythril/), version: 4.8.4.1 Skipping link https://files.pythonhosted.org/packages/11/12/91600af9401c88ed1d29731de245657b5517f164af05ee9d27565b48b290/z3_solver_mythril-4.8.4.1-py3-none-manylinux1_x86_64.whl#sha256=1e1ac57e486adfcf391f7ecc7b6de4da7ebbb7af03da32687a7e5ed7870be4a4 (from https://pypi.org/simple/z3-solver-mythril/); it is not compatible with this Python Using version 4.8.4.1 (newest of versions: 4.8.4.1) Created temporary directory: /tmp/pip-unpack-cay1qp4b Downloading https://files.pythonhosted.org/packages/3c/f7/d7e22110f59de19ed69d6fe8fdb06f697927d41de192aefae8bf76022566/z3-solver-mythril-4.8.4.1.tar.gz (4.2MB) Downloading from URL https://files.pythonhosted.org/packages/3c/f7/d7e22110f59de19ed69d6fe8fdb06f697927d41de192aefae8bf76022566/z3-solver-mythril-4.8.4.1.tar.gz#sha256=16986cb10e18da3d70ba0e9694b037eeea43524ac725d10cf4cdc6387164b8b4 (from https://pypi.org/simple/z3-solver-mythril/) Added z3-solver-mythril==4.8.4.1 from https://files.pythonhosted.org/packages/3c/f7/d7e22110f59de19ed69d6fe8fdb06f697927d41de192aefae8bf76022566/z3-solver-mythril-4.8.4.1.tar.gz#sha256=16986cb10e18da3d70ba0e9694b037eeea43524ac725d10cf4cdc6387164b8b4 to build tracker '/tmp/pip-req-tracker-c0ln70ql' Running setup.py (path:/tmp/pip-wheel-cy5479rh/z3-solver-mythril/setup.py) egg_info for package z3-solver-mythril Running command python setup.py egg_info running egg_info creating pip-egg-info/z3_solver_mythril.egg-info writing dependency_links to pip-egg-info/z3_solver_mythril.egg-info/dependency_links.txt writing top-level names to pip-egg-info/z3_solver_mythril.egg-info/top_level.txt writing pip-egg-info/z3_solver_mythril.egg-info/PKG-INFO writing manifest file 'pip-egg-info/z3_solver_mythril.egg-info/SOURCES.txt' reading manifest file 'pip-egg-info/z3_solver_mythril.egg-info/SOURCES.txt' writing manifest file 'pip-egg-info/z3_solver_mythril.egg-info/SOURCES.txt' Source in /tmp/pip-wheel-cy5479rh/z3-solver-mythril has version 4.8.4.1, which satisfies requirement z3-solver-mythril==4.8.4.1 from https://files.pythonhosted.org/packages/3c/f7/d7e22110f59de19ed69d6fe8fdb06f697927d41de192aefae8bf76022566/z3-solver-mythril-4.8.4.1.tar.gz#sha256=16986cb10e18da3d70ba0e9694b037eeea43524ac725d10cf4cdc6387164b8b4 Removed z3-solver-mythril==4.8.4.1 from https://files.pythonhosted.org/packages/3c/f7/d7e22110f59de19ed69d6fe8fdb06f697927d41de192aefae8bf76022566/z3-solver-mythril-4.8.4.1.tar.gz#sha256=16986cb10e18da3d70ba0e9694b037eeea43524ac725d10cf4cdc6387164b8b4 from build tracker '/tmp/pip-req-tracker-c0ln70ql' Building wheels for collected packages: z3-solver-mythril Created temporary directory: /tmp/pip-wheel-_y0kg7vx Running setup.py bdist_wheel for z3-solver-mythril: started Destination directory: /tmp/pip-wheel-_y0kg7vx Running command /usr/bin/python3 -u -c "import setuptools, tokenize;__file__='/tmp/pip-wheel-cy5479rh/z3-solver-mythril/setup.py';f=getattr(tokenize, 'open', open)(__file__);code=f.read().replace('\r\n', '\n');f.close();exec(compile(code, __file__, 'exec'))" bdist_wheel -d /tmp/pip-wheel-_y0kg7vx running bdist_wheel running build Configuring Z3 New component: 'util' New component: 'polynomial' New component: 'sat' New component: 'nlsat' New component: 'lp' 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: 'macros' 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: 'proofs' New component: 'solver' New component: 'sat_tactic' New component: 'arith_tactics' New component: 'nlsat_tactic' New component: 'subpaving_tactic' New component: 'aig_tactic' New component: 'ackermannization' New component: 'cmd_context' New component: 'smt2parser' New component: 'fpa' 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: 'sat_solver' New component: 'fd_solver' New component: 'muz' New component: 'dataflow' New component: 'transforms' New component: 'rel' New component: 'spacer' New component: 'clp' New component: 'tab' New component: 'ddnf' New component: 'bmc' New component: 'fp' New component: 'ufbv_tactic' New component: 'smtlogic_tactics' New component: 'fpa_tactics' New component: 'portfolio' New component: 'opt' New component: 'api' New component: 'extra_cmds' New component: 'shell' New component: 'test' New component: 'api_dll' New component: 'dotnet' New component: 'dotnetcore' New component: 'java' New component: 'ml' New component: 'cpp' Python bindings directory was detected. New component: 'python' New component: 'python_install' New component: 'js' 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/z3_version.h from src/util/z3_version.h.in Generated 'src/util/z3_version.h' Generating src/api/dotnet/Properties/AssemblyInfo.cs from src/api/dotnet/Properties/AssemblyInfo.cs.in Generated 'src/ackermannization/ackermannization_params.hpp' Generated 'src/ackermannization/ackermannize_bv_tactic_params.hpp' Generated 'src/muz/base/fp_params.hpp' Generated 'src/util/lp/lp_params.hpp' Generated 'src/smt/params/smt_params_helper.hpp' Generated 'src/opt/opt_params.hpp' Generated 'src/math/polynomial/algebraic_params.hpp' Generated 'src/math/realclosure/rcf_params.hpp' Generated 'src/solver/combined_solver_params.hpp' Generated 'src/solver/parallel_params.hpp' Generated 'src/solver/solver_params.hpp' Generated 'src/tactic/tactic_params.hpp' Generated 'src/tactic/sls/sls_params.hpp' Generated 'src/tactic/smtlogics/qfufbv_tactic_params.hpp' Generated 'src/model/model_evaluator_params.hpp' Generated 'src/model/model_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/ast/pp_params.hpp' Generated 'src/ast/fpa/fpa2bv_rewriter_params.hpp' Generated 'src/ast/normal_forms/nnf_params.hpp' Generated 'src/ast/rewriter/poly_rewriter_params.hpp' Generated 'src/ast/rewriter/bv_rewriter_params.hpp' Generated 'src/ast/rewriter/bool_rewriter_params.hpp' Generated 'src/ast/rewriter/array_rewriter_params.hpp' Generated 'src/ast/rewriter/arith_rewriter_params.hpp' Generated 'src/ast/rewriter/rewriter_params.hpp' Generated 'src/ast/rewriter/fpa_rewriter_params.hpp' Generated 'src/ast/pattern/pattern_inference_params_helper.hpp' Generated 'src/nlsat/nlsat_params.hpp' Generated 'src/parsers/util/parser_params.hpp' Generated 'src/ast/pattern/database.h' Component api Component portfolio Component smtlogic_tactics Component ackermannization Component model Component rewriter Component ast Component util Component polynomial Component automata Component solver Component tactic Component proofs Component sat_solver Component core_tactics Component macros Component normal_forms Component aig_tactic Component bv_tactics Component bit_blaster Component arith_tactics Component sat Component sat_tactic Component nlsat_tactic Component nlsat Component smt_tactic Component smt Component cmd_context Component proto_model Component smt_params Component pattern Component smt2parser Component parser_util Component substitution Component grobner Component euclid Component simplex Component fpa Component lp Component fp Component muz Component qe Component clp Component transforms Component hilbert Component dataflow Component tab Component rel Component bmc Component fd_solver Component ddnf Component spacer Component ufbv_tactic Component fpa_tactics Component sls_tactic Component subpaving_tactic Component subpaving Component interval Component realclosure Component opt Component extra_cmds Component shell Generated 'src/shell/install_tactic.cpp' Component api Component portfolio Component smtlogic_tactics Component ackermannization Component model Component rewriter Component ast Component util Component polynomial Component automata Component solver Component tactic Component proofs Component sat_solver Component core_tactics Component macros Component normal_forms Component aig_tactic Component bv_tactics Component bit_blaster Component arith_tactics Component sat Component sat_tactic Component nlsat_tactic Component nlsat Component smt_tactic Component smt Component cmd_context Component proto_model Component smt_params Component pattern Component smt2parser Component parser_util Component substitution Component grobner Component euclid Component simplex Component fpa Component lp Component fp Component muz Component qe Component clp Component transforms Component hilbert Component dataflow Component tab Component rel Component bmc Component fd_solver Component ddnf Component spacer Component ufbv_tactic Component fpa_tactics Component sls_tactic Component subpaving_tactic Component subpaving Component interval Component realclosure Component opt Component fuzzing Component test Generated 'src/test/install_tactic.cpp' Component api Component portfolio Component smtlogic_tactics Component ackermannization Component model Component rewriter Component ast Component util Component polynomial Component automata Component solver Component tactic Component proofs Component sat_solver Component core_tactics Component macros Component normal_forms Component aig_tactic Component bv_tactics Component bit_blaster Component arith_tactics Component sat Component sat_tactic Component nlsat_tactic Component nlsat Component smt_tactic Component smt Component cmd_context Component proto_model Component smt_params Component pattern Component smt2parser Component parser_util Component substitution Component grobner Component euclid Component simplex Component fpa Component lp Component fp Component muz Component qe Component clp Component transforms Component hilbert Component dataflow Component tab Component rel Component bmc Component fd_solver Component ddnf Component spacer Component ufbv_tactic Component fpa_tactics Component sls_tactic Component subpaving_tactic Component subpaving Component interval Component realclosure Component opt Component extra_cmds Component api_dll 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/z3/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/z3/z3core.py' Listing 'src/api/python/z3'... Compiling 'src/api/python/z3/z3consts.py'... Compiling 'src/api/python/z3/z3core.py'... Generated python bytecode Copied 'z3core.py' Copied 'z3consts.py' Copied 'z3consts.cpython-34.pyc' Copied 'z3core.cpython-34.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: /usr 64-bit: False FP math: ARM-VFP Python pkg dir: /usr/lib/python3/dist-packages Python version: 3.4 Writing build/Makefile Copied Z3Py example 'parallel.py' to 'build/python' Copied Z3Py example 'rc2.py' to 'build/python' Copied Z3Py example 'all_interval_series.py' to 'build/python' Copied Z3Py example 'mini_quip.py' to 'build/python' Copied Z3Py example 'mini_ic3.py' to 'build/python' Copied Z3Py example 'visitor.py' to 'build/python' Copied Z3Py example 'socrates.py' to 'build/python' Copied Z3Py example 'example.py' to 'build/python' Makefile was successfully generated. compilation mode: Release Type 'cd build; make' to build Z3 Building Z3 src/smt/smt_statistics.cpp src/util/common_msgs.cpp src/util/luby.cpp src/util/approx_nat.cpp src/api/dll/dll.cpp src/util/approx_set.cpp src/util/z3_exception.cpp src/util/cooperate.cpp src/util/memory_manager.cpp src/util/page.cpp src/util/timeit.cpp src/api/api_commands.cpp src/api/api_log.cpp src/util/timer.cpp src/util/stack.cpp src/util/util.cpp src/util/timeout.cpp src/util/bit_util.cpp src/util/lbool.cpp src/util/mpn.cpp src/util/fixed_bit_vector.cpp src/util/scoped_ctrl_c.cpp src/util/hash.cpp src/util/scoped_timer.cpp src/shell/z3_log_frontend.cpp src/solver/smt_logics.cpp src/math/automata/automaton.cpp src/util/debug.cpp src/util/prime_generator.cpp src/util/small_object_allocator.cpp src/util/trace.cpp src/util/permutation.cpp src/util/bit_vector.cpp src/util/smt2_util.cpp src/util/symbol.cpp src/util/region.cpp src/util/warning.cpp src/util/min_cut.cpp src/api/api_log_macros.cpp src/api/z3_replayer.cpp src/sat/sat_bdd.cpp src/util/cmd_context_types.cpp src/util/mpz.cpp src/util/rlimit.cpp src/util/statistics.cpp src/math/euclid/euclidean_solver.cpp src/math/realclosure/mpz_matrix.cpp src/math/interval/interval_mpq.cpp src/sat/sat_clause.cpp src/sat/sat_watched.cpp src/sat/sat_clause_set.cpp src/sat/sat_clause_use_list.cpp src/util/mpq_inf.cpp src/util/mpff.cpp src/util/mpq.cpp src/util/mpfx.cpp src/shell/mem_initializer.cpp src/smt/old_interval.cpp src/smt/params/qi_params.cpp src/smt/params/dyn_ack_params.cpp src/smt/params/preprocessor_params.cpp src/smt/params/theory_pb_params.cpp src/smt/params/theory_arith_params.cpp src/smt/params/theory_array_params.cpp src/smt/params/theory_str_params.cpp src/smt/params/theory_seq_params.cpp src/smt/params/theory_bv_params.cpp src/ast/pattern/pattern_inference_params.cpp src/math/subpaving/subpaving_mpff.cpp src/math/subpaving/subpaving_mpq.cpp src/math/subpaving/subpaving.cpp src/math/realclosure/realclosure.cpp src/util/env_params.cpp src/util/params.cpp src/util/s_integer.cpp src/util/gparams.cpp src/util/rational.cpp src/util/inf_rational.cpp src/util/inf_int_rational.cpp src/util/mpf.cpp src/util/hwf.cpp src/util/sexpr.cpp src/util/mpbq.cpp src/api/dll/mem_initializer.cpp src/muz/spacer/spacer_matrix.cpp src/smt/smt_quantifier_stat.cpp src/smt/proto_model/value_factory.cpp src/tactic/arith/linear_equation.cpp src/ast/display_dimacs.cpp src/ast/has_free_vars.cpp src/ast/for_each_ast.cpp src/ast/ast_lt.cpp src/ast/num_occurs.cpp src/math/subpaving/subpaving_mpf.cpp src/math/subpaving/subpaving_mpfx.cpp src/math/subpaving/subpaving_hwf.cpp src/math/simplex/simplex.cpp src/math/hilbert/hilbert_basis.cpp src/util/lp/lp_utils.cpp src/sat/sat_config.cpp src/sat/sat_scc.cpp src/sat/sat_parallel.cpp src/sat/sat_probing.cpp src/sat/sat_drat.cpp src/sat/sat_mus.cpp src/sat/sat_elim_vars.cpp src/sat/sat_elim_eqs.cpp src/sat/sat_cleaner.cpp src/sat/sat_simplifier.cpp src/sat/sat_model_converter.cpp src/sat/sat_asymm_branch.cpp src/sat/sat_integrity_checker.cpp src/sat/sat_iff3_finder.cpp src/sat/dimacs.cpp src/sat/sat_lookahead.cpp src/sat/sat_big.cpp src/util/inf_s_integer.cpp src/muz/rel/tbv.cpp src/muz/base/bind_variables.cpp src/smt/smt_value_sort.cpp src/smt/arith_eq_solver.cpp src/smt/uses_theory.cpp src/smt/fingerprints.cpp src/smt/smt_almost_cg_table.cpp src/smt/cost_evaluator.cpp src/smt/params/smt_params.cpp src/cmd_context/tactic_manager.cpp src/ackermannization/ackr_helper.cpp src/math/subpaving/tactic/expr2subpaving.cpp src/tactic/arith/bound_propagator.cpp src/parsers/util/simple_parser.cpp src/parsers/util/scanner.cpp ../src/parsers/util/scanner.cpp: In member function ‘scanner::token scanner::scan()’: ../src/parsers/util/scanner.cpp:483:15: warning: case label value is less than minimum value for type case -1: ^ src/parsers/util/cost_parser.cpp src/ast/rewriter/mk_extract_proc.cpp src/ast/rewriter/datatype_rewriter.cpp src/ast/ast_smt_pp.cpp src/ast/func_decl_dependencies.cpp src/ast/ast_util.cpp src/ast/fpa_decl_plugin.cpp src/ast/occurs.cpp src/ast/pp.cpp src/ast/used_vars.cpp src/ast/reg_decl_plugins.cpp src/ast/macro_substitution.cpp src/ast/expr_map.cpp src/ast/csp_decl_plugin.cpp src/ast/ast_ll_pp.cpp src/ast/format.cpp src/ast/expr_stat.cpp src/ast/for_each_expr.cpp src/ast/act_cache.cpp src/math/simplex/model_based_opt.cpp src/sat/sat_solver.cpp src/sat/sat_unit_walk.cpp src/math/polynomial/polynomial_cache.cpp src/shell/main.cpp src/qe/qe_solve_plugin.cpp src/smt/elim_term_ite.cpp src/smt/theory_opt.cpp src/smt/smt_cg_table.cpp src/smt/smt_literal.cpp src/smt/smt_farkas_util.cpp src/smt/proto_model/numeral_factory.cpp src/ast/pattern/pattern_inference.cpp src/cmd_context/check_logic.cpp src/cmd_context/pdecl.cpp src/math/grobner/grobner.cpp src/parsers/util/pattern_validation.cpp src/tactic/equiv_proof_converter.cpp src/tactic/replace_proof_converter.cpp src/model/model_v2_pp.cpp src/model/model_pp.cpp src/model/model_core.cpp src/ast/normal_forms/name_exprs.cpp src/ast/rewriter/enum2bv_rewriter.cpp src/ast/rewriter/bv_trailing.cpp src/ast/rewriter/label_rewriter.cpp src/ast/rewriter/factor_rewriter.cpp src/ast/rewriter/pb_rewriter.cpp src/ast/rewriter/rewriter.cpp src/ast/rewriter/fpa_rewriter.cpp src/ast/rewriter/dl_rewriter.cpp src/ast/rewriter/arith_rewriter.cpp src/ast/rewriter/bool_rewriter.cpp src/ast/rewriter/push_app_ite.cpp src/ast/rewriter/expr_replacer.cpp src/ast/rewriter/factor_equivs.cpp src/ast/rewriter/maximize_ac_sharing.cpp src/ast/rewriter/bv_bounds.cpp src/ast/rewriter/pb2bv_rewriter.cpp src/ast/rewriter/inj_axiom.cpp src/ast/expr_substitution.cpp src/ast/bv_decl_plugin.cpp src/ast/pb_decl_plugin.cpp src/ast/seq_decl_plugin.cpp src/ast/ast_smt2_pp.cpp src/ast/ast_pp_dot.cpp src/ast/expr2var.cpp src/ast/recfun_decl_plugin.cpp src/ast/shared_occs.cpp src/ast/expr_abstract.cpp src/ast/static_features.cpp src/ast/expr_functors.cpp src/ast/array_decl_plugin.cpp src/ast/ast.cpp src/ast/arith_decl_plugin.cpp src/ast/ast_translation.cpp src/ast/datatype_decl_plugin.cpp src/ast/well_sorted.cpp src/ast/expr2polynomial.cpp src/ast/dl_decl_plugin.cpp src/ast/decl_collector.cpp src/util/lp/binary_heap_priority_queue.cpp src/util/lp/lp_settings.cpp src/nlsat/nlsat_types.cpp src/sat/ba_solver.cpp src/sat/sat_local_search.cpp src/math/polynomial/algebraic_numbers.cpp src/math/polynomial/upolynomial.cpp src/math/polynomial/rpolynomial.cpp src/api/dll/gparams_register_modules.cpp src/shell/gparams_register_modules.cpp src/muz/spacer/spacer_mev_array.cpp src/muz/spacer/spacer_antiunify.cpp src/muz/spacer/spacer_sem_matcher.cpp src/muz/rel/doc.cpp src/qe/nlarith_util.cpp src/qe/qe_term_graph.cpp src/qe/qe_dl_plugin.cpp src/qe/qe_array_plugin.cpp src/qe/qe_arith.cpp src/qe/qe_datatypes.cpp src/qe/qe_bool_plugin.cpp src/qe/qe_arith_plugin.cpp src/qe/qe_datatype_plugin.cpp src/qe/qe_bv_plugin.cpp src/smt/expr_context_simplifier.cpp src/smt/smt_clause.cpp src/smt/proto_model/datatype_factory.cpp src/smt/proto_model/proto_model.cpp src/smt/proto_model/array_factory.cpp src/smt/proto_model/struct_factory.cpp src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp src/ast/rewriter/bit_blaster/bit_blaster.cpp src/ast/fpa/fpa2bv_converter.cpp src/ast/fpa/fpa2bv_rewriter.cpp src/ast/fpa/bv2fpa_converter.cpp src/tactic/arith/bv2real_rewriter.cpp src/ast/proofs/proof_checker.cpp src/ast/proofs/proof_utils.cpp src/ast/substitution/matcher.cpp src/ast/substitution/unifier.cpp src/ast/substitution/substitution.cpp src/ast/substitution/substitution_tree.cpp src/model/model.cpp src/model/model_implicant.cpp src/model/model_smt2_pp.cpp src/model/model2expr.cpp src/model/model_evaluator.cpp src/model/func_interp.cpp src/ast/normal_forms/nnf.cpp src/ast/normal_forms/pull_quant.cpp src/ast/normal_forms/defined_names.cpp src/ast/macros/macro_util.cpp src/ast/rewriter/mk_simplified_app.cpp src/ast/rewriter/expr_safe_replace.cpp src/ast/rewriter/elim_bounds.cpp src/ast/rewriter/seq_rewriter.cpp src/ast/rewriter/bv_elim.cpp src/ast/rewriter/der.cpp src/ast/rewriter/var_subst.cpp src/ast/rewriter/th_rewriter.cpp src/ast/rewriter/bv_rewriter.cpp src/ast/rewriter/array_rewriter.cpp src/ast/rewriter/distribute_forall.cpp src/ast/ast_pp_util.cpp src/ast/ast_printer.cpp src/util/lp/dense_matrix.cpp src/util/lp/binary_heap_upair_queue.cpp src/util/lp/indexed_vector.cpp src/nlsat/nlsat_interval_set.cpp src/nlsat/nlsat_clause.cpp src/nlsat/nlsat_evaluator.cpp src/math/polynomial/sexpr2upolynomial.cpp src/math/polynomial/polynomial.cpp src/opt/pb_sls.cpp src/tactic/ufbv/ufbv_rewriter.cpp src/muz/spacer/spacer_sym_mux.cpp src/muz/spacer/spacer_iuc_proof.cpp src/muz/spacer/spacer_mbc.cpp src/muz/spacer/spacer_qe_project.cpp src/muz/spacer/spacer_unsat_core_learner.cpp src/muz/base/dl_boogie_proof.cpp src/qe/qe_arrays.cpp src/qe/qe_mbp.cpp src/tactic/bv/bit_blaster_model_converter.cpp src/smt/cached_var_subst.cpp src/smt/watch_list.cpp src/ackermannization/ackr_model_converter.cpp src/ackermannization/lackr_model_constructor.cpp src/solver/check_sat_result.cpp src/tactic/horn_subsume_model_converter.cpp src/tactic/model_converter.cpp src/tactic/generic_model_converter.cpp src/ast/macros/macro_manager.cpp src/ast/macros/quasi_macros.cpp src/ast/rewriter/quant_hoist.cpp src/ast/rewriter/bit2int.cpp src/ast/rewriter/ast_counter.cpp src/nlsat/nlsat_explain.cpp src/nlsat/nlsat_solver.cpp src/math/polynomial/upolynomial_factorization.cpp src/cmd_context/extra_cmds/polynomial_cmds.cpp src/cmd_context/extra_cmds/subpaving_cmds.cpp src/cmd_context/extra_cmds/dbg_cmds.cpp src/api/api_bv.cpp src/api/api_pb.cpp src/api/api_algebraic.cpp src/api/api_model.cpp src/api/api_stats.cpp src/api/api_qe.cpp src/api/api_rcf.cpp src/api/api_config_params.cpp src/api/api_goal.cpp src/api/api_quant.cpp src/api/api_seq.cpp src/api/api_ast_vector.cpp src/api/api_polynomial.cpp src/api/api_ast.cpp src/api/api_ast_map.cpp src/api/api_array.cpp src/api/api_numeral.cpp src/api/api_context.cpp src/api/api_params.cpp src/tactic/portfolio/solver2lookahead.cpp src/tactic/fpa/fpa2bv_model_converter.cpp src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp src/muz/spacer/spacer_farkas_learner.cpp src/muz/spacer/spacer_proof_utils.cpp src/muz/spacer/spacer_unsat_core_plugin.cpp src/muz/base/hnf.cpp src/qe/qe_cmd.cpp src/qe/qe_mbi.cpp src/tactic/bv/bvarray2uf_rewriter.cpp src/smt/smt2_extra_cmds.cpp src/smt/smt_implied_equalities.cpp src/ast/pattern/expr_pattern_match.cpp src/parsers/smt2/marshal.cpp src/parsers/smt2/smt2parser.cpp src/cmd_context/context_params.cpp src/cmd_context/simplify_cmd.cpp src/cmd_context/eval_cmd.cpp src/cmd_context/cmd_context_to_goal.cpp src/cmd_context/cmd_util.cpp src/cmd_context/cmd_context.cpp src/cmd_context/parametric_cmd.cpp src/cmd_context/basic_cmds.cpp src/ackermannization/ackermannize_bv_model_converter.cpp src/ackermannization/lackr_model_converter_lazy.cpp src/tactic/aig/aig.cpp src/tactic/arith/bv2int_rewriter.cpp src/tactic/arith/bound_manager.cpp src/tactic/arith/probe_arith.cpp src/tactic/arith/pb2bv_model_converter.cpp src/sat/tactic/atom2bool_var.cpp src/solver/solver.cpp src/solver/mus.cpp src/solver/combined_solver.cpp src/tactic/core/collect_occs.cpp src/tactic/dependency_converter.cpp src/tactic/goal_util.cpp src/tactic/goal_num_occurs.cpp src/tactic/goal_shared_occs.cpp src/tactic/probe.cpp src/tactic/goal.cpp src/tactic/proof_converter.cpp src/ast/macros/macro_finder.cpp src/util/lp/matrix.cpp src/util/lp/permutation_matrix.cpp src/api/api_arith.cpp src/api/api_fpa.cpp src/api/api_datatype.cpp src/api/api_parsers.cpp src/api/api_solver.cpp src/opt/opt_pareto.cpp src/tactic/portfolio/default_tactic.cpp src/tactic/fpa/fpa2bv_tactic.cpp src/tactic/fpa/qffplra_tactic.cpp src/tactic/smtlogics/qfnia_tactic.cpp src/tactic/smtlogics/qfauflia_tactic.cpp src/tactic/smtlogics/qfuf_tactic.cpp src/tactic/smtlogics/qfidl_tactic.cpp src/tactic/smtlogics/qflia_tactic.cpp src/tactic/smtlogics/quant_tactics.cpp src/tactic/smtlogics/qflra_tactic.cpp src/tactic/smtlogics/nra_tactic.cpp src/tactic/smtlogics/qfnra_tactic.cpp src/tactic/ufbv/quasi_macros_tactic.cpp src/tactic/ufbv/ufbv_tactic.cpp src/tactic/ufbv/ufbv_rewriter_tactic.cpp src/tactic/ufbv/macro_finder_tactic.cpp src/muz/spacer/spacer_iuc_solver.cpp src/muz/spacer/spacer_manager.cpp src/muz/spacer/spacer_prop_solver.cpp src/muz/spacer/spacer_legacy_mev.cpp src/muz/spacer/spacer_legacy_mbp.cpp src/tactic/fd_solver/enum2bv_solver.cpp src/tactic/fd_solver/bounded_int2bv_solver.cpp src/tactic/fd_solver/fd_solver.cpp src/tactic/fd_solver/pb2bv_solver.cpp src/sat/sat_solver/inc_sat_solver.cpp src/qe/qe_sat_tactic.cpp src/qe/qe_tactic.cpp src/qe/qsat.cpp src/qe/nlqsat.cpp src/qe/qe_lite.cpp src/tactic/sls/sls_tactic.cpp src/tactic/sls/sls_engine.cpp src/smt/tactic/ctx_solver_simplify_tactic.cpp src/smt/tactic/smt_tactic.cpp src/tactic/bv/bvarray2uf_tactic.cpp src/tactic/bv/bv_bounds_tactic.cpp src/tactic/bv/bv1_blaster_tactic.cpp src/tactic/bv/bv_bound_chk_tactic.cpp src/tactic/bv/max_bv_sharing_tactic.cpp src/tactic/bv/bv_size_reduction_tactic.cpp src/tactic/bv/dt2bv_tactic.cpp src/tactic/bv/bit_blaster_tactic.cpp src/tactic/bv/elim_small_bv_tactic.cpp src/smt/asserted_formulas.cpp src/smt/smt_solver.cpp src/parsers/smt2/smt2scanner.cpp src/cmd_context/echo_tactic.cpp src/cmd_context/tactic_cmds.cpp src/ackermannization/lackr.cpp src/ackermannization/ackr_bound_probe.cpp src/tactic/aig/aig_tactic.cpp src/math/subpaving/tactic/subpaving_tactic.cpp src/nlsat/tactic/goal2nlsat.cpp src/nlsat/tactic/qfnra_nlsat_tactic.cpp src/nlsat/tactic/nlsat_tactic.cpp src/tactic/arith/degree_shift_tactic.cpp src/tactic/arith/diff_neq_tactic.cpp src/tactic/arith/lia2pb_tactic.cpp src/tactic/arith/fm_tactic.cpp src/tactic/arith/lia2card_tactic.cpp src/tactic/arith/arith_bounds_tactic.cpp src/tactic/arith/pb2bv_tactic.cpp src/tactic/arith/eq2bv_tactic.cpp src/tactic/arith/nla2bv_tactic.cpp src/tactic/arith/fix_dl_var_tactic.cpp src/tactic/arith/add_bounds_tactic.cpp src/tactic/arith/normalize_bounds_tactic.cpp src/tactic/arith/card2bv_tactic.cpp src/tactic/arith/recover_01_tactic.cpp src/tactic/arith/propagate_ineqs_tactic.cpp src/tactic/arith/purify_arith_tactic.cpp src/tactic/arith/factor_tactic.cpp src/sat/tactic/goal2sat.cpp src/sat/tactic/sat_tactic.cpp src/solver/parallel_tactic.cpp src/solver/solver_na2as.cpp src/solver/solver_pool.cpp src/solver/solver2tactic.cpp src/solver/tactic2solver.cpp src/tactic/core/cofactor_elim_term_ite.cpp src/tactic/core/nnf_tactic.cpp src/tactic/core/reduce_args_tactic.cpp src/tactic/core/occf_tactic.cpp src/tactic/core/der_tactic.cpp src/tactic/core/symmetry_reduce_tactic.cpp src/tactic/core/pb_preprocess_tactic.cpp src/tactic/core/simplify_tactic.cpp src/tactic/core/tseitin_cnf_tactic.cpp src/tactic/core/split_clause_tactic.cpp src/tactic/core/propagate_values_tactic.cpp src/tactic/core/elim_term_ite_tactic.cpp src/tactic/core/dom_simplify_tactic.cpp src/tactic/core/ctx_simplify_tactic.cpp src/tactic/core/distribute_forall_tactic.cpp src/tactic/core/solve_eqs_tactic.cpp src/tactic/core/cofactor_term_ite_tactic.cpp src/tactic/core/blast_term_ite_tactic.cpp src/tactic/core/injectivity_tactic.cpp src/tactic/core/collect_statistics_tactic.cpp src/tactic/core/elim_uncnstr_tactic.cpp src/tactic/core/reduce_invertible_tactic.cpp src/tactic/tactic.cpp src/tactic/tactical.cpp src/tactic/sine_filter.cpp src/util/lp/scaler.cpp src/util/lp/eta_matrix.cpp src/shell/dimacs_frontend.cpp src/api/api_tactic.cpp src/tactic/portfolio/smt_strategic_solver.cpp src/tactic/fpa/qffp_tactic.cpp src/tactic/smtlogics/qfbv_tactic.cpp src/tactic/smtlogics/qfufbv_tactic.cpp src/tactic/smtlogics/qfaufbv_tactic.cpp src/muz/spacer/spacer_util.cpp src/muz/spacer/spacer_json.cpp src/qe/qe.cpp src/tactic/sls/bvsls_opt_engine.cpp src/smt/tactic/unit_subsumption_tactic.cpp src/smt/smt_model_generator.cpp src/smt/theory_fpa.cpp src/smt/theory_array_base.cpp src/smt/smt_checker.cpp src/smt/smt_model_finder.cpp src/smt/smt_theory.cpp src/smt/theory_datatype.cpp src/smt/smt_context_stat.cpp src/smt/qi_queue.cpp src/smt/smt_enode.cpp src/smt/dyn_ack.cpp src/smt/theory_array_full.cpp src/smt/smt_case_split_queue.cpp src/smt/smt_quick_checker.cpp src/smt/arith_eq_adapter.cpp src/smt/smt_conflict_resolution.cpp src/smt/theory_recfun.cpp src/smt/theory_wmaxsat.cpp src/smt/smt_relevancy.cpp src/smt/theory_bv.cpp src/smt/smt_for_each_relevant_expr.cpp src/smt/theory_jobscheduler.cpp src/smt/smt_kernel.cpp src/smt/theory_array.cpp src/smt/smt_justification.cpp src/smt/theory_dummy.cpp src/smt/theory_pb.cpp src/smt/smt_internalizer.cpp src/smt/smt_arith_value.cpp src/smt/smt_consequences.cpp src/smt/smt_context.cpp src/smt/theory_dl.cpp src/smt/smt_model_checker.cpp src/smt/mam.cpp src/smt/smt_context_pp.cpp src/smt/smt_context_inv.cpp src/smt/smt_quantifier.cpp src/ackermannization/ackermannize_bv_tactic.cpp src/api/dll/install_tactic.cpp src/shell/install_tactic.cpp src/muz/spacer/spacer_generalizers.cpp src/muz/dataflow/dataflow.cpp src/smt/theory_utvpi.cpp src/smt/theory_seq.cpp src/smt/theory_diff_logic.cpp src/util/lp/row_eta_matrix.cpp src/util/lp/square_sparse_matrix.cpp src/util/lp/square_dense_submatrix.cpp src/opt/opt_context.cpp src/opt/optsmt.cpp src/opt/wmax.cpp src/opt/opt_cmds.cpp src/opt/maxsmt.cpp src/opt/sortmax.cpp src/opt/opt_parse.cpp src/opt/maxlex.cpp src/opt/opt_solver.cpp src/opt/maxres.cpp src/muz/fp/datalog_parser.cpp src/muz/ddnf/ddnf.cpp src/muz/clp/clp_context.cpp src/muz/spacer/spacer_quant_generalizer.cpp src/muz/spacer/spacer_sat_answer.cpp src/muz/spacer/spacer_callback.cpp src/muz/spacer/spacer_pdr.cpp src/muz/transforms/dl_mk_array_instantiation.cpp src/muz/transforms/dl_mk_bit_blast.cpp src/muz/transforms/dl_mk_scale.cpp src/muz/transforms/dl_mk_coi_filter.cpp src/muz/transforms/dl_mk_magic_symbolic.cpp src/muz/transforms/dl_mk_quantifier_abstraction.cpp src/muz/transforms/dl_mk_filter_rules.cpp src/muz/transforms/dl_mk_magic_sets.cpp src/muz/transforms/dl_mk_quantifier_instantiation.cpp src/muz/transforms/dl_mk_separate_negated_tails.cpp src/muz/transforms/dl_mk_karr_invariants.cpp src/muz/transforms/dl_mk_backwards.cpp src/muz/transforms/dl_mk_unbound_compressor.cpp src/muz/transforms/dl_mk_array_eq_rewrite.cpp src/muz/transforms/dl_mk_loop_counter.cpp src/muz/base/dl_rule_set.cpp src/muz/base/dl_rule_subsumption_index.cpp src/muz/base/dl_rule_transformer.cpp src/muz/base/dl_util.cpp src/muz/base/dl_rule.cpp src/muz/base/dl_costs.cpp src/muz/base/dl_context.cpp src/muz/base/rule_properties.cpp src/smt/theory_arith.cpp src/smt/theory_dense_diff_logic.cpp src/smt/smt_setup.cpp src/smt/theory_str.cpp src/util/lp/lu.cpp src/shell/opt_frontend.cpp src/shell/smtlib_frontend.cpp src/api/api_opt.cpp src/muz/fp/horn_tactic.cpp src/muz/tab/tab_context.cpp src/muz/spacer/spacer_legacy_frames.cpp src/muz/spacer/spacer_context.cpp src/muz/rel/dl_external_relation.cpp src/muz/transforms/dl_mk_slice.cpp src/muz/transforms/dl_mk_subsumption_checker.cpp src/muz/transforms/dl_mk_array_blast.cpp src/muz/transforms/dl_mk_coalesce.cpp src/muz/transforms/dl_mk_unfold.cpp src/muz/transforms/dl_transforms.cpp src/muz/transforms/dl_mk_elim_term_ite.cpp src/muz/transforms/dl_mk_rule_inliner.cpp src/muz/transforms/dl_mk_interp_tail_simplifier.cpp src/util/lp/lp_core_solver_base.cpp src/util/lp/core_solver_pretty_printer.cpp src/api/api_datalog.cpp src/muz/fp/dl_register_engine.cpp src/muz/bmc/dl_bmc_engine.cpp src/muz/spacer/spacer_dl_interface.cpp src/muz/rel/dl_mk_simple_joins.cpp src/muz/rel/dl_table.cpp src/muz/rel/dl_instruction.cpp src/muz/rel/dl_sparse_table.cpp src/muz/rel/dl_sieve_relation.cpp src/muz/rel/dl_product_relation.cpp src/muz/rel/dl_mk_similarity_compressor.cpp src/muz/rel/check_relation.cpp src/muz/rel/karr_relation.cpp src/muz/rel/dl_base.cpp src/muz/rel/dl_lazy_table.cpp src/muz/rel/udoc_relation.cpp src/muz/rel/dl_table_relation.cpp src/muz/transforms/dl_mk_synchronize.cpp src/util/lp/lp_solver.cpp src/util/lp/lp_dual_core_solver.cpp src/muz/fp/dl_cmds.cpp src/muz/rel/dl_compiler.cpp src/muz/rel/dl_check_table.cpp src/muz/rel/aig_exporter.cpp src/muz/rel/dl_mk_explanations.cpp src/muz/rel/dl_interval_relation.cpp src/muz/rel/dl_finite_product_relation.cpp src/muz/rel/dl_relation_manager.cpp src/smt/theory_lra.cpp src/util/lp/lp_bound_propagator.cpp src/util/lp/lar_core_solver.cpp src/util/lp/static_matrix.cpp src/util/lp/gomory.cpp src/util/lp/nra_solver.cpp src/util/lp/lp_primal_core_solver.cpp src/util/lp/lp_dual_simplex.cpp src/util/lp/int_solver.cpp src/util/lp/lar_solver.cpp src/shell/datalog_frontend.cpp src/muz/rel/dl_bound_relation.cpp src/muz/rel/rel_context.cpp src/util/lp/lp_primal_simplex.cpp src/util/lp/random_updater.cpp src/shell/lp_frontend.cpp g++ -o libz3.so -shared api/dll/dll.o api/dll/gparams_register_modules.o api/dll/install_tactic.o api/dll/mem_initializer.o api/api_arith.o api/api_fpa.o api/api_datatype.o api/api_tactic.o api/api_log_macros.o api/api_bv.o api/api_pb.o api/api_commands.o api/api_algebraic.o api/api_parsers.o api/api_model.o api/api_stats.o api/api_qe.o api/api_rcf.o api/api_config_params.o api/api_goal.o api/api_quant.o api/api_seq.o api/z3_replayer.o api/api_ast_vector.o api/api_polynomial.o api/api_solver.o api/api_ast.o api/api_ast_map.o api/api_datalog.o api/api_array.o api/api_numeral.o api/api_context.o api/api_log.o api/api_opt.o api/api_params.o cmd_context/extra_cmds/extra_cmds.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a tactic/ufbv/ufbv_tactic.a muz/fp/fp.a muz/bmc/bmc.a muz/ddnf/ddnf.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a tactic/fd_solver/fd_solver.a sat/sat_solver/sat_solver.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a smt/smt.a smt/proto_model/proto_model.a smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/pattern/pattern.a ast/fpa/fpa.a parsers/smt2/smt2parser.a cmd_context/cmd_context.a ackermannization/ackermannization.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a sat/tactic/sat_tactic.a solver/solver.a ast/proofs/proofs.a tactic/core/core_tactics.a math/euclid/euclid.a math/grobner/grobner.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/macros/macros.a ast/rewriter/rewriter.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a math/automata/automata.a math/simplex/simplex.a math/hilbert/hilbert.a util/lp/lp.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a -fopenmp -lrt -Wl,-soname,libz3.so g++ -o z3 shell/z3_log_frontend.o shell/dimacs_frontend.o shell/gparams_register_modules.o shell/datalog_frontend.o shell/opt_frontend.o shell/main.o shell/lp_frontend.o shell/install_tactic.o shell/mem_initializer.o shell/smtlib_frontend.o cmd_context/extra_cmds/extra_cmds.a api/api.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a tactic/ufbv/ufbv_tactic.a muz/fp/fp.a muz/bmc/bmc.a muz/ddnf/ddnf.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a tactic/fd_solver/fd_solver.a sat/sat_solver/sat_solver.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a smt/smt.a smt/proto_model/proto_model.a smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/pattern/pattern.a ast/fpa/fpa.a parsers/smt2/smt2parser.a cmd_context/cmd_context.a ackermannization/ackermannization.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a sat/tactic/sat_tactic.a solver/solver.a ast/proofs/proofs.a tactic/core/core_tactics.a math/euclid/euclid.a math/grobner/grobner.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/macros/macros.a ast/rewriter/rewriter.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a math/automata/automata.a math/simplex/simplex.a math/hilbert/hilbert.a util/lp/lp.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a -lpthread -fopenmp -lrt ln -f -s ../libz3.so python Z3 was successfully built. Z3Py scripts can already be executed in the 'build/python' directory. Z3Py scripts stored in arbitrary directories can be executed if the 'build/python' directory is added to the PYTHONPATH environment variable and the 'build' directory is added to the LD_LIBRARY_PATH environment variable. Use the following command to install Z3 at prefix /usr. sudo make install Copying binaries running build_py creating build creating build/lib creating build/lib/z3 copying z3/z3rcf.py -> build/lib/z3 copying z3/__init__.py -> build/lib/z3 copying z3/z3.py -> build/lib/z3 copying z3/z3num.py -> build/lib/z3 copying z3/z3core.py -> build/lib/z3 copying z3/z3util.py -> build/lib/z3 copying z3/z3consts.py -> build/lib/z3 copying z3/z3printer.py -> build/lib/z3 copying z3/z3types.py -> build/lib/z3 copying z3/z3poly.py -> build/lib/z3 running egg_info creating z3_solver_mythril.egg-info writing dependency_links to z3_solver_mythril.egg-info/dependency_links.txt writing z3_solver_mythril.egg-info/PKG-INFO writing top-level names to z3_solver_mythril.egg-info/top_level.txt writing manifest file 'z3_solver_mythril.egg-info/SOURCES.txt' reading manifest file 'z3_solver_mythril.egg-info/SOURCES.txt' writing manifest file 'z3_solver_mythril.egg-info/SOURCES.txt' creating build/lib/z3/lib copying z3/lib/libz3.so -> build/lib/z3/lib creating build/lib/z3/include copying z3/include/z3_polynomial.h -> build/lib/z3/include copying z3/include/z3_v1.h -> build/lib/z3/include copying z3/include/z3_macros.h -> build/lib/z3/include copying z3/include/api_log_macros.h -> build/lib/z3/include copying z3/include/z3_rcf.h -> build/lib/z3/include copying z3/include/z3.h -> build/lib/z3/include copying z3/include/z3_logger.h -> build/lib/z3/include copying z3/include/api_goal.h -> build/lib/z3/include copying z3/include/z3_api.h -> build/lib/z3/include copying z3/include/z3_private.h -> build/lib/z3/include copying z3/include/api_util.h -> build/lib/z3/include copying z3/include/api_ast_map.h -> build/lib/z3/include copying z3/include/z3_spacer.h -> build/lib/z3/include copying z3/include/api_stats.h -> build/lib/z3/include copying z3/include/api_context.h -> build/lib/z3/include copying z3/include/z3_replayer.h -> build/lib/z3/include copying z3/include/api_solver.h -> build/lib/z3/include copying z3/include/api_model.h -> build/lib/z3/include copying z3/include/api_tactic.h -> build/lib/z3/include copying z3/include/z3_fixedpoint.h -> build/lib/z3/include copying z3/include/api_datalog.h -> build/lib/z3/include copying z3/include/z3_algebraic.h -> build/lib/z3/include copying z3/include/z3_optimization.h -> build/lib/z3/include copying z3/include/z3_ast_containers.h -> build/lib/z3/include copying z3/include/z3_fpa.h -> build/lib/z3/include copying z3/include/api_polynomial.h -> build/lib/z3/include copying z3/include/api_ast_vector.h -> build/lib/z3/include creating build/lib/z3/include/c++ copying z3/include/c++/z3++.h -> build/lib/z3/include/c++ installing to build/bdist.linux-armv7l/wheel running install running install_lib creating build/bdist.linux-armv7l creating build/bdist.linux-armv7l/wheel creating build/bdist.linux-armv7l/wheel/z3 creating build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3_polynomial.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3_v1.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3_macros.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/api_log_macros.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3_rcf.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3_logger.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/api_goal.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3_api.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3_private.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/api_util.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/api_ast_map.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3_spacer.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/api_stats.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/api_context.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3_replayer.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/api_solver.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/api_model.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/api_tactic.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3_fixedpoint.h -> build/bdist.linux-armv7l/wheel/z3/include creating build/bdist.linux-armv7l/wheel/z3/include/c++ copying build/lib/z3/include/c++/z3++.h -> build/bdist.linux-armv7l/wheel/z3/include/c++ copying build/lib/z3/include/api_datalog.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3_algebraic.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3_optimization.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3_ast_containers.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/z3_fpa.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/api_polynomial.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/include/api_ast_vector.h -> build/bdist.linux-armv7l/wheel/z3/include copying build/lib/z3/z3rcf.py -> build/bdist.linux-armv7l/wheel/z3 copying build/lib/z3/__init__.py -> build/bdist.linux-armv7l/wheel/z3 copying build/lib/z3/z3.py -> build/bdist.linux-armv7l/wheel/z3 copying build/lib/z3/z3num.py -> build/bdist.linux-armv7l/wheel/z3 creating build/bdist.linux-armv7l/wheel/z3/lib copying build/lib/z3/lib/libz3.so -> build/bdist.linux-armv7l/wheel/z3/lib copying build/lib/z3/z3core.py -> build/bdist.linux-armv7l/wheel/z3 copying build/lib/z3/z3util.py -> build/bdist.linux-armv7l/wheel/z3 copying build/lib/z3/z3consts.py -> build/bdist.linux-armv7l/wheel/z3 copying build/lib/z3/z3printer.py -> build/bdist.linux-armv7l/wheel/z3 copying build/lib/z3/z3types.py -> build/bdist.linux-armv7l/wheel/z3 copying build/lib/z3/z3poly.py -> build/bdist.linux-armv7l/wheel/z3 running install_data creating build/bdist.linux-armv7l/wheel/z3_solver_mythril-4.8.4.1.data creating build/bdist.linux-armv7l/wheel/z3_solver_mythril-4.8.4.1.data/data creating build/bdist.linux-armv7l/wheel/z3_solver_mythril-4.8.4.1.data/data/bin copying bin/z3 -> build/bdist.linux-armv7l/wheel/z3_solver_mythril-4.8.4.1.data/data/bin running install_egg_info Copying z3_solver_mythril.egg-info to build/bdist.linux-armv7l/wheel/z3_solver_mythril-4.8.4.1-py3.4.egg-info running install_scripts creating build/bdist.linux-armv7l/wheel/z3_solver_mythril-4.8.4.1.dist-info/WHEEL creating '/tmp/pip-wheel-_y0kg7vx/z3_solver_mythril-4.8.4.1-py3-none-manylinux1_armv7l.whl' and adding 'build/bdist.linux-armv7l/wheel' to it adding 'z3/__init__.py' adding 'z3/z3.py' adding 'z3/z3consts.py' adding 'z3/z3core.py' adding 'z3/z3num.py' adding 'z3/z3poly.py' adding 'z3/z3printer.py' adding 'z3/z3rcf.py' adding 'z3/z3types.py' adding 'z3/z3util.py' adding 'z3/include/api_ast_map.h' adding 'z3/include/api_ast_vector.h' adding 'z3/include/api_context.h' adding 'z3/include/api_datalog.h' adding 'z3/include/api_goal.h' adding 'z3/include/api_log_macros.h' adding 'z3/include/api_model.h' adding 'z3/include/api_polynomial.h' adding 'z3/include/api_solver.h' adding 'z3/include/api_stats.h' adding 'z3/include/api_tactic.h' adding 'z3/include/api_util.h' adding 'z3/include/z3.h' adding 'z3/include/z3_algebraic.h' adding 'z3/include/z3_api.h' adding 'z3/include/z3_ast_containers.h' adding 'z3/include/z3_fixedpoint.h' adding 'z3/include/z3_fpa.h' adding 'z3/include/z3_logger.h' adding 'z3/include/z3_macros.h' adding 'z3/include/z3_optimization.h' adding 'z3/include/z3_polynomial.h' adding 'z3/include/z3_private.h' adding 'z3/include/z3_rcf.h' adding 'z3/include/z3_replayer.h' adding 'z3/include/z3_spacer.h' adding 'z3/include/z3_v1.h' adding 'z3/include/c++/z3++.h' adding 'z3/lib/libz3.so' adding 'z3_solver_mythril-4.8.4.1.data/data/bin/z3' adding 'z3_solver_mythril-4.8.4.1.dist-info/METADATA' adding 'z3_solver_mythril-4.8.4.1.dist-info/WHEEL' adding 'z3_solver_mythril-4.8.4.1.dist-info/top_level.txt' adding 'z3_solver_mythril-4.8.4.1.dist-info/RECORD' removing build/bdist.linux-armv7l/wheel Running setup.py bdist_wheel for z3-solver-mythril: finished with status 'done' Stored in directory: /tmp/tmpgvb4rlv1 Successfully built z3-solver-mythril Cleaning up... Removing source in /tmp/pip-wheel-cy5479rh/z3-solver-mythril Removed build tracker '/tmp/pip-req-tracker-c0ln70ql'