Your message dated Mon, 26 Sep 2016 06:36:50 +0000
with message-id <e1bopx0-000290...@franck.debian.org>
and subject line Bug#835743: fixed in z3 4.4.1-0.3
has caused the Debian Bug report #835743,
regarding z3: FTBFS: ../src/util/mpz.cpp:137:8: error: call of overloaded
'set(mpz&, long unsigned int)' is ambiguous
to be marked as done.
This means that you claim that the problem has been dealt with.
If this is not the case it is now your responsibility to reopen the
Bug report if necessary, and/or fix the problem forthwith.
(NB: If you are a system administrator and have no idea what this
message is talking about, this may indicate a serious mail system
misconfiguration somewhere. Please contact ow...@bugs.debian.org
immediately.)
--
835743: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=835743
Debian Bug Tracking System
Contact ow...@bugs.debian.org with problems
--- Begin Message ---
Source: z3
Version: 4.4.1-0.2
Severity: serious
Tags: stretch sid
User: debian...@lists.debian.org
Usertags: qa-ftbfs-20160828 qa-ftbfs
Justification: FTBFS on amd64
Hi,
During a rebuild of all packages in sid, your package failed to build on
amd64.
Relevant part (hopefully):
> make[2]: Entering directory '/<<PKGBUILDDIR>>/build'
> src/shell/datalog_frontend.cpp
> src/shell/gparams_register_modules.cpp
> src/shell/z3_log_frontend.cpp
> src/shell/main.cpp
> src/shell/install_tactic.cpp
> src/shell/dimacs_frontend.cpp
> src/shell/mem_initializer.cpp
> src/shell/opt_frontend.cpp
> src/shell/smtlib_frontend.cpp
> src/api/api_params.cpp
> src/api/api_opt.cpp
> src/api/api_algebraic.cpp
> src/api/api_log_macros.cpp
> src/api/api_quant.cpp
> src/api/api_solver_old.cpp
> src/api/api_ast_vector.cpp
> src/api/api_bv.cpp
> src/api/api_context.cpp
> src/api/api_datalog.cpp
> src/api/api_arith.cpp
> src/api/api_ast.cpp
> src/api/api_polynomial.cpp
> src/api/api_ast_map.cpp
> src/api/api_numeral.cpp
> src/api/api_interp.cpp
> src/api/api_stats.cpp
> src/api/api_model.cpp
> src/api/api_config_params.cpp
> src/api/api_solver.cpp
> src/api/z3_replayer.cpp
> src/api/api_array.cpp
> src/api/api_pb.cpp
> src/api/api_goal.cpp
> src/api/api_commands.cpp
> src/api/api_log.cpp
> src/api/api_rcf.cpp
> src/api/api_fpa.cpp
> src/api/api_parsers.cpp
> src/api/api_datatype.cpp
> src/api/api_user_theory.cpp
> src/api/api_tactic.cpp
> src/opt/wmax.cpp
> src/opt/opt_pareto.cpp
> src/opt/opt_cmds.cpp
> src/opt/hitting_sets.cpp
> src/opt/maxsmt.cpp
> src/opt/pb_sls.cpp
> src/opt/opt_context.cpp
> src/opt/mus.cpp
> src/opt/bcd2.cpp
> src/opt/fu_malik.cpp
> src/opt/maxsls.cpp
> src/opt/opt_solver.cpp
> src/opt/maxres.cpp
> src/opt/mss.cpp
> src/opt/maxhs.cpp
> src/opt/optsmt.cpp
> src/parsers/smt/smtparser.cpp
> src/parsers/smt/smtlib.cpp
> src/parsers/smt/smtlib_solver.cpp
> src/tactic/portfolio/default_tactic.cpp
> src/tactic/portfolio/smt_strategic_solver.cpp
> src/sat/sat_solver/inc_sat_solver.cpp
> src/tactic/ufbv/ufbv_tactic.cpp
> src/tactic/ufbv/ufbv_rewriter.cpp
> src/tactic/ufbv/ufbv_rewriter_tactic.cpp
> src/tactic/ufbv/quasi_macros_tactic.cpp
> src/tactic/ufbv/macro_finder_tactic.cpp
> src/tactic/fpa/qffp_tactic.cpp
> src/tactic/fpa/fpa2bv_model_converter.cpp
> src/tactic/fpa/fpa2bv_tactic.cpp
> src/tactic/smtlogics/qfufnra_tactic.cpp
> src/tactic/smtlogics/nra_tactic.cpp
> src/tactic/smtlogics/qfnra_tactic.cpp
> src/tactic/smtlogics/qfufbv_tactic.cpp
> src/tactic/smtlogics/quant_tactics.cpp
> src/tactic/smtlogics/qfbv_tactic.cpp
> src/tactic/smtlogics/qfuf_tactic.cpp
> src/tactic/smtlogics/qflia_tactic.cpp
> src/tactic/smtlogics/qfnia_tactic.cpp
> src/tactic/smtlogics/qfidl_tactic.cpp
> src/tactic/smtlogics/qfaufbv_tactic.cpp
> src/tactic/smtlogics/qflra_tactic.cpp
> src/tactic/smtlogics/qfauflia_tactic.cpp
> src/tactic/nlsat_smt/nl_purify_tactic.cpp
> src/muz/fp/dl_cmds.cpp
> src/muz/fp/datalog_parser.cpp
> src/muz/fp/dl_register_engine.cpp
> src/muz/fp/horn_tactic.cpp
> src/muz/duality/duality_dl_interface.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_generalizers.cpp
> src/muz/pdr/pdr_farkas_learner.cpp
> src/muz/pdr/pdr_closure.cpp
> src/muz/pdr/pdr_manager.cpp
> src/muz/pdr/pdr_smt_context_manager.cpp
> src/muz/pdr/pdr_prop_solver.cpp
> src/muz/pdr/pdr_reachable_cache.cpp
> src/muz/pdr/pdr_dl_interface.cpp
> src/muz/pdr/pdr_context.cpp
> src/muz/pdr/pdr_util.cpp
> src/muz/pdr/pdr_sym_mux.cpp
> src/muz/rel/dl_mk_similarity_compressor.cpp
> src/muz/rel/dl_bound_relation.cpp
> src/muz/rel/dl_interval_relation.cpp
> src/muz/rel/dl_sieve_relation.cpp
> src/muz/rel/udoc_relation.cpp
> src/muz/rel/dl_compiler.cpp
> src/muz/rel/karr_relation.cpp
> src/muz/rel/dl_sparse_table.cpp
> src/muz/rel/dl_finite_product_relation.cpp
> src/muz/rel/dl_base.cpp
> src/muz/rel/dl_mk_partial_equiv.cpp
> src/muz/rel/dl_table.cpp
> src/muz/rel/tbv.cpp
> src/muz/rel/doc.cpp
> src/muz/rel/dl_relation_manager.cpp
> src/muz/rel/dl_mk_explanations.cpp
> src/muz/rel/dl_check_table.cpp
> src/muz/rel/dl_mk_simple_joins.cpp
> src/muz/rel/aig_exporter.cpp
> src/muz/rel/dl_instruction.cpp
> src/muz/rel/dl_product_relation.cpp
> src/muz/rel/check_relation.cpp
> src/muz/rel/dl_lazy_table.cpp
> src/muz/rel/dl_external_relation.cpp
> src/muz/rel/dl_table_relation.cpp
> src/muz/rel/rel_context.cpp
> src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
> src/muz/transforms/dl_mk_rule_inliner.cpp
> src/muz/transforms/dl_mk_unbound_compressor.cpp
> src/muz/transforms/dl_mk_filter_rules.cpp
> src/muz/transforms/dl_mk_loop_counter.cpp
> src/muz/transforms/dl_transforms.cpp
> src/muz/transforms/dl_mk_quantifier_instantiation.cpp
> src/muz/transforms/dl_mk_subsumption_checker.cpp
> src/muz/transforms/dl_mk_bit_blast.cpp
> src/muz/transforms/dl_mk_coalesce.cpp
> src/muz/transforms/dl_mk_karr_invariants.cpp
> src/muz/transforms/dl_mk_unfold.cpp
> src/muz/transforms/dl_mk_magic_sets.cpp
> src/muz/transforms/dl_mk_magic_symbolic.cpp
> src/muz/transforms/dl_mk_slice.cpp
> src/muz/transforms/dl_mk_backwards.cpp
> src/muz/transforms/dl_mk_scale.cpp
> src/muz/transforms/dl_mk_array_blast.cpp
> src/muz/transforms/dl_mk_separate_negated_tails.cpp
> src/muz/transforms/dl_mk_quantifier_abstraction.cpp
> src/muz/transforms/dl_mk_coi_filter.cpp
> src/muz/dataflow/dataflow.cpp
> src/muz/base/rule_properties.cpp
> src/muz/base/bind_variables.cpp
> src/muz/base/dl_context.cpp
> src/muz/base/hnf.cpp
> src/muz/base/dl_util.cpp
> src/muz/base/dl_rule_set.cpp
> src/muz/base/dl_rule_transformer.cpp
> src/muz/base/dl_rule.cpp
> src/muz/base/dl_rule_subsumption_index.cpp
> src/muz/base/dl_costs.cpp
> src/muz/base/proof_utils.cpp
> src/muz/base/dl_boogie_proof.cpp
> src/duality/duality_rpfp.cpp
> src/duality/duality_wrapper.cpp
> src/duality/duality_profiling.cpp
> src/duality/duality_solver.cpp
> src/qe/qe_bool_plugin.cpp
> src/qe/qe_bv_plugin.cpp
> src/qe/qe_array_plugin.cpp
> src/qe/vsubst_tactic.cpp
> src/qe/qe_lite.cpp
> src/qe/qe_datatype_plugin.cpp
> src/qe/qe_tactic.cpp
> src/qe/qe_util.cpp
> src/qe/qe_cmd.cpp
> src/qe/qe_sat_tactic.cpp
> src/qe/qe_dl_plugin.cpp
> src/qe/qe_arith_plugin.cpp
> src/qe/nlarith_util.cpp
> src/qe/qe_arith.cpp
> src/qe/qe.cpp
> src/tactic/sls/sls_engine.cpp
> src/tactic/sls/bvsls_opt_engine.cpp
> src/tactic/sls/sls_tactic.cpp
> src/smt/tactic/ctx_solver_simplify_tactic.cpp
> src/smt/tactic/smt_tactic.cpp
> src/smt/tactic/unit_subsumption_tactic.cpp
> src/tactic/bv/max_bv_sharing_tactic.cpp
> src/tactic/bv/bit_blaster_tactic.cpp
> src/tactic/bv/bv_size_reduction_tactic.cpp
> src/tactic/bv/bit_blaster_model_converter.cpp
> src/tactic/bv/bv1_blaster_tactic.cpp
> src/smt/user_plugin/user_decl_plugin.cpp
> src/smt/user_plugin/user_simplifier_plugin.cpp
> src/smt/user_plugin/user_smt_theory.cpp
> src/smt/theory_datatype.cpp
> src/smt/smt_statistics.cpp
> src/smt/mam.cpp
> src/smt/smt_theory.cpp
> src/smt/smt_quick_checker.cpp
> src/smt/smt_literal.cpp
> src/smt/watch_list.cpp
> src/smt/arith_eq_adapter.cpp
> src/smt/smt_checker.cpp
> src/smt/dyn_ack.cpp
> src/smt/smt_enode.cpp
> src/smt/smt_internalizer.cpp
> src/smt/smt_conflict_resolution.cpp
> src/smt/theory_array_full.cpp
> src/smt/theory_fpa.cpp
> src/smt/theory_opt.cpp
> src/smt/smt_case_split_queue.cpp
> src/smt/theory_diff_logic.cpp
> src/smt/smt_kernel.cpp
> src/smt/theory_dl.cpp
> src/smt/smt_context.cpp
> src/smt/uses_theory.cpp
> src/smt/smt_model_finder.cpp
> src/smt/smt_cg_table.cpp
> src/smt/theory_wmaxsat.cpp
> src/smt/smt_farkas_util.cpp
> src/smt/theory_dummy.cpp
> src/smt/smt_relevancy.cpp
> src/smt/theory_utvpi.cpp
> src/smt/smt_solver.cpp
> src/smt/smt_context_inv.cpp
> src/smt/theory_bv.cpp
> src/smt/cost_evaluator.cpp
> src/smt/expr_context_simplifier.cpp
> src/smt/smt_clause.cpp
> src/smt/theory_dense_diff_logic.cpp
> src/smt/theory_pb.cpp
> src/smt/smt_setup.cpp
> src/smt/smt_justification.cpp
> src/smt/fingerprints.cpp
> src/smt/theory_array_base.cpp
> src/smt/qi_queue.cpp
> src/smt/smt_context_pp.cpp
> src/smt/asserted_formulas.cpp
> src/smt/smt_model_checker.cpp
> src/smt/cached_var_subst.cpp
> src/smt/smt_model_generator.cpp
> src/smt/smt_almost_cg_table.cpp
> src/smt/smt_context_stat.cpp
> src/smt/smt_quantifier_stat.cpp
> src/smt/smt_for_each_relevant_expr.cpp
> src/smt/theory_array.cpp
> src/smt/old_interval.cpp
> src/smt/arith_eq_solver.cpp
> src/smt/smt_value_sort.cpp
> src/smt/theory_arith.cpp
> src/smt/elim_term_ite.cpp
> src/smt/smt_implied_equalities.cpp
> src/smt/smt_quantifier.cpp
> src/smt/proto_model/numeral_factory.cpp
> src/smt/proto_model/proto_model.cpp
> src/smt/proto_model/struct_factory.cpp
> src/smt/proto_model/value_factory.cpp
> src/smt/proto_model/datatype_factory.cpp
> src/smt/proto_model/array_factory.cpp
> src/smt/params/theory_bv_params.cpp
> src/smt/params/qi_params.cpp
> src/smt/params/theory_arith_params.cpp
> src/smt/params/preprocessor_params.cpp
> src/smt/params/theory_array_params.cpp
> src/smt/params/theory_pb_params.cpp
> src/smt/params/smt_params.cpp
> src/smt/params/dyn_ack_params.cpp
> src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
> src/ast/rewriter/bit_blaster/bit_blaster.cpp
> src/ast/pattern/expr_pattern_match.cpp
> src/ast/pattern/pattern_inference.cpp
> src/ast/pattern/pattern_inference_params.cpp
> src/ast/macros/quasi_macros.cpp
> src/ast/macros/macro_finder.cpp
> src/ast/macros/macro_util.cpp
> src/ast/macros/macro_manager.cpp
> src/ast/fpa/fpa2bv_converter.cpp
> src/ast/simplifier/bv_simplifier_params.cpp
> src/ast/simplifier/simplifier.cpp
> src/ast/simplifier/array_simplifier_plugin.cpp
> src/ast/simplifier/distribute_forall.cpp
> src/ast/simplifier/arith_simplifier_plugin.cpp
> src/ast/simplifier/bit2int.cpp
> src/ast/simplifier/simplifier_plugin.cpp
> src/ast/simplifier/array_simplifier_params.cpp
> src/ast/simplifier/datatype_simplifier_plugin.cpp
> src/ast/simplifier/arith_simplifier_params.cpp
> src/ast/simplifier/inj_axiom.cpp
> src/ast/simplifier/basic_simplifier_plugin.cpp
> src/ast/simplifier/elim_bounds.cpp
> src/ast/simplifier/push_app_ite.cpp
> src/ast/simplifier/poly_simplifier_plugin.cpp
> src/ast/simplifier/bv_elim.cpp
> src/ast/simplifier/pull_ite_tree.cpp
> src/ast/simplifier/bv_simplifier_plugin.cpp
> src/ast/simplifier/fpa_simplifier_plugin.cpp
> src/ast/simplifier/maximise_ac_sharing.cpp
> src/ast/proof_checker/proof_checker.cpp
> src/parsers/smt2/smt2parser.cpp
> src/parsers/smt2/smt2scanner.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/cmd_context/cmd_context.cpp
> src/cmd_context/basic_cmds.cpp
> src/cmd_context/context_params.cpp
> src/cmd_context/parametric_cmd.cpp
> src/cmd_context/pdecl.cpp
> src/cmd_context/cmd_context_to_goal.cpp
> src/cmd_context/tactic_cmds.cpp
> src/cmd_context/simplify_cmd.cpp
> src/cmd_context/echo_tactic.cpp
> src/cmd_context/interpolant_cmds.cpp
> src/cmd_context/eval_cmd.cpp
> src/cmd_context/cmd_util.cpp
> src/cmd_context/tactic_manager.cpp
> src/cmd_context/check_logic.cpp
> src/interp/iz3proof_itp.cpp
> src/interp/iz3base.cpp
> src/interp/iz3proof.cpp
> src/interp/iz3translate.cpp
> src/interp/iz3mgr.cpp
> src/interp/iz3checker.cpp
> src/interp/iz3pp.cpp
> src/interp/iz3interp.cpp
> src/interp/iz3scopes.cpp
> src/interp/iz3foci.cpp
> src/interp/iz3profiling.cpp
> src/interp/iz3translate_direct.cpp
> src/solver/combined_solver.cpp
> src/solver/check_sat_result.cpp
> src/solver/solver.cpp
> src/solver/solver_na2as.cpp
> src/solver/tactic2solver.cpp
> src/tactic/aig/aig_tactic.cpp
> src/tactic/aig/aig.cpp
> src/math/subpaving/tactic/expr2subpaving.cpp
> src/math/subpaving/tactic/subpaving_tactic.cpp
> src/nlsat/tactic/qfnra_nlsat_tactic.cpp
> src/nlsat/tactic/nlsat_tactic.cpp
> src/nlsat/tactic/goal2nlsat.cpp
> src/tactic/arith/factor_tactic.cpp
> src/tactic/arith/arith_bounds_tactic.cpp
> src/tactic/arith/lia2card_tactic.cpp
> src/tactic/arith/bound_manager.cpp
> src/tactic/arith/bv2real_rewriter.cpp
> src/tactic/arith/bv2int_rewriter.cpp
> src/tactic/arith/bound_propagator.cpp
> src/tactic/arith/diff_neq_tactic.cpp
> src/tactic/arith/lia2pb_tactic.cpp
> src/tactic/arith/card2bv_tactic.cpp
> src/tactic/arith/pb2bv_tactic.cpp
> src/tactic/arith/fix_dl_var_tactic.cpp
> src/tactic/arith/recover_01_tactic.cpp
> src/tactic/arith/elim01_tactic.cpp
> src/tactic/arith/linear_equation.cpp
> src/tactic/arith/add_bounds_tactic.cpp
> src/tactic/arith/nla2bv_tactic.cpp
> src/tactic/arith/degree_shift_tactic.cpp
> src/tactic/arith/probe_arith.cpp
> src/tactic/arith/normalize_bounds_tactic.cpp
> src/tactic/arith/eq2bv_tactic.cpp
> src/tactic/arith/fm_tactic.cpp
> src/tactic/arith/pb2bv_model_converter.cpp
> src/tactic/arith/propagate_ineqs_tactic.cpp
> src/tactic/arith/purify_arith_tactic.cpp
> src/sat/tactic/goal2sat.cpp
> src/sat/tactic/atom2bool_var.cpp
> src/sat/tactic/sat_tactic.cpp
> src/tactic/core/symmetry_reduce_tactic.cpp
> src/tactic/core/elim_uncnstr_tactic.cpp
> src/tactic/core/simplify_tactic.cpp
> src/tactic/core/nnf_tactic.cpp
> src/tactic/core/der_tactic.cpp
> src/tactic/core/reduce_args_tactic.cpp
> src/tactic/core/distribute_forall_tactic.cpp
> src/tactic/core/elim_term_ite_tactic.cpp
> src/tactic/core/cofactor_elim_term_ite.cpp
> src/tactic/core/ctx_simplify_tactic.cpp
> src/tactic/core/occf_tactic.cpp
> src/tactic/core/blast_term_ite_tactic.cpp
> src/tactic/core/propagate_values_tactic.cpp
> src/tactic/core/cofactor_term_ite_tactic.cpp
> src/tactic/core/split_clause_tactic.cpp
> src/tactic/core/solve_eqs_tactic.cpp
> src/tactic/core/pb_preprocess_tactic.cpp
> src/tactic/core/tseitin_cnf_tactic.cpp
> src/math/euclid/euclidean_solver.cpp
> src/math/grobner/grobner.cpp
> src/parsers/util/simple_parser.cpp
> src/parsers/util/scanner.cpp
> src/parsers/util/cost_parser.cpp
> src/parsers/util/pattern_validation.cpp
> src/ast/substitution/matcher.cpp
> src/ast/substitution/substitution.cpp
> src/ast/substitution/unifier.cpp
> src/ast/substitution/substitution_tree.cpp
> src/tactic/goal.cpp
> src/tactic/goal_shared_occs.cpp
> src/tactic/goal_num_occurs.cpp
> src/tactic/tactical.cpp
> src/tactic/proof_converter.cpp
> src/tactic/tactic.cpp
> src/tactic/horn_subsume_model_converter.cpp
> src/tactic/equiv_proof_converter.cpp
> src/tactic/extension_model_converter.cpp
> src/tactic/probe.cpp
> src/tactic/goal_util.cpp
> src/tactic/model_converter.cpp
> src/tactic/filter_model_converter.cpp
> src/tactic/replace_proof_converter.cpp
> src/model/func_interp.cpp
> src/model/model_implicant.cpp
> src/model/model2expr.cpp
> src/model/model_core.cpp
> src/model/model_v2_pp.cpp
> src/model/model_smt2_pp.cpp
> src/model/model_pp.cpp
> src/model/model.cpp
> src/model/model_evaluator.cpp
> src/ast/normal_forms/nnf.cpp
> src/ast/normal_forms/name_exprs.cpp
> src/ast/normal_forms/defined_names.cpp
> src/ast/normal_forms/pull_quant.cpp
> src/ast/rewriter/fpa_rewriter.cpp
> src/ast/rewriter/bool_rewriter.cpp
> src/ast/rewriter/factor_rewriter.cpp
> src/ast/rewriter/var_subst.cpp
> src/ast/rewriter/expr_safe_replace.cpp
> src/ast/rewriter/expr_replacer.cpp
> src/ast/rewriter/th_rewriter.cpp
> src/ast/rewriter/arith_rewriter.cpp
> src/ast/rewriter/ast_counter.cpp
> src/ast/rewriter/bv_rewriter.cpp
> src/ast/rewriter/rewriter.cpp
> src/ast/rewriter/array_rewriter.cpp
> src/ast/rewriter/quant_hoist.cpp
> src/ast/rewriter/dl_rewriter.cpp
> src/ast/rewriter/pb_rewriter.cpp
> src/ast/rewriter/mk_simplified_app.cpp
> src/ast/rewriter/der.cpp
> src/ast/rewriter/datatype_rewriter.cpp
> src/ast/func_decl_dependencies.cpp
> src/ast/ast_smt2_pp.cpp
> src/ast/shared_occs.cpp
> src/ast/has_free_vars.cpp
> src/ast/for_each_ast.cpp
> src/ast/ast_pp_util.cpp
> src/ast/expr_abstract.cpp
> src/ast/expr2var.cpp
> src/ast/format.cpp
> src/ast/expr_substitution.cpp
> src/ast/for_each_expr.cpp
> src/ast/num_occurs.cpp
> src/ast/bv_decl_plugin.cpp
> src/ast/dl_decl_plugin.cpp
> src/ast/datatype_decl_plugin.cpp
> src/ast/ast_util.cpp
> src/ast/ast_translation.cpp
> src/ast/macro_substitution.cpp
> src/ast/expr_map.cpp
> src/ast/expr_functors.cpp
> src/ast/used_vars.cpp
> src/ast/reg_decl_plugins.cpp
> src/ast/decl_collector.cpp
> src/ast/ast_smt_pp.cpp
> src/ast/arith_decl_plugin.cpp
> src/ast/seq_decl_plugin.cpp
> src/ast/pp.cpp
> src/ast/pb_decl_plugin.cpp
> src/ast/ast.cpp
> src/ast/ast_ll_pp.cpp
> src/ast/act_cache.cpp
> src/ast/well_sorted.cpp
> src/ast/expr_stat.cpp
> src/ast/ast_printer.cpp
> src/ast/ast_lt.cpp
> src/ast/array_decl_plugin.cpp
> src/ast/static_features.cpp
> src/ast/occurs.cpp
> src/ast/expr2polynomial.cpp
> src/ast/fpa_decl_plugin.cpp
> src/math/subpaving/subpaving.cpp
> src/math/subpaving/subpaving_mpfx.cpp
> src/math/subpaving/subpaving_mpf.cpp
> src/math/subpaving/subpaving_mpff.cpp
> src/math/subpaving/subpaving_hwf.cpp
> src/math/subpaving/subpaving_mpq.cpp
> src/math/realclosure/mpz_matrix.cpp
> src/math/realclosure/realclosure.cpp
> src/math/interval/interval_mpq.cpp
> src/math/simplex/simplex.cpp
> src/math/hilbert/hilbert_basis.cpp
> src/nlsat/nlsat_evaluator.cpp
> src/nlsat/nlsat_explain.cpp
> src/nlsat/nlsat_solver.cpp
> src/nlsat/nlsat_clause.cpp
> src/nlsat/nlsat_types.cpp
> src/nlsat/nlsat_interval_set.cpp
> src/sat/sat_integrity_checker.cpp
> src/sat/sat_elim_eqs.cpp
> src/sat/sat_config.cpp
> src/sat/sat_iff3_finder.cpp
> src/sat/sat_probing.cpp
> src/sat/sat_mus.cpp
> src/sat/dimacs.cpp
> src/sat/sat_cleaner.cpp
> src/sat/sat_simplifier.cpp
> src/sat/sat_clause_use_list.cpp
> src/sat/sat_clause.cpp
> src/sat/sat_solver.cpp
> src/sat/sat_scc.cpp
> src/sat/sat_model_converter.cpp
> src/sat/sat_clause_set.cpp
> src/sat/sat_bceq.cpp
> src/sat/sat_sls.cpp
> src/sat/sat_asymm_branch.cpp
> src/sat/sat_watched.cpp
> src/math/polynomial/polynomial_cache.cpp
> src/math/polynomial/upolynomial.cpp
> src/math/polynomial/sexpr2upolynomial.cpp
> src/math/polynomial/upolynomial_factorization.cpp
> src/math/polynomial/rpolynomial.cpp
> src/math/polynomial/polynomial_factorization.cpp
> src/math/polynomial/algebraic_numbers.cpp
> src/math/polynomial/polynomial.cpp
> src/util/util.cpp
> src/util/stack.cpp
> src/util/scoped_ctrl_c.cpp
> src/util/bit_util.cpp
> src/util/scoped_timer.cpp
> src/util/hash.cpp
> src/util/lbool.cpp
> src/util/sexpr.cpp
> src/util/fixed_bit_vector.cpp
> src/util/approx_set.cpp
> src/util/timer.cpp
> src/util/inf_rational.cpp
> src/util/common_msgs.cpp
> src/util/permutation.cpp
> src/util/small_object_allocator.cpp
> src/util/smt2_util.cpp
> src/util/mpz.cpp
> ../src/util/mpz.cpp: In instantiation of 'mpz_manager<SYNCH>::mpz_manager()
> [with bool SYNCH = true]':
> ../src/util/mpz.cpp:2073:16: required from here
> ../src/util/mpz.cpp:137:8: error: call of overloaded 'set(mpz&, long unsigned
> int)' is ambiguous
> set(m_two64, UINT64_MAX);
> ~~~^~~~~~~~~~~~~~~~~~~~~
> In file included from ../src/util/mpz.cpp:20:0:
> ../src/util/mpz.h:646:10: note: candidate: void mpz_manager<SYNCH>::set(mpz&,
> const mpz&) [with bool SYNCH = true]
> void set(mpz & target, mpz const & source) {
> ^~~
> ../src/util/mpz.h:658:10: note: candidate: void mpz_manager<SYNCH>::set(mpz&,
> int) [with bool SYNCH = true]
> void set(mpz & a, int val) {
> ^~~
> ../src/util/mpz.h:663:10: note: candidate: void mpz_manager<SYNCH>::set(mpz&,
> unsigned int) [with bool SYNCH = true]
> void set(mpz & a, unsigned val) {
> ^~~
> ../src/util/mpz.h:672:10: note: candidate: void mpz_manager<SYNCH>::set(mpz&,
> int64) [with bool SYNCH = true; int64 = long long int]
> void set(mpz & a, int64 val) {
> ^~~
> ../src/util/mpz.h:676:10: note: candidate: void mpz_manager<SYNCH>::set(mpz&,
> uint64) [with bool SYNCH = true; uint64 = long long unsigned int]
> void set(mpz & a, uint64 val) {
> ^~~
> ../src/util/mpz.cpp: In instantiation of 'mpz_manager<SYNCH>::mpz_manager()
> [with bool SYNCH = false]':
> ../src/util/mpz.cpp:2074:16: required from here
> ../src/util/mpz.cpp:137:8: error: call of overloaded 'set(mpz&, long unsigned
> int)' is ambiguous
> set(m_two64, UINT64_MAX);
> ~~~^~~~~~~~~~~~~~~~~~~~~
> In file included from ../src/util/mpz.cpp:20:0:
> ../src/util/mpz.h:646:10: note: candidate: void mpz_manager<SYNCH>::set(mpz&,
> const mpz&) [with bool SYNCH = false]
> void set(mpz & target, mpz const & source) {
> ^~~
> ../src/util/mpz.h:658:10: note: candidate: void mpz_manager<SYNCH>::set(mpz&,
> int) [with bool SYNCH = false]
> void set(mpz & a, int val) {
> ^~~
> ../src/util/mpz.h:663:10: note: candidate: void mpz_manager<SYNCH>::set(mpz&,
> unsigned int) [with bool SYNCH = false]
> void set(mpz & a, unsigned val) {
> ^~~
> ../src/util/mpz.h:672:10: note: candidate: void mpz_manager<SYNCH>::set(mpz&,
> int64) [with bool SYNCH = false; int64 = long long int]
> void set(mpz & a, int64 val) {
> ^~~
> ../src/util/mpz.h:676:10: note: candidate: void mpz_manager<SYNCH>::set(mpz&,
> uint64) [with bool SYNCH = false; uint64 = long long unsigned int]
> void set(mpz & a, uint64 val) {
> ^~~
> Makefile:141: recipe for target 'util/mpz.o' failed
> make[2]: *** [util/mpz.o] Error 1
The full build log is available from:
http://people.debian.org/~lucas/logs/2016/08/28/z3_4.4.1-0.2_unstable.log
A list of current common problems and possible solutions is available at
http://wiki.debian.org/qa.debian.org/FTBFS . You're welcome to contribute!
About the archive rebuild: The rebuild was done on EC2 VM instances from
Amazon Web Services, using a clean, minimal and up-to-date chroot. Every
failed build was retried once to eliminate random failures.
--- End Message ---
--- Begin Message ---
Source: z3
Source-Version: 4.4.1-0.3
We believe that the bug you reported is fixed in the latest version of
z3, which is due to be installed in the Debian FTP archive.
A summary of the changes between this version and the previous one is
attached.
Thank you for reporting the bug, which will now be closed. If you
have further comments please address them to 835...@bugs.debian.org,
and the maintainer will reopen the bug report if appropriate.
Debian distribution maintenance software
pp.
Gianfranco Costamagna <locutusofb...@debian.org> (supplier of updated z3
package)
(This message was generated automatically at their request; if you
believe that there is a problem with it please contact the archive
administrators by mailing ftpmas...@ftp-master.debian.org)
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA256
Format: 1.8
Date: Sun, 25 Sep 2016 23:06:24 +0200
Source: z3
Binary: z3 libz3-4 libz3-dev python-z3 libz3-cil libz3-ocaml-dev libz3-java
libz3-jni
Architecture: source
Version: 4.4.1-0.3
Distribution: unstable
Urgency: medium
Maintainer: Michael Tautschnig <m...@debian.org>
Changed-By: Gianfranco Costamagna <locutusofb...@debian.org>
Description:
libz3-4 - theorem prover from Microsoft Research - runtime libraries
libz3-cil - theorem prover from Microsoft Research - CLI bindings
libz3-dev - theorem prover from Microsoft Research - development files
libz3-java - theorem prover from Microsoft Research - java bindings
libz3-jni - theorem prover from Microsoft Research - JNI library
libz3-ocaml-dev - theorem prover from Microsoft Research - OCaml bindings
python-z3 - theorem prover from Microsoft Research - Python bindings
z3 - theorem prover from Microsoft Research
Closes: 835743 835754
Changes:
z3 (4.4.1-0.3) unstable; urgency=medium
.
* Non-maintainer upload.
.
[ Fabian Wolff ]
* debian/patches/f02d273ee39ae047222e362c37213d29135dc661.patch:
Fix build failure with new gnu++14 standard. (Closes: #835754)
* debian/patches/27399309009314f56cdfbd8333f287b1a9b7a3a6.patch:
Fix build failure with new compiler and clang. (Closes: #835743)
.
[ Gianfranco Costamagna ]
* debian/patches/fix-build.patch: tweak the casts a little bit
more to really fix 835743.
Checksums-Sha1:
2a36b942e4ad65148f9e788646c7d9bc896eb540 2787 z3_4.4.1-0.3.dsc
5e2e60e354b2445fb5e000bd8c7ed1063003ecad 14280 z3_4.4.1-0.3.debian.tar.xz
Checksums-Sha256:
8678a2d34717dc16b548411d8ae9083077b56743bd371a8cc40d797b34d6eda6 2787
z3_4.4.1-0.3.dsc
d3243ca3d0cd5edebecd1063ce7a9a51f912882b49a451ceb14dde35a6839d4d 14280
z3_4.4.1-0.3.debian.tar.xz
Files:
640f36384685da84d3c150675dc739cd 2787 science extra z3_4.4.1-0.3.dsc
c6bd61a8b4bc45a6f00021fc019f36de 14280 science extra z3_4.4.1-0.3.debian.tar.xz
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2
iQIcBAEBCAAGBQJX6LtfAAoJEPNPCXROn13ZmF4P/AljsPWLLfTDR0/kCnl2pm2F
xzBawtjh9+e9m8jdd3upUJeE6I5jVMlwaV3nu/k9Pembl2wyJLvE6LJH1VmtRTHv
PMSjr9CyKWIDSB3nNu8rHqMKh+RuaWr1BPlknLZajzHnuLY5kUSIw6cxuYcHrgrn
urxN3Wto/eXYEHmlkD7gYxGuG1CqTCMvena9kBKhkSp4zPWrTAixs15g3x92+NbE
RkECJJRcplRypi0Sbg2m0G9mm1AKfv/7U5MGja2WJkNI+aLIpTGoxNTmzMHDcyHb
6VzV6MJYXAMpnY2ab9VxvdrIu0Ha+Mm7ssP3L5rwdMGwaqft7U8M9YbtPO2235ft
LqKOOVQOBQPG0BtimYsEij1TisPezeE2XVRM8RrrbZOj4Szqc+7xsdQ5vuMJuyBg
VKTiPcz4lpjLED6EWemJQI/cH4nDAtIV+PvvrB5hn70aZ1yGsq4jgyvSa5iwYp/H
WU157Ngqd0uzC+131aq+JzQp99vzxbLCNMDX9IUlyw35RrIUh5LSYB4CUj+L7/un
xalWJmnHxcOJe6uIp9IEjUy/mfUrZJfbRUGwXT+tZIQwSXDdcg2s2hAGaif+d56q
Ai25QFKVRCUd6ZXpLcMtgnQOsf70QGtaZ95+TNcIPKJEIZQXQF+TzdbHA6SnSB0D
7KOKY6jsY2R4fqP6KAKX
=EjpS
-----END PGP SIGNATURE-----
--- End Message ---
