Bug#835743: z3: FTBFS: ../src/util/mpz.cpp:137:8: error: call of overloaded 'set(mpz&, long unsigned int)' is ambiguous

2016-09-26 Thread Gianfranco Costamagna 
Hi,
> thanks for the patches!
> (feel free to ping directly in case of RC bug fixes if you need a sponsor!)
> 
at the end I'm uploading it with a new couple of casts (and patches forwarded 
upstream).

I hope I did the cast correctly, the build is fine now.


G.
diff -Nru z3-4.4.1/debian/changelog z3-4.4.1/debian/changelog
--- z3-4.4.1/debian/changelog   2016-07-20 13:07:58.0 +0200
+++ z3-4.4.1/debian/changelog   2016-09-26 07:28:12.0 +0200
@@ -1,3 +1,19 @@
+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.
+
+ -- Gianfranco Costamagna   Sun, 25 Sep 2016 
23:06:24 +0200
+
 z3 (4.4.1-0.2) unstable; urgency=medium
 
   * Non-maintainer upload.
diff -Nru 
z3-4.4.1/debian/patches/27399309009314f56cdfbd8333f287b1a9b7a3a6.patch 
z3-4.4.1/debian/patches/27399309009314f56cdfbd8333f287b1a9b7a3a6.patch
--- z3-4.4.1/debian/patches/27399309009314f56cdfbd8333f287b1a9b7a3a6.patch  
1970-01-01 01:00:00.0 +0100
+++ z3-4.4.1/debian/patches/27399309009314f56cdfbd8333f287b1a9b7a3a6.patch  
2016-09-25 23:46:37.0 +0200
@@ -0,0 +1,23 @@
+From 27399309009314f56cdfbd8333f287b1a9b7a3a6 Mon Sep 17 00:00:00 2001
+From: Nuno Lopes 
+Date: Fri, 27 Nov 2015 12:13:44 +
+Subject: [PATCH] fix build with clang
+
+Signed-off-by: Nuno Lopes 
+---
+ src/util/mpz.cpp | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
+index 8559279..7dca14b 100644
+--- a/src/util/mpz.cpp
 b/src/util/mpz.cpp
+@@ -134,7 +134,7 @@ mpz_manager::mpz_manager():
+ #endif
+ 
+ mpz one(1);
+-set(m_two64, UINT64_MAX);
++set(m_two64, (uint64)UINT64_MAX);
+ add(m_two64, one, m_two64);
+ }
+ 
diff -Nru 
z3-4.4.1/debian/patches/f02d273ee39ae047222e362c37213d29135dc661.patch 
z3-4.4.1/debian/patches/f02d273ee39ae047222e362c37213d29135dc661.patch
--- z3-4.4.1/debian/patches/f02d273ee39ae047222e362c37213d29135dc661.patch  
1970-01-01 01:00:00.0 +0100
+++ z3-4.4.1/debian/patches/f02d273ee39ae047222e362c37213d29135dc661.patch  
2016-09-25 23:46:37.0 +0200
@@ -0,0 +1,23 @@
+From f02d273ee39ae047222e362c37213d29135dc661 Mon Sep 17 00:00:00 2001
+From: Jonathan Wakely 
+Date: Tue, 2 Feb 2016 23:39:11 +
+Subject: [PATCH] Convert stream to bool explicitly
+
+In C++11 there is no implicit conversion from iostream classes to `void*`, 
just an explicit conversion to bool.
+---
+ src/util/debug.cpp | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/src/util/debug.cpp b/src/util/debug.cpp
+index 54c67fe..66676c6 100644
+--- a/src/util/debug.cpp
 b/src/util/debug.cpp
