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

+--- 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 */

var/spack/repos/builtin/packages/z3/fix_1016_2.patch

+--- 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 */

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'