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.000000000 +0200
+++ z3-4.4.1/debian/changelog 2016-09-26 07:28:12.000000000 +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 <locutusofb...@debian.org> 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.000000000 +0100
+++ z3-4.4.1/debian/patches/27399309009314f56cdfbd8333f287b1a9b7a3a6.patch
2016-09-25 23:46:37.000000000 +0200
@@ -0,0 +1,23 @@
+From 27399309009314f56cdfbd8333f287b1a9b7a3a6 Mon Sep 17 00:00:00 2001
+From: Nuno Lopes <nlo...@microsoft.com>
+Date: Fri, 27 Nov 2015 12:13:44 +0000
+Subject: [PATCH] fix build with clang
+
+Signed-off-by: Nuno Lopes <nlo...@microsoft.com>
+---
+ 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<SYNCH>::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.000000000 +0100
+++ z3-4.4.1/debian/patches/f02d273ee39ae047222e362c37213d29135dc661.patch
2016-09-25 23:46:37.000000000 +0200
@@ -0,0 +1,23 @@
+From f02d273ee39ae047222e362c37213d29135dc661 Mon Sep 17 00:00:00 2001
+From: Jonathan Wakely <git...@kayari.org>
+Date: Tue, 2 Feb 2016 23:39:11 +0000
+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.000000000
+0100
+++ z3-4.4.1/debian/patches/fix-build.patch 2016-09-26 08:08:19.000000000
+0200
@@ -0,0 +1,53 @@
+Author: Gianfranco Costamagna <locutusofb...@debian.org>
+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>(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>(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>(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) {
+ scoped_mpff a(m), b(m), c(m);
+ m.round_to_plus_inf();
+ m.set(a, 1);
+- m.set(b, UINT64_MAX);
++ m.set(b, static_cast<uint64>(UINT64_MAX));
+ m.div(a, b, c);
+ m.display_raw(std::cout, a); std::cout << "\n";
+ m.display_raw(std::cout, b); std::cout << "\n";
+--- z3-4.4.1.orig/src/test/mpz.cpp
++++ z3-4.4.1/src/test/mpz.cpp
+@@ -280,7 +280,7 @@ void tst_int_min_bug() {
+ mpz big;
+ mpz expected;
+ mpz r;
+- m.set(big, UINT64_MAX);
++ m.set(big, static_cast<uint64>(UINT64_MAX));
+ m.set(expected, "18446744075857035263");
+ m.sub(big, intmin, r);
+ std::cout << "r: " << m.to_string(r) << "\nexpected: " <<
m.to_string(expected) << "\n";
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.000000000 +0200
+++ z3-4.4.1/debian/patches/series 2016-09-26 07:25:29.000000000 +0200
@@ -6,3 +6,6 @@
typos.patch
hardening.patch
kfreebsd.patch
+f02d273ee39ae047222e362c37213d29135dc661.patch
+27399309009314f56cdfbd8333f287b1a9b7a3a6.patch
+fix-build.patch
signature.asc
Description: OpenPGP digital signature