+@@ -76,7 +76,7 @@ void invoke_gdb() {
+ for (;;) {
+ std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke 
(G)DB\n";
+ char result;
+-bool ok = (std::cin >> result);
++bool ok = bool(std::cin >> result);
+ if (!ok) exit(ERR_INTERNAL_FATAL); // happens if std::cin is eof or 
unattached.
+ switch(result) {
+ case 'C':
diff -Nru z3-4.4.1/debian/patches/fix-build.patch 
z3-4.4.1/debian/patches/fix-build.patch
--- z3-4.4.1/debian/patches/fix-build.patch 1970-01-01 01:00:00.0 
+0100
+++ z3-4.4.1/debian/patches/fix-build.patch 2016-09-26 08:08:19.0 
+0200
@@ -0,0 +1,53 @@
+Author: Gianfranco Costamagna 
+Description: Add some more casts to fix the build (Bug: #835743)
+Forwarded: https://github.com/Z3Prover/z3/pull/746
+   https://github.com/Z3Prover/z3/pull/747
+--- z3-4.4.1.orig/src/test/mpff.cpp
 z3-4.4.1/src/test/mpff.cpp
+@@ -207,7 +207,7 @@ static void tst_set64(unsigned N, unsign
+ mpff_manager fm(prec);
+ scoped_mpff a(fm);
+ 
+-fm.set(a, INT64_MAX);
++fm.set(a, static_cast(INT64_MAX));
+ SASSERT(fm.is_int64(a));
+ SASSERT(fm.is_uint64(a));
+ fm.inc(a);
+@@ -221,7 +221,7 @@ static void tst_set64(unsigned N, unsign
+ SASSERT(fm.is_int64(a));
+ SASSERT(fm.is_uint64(a));
+ 
+-fm.set(a, INT64_MIN);
++fm.set(a, static_cast(INT64_MIN));
+ SASSERT(fm.is_int64(a));
+ SASSERT(!fm.is_uint64(a));
+ fm.dec(a);
+@@ -235,7 +235,7 @@ static void tst_set64(unsigned N, unsign
+ SASSERT(fm.is_int64(a));
+ SASSERT(!fm.is_uint64(a));
+ 
+-fm.set(a, UINT64_MAX);
++fm.set(a, static_cast(UINT64_MAX));
+ SASSERT(fm.is_uint64(a));
+ SASSERT(!fm.is_int64(a));
+ fm.inc(a);
+@@ -600,7 +600,7 @@ static void tst_div(unsigned prec) {
+

Bug#835743: z3: FTBFS: ../src/util/mpz.cpp:137:8: error: call of overloaded 'set(mpz&, long unsigned int)' is ambiguous

2016-09-25 Thread Gianfranco Costamagna 
Control: tags -1 +pending
On Wed, 14 Sep 2016 18:20:38 +0200 Fabian Wolff  wrote:
> Control: tags -1 + upstream patch fixed-upstream
> 

Hi,

the following debdiff is being build-tested and uploaded on deferred/2

thanks for the patches!
(feel free to ping directly in case of RC bug fixes if you need a sponsor!)

Gianfranco
diff -Nru z3-4.4.1/debian/changelog z3-4.4.1/debian/changelog
--- z3-4.4.1/debian/changelog   2016-07-20 13:07:58.0 +0200
+++ z3-4.4.1/debian/changelog   2016-09-25 23:09:40.0 +0200
@@ -1,3 +1,15 @@
+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   Sun, 25 Sep 2016 
23:06:24 +0200
+
 z3 (4.4.1-0.2) unstable; urgency=medium
 
   * Non-maintainer upload.
diff -Nru 
z3-4.4.1/debian/patches/27399309009314f56cdfbd8333f287b1a9b7a3a6.patch 
z3-4.4.1/debian/patches/27399309009314f56cdfbd8333f287b1a9b7a3a6.patch
--- z3-4.4.1/debian/patches/27399309009314f56cdfbd8333f287b1a9b7a3a6.patch  
1970-01-01 01:00:00.0 +0100
+++ z3-4.4.1/debian/patches/27399309009314f56cdfbd8333f287b1a9b7a3a6.patch  
2016-09-25 23:10:20.0 +0200
@@ -0,0 +1,23 @@
+From 27399309009314f56cdfbd8333f287b1a9b7a3a6 Mon Sep 17 00:00:00 2001
+From: Nuno Lopes 
+Date: Fri, 27 Nov 2015 12:13:44 +
+Subject: [PATCH] fix build with clang
+
+Signed-off-by: Nuno Lopes 
+---
+ src/util/mpz.cpp | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
+index 8559279..7dca14b 100644
+--- a/src/util/mpz.cpp
 b/src/util/mpz.cpp
+@@ -134,7 +134,7 @@ mpz_manager::mpz_manager():
+ #endif
+ 
+ mpz one(1);
+-set(m_two64, UINT64_MAX);
++set(m_two64, (uint64)UINT64_MAX);
+ add(m_two64, one, m_two64);
+ }
+ 
diff -Nru 
z3-4.4.1/debian/patches/f02d273ee39ae047222e362c37213d29135dc661.patch 
z3-4.4.1/debian/patches/f02d273ee39ae047222e362c37213d29135dc661.patch
--- z3-4.4.1/debian/patches/f02d273ee39ae047222e362c37213d29135dc661.patch  
1970-01-01 01:00:00.0 +0100
+++ z3-4.4.1/debian/patches/f02d273ee39ae047222e362c37213d29135dc661.patch  
2016-09-25 23:10:14.0 +0200
@@ -0,0 +1,23 @@
+From f02d273ee39ae047222e362c37213d29135dc661 Mon Sep 17 00:00:00 2001
+From: Jonathan Wakely 
+Date: Tue, 2 Feb 2016 23:39:11 +
+Subject: [PATCH] Convert stream to bool explicitly
+
+In C++11 there is no implicit conversion from iostream classes to `void*`, 
just an explicit conversion to bool.
+---
+ src/util/debug.cpp | 2 +-
+ 1 file changed, 1 insertion(+), 1 deletion(-)
+
+diff --git a/src/util/debug.cpp b/src/util/debug.cpp
+index 54c67fe..66676c6 100644
+--- a/src/util/debug.cpp
 b/src/util/debug.cpp
+@@ -76,7 +76,7 @@ void invoke_gdb() {
+ for (;;) {
+ std::cerr << "(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke 
(G)DB\n";
+ char result;
+-bool ok = (std::cin >> result);
++bool ok = bool(std::cin >> result);
+ if (!ok) exit(ERR_INTERNAL_FATAL); // happens if std::cin is eof or 
unattached.
+ switch(result) {
+ case 'C':
diff -Nru z3-4.4.1/debian/patches/series z3-4.4.1/debian/patches/series
--- z3-4.4.1/debian/patches/series  2016-07-20 13:07:58.0 +0200
+++ z3-4.4.1/debian/patches/series  2016-09-25 23:08:44.0 +0200
@@ -6,3 +6,5 @@
 typos.patch
 hardening.patch
 kfreebsd.patch
+f02d273ee39ae047222e362c37213d29135dc661.patch
+27399309009314f56cdfbd8333f287b1a9b7a3a6.patch


signature.asc
Description: OpenPGP digital signature

Bug#835743: z3: FTBFS: ../src/util/mpz.cpp:137:8: error: call of overloaded 'set(mpz&, long unsigned int)' is ambiguous

2016-09-14 Thread Fabian Wolff 
Control: tags -1 + upstream patch fixed-upstream

Hi,

the following patch fixes this issue:

--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -134,7 +134,7 @@
 #endif
 
 mpz one(1);
-set(m_two64, UINT64_MAX);
+set(m_two64, static_cast(UINT64_MAX));
 add(m_two64, one, m_two64);
 }
 

The problem has already been fixed in the upstream repository by this commit:

  https://github.com/Z3Prover/z3/commit/27399309009314f56cdfbd8333f287b1a9b7a3a6

Kind regards,
Fabian

Bug#835743: z3: FTBFS: ../src/util/mpz.cpp:137:8: error: call of overloaded 'set(mpz&, long unsigned int)' is ambiguous

2016-08-28 Thread Lucas Nussbaum 
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 '/<>/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
>