Cook: z3 4.7.1 ================================================================================ QA: checking package receipt... Checking build dependencies... Extracting source archive "z3-4.7.1.tar.gz" Executing: compile_rules CFLAGS : -march=i486 -Os -pipe -mindirect-branch=thunk CXXLAGS : -march=i486 -Os -pipe -mindirect-branch=thunk CPPFLAGS : -D_GLIBCXX_USE_C99_MATH=1 LDFLAGS : -Wl,-Os,--as-needed New component: 'util' New component: 'lp' 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: '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: 'sat_tactic' New component: 'arith_tactics' New component: 'nlsat_tactic' New component: 'subpaving_tactic' New component: 'aig_tactic' New component: 'proofs' New component: 'solver' New component: 'ackermannization' New component: 'interp' New component: 'cmd_context' New component: 'extra_cmds' 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: 'duality' New component: 'muz' New component: 'dataflow' New component: 'transforms' New component: 'rel' New component: 'pdr' New component: 'spacer' 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: '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' 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/sat/sat_scc_params.hpp' Generated 'src/sat/sat_simplifier_params.hpp' Generated 'src/sat/sat_asymm_branch_params.hpp' Generated 'src/sat/sat_params.hpp' Generated 'src/math/polynomial/algebraic_params.hpp' Generated 'src/math/realclosure/rcf_params.hpp' Generated 'src/tactic/smtlogics/qfufbv_tactic_params.hpp' Generated 'src/tactic/sls/sls_params.hpp' Generated 'src/ackermannization/ackermannize_bv_tactic_params.hpp' Generated 'src/ackermannization/ackermannization_params.hpp' Generated 'src/parsers/util/parser_params.hpp' Generated 'src/muz/base/fixedpoint_params.hpp' Generated 'src/ast/pp_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/bv_rewriter_params.hpp' Generated 'src/ast/rewriter/poly_rewriter_params.hpp' Generated 'src/ast/rewriter/bool_rewriter_params.hpp' Generated 'src/ast/rewriter/fpa_rewriter_params.hpp' Generated 'src/ast/rewriter/rewriter_params.hpp' Generated 'src/ast/fpa/fpa2bv_rewriter_params.hpp' Generated 'src/ast/normal_forms/nnf_params.hpp' Generated 'src/smt/params/smt_params_helper.hpp' Generated 'src/solver/combined_solver_params.hpp' Generated 'src/util/lp/lp_params.hpp' Generated 'src/model/model_params.hpp' Generated 'src/model/model_evaluator_params.hpp' Generated 'src/interp/interp_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/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/__init__.py ... Compiling src/api/python/z3/z3.py ... Compiling src/api/python/z3/z3consts.py ... Compiling src/api/python/z3/z3core.py ... Compiling src/api/python/z3/z3num.py ... Compiling src/api/python/z3/z3poly.py ... Compiling src/api/python/z3/z3printer.py ... Compiling src/api/python/z3/z3rcf.py ... Compiling src/api/python/z3/z3types.py ... Compiling src/api/python/z3/z3util.py ... Generated python bytecode Copied 'z3consts.py' Copied 'z3poly.py' Copied 'z3.py' Copied 'z3util.py' Copied 'z3types.py' Copied 'z3printer.py' Copied '__init__.py' Copied 'z3rcf.py' Copied 'z3core.py' Copied 'z3num.py' Copied 'z3poly.pyc' Copied 'z3consts.pyc' Copied 'z3util.pyc' Copied 'z3.pyc' Copied 'z3rcf.pyc' Copied 'z3num.pyc' Copied 'z3types.pyc' Copied '__init__.pyc' Copied 'z3core.pyc' Copied 'z3printer.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: SSE2-GCC Python pkg dir: /usr/lib/python2.7/site-packages Python version: 2.7 Writing build/Makefile Copied Z3Py example 'parallel.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' Copied Z3Py example 'all_interval_series.py' to 'build/python' Makefile was successfully generated. compilation mode: Release Type 'cd build; make' to build Z3 src/smt/smt_statistics.cpp src/interp/iz3profiling.cpp src/util/luby.cpp src/util/approx_nat.cpp src/util/common_msgs.cpp src/api/dll/dll.cpp src/util/memory_manager.cpp src/util/cooperate.cpp src/util/timeit.cpp src/util/z3_exception.cpp src/util/page.cpp src/util/approx_set.cpp src/api/api_commands.cpp src/api/api_log.cpp src/util/mpn.cpp src/util/timeout.cpp src/util/util.cpp src/util/timer.cpp src/util/scoped_timer.cpp src/util/stack.cpp src/util/scoped_ctrl_c.cpp src/util/bit_util.cpp src/shell/z3_log_frontend.cpp src/util/debug.cpp src/util/trace.cpp src/util/lbool.cpp src/util/hash.cpp src/util/fixed_bit_vector.cpp src/api/z3_replayer.cpp src/solver/smt_logics.cpp src/math/automata/automaton.cpp src/util/symbol.cpp src/util/bit_vector.cpp src/util/smt2_util.cpp src/util/permutation.cpp src/util/warning.cpp src/util/prime_generator.cpp src/util/region.cpp src/util/min_cut.cpp src/util/small_object_allocator.cpp src/api/api_log_macros.cpp src/interp/iz3scopes.cpp src/sat/sat_par.cpp src/util/rlimit.cpp src/util/mpz.cpp src/util/cmd_context_types.cpp src/util/statistics.cpp src/smt/params/theory_array_params.cpp src/smt/params/qi_params.cpp src/smt/params/dyn_ack_params.cpp src/smt/params/theory_arith_params.cpp src/smt/params/theory_pb_params.cpp src/smt/params/theory_bv_params.cpp src/smt/params/theory_str_params.cpp src/ast/pattern/pattern_inference_params.cpp src/math/euclid/euclidean_solver.cpp src/math/realclosure/mpz_matrix.cpp src/math/interval/interval_mpq.cpp src/sat/sat_clause_set.cpp src/sat/sat_clause.cpp src/sat/sat_clause_use_list.cpp src/sat/sat_watched.cpp src/sat/sat_model_converter.cpp src/util/hwf.cpp src/util/gparams.cpp src/util/mpff.cpp src/util/mpf.cpp src/util/mpfx.cpp src/util/mpq.cpp src/util/env_params.cpp src/util/mpq_inf.cpp src/shell/mem_initializer.cpp src/smt/old_interval.cpp src/smt/params/preprocessor_params.cpp src/math/realclosure/realclosure.cpp src/sat/sat_config.cpp src/util/sexpr.cpp src/util/inf_rational.cpp src/util/mpbq.cpp src/util/rational.cpp src/util/params.cpp src/util/inf_int_rational.cpp src/util/s_integer.cpp src/api/dll/mem_initializer.cpp src/muz/spacer/spacer_matrix.cpp src/muz/rel/tbv.cpp src/smt/smt_quantifier_stat.cpp src/smt/proto_model/value_factory.cpp src/tactic/arith/linear_equation.cpp src/ast/for_each_ast.cpp src/ast/pb_decl_plugin.cpp src/ast/ast_lt.cpp src/ast/num_occurs.cpp src/ast/ast_util.cpp src/ast/has_free_vars.cpp src/math/subpaving/subpaving.cpp src/math/subpaving/subpaving_hwf.cpp src/math/subpaving/subpaving_mpfx.cpp src/math/subpaving/subpaving_mpq.cpp src/math/subpaving/subpaving_mpf.cpp src/math/subpaving/subpaving_mpff.cpp src/math/simplex/simplex.cpp src/math/hilbert/hilbert_basis.cpp src/sat/sat_asymm_branch.cpp src/sat/sat_elim_eqs.cpp src/sat/sat_probing.cpp src/sat/sat_iff3_finder.cpp src/sat/sat_cleaner.cpp src/sat/dimacs.cpp src/sat/sat_integrity_checker.cpp src/sat/sat_mus.cpp src/sat/sat_scc.cpp src/sat/sat_simplifier.cpp src/sat/sat_solver.cpp src/util/lp/lp_utils.cpp src/util/inf_s_integer.cpp src/shell/dimacs_frontend.cpp src/muz/base/bind_variables.cpp src/smt/fingerprints.cpp src/smt/smt_value_sort.cpp src/smt/smt_almost_cg_table.cpp src/smt/cost_evaluator.cpp src/smt/arith_eq_solver.cpp src/smt/uses_theory.cpp src/smt/params/smt_params.cpp src/cmd_context/pdecl.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/scanner.cpp src/parsers/util/simple_parser.cpp src/parsers/util/cost_parser.cpp src/ast/rewriter/datatype_rewriter.cpp src/ast/rewriter/mk_extract_proc.cpp src/ast/rewriter/dl_rewriter.cpp src/ast/format.cpp src/ast/used_vars.cpp src/ast/for_each_expr.cpp src/ast/expr_map.cpp src/ast/occurs.cpp src/ast/ast_ll_pp.cpp src/ast/expr_stat.cpp src/ast/func_decl_dependencies.cpp src/ast/ast_translation.cpp src/ast/macro_substitution.cpp src/ast/reg_decl_plugins.cpp src/ast/pp.cpp src/ast/factor_equivs.cpp src/ast/fpa_decl_plugin.cpp src/ast/ast_smt_pp.cpp src/ast/act_cache.cpp src/math/simplex/model_based_opt.cpp src/nlsat/nlsat_types.cpp src/math/polynomial/polynomial_cache.cpp src/api/dll/gparams_register_modules.cpp src/shell/gparams_register_modules.cpp src/shell/main.cpp src/smt/theory_opt.cpp src/smt/elim_term_ite.cpp src/ast/normal_forms/name_exprs.cpp src/ast/rewriter/bv_trailing.cpp src/ast/rewriter/bv_bounds.cpp src/ast/rewriter/label_rewriter.cpp src/ast/rewriter/bool_rewriter.cpp src/ast/rewriter/fpa_rewriter.cpp src/ast/rewriter/rewriter.cpp src/ast/rewriter/expr_replacer.cpp src/ast/expr_functors.cpp src/ast/ast_printer.cpp src/ast/expr2var.cpp src/ast/arith_decl_plugin.cpp src/ast/shared_occs.cpp src/ast/datatype_decl_plugin.cpp src/ast/ast_pp_util.cpp src/ast/expr2polynomial.cpp src/nlsat/nlsat_interval_set.cpp src/nlsat/nlsat_clause.cpp src/nlsat/nlsat_evaluator.cpp src/math/polynomial/rpolynomial.cpp src/math/polynomial/upolynomial.cpp src/math/polynomial/polynomial.cpp src/util/lp/lp_settings_instances.cpp src/util/lp/binary_heap_priority_queue_instances.cpp src/muz/spacer/spacer_antiunify.cpp src/smt/smt_farkas_util.cpp src/smt/smt_cg_table.cpp src/smt/smt_clause.cpp src/smt/smt_literal.cpp src/smt/proto_model/numeral_factory.cpp src/ast/pattern/pattern_inference.cpp src/ast/fpa/fpa2bv_converter.cpp src/cmd_context/check_logic.cpp src/interp/iz3mgr.cpp src/ast/proofs/proof_utils.cpp src/ast/proofs/proof_checker.cpp src/tactic/aig/aig.cpp src/tactic/arith/bound_manager.cpp src/tactic/arith/bv2int_rewriter.cpp src/tactic/arith/bv2real_rewriter.cpp src/sat/tactic/atom2bool_var.cpp src/tactic/core/collect_occs.cpp src/math/grobner/grobner.cpp src/parsers/util/pattern_validation.cpp src/tactic/goal.cpp src/tactic/goal_num_occurs.cpp src/tactic/goal_shared_occs.cpp src/tactic/proof_converter.cpp src/tactic/goal_util.cpp src/model/model_v2_pp.cpp src/model/func_interp.cpp src/model/model_pp.cpp src/model/model_smt2_pp.cpp src/model/model_core.cpp src/ast/normal_forms/pull_quant.cpp src/ast/normal_forms/defined_names.cpp src/ast/normal_forms/nnf.cpp src/ast/macros/macro_util.cpp src/ast/rewriter/mk_simplified_app.cpp src/ast/rewriter/maximize_ac_sharing.cpp src/ast/rewriter/inj_axiom.cpp src/ast/rewriter/push_app_ite.cpp src/ast/rewriter/arith_rewriter.cpp src/ast/rewriter/array_rewriter.cpp src/ast/rewriter/distribute_forall.cpp src/ast/rewriter/pb_rewriter.cpp src/ast/rewriter/bv_rewriter.cpp src/ast/rewriter/elim_bounds.cpp src/ast/rewriter/enum2bv_rewriter.cpp src/ast/rewriter/seq_rewriter.cpp src/ast/rewriter/var_subst.cpp src/ast/rewriter/bv_elim.cpp src/ast/rewriter/der.cpp src/ast/rewriter/factor_rewriter.cpp src/ast/rewriter/th_rewriter.cpp src/ast/rewriter/expr_safe_replace.cpp src/ast/rewriter/pb2bv_rewriter.cpp src/ast/expr_substitution.cpp src/ast/bv_decl_plugin.cpp src/ast/array_decl_plugin.cpp src/ast/dl_decl_plugin.cpp src/ast/seq_decl_plugin.cpp src/ast/ast_smt2_pp.cpp src/ast/well_sorted.cpp src/ast/ast_pp_dot.cpp src/ast/decl_collector.cpp src/ast/expr_abstract.cpp src/ast/static_features.cpp src/ast/ast.cpp src/math/polynomial/sexpr2upolynomial.cpp src/math/polynomial/algebraic_numbers.cpp src/util/lp/indexed_vector_instances.cpp src/util/lp/dense_matrix_instances.cpp src/util/lp/binary_heap_upair_queue_instances.cpp src/muz/spacer/spacer_mev_array.cpp src/muz/spacer/spacer_unsat_core_learner.cpp src/muz/spacer/spacer_sym_mux.cpp src/muz/pdr/pdr_sym_mux.cpp src/muz/rel/doc.cpp src/muz/base/dl_boogie_proof.cpp src/qe/qe_dl_plugin.cpp src/qe/qe_bool_plugin.cpp src/qe/nlarith_util.cpp src/qe/qe_datatype_plugin.cpp src/qe/qe_bv_plugin.cpp src/qe/qe_array_plugin.cpp src/qe/qe_arith_plugin.cpp src/smt/cached_var_subst.cpp src/smt/watch_list.cpp src/smt/expr_context_simplifier.cpp src/smt/proto_model/array_factory.cpp src/smt/proto_model/proto_model.cpp src/smt/proto_model/struct_factory.cpp src/smt/proto_model/datatype_factory.cpp src/ast/rewriter/bit_blaster/bit_blaster.cpp src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp src/ast/fpa/fpa2bv_rewriter.cpp src/ast/fpa/bv2fpa_converter.cpp src/interp/iz3pp.cpp src/solver/check_sat_result.cpp src/tactic/arith/probe_arith.cpp src/ast/substitution/substitution_tree.cpp src/ast/substitution/unifier.cpp src/ast/substitution/substitution.cpp src/ast/substitution/matcher.cpp src/tactic/equiv_proof_converter.cpp src/tactic/probe.cpp src/tactic/replace_proof_converter.cpp src/model/model_evaluator.cpp src/model/model2expr.cpp src/model/model.cpp src/model/model_implicant.cpp src/ast/macros/quasi_macros.cpp src/ast/macros/macro_manager.cpp src/ast/rewriter/quant_hoist.cpp src/ast/rewriter/ast_counter.cpp src/ast/rewriter/bit2int.cpp src/nlsat/nlsat_solver.cpp src/nlsat/nlsat_explain.cpp src/math/polynomial/upolynomial_factorization.cpp src/opt/pb_sls.cpp src/opt/opt_pareto.cpp src/tactic/ufbv/ufbv_rewriter.cpp src/muz/spacer/spacer_qe_project.cpp src/muz/spacer/spacer_virtual_solver.cpp src/muz/spacer/spacer_unsat_core_plugin.cpp src/duality/duality_wrapper.cpp src/duality/duality_profiling.cpp src/qe/qe_arrays.cpp src/qe/qe_arith.cpp src/qe/qe_datatypes.cpp src/qe/qe_mbp.cpp src/tactic/bv/bit_blaster_model_converter.cpp src/smt/smt_solver.cpp src/smt/smt_implied_equalities.cpp src/cmd_context/context_params.cpp src/interp/iz3proof.cpp src/interp/iz3checker.cpp src/interp/iz3base.cpp src/interp/iz3proof_itp.cpp src/ackermannization/lackr_model_constructor.cpp src/ackermannization/ackr_bound_probe.cpp src/ackermannization/ackr_model_converter.cpp src/solver/combined_solver.cpp src/solver/solver_na2as.cpp src/solver/solver.cpp src/solver/mus.cpp src/tactic/extension_model_converter.cpp src/tactic/model_converter.cpp src/tactic/filter_model_converter.cpp src/ast/macros/macro_finder.cpp src/util/lp/matrix_instances.cpp src/util/lp/permutation_matrix_instances.cpp src/api/api_quant.cpp src/api/api_model.cpp src/api/api_ast_map.cpp src/api/api_fpa.cpp src/api/api_tactic.cpp src/api/api_array.cpp src/api/api_context.cpp src/api/api_polynomial.cpp src/api/api_params.cpp src/api/api_datatype.cpp src/api/api_rcf.cpp src/api/api_config_params.cpp src/api/api_ast.cpp src/api/api_qe.cpp src/api/api_pb.cpp src/api/api_solver.cpp src/api/api_parsers.cpp src/api/api_numeral.cpp src/api/api_bv.cpp src/api/api_ast_vector.cpp src/api/api_arith.cpp src/api/api_stats.cpp src/api/api_algebraic.cpp src/api/api_seq.cpp src/tactic/portfolio/default_tactic.cpp src/tactic/portfolio/bounded_int2bv_solver.cpp src/tactic/portfolio/enum2bv_solver.cpp src/tactic/portfolio/pb2bv_solver.cpp src/tactic/portfolio/fd_solver.cpp src/tactic/fpa/fpa2bv_tactic.cpp src/tactic/fpa/qffplra_tactic.cpp src/tactic/fpa/fpa2bv_model_converter.cpp src/tactic/smtlogics/qfufnra_tactic.cpp src/tactic/smtlogics/qfnia_tactic.cpp src/tactic/smtlogics/qfuf_tactic.cpp src/tactic/smtlogics/qflia_tactic.cpp src/tactic/smtlogics/qfaufbv_tactic.cpp src/tactic/smtlogics/quant_tactics.cpp src/tactic/smtlogics/qfufbv_tactic.cpp src/tactic/smtlogics/qfidl_tactic.cpp src/tactic/smtlogics/qfauflia_tactic.cpp src/tactic/smtlogics/qfufbv_ackr_model_converter.cpp src/tactic/smtlogics/nra_tactic.cpp src/tactic/smtlogics/qfnra_tactic.cpp src/tactic/smtlogics/qflra_tactic.cpp src/sat/sat_solver/inc_sat_solver.cpp src/tactic/ufbv/ufbv_rewriter_tactic.cpp src/tactic/ufbv/quasi_macros_tactic.cpp src/tactic/ufbv/ufbv_tactic.cpp src/tactic/ufbv/macro_finder_tactic.cpp src/tactic/nlsat_smt/nl_purify_tactic.cpp src/muz/spacer/spacer_itp_solver.cpp src/duality/duality_solver.cpp src/duality/duality_rpfp.cpp src/qe/nlqsat.cpp src/qe/qe_sat_tactic.cpp src/qe/qsat.cpp src/qe/qe_lite.cpp src/qe/qe_tactic.cpp src/qe/qe_cmd.cpp src/smt/tactic/smt_tactic.cpp src/smt/tactic/ctx_solver_simplify_tactic.cpp src/tactic/bv/max_bv_sharing_tactic.cpp src/tactic/bv/bv_bound_chk_tactic.cpp src/tactic/bv/bv_size_reduction_tactic.cpp src/tactic/bv/bit_blaster_tactic.cpp src/tactic/bv/bvarray2uf_rewriter.cpp src/tactic/bv/bv1_blaster_tactic.cpp src/tactic/bv/dt2bv_tactic.cpp src/tactic/bv/bvarray2uf_tactic.cpp src/tactic/bv/bv_bounds_tactic.cpp src/tactic/bv/elim_small_bv_tactic.cpp src/smt/asserted_formulas.cpp src/smt/smt2_extra_cmds.cpp src/ast/pattern/expr_pattern_match.cpp src/parsers/smt2/marshal.cpp src/cmd_context/extra_cmds/subpaving_cmds.cpp src/cmd_context/extra_cmds/polynomial_cmds.cpp src/cmd_context/extra_cmds/dbg_cmds.cpp src/cmd_context/simplify_cmd.cpp src/cmd_context/interpolant_cmds.cpp src/cmd_context/cmd_context_to_goal.cpp src/cmd_context/tactic_cmds.cpp src/cmd_context/echo_tactic.cpp src/cmd_context/eval_cmd.cpp src/cmd_context/cmd_context.cpp src/cmd_context/parametric_cmd.cpp src/cmd_context/cmd_util.cpp src/cmd_context/basic_cmds.cpp src/ackermannization/ackermannize_bv_model_converter.cpp src/ackermannization/lackr_model_converter_lazy.cpp src/ackermannization/lackr.cpp src/solver/solver2tactic.cpp src/solver/tactic2solver.cpp src/solver/solver_pool.cpp src/tactic/aig/aig_tactic.cpp src/math/subpaving/tactic/subpaving_tactic.cpp src/nlsat/tactic/nlsat_tactic.cpp src/nlsat/tactic/goal2nlsat.cpp src/nlsat/tactic/qfnra_nlsat_tactic.cpp src/tactic/arith/lia2card_tactic.cpp src/tactic/arith/factor_tactic.cpp src/tactic/arith/degree_shift_tactic.cpp src/tactic/arith/normalize_bounds_tactic.cpp src/tactic/arith/card2bv_tactic.cpp src/tactic/arith/arith_bounds_tactic.cpp src/tactic/arith/recover_01_tactic.cpp src/tactic/arith/fix_dl_var_tactic.cpp src/tactic/arith/pb2bv_model_converter.cpp src/tactic/arith/eq2bv_tactic.cpp src/tactic/arith/purify_arith_tactic.cpp src/tactic/arith/propagate_ineqs_tactic.cpp src/tactic/arith/pb2bv_tactic.cpp src/tactic/arith/nla2bv_tactic.cpp src/tactic/arith/fm_tactic.cpp src/tactic/arith/lia2pb_tactic.cpp src/tactic/arith/elim01_tactic.cpp src/tactic/arith/diff_neq_tactic.cpp src/tactic/arith/add_bounds_tactic.cpp src/sat/tactic/sat_tactic.cpp src/sat/tactic/goal2sat.cpp src/tactic/core/cofactor_term_ite_tactic.cpp src/tactic/core/solve_eqs_tactic.cpp src/tactic/core/occf_tactic.cpp src/tactic/core/cofactor_elim_term_ite.cpp src/tactic/core/ctx_simplify_tactic.cpp src/tactic/core/der_tactic.cpp src/tactic/core/collect_statistics_tactic.cpp src/tactic/core/simplify_tactic.cpp src/tactic/core/elim_term_ite_tactic.cpp src/tactic/core/distribute_forall_tactic.cpp src/tactic/core/pb_preprocess_tactic.cpp src/tactic/core/propagate_values_tactic.cpp src/tactic/core/dom_simplify_tactic.cpp src/tactic/core/symmetry_reduce_tactic.cpp src/tactic/core/nnf_tactic.cpp src/tactic/core/injectivity_tactic.cpp src/tactic/core/split_clause_tactic.cpp src/tactic/core/blast_term_ite_tactic.cpp src/tactic/core/elim_uncnstr_tactic.cpp src/tactic/core/tseitin_cnf_tactic.cpp src/tactic/core/reduce_args_tactic.cpp src/tactic/horn_subsume_model_converter.cpp src/tactic/sine_filter.cpp src/tactic/tactic.cpp src/tactic/tactical.cpp src/util/lp/scaler_instances.cpp src/util/lp/eta_matrix_instances.cpp src/api/api_goal.cpp src/api/api_interp.cpp src/tactic/portfolio/smt_strategic_solver.cpp src/tactic/fpa/qffp_tactic.cpp src/tactic/smtlogics/qfbv_tactic.cpp src/muz/spacer/spacer_farkas_learner.cpp src/muz/pdr/pdr_farkas_learner.cpp src/muz/pdr/pdr_smt_context_manager.cpp src/muz/base/hnf.cpp src/qe/qe.cpp src/tactic/sls/sls_tactic.cpp src/tactic/sls/sls_engine.cpp src/smt/tactic/unit_subsumption_tactic.cpp src/smt/theory_str.cpp src/smt/smt_conflict_resolution.cpp src/smt/theory_array_base.cpp src/smt/smt_consequences.cpp src/smt/theory_fpa.cpp src/smt/smt_quantifier.cpp src/smt/theory_datatype.cpp src/smt/theory_wmaxsat.cpp src/smt/smt_internalizer.cpp src/smt/smt_context_inv.cpp src/smt/arith_eq_adapter.cpp src/smt/smt_model_finder.cpp src/smt/smt_quick_checker.cpp src/smt/theory_dl.cpp src/smt/smt_model_checker.cpp src/smt/smt_model_generator.cpp src/smt/smt_case_split_queue.cpp src/smt/smt_kernel.cpp src/smt/smt_theory.cpp src/smt/dyn_ack.cpp src/smt/theory_dummy.cpp src/smt/smt_justification.cpp src/smt/smt_for_each_relevant_expr.cpp src/smt/theory_array.cpp src/smt/smt_context_stat.cpp src/smt/smt_relevancy.cpp src/smt/smt_context_pp.cpp src/smt/theory_bv.cpp src/smt/smt_checker.cpp src/smt/smt_context.cpp src/smt/theory_pb.cpp src/smt/theory_array_full.cpp src/smt/mam.cpp src/smt/smt_enode.cpp src/smt/qi_queue.cpp src/smt/theory_seq.cpp src/parsers/smt2/smt2scanner.cpp src/parsers/smt2/smt2parser.cpp src/interp/iz3translate_direct.cpp src/interp/iz3translate.cpp src/interp/iz3interp.cpp src/ackermannization/ackermannize_bv_tactic.cpp src/api/dll/install_tactic.cpp src/shell/install_tactic.cpp src/opt/optsmt.cpp src/muz/spacer/spacer_smt_context_manager.cpp src/muz/spacer/spacer_legacy_mev.cpp src/muz/spacer/spacer_legacy_mbp.cpp src/tactic/sls/bvsls_opt_engine.cpp src/smt/theory_diff_logic.cpp src/smt/theory_utvpi.cpp src/smt/smt_setup.cpp src/util/lp/square_dense_submatrix_instances.cpp src/util/lp/row_eta_matrix_instances.cpp src/util/lp/sparse_matrix_instances.cpp src/opt/opt_solver.cpp src/opt/opt_context.cpp src/opt/wmax.cpp src/opt/sortmax.cpp src/opt/maxres.cpp src/opt/maxsmt.cpp src/muz/spacer/spacer_util.cpp src/muz/spacer/spacer_manager.cpp src/muz/spacer/spacer_prop_solver.cpp src/muz/pdr/pdr_manager.cpp src/muz/pdr/pdr_reachable_cache.cpp src/muz/pdr/pdr_prop_solver.cpp src/muz/pdr/pdr_util.cpp src/smt/theory_arith.cpp src/smt/theory_dense_diff_logic.cpp src/util/lp/lu_instances.cpp src/shell/opt_frontend.cpp src/api/api_opt.cpp src/opt/opt_parse.cpp src/opt/opt_cmds.cpp src/muz/dataflow/dataflow.cpp src/util/lp/lp_core_solver_base_instances.cpp src/util/lp/core_solver_pretty_printer_instances.cpp src/shell/smtlib_frontend.cpp src/muz/fp/datalog_parser.cpp src/muz/ddnf/ddnf.cpp src/muz/bmc/dl_bmc_engine.cpp src/muz/tab/tab_context.cpp src/muz/clp/clp_context.cpp src/muz/pdr/pdr_closure.cpp src/muz/transforms/dl_mk_coi_filter.cpp src/muz/transforms/dl_mk_quantifier_instantiation.cpp src/muz/transforms/dl_mk_scale.cpp src/muz/transforms/dl_mk_rule_inliner.cpp src/muz/transforms/dl_mk_array_eq_rewrite.cpp src/muz/transforms/dl_mk_karr_invariants.cpp src/muz/transforms/dl_mk_backwards.cpp src/muz/transforms/dl_mk_magic_symbolic.cpp src/muz/transforms/dl_mk_filter_rules.cpp src/muz/transforms/dl_mk_magic_sets.cpp src/muz/transforms/dl_mk_unbound_compressor.cpp src/muz/transforms/dl_mk_bit_blast.cpp src/muz/transforms/dl_mk_loop_counter.cpp src/muz/transforms/dl_mk_separate_negated_tails.cpp src/muz/transforms/dl_mk_quantifier_abstraction.cpp src/muz/transforms/dl_mk_array_instantiation.cpp src/muz/transforms/dl_mk_slice.cpp src/muz/transforms/dl_mk_interp_tail_simplifier.cpp src/muz/base/rule_properties.cpp src/muz/base/dl_rule_transformer.cpp src/muz/base/dl_rule_set.cpp src/muz/base/dl_context.cpp src/muz/base/dl_costs.cpp src/muz/base/dl_rule_subsumption_index.cpp src/muz/base/dl_util.cpp src/muz/base/dl_rule.cpp src/util/lp/lp_dual_core_solver_instances.cpp src/util/lp/lp_solver_instances.cpp src/muz/fp/horn_tactic.cpp src/muz/spacer/spacer_legacy_frames.cpp src/muz/spacer/spacer_context.cpp src/muz/spacer/spacer_dl_interface.cpp src/muz/spacer/spacer_generalizers.cpp src/muz/pdr/pdr_generalizers.cpp src/muz/pdr/pdr_context.cpp src/muz/pdr/pdr_dl_interface.cpp src/muz/rel/dl_external_relation.cpp src/muz/transforms/dl_mk_unfold.cpp src/muz/transforms/dl_mk_subsumption_checker.cpp src/muz/transforms/dl_mk_array_blast.cpp src/muz/transforms/dl_transforms.cpp src/muz/transforms/dl_mk_coalesce.cpp src/smt/theory_lra.cpp src/util/lp/lar_core_solver_instances.cpp src/util/lp/lp_primal_core_solver_instances.cpp src/util/lp/lp_bound_propagator.cpp src/util/lp/quick_xplain.cpp src/util/lp/lp_dual_simplex_instances.cpp src/util/lp/static_matrix_instances.cpp src/api/api_datalog.cpp src/muz/fp/dl_register_engine.cpp src/muz/duality/duality_dl_interface.cpp src/muz/rel/udoc_relation.cpp src/muz/rel/dl_lazy_table.cpp src/muz/rel/dl_instruction.cpp src/muz/rel/dl_sparse_table.cpp src/muz/rel/dl_table_relation.cpp src/muz/rel/dl_base.cpp src/muz/rel/check_relation.cpp src/muz/rel/dl_sieve_relation.cpp src/muz/rel/dl_table.cpp src/muz/rel/dl_mk_similarity_compressor.cpp In member function 'virtual datalog::relation_transformer_fn* datalog::table_relation_plugin::mk_select_equal_and_project_fn(const datalog::relation_base&, app* const&, unsigned int)': cc1plus: warning: 'void* __builtin_memset(void*, int, unsigned int)' specified size 4294967292 exceeds maximum object size 2147483647 [-Wstringop-overflow=] src/muz/rel/dl_mk_simple_joins.cpp src/util/lp/random_updater_instances.cpp src/util/lp/lp_primal_simplex_instances.cpp src/shell/lp_frontend.cpp src/muz/fp/dl_cmds.cpp src/muz/rel/karr_relation.cpp src/muz/rel/dl_interval_relation.cpp src/muz/rel/aig_exporter.cpp src/muz/rel/dl_bound_relation.cpp src/muz/rel/dl_compiler.cpp src/muz/rel/dl_product_relation.cpp src/muz/rel/dl_finite_product_relation.cpp src/muz/rel/dl_mk_explanations.cpp In member function 'void datalog::compiler::make_select_equal_and_project(datalog::compiler::reg_idx, datalog::relation_element, unsigned int, datalog::compiler::reg_idx&, bool, datalog::instruction_block&)': cc1plus: warning: 'void* __builtin_memset(void*, int, unsigned int)' specified size 4294967292 exceeds maximum object size 2147483647 [-Wstringop-overflow=] src/muz/rel/dl_relation_manager.cpp src/muz/rel/dl_check_table.cpp src/muz/rel/rel_context.cpp src/shell/datalog_frontend.cpp g++ -o z3 shell/dimacs_frontend.o shell/z3_log_frontend.o shell/datalog_frontend.o shell/install_tactic.o shell/lp_frontend.o shell/gparams_register_modules.o shell/main.o shell/smtlib_frontend.o shell/opt_frontend.o shell/mem_initializer.o api/api.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a sat/sat_solver/sat_solver.a tactic/ufbv/ufbv_tactic.a tactic/nlsat_smt/nlsat_smt_tactic.a muz/fp/fp.a muz/duality/duality_intf.a muz/ddnf/ddnf.a muz/bmc/bmc.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/pdr/pdr.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a duality/duality.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/extra_cmds/extra_cmds.a cmd_context/cmd_context.a interp/interp.a ackermannization/ackermannization.a solver/solver.a ast/proofs/proofs.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 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 nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/lp/lp.a util/util.a -lpthread -Wl,-Os,--as-needed -fopenmp -lrt g++ -o libz3.so -shared api/dll/dll.o api/dll/install_tactic.o api/dll/gparams_register_modules.o api/dll/mem_initializer.o api/api_goal.o api/api_interp.o api/api_quant.o api/api_opt.o api/api_model.o api/api_ast_map.o api/api_fpa.o api/api_tactic.o api/z3_replayer.o api/api_log_macros.o api/api_array.o api/api_datalog.o api/api_context.o api/api_polynomial.o api/api_params.o api/api_datatype.o api/api_commands.o api/api_rcf.o api/api_config_params.o api/api_ast.o api/api_qe.o api/api_pb.o api/api_solver.o api/api_parsers.o api/api_numeral.o api/api_log.o api/api_bv.o api/api_ast_vector.o api/api_arith.o api/api_stats.o api/api_algebraic.o api/api_seq.o opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a sat/sat_solver/sat_solver.a tactic/ufbv/ufbv_tactic.a tactic/nlsat_smt/nlsat_smt_tactic.a muz/fp/fp.a muz/duality/duality_intf.a muz/ddnf/ddnf.a muz/bmc/bmc.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/pdr/pdr.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a duality/duality.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/extra_cmds/extra_cmds.a cmd_context/cmd_context.a interp/interp.a ackermannization/ackermannization.a solver/solver.a ast/proofs/proofs.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 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 nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/lp/lp.a util/util.a -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 src/api/api_interp.cpp src/api/api_solver.cpp src/smt/smt_implied_equalities.cpp g++ -o libz3.so -shared api/dll/dll.o api/dll/install_tactic.o api/dll/gparams_register_modules.o api/dll/mem_initializer.o api/api_goal.o api/api_interp.o api/api_quant.o api/api_opt.o api/api_model.o api/api_ast_map.o api/api_fpa.o api/api_tactic.o api/z3_replayer.o api/api_log_macros.o api/api_array.o api/api_datalog.o api/api_context.o api/api_polynomial.o api/api_params.o api/api_datatype.o api/api_commands.o api/api_rcf.o api/api_config_params.o api/api_ast.o api/api_qe.o api/api_pb.o api/api_solver.o api/api_parsers.o api/api_numeral.o api/api_log.o api/api_bv.o api/api_ast_vector.o api/api_arith.o api/api_stats.o api/api_algebraic.o api/api_seq.o opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a sat/sat_solver/sat_solver.a tactic/ufbv/ufbv_tactic.a tactic/nlsat_smt/nlsat_smt_tactic.a muz/fp/fp.a muz/duality/duality_intf.a muz/ddnf/ddnf.a muz/bmc/bmc.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/pdr/pdr.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a duality/duality.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/extra_cmds/extra_cmds.a cmd_context/cmd_context.a interp/interp.a ackermannization/ackermannization.a solver/solver.a ast/proofs/proofs.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 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 nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/lp/lp.a util/util.a -fopenmp -lrt g++ -o z3 shell/dimacs_frontend.o shell/z3_log_frontend.o shell/datalog_frontend.o shell/install_tactic.o shell/lp_frontend.o shell/gparams_register_modules.o shell/main.o shell/smtlib_frontend.o shell/opt_frontend.o shell/mem_initializer.o api/api.a opt/opt.a tactic/portfolio/portfolio.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a sat/sat_solver/sat_solver.a tactic/ufbv/ufbv_tactic.a tactic/nlsat_smt/nlsat_smt_tactic.a muz/fp/fp.a muz/duality/duality_intf.a muz/ddnf/ddnf.a muz/bmc/bmc.a muz/tab/tab.a muz/clp/clp.a muz/spacer/spacer.a muz/pdr/pdr.a muz/rel/rel.a muz/transforms/transforms.a muz/dataflow/dataflow.a muz/base/muz.a duality/duality.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/extra_cmds/extra_cmds.a cmd_context/cmd_context.a interp/interp.a ackermannization/ackermannization.a solver/solver.a ast/proofs/proofs.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 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 nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/lp/lp.a util/util.a -lpthread -Wl,-Os,--as-needed -fopenmp -lrt ln -f -s ../libz3.so python Z3 was successfully installed. ================================================================================ Executing strip on all files... Done Time: 2.52s. Size: 49201096 B -> 43033752 B. Save: 6023 KB. ================================================================================ Pack: z3 4.7.1 ================================================================================ Executing: genpkg_rules Copying folders and files... Done Copying "receipt"... Done Determining package architecture... i486 Creating the list of files... Done Creating md5sum of files... Done Compressing the FS... Done Creating full cpio archive... Done QA: checking for empty package... Done Removing old package "z3-4.7.1-i486.tazpkg" Done The release checksum has changed. ================================================================================ Package "z3-4.7.1-i486.tazpkg" created Pack: z3-dev 4.7.1 ================================================================================ Executing: genpkg_rules Copying folders and files... Done Copying "receipt"... Done Determining package architecture... any Creating the list of files... Done Creating md5sum of files... Done Compressing the FS... Done Creating full cpio archive... Done QA: checking for empty package... Done The release checksum has not changed. ================================================================================ Package "z3-dev-4.7.1-any.tazpkg" created Post-check ================================================================================ Checking build... Done Checking 'any' arch... Done Checking libtool in source/z3-4.7.1... Done Checking site script in source/z3-4.7.1... Done Checking ownership in install... Done Checking permissions in install... Failed Problems found: 0750 /usr/include/z3++.h 0750 /usr/include/z3.h 0750 /usr/include/z3_algebraic.h 0750 /usr/include/z3_api.h 0750 /usr/include/z3_ast_containers.h 0750 /usr/include/z3_fixedpoint.h 0750 /usr/include/z3_fpa.h 0750 /usr/include/z3_interp.h 0750 /usr/include/z3_macros.h 0750 /usr/include/z3_optimization.h 0750 /usr/include/z3_polynomial.h 0750 /usr/include/z3_rcf.h 0750 /usr/include/z3_spacer.h 0750 /usr/include/z3_v1.h Checking broken symlinks in install... Done Querying Repology... Done Updating activity log... Done ================================================================================ Summary for: z3 4.7.1 ================================================================================ Src file : z3-4.7.1.tar.gz Src size : 31.3M Source dir : 195.4M Produced : 41.5M Cook time : 669s ~ 11m 09s Cook date : 2020-09-13 11:01 Target arch : any, i486 -------------------------------------------------------------------------------- # : Packed : Compressed : Files : Package name -------------------------------------------------------------------------------- 1 : 41.1M : 11.7M : 2 : z3-4.7.1-i486.tazpkg 2 : 496.0K : 62.6K : 14 : z3-dev-4.7.1-any.tazpkg ================================================================================