From 94c9e5f9a0ea307f0922afb84ee6ca07103a7029 Mon Sep 17 00:00:00 2001
From: t-karatsu <49965247+t-karatsu@users.noreply.github.com>
Date: Fri, 15 Nov 2019 07:28:05 +0900
Subject: [PATCH] z3: bugfix about python dependency and fallthrough
 annotation. (#13713)

* z3:

* Fixed python dependency to always be required.

* bugfix about fallthrough annotation.

* z3: Add patch for before ver.4.4.1.

* Update var/spack/repos/builtin/packages/z3/package.py

Co-Authored-By: Adam J. Stewart <ajstewart426@gmail.com>
---
 var/spack/repos/builtin/packages/z3/fix_1016_1.patch | 12 ++++++++++++
 var/spack/repos/builtin/packages/z3/fix_1016_2.patch | 12 ++++++++++++
 var/spack/repos/builtin/packages/z3/package.py       |  8 ++++++--
 3 files changed, 30 insertions(+), 2 deletions(-)
 create mode 100644 var/spack/repos/builtin/packages/z3/fix_1016_1.patch
 create mode 100644 var/spack/repos/builtin/packages/z3/fix_1016_2.patch

diff --git a/var/spack/repos/builtin/packages/z3/fix_1016_1.patch b/var/spack/repos/builtin/packages/z3/fix_1016_1.patch
new file mode 100644
index 0000000000..181fa96035
--- /dev/null
+++ b/var/spack/repos/builtin/packages/z3/fix_1016_1.patch
@@ -0,0 +1,12 @@
+--- spack-src/src/util/hash.cpp.org	2019-11-14 11:12:11.233379342 +0900
++++ spack-src/src/util/hash.cpp	2019-11-14 11:15:51.356519168 +0900
+@@ -75,8 +75,8 @@
+         __fallthrough;
+     case 1 : 
+         a+=str[0];
+-        __fallthrough;
+         /* case 0: nothing left to add */
++        break;
+     }
+     mix(a,b,c);
+     /*-------------------------------------------- report the result */
diff --git a/var/spack/repos/builtin/packages/z3/fix_1016_2.patch b/var/spack/repos/builtin/packages/z3/fix_1016_2.patch
new file mode 100644
index 0000000000..95eccbf8cd
--- /dev/null
+++ b/var/spack/repos/builtin/packages/z3/fix_1016_2.patch
@@ -0,0 +1,12 @@
+--- spack-src/src/util/hash.cpp.org	2019-11-13 13:25:33.317336437 +0900
++++ spack-src/src/util/hash.cpp	2019-11-13 13:26:12.671491961 +0900
+@@ -83,8 +83,8 @@
+         Z3_fallthrough;
+     case 1 : 
+         a+=str[0];
+-        Z3_fallthrough;
+         /* case 0: nothing left to add */
++        break;
+     }
+     mix(a,b,c);
+     /*-------------------------------------------- report the result */
diff --git a/var/spack/repos/builtin/packages/z3/package.py b/var/spack/repos/builtin/packages/z3/package.py
index b558fa010f..1f166ce54c 100644
--- a/var/spack/repos/builtin/packages/z3/package.py
+++ b/var/spack/repos/builtin/packages/z3/package.py
@@ -20,8 +20,12 @@ class Z3(MakefilePackage):
 
     phases = ['bootstrap', 'build', 'install']
 
-    variant('python', default=False, description='Enable python support')
-    depends_on('python', when='+python')
+    variant('python', default=False, description='Enable python binding')
+    depends_on('python', type=('build', 'run'))
+
+    # Referenced: https://github.com/Z3Prover/z3/issues/1016
+    patch('fix_1016_1.patch', when='@:4.4.1')
+    patch('fix_1016_2.patch', when='@4.5.0')
 
     build_directory = 'build'
 
-- 
GitLab