Version 4.15.8

- Make the doc subpackage noarch again

sources

@@ -1 +1 @@
-SHA512 (z3-4.15.4.tar.gz) = 3037a6c9077cf5b5bbc9db89973311e66233144ad6c8fc8da9fb2aa35bb34944068874868cf571b247130251a8361cbd1e24288768cc49e4166985cf0ca921a2
+SHA512 (z3-4.15.8.tar.gz) = e31df90b0edb3fd4a49a1069d78135d03c6b196c2bc8359a67273e02eba7214a7ff8654488f076ce7a0cf6edffdff9afc403799db3a6e5a1585a6d4c99c4df2a

z3-s390x-doc.patch

@@ -0,0 +1,505 @@
+--- a/doc/api/html/z3.z3core.html
++++ b/doc/api/html/z3.z3core.html
+@@ -277,13 +277,21 @@ Data descriptors defined here:<br>
+     a3,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_ast_map_keys"><strong>Z3_ast_map_keys</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_ast_map_keys"><strong>Z3_ast_map_keys</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_ast_map_reset"><strong>Z3_ast_map_reset</strong></a>(
+     a0,
+     a1,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_ast_map_size"><strong>Z3_ast_map_size</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_ast_map_size"><strong>Z3_ast_map_size</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_ast_map_to_string"><strong>Z3_ast_map_to_string</strong></a>(
+     a0,
+     a1,
+@@ -833,7 +841,11 @@ Data descriptors defined here:<br>
+     a2,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_get_app_decl"><strong>Z3_get_app_decl</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_get_app_decl"><strong>Z3_get_app_decl</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_get_app_num_args"><strong>Z3_get_app_num_args</strong></a>(
+     a0,
+     a1,
+@@ -866,9 +878,17 @@ Data descriptors defined here:<br>
+     a1,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_get_ast_hash"><strong>Z3_get_ast_hash</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_get_ast_hash"><strong>Z3_get_ast_hash</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_get_ast_id"><strong>Z3_get_ast_id</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_get_ast_kind"><strong>Z3_get_ast_kind</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_get_ast_kind"><strong>Z3_get_ast_kind</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_get_bool_value"><strong>Z3_get_bool_value</strong></a>(
+     a0,
+     a1,
+@@ -1347,7 +1367,11 @@ Data descriptors defined here:<br>
+     a2,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_goal_dec_ref"><strong>Z3_goal_dec_ref</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_goal_dec_ref"><strong>Z3_goal_dec_ref</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_goal_depth"><strong>Z3_goal_depth</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+  <dl><dt><a name="-Z3_goal_formula"><strong>Z3_goal_formula</strong></a>(
+     a0,
+@@ -1355,7 +1379,11 @@ Data descriptors defined here:<br>
+     a2,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_goal_inc_ref"><strong>Z3_goal_inc_ref</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_goal_inc_ref"><strong>Z3_goal_inc_ref</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_goal_inconsistent"><strong>Z3_goal_inconsistent</strong></a>(
+     a0,
+     a1,
+@@ -1420,7 +1448,11 @@ Data descriptors defined here:<br>
+ )</dt></dl>
+  <dl><dt><a name="-Z3_is_app"><strong>Z3_is_app</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+  <dl><dt><a name="-Z3_is_as_array"><strong>Z3_is_as_array</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_is_char_sort"><strong>Z3_is_char_sort</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_is_char_sort"><strong>Z3_is_char_sort</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_is_eq_ast"><strong>Z3_is_eq_ast</strong></a>(
+     a0,
+     a1,
+@@ -1532,7 +1564,12 @@ Data descriptors defined here:<br>
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+  <dl><dt><a name="-Z3_mk_bool_sort"><strong>Z3_mk_bool_sort</strong></a>(a0, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_mk_bound"><strong>Z3_mk_bound</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bound"><strong>Z3_mk_bound</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_bv2int"><strong>Z3_mk_bv2int</strong></a>(
+     a0,
+     a1,
+@@ -1546,7 +1583,12 @@ Data descriptors defined here:<br>
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+  <dl><dt><a name="-Z3_mk_bv_sort"><strong>Z3_mk_bv_sort</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvadd"><strong>Z3_mk_bvadd</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvadd"><strong>Z3_mk_bvadd</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_bvadd_no_overflow"><strong>Z3_mk_bvadd_no_overflow</strong></a>(
+     a0,
+     a1,
+@@ -1560,7 +1602,12 @@ Data descriptors defined here:<br>
+     a2,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvand"><strong>Z3_mk_bvand</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvand"><strong>Z3_mk_bvand</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_bvashr"><strong>Z3_mk_bvashr</strong></a>(
+     a0,
+     a1,
+@@ -1573,7 +1620,12 @@ Data descriptors defined here:<br>
+     a2,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvmul"><strong>Z3_mk_bvmul</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvmul"><strong>Z3_mk_bvmul</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_bvmul_no_overflow"><strong>Z3_mk_bvmul_no_overflow</strong></a>(
+     a0,
+     a1,
+@@ -1599,7 +1651,12 @@ Data descriptors defined here:<br>
+     a1,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvnor"><strong>Z3_mk_bvnor</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvnor"><strong>Z3_mk_bvnor</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_bvnot"><strong>Z3_mk_bvnot</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+  <dl><dt><a name="-Z3_mk_bvor"><strong>Z3_mk_bvor</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+  <dl><dt><a name="-Z3_mk_bvredand"><strong>Z3_mk_bvredand</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+@@ -1616,11 +1673,36 @@ Data descriptors defined here:<br>
+     a2,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvsge"><strong>Z3_mk_bvsge</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvsgt"><strong>Z3_mk_bvsgt</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvshl"><strong>Z3_mk_bvshl</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvsle"><strong>Z3_mk_bvsle</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvslt"><strong>Z3_mk_bvslt</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvsge"><strong>Z3_mk_bvsge</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvsgt"><strong>Z3_mk_bvsgt</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvshl"><strong>Z3_mk_bvshl</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvsle"><strong>Z3_mk_bvsle</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvslt"><strong>Z3_mk_bvslt</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_bvsmod"><strong>Z3_mk_bvsmod</strong></a>(
+     a0,
+     a1,
+@@ -1633,7 +1715,12 @@ Data descriptors defined here:<br>
+     a2,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvsub"><strong>Z3_mk_bvsub</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvsub"><strong>Z3_mk_bvsub</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_bvsub_no_overflow"><strong>Z3_mk_bvsub_no_overflow</strong></a>(
+     a0,
+     a1,
+@@ -1653,10 +1740,30 @@ Data descriptors defined here:<br>
+     a2,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvuge"><strong>Z3_mk_bvuge</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvugt"><strong>Z3_mk_bvugt</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvule"><strong>Z3_mk_bvule</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvult"><strong>Z3_mk_bvult</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvuge"><strong>Z3_mk_bvuge</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvugt"><strong>Z3_mk_bvugt</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvule"><strong>Z3_mk_bvule</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvult"><strong>Z3_mk_bvult</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_bvurem"><strong>Z3_mk_bvurem</strong></a>(
+     a0,
+     a1,
+@@ -1669,7 +1776,12 @@ Data descriptors defined here:<br>
+     a2,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_mk_bvxor"><strong>Z3_mk_bvxor</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_bvxor"><strong>Z3_mk_bvxor</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_char"><strong>Z3_mk_char</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+  <dl><dt><a name="-Z3_mk_char_from_bv"><strong>Z3_mk_char_from_bv</strong></a>(
+     a0,
+@@ -1705,7 +1817,12 @@ Data descriptors defined here:<br>
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+  <dl><dt><a name="-Z3_mk_config"><strong>Z3_mk_config</strong></a>(_elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_mk_const"><strong>Z3_mk_const</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_const"><strong>Z3_mk_const</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_const_array"><strong>Z3_mk_const_array</strong></a>(
+     a0,
+     a1,
+@@ -1765,7 +1882,11 @@ Data descriptors defined here:<br>
+     a2,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_mk_empty_set"><strong>Z3_mk_empty_set</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_empty_set"><strong>Z3_mk_empty_set</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_enumeration_sort"><strong>Z3_mk_enumeration_sort</strong></a>(
+     a0,
+     a1,
+@@ -2056,7 +2177,10 @@ Data descriptors defined here:<br>
+     a0,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_mk_fpa_sort_half"><strong>Z3_mk_fpa_sort_half</strong></a>(a0, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_fpa_sort_half"><strong>Z3_mk_fpa_sort_half</strong></a>(
++    a0,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_fpa_sort_quadruple"><strong>Z3_mk_fpa_sort_quadruple</strong></a>(
+     a0,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+@@ -2197,7 +2321,12 @@ Data descriptors defined here:<br>
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+  <dl><dt><a name="-Z3_mk_int2real"><strong>Z3_mk_int2real</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_mk_int64"><strong>Z3_mk_int64</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_int64"><strong>Z3_mk_int64</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_int_sort"><strong>Z3_mk_int_sort</strong></a>(a0, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+  <dl><dt><a name="-Z3_mk_int_symbol"><strong>Z3_mk_int_symbol</strong></a>(
+     a0,
+@@ -2333,7 +2462,12 @@ Data descriptors defined here:<br>
+     a5,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_mk_power"><strong>Z3_mk_power</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_power"><strong>Z3_mk_power</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_probe"><strong>Z3_mk_probe</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+  <dl><dt><a name="-Z3_mk_quantifier"><strong>Z3_mk_quantifier</strong></a>(
+     a0,
+@@ -2426,7 +2560,11 @@ Data descriptors defined here:<br>
+     a3,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_mk_re_option"><strong>Z3_mk_re_option</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_re_option"><strong>Z3_mk_re_option</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_re_plus"><strong>Z3_mk_re_plus</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+  <dl><dt><a name="-Z3_mk_re_power"><strong>Z3_mk_re_power</strong></a>(
+     a0,
+@@ -2520,7 +2658,11 @@ Data descriptors defined here:<br>
+     a2,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_mk_seq_empty"><strong>Z3_mk_seq_empty</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_seq_empty"><strong>Z3_mk_seq_empty</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_seq_extract"><strong>Z3_mk_seq_extract</strong></a>(
+     a0,
+     a1,
+@@ -2627,7 +2769,11 @@ Data descriptors defined here:<br>
+     a2,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_mk_seq_to_re"><strong>Z3_mk_seq_to_re</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_seq_to_re"><strong>Z3_mk_seq_to_re</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_seq_unit"><strong>Z3_mk_seq_unit</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+  <dl><dt><a name="-Z3_mk_set_add"><strong>Z3_mk_set_add</strong></a>(
+     a0,
+@@ -2683,7 +2829,10 @@ Data descriptors defined here:<br>
+     a2,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_mk_simple_solver"><strong>Z3_mk_simple_solver</strong></a>(a0, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_mk_simple_solver"><strong>Z3_mk_simple_solver</strong></a>(
++    a0,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_mk_simplifier"><strong>Z3_mk_simplifier</strong></a>(
+     a0,
+     a1,
+@@ -3052,7 +3201,11 @@ Data descriptors defined here:<br>
+     a2,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_optimize_pop"><strong>Z3_optimize_pop</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_optimize_pop"><strong>Z3_optimize_pop</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_optimize_push"><strong>Z3_optimize_push</strong></a>(
+     a0,
+     a1,
+@@ -3288,8 +3441,18 @@ Data descriptors defined here:<br>
+     a1,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_probe_eq"><strong>Z3_probe_eq</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_probe_ge"><strong>Z3_probe_ge</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_probe_eq"><strong>Z3_probe_eq</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
++ <dl><dt><a name="-Z3_probe_ge"><strong>Z3_probe_ge</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_probe_get_descr"><strong>Z3_probe_get_descr</strong></a>(
+     a0,
+     a1,
+@@ -3300,16 +3463,36 @@ Data descriptors defined here:<br>
+     a1,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_probe_gt"><strong>Z3_probe_gt</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_probe_gt"><strong>Z3_probe_gt</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_probe_inc_ref"><strong>Z3_probe_inc_ref</strong></a>(
+     a0,
+     a1,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_probe_le"><strong>Z3_probe_le</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_probe_lt"><strong>Z3_probe_lt</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_probe_le"><strong>Z3_probe_le</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
++ <dl><dt><a name="-Z3_probe_lt"><strong>Z3_probe_lt</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_probe_not"><strong>Z3_probe_not</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_probe_or"><strong>Z3_probe_or</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_probe_or"><strong>Z3_probe_or</strong></a>(
++    a0,
++    a1,
++    a2,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_qe_lite"><strong>Z3_qe_lite</strong></a>(a0, a1, a2, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+  <dl><dt><a name="-Z3_qe_model_project"><strong>Z3_qe_model_project</strong></a>(
+     a0,
+@@ -3605,7 +3788,11 @@ Data descriptors defined here:<br>
+     a3,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_solver_check"><strong>Z3_solver_check</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_solver_check"><strong>Z3_solver_check</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_solver_check_assumptions"><strong>Z3_solver_check_assumptions</strong></a>(
+     a0,
+     a1,
+@@ -3862,7 +4049,11 @@ Data descriptors defined here:<br>
+     a3,
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+- <dl><dt><a name="-Z3_solver_reset"><strong>Z3_solver_reset</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_solver_reset"><strong>Z3_solver_reset</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_solver_set_initial_value"><strong>Z3_solver_set_initial_value</strong></a>(
+     a0,
+     a1,
+@@ -4118,7 +4309,11 @@ Data descriptors defined here:<br>
+     _elems=&lt;z3.z3core.Elementaries object&gt;
+ )</dt></dl>
+  <dl><dt><a name="-Z3_to_app"><strong>Z3_to_app</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
+- <dl><dt><a name="-Z3_to_func_decl"><strong>Z3_to_func_decl</strong></a>(a0, a1, _elems=&lt;z3.z3core.Elementaries object&gt;)</dt></dl>
++ <dl><dt><a name="-Z3_to_func_decl"><strong>Z3_to_func_decl</strong></a>(
++    a0,
++    a1,
++    _elems=&lt;z3.z3core.Elementaries object&gt;
++)</dt></dl>
+  <dl><dt><a name="-Z3_toggle_warning_messages"><strong>Z3_toggle_warning_messages</strong></a>(
+     a0,
+     _elems=&lt;z3.z3core.Elementaries object&gt;

z3.spec

@@ -11,19 +11,22 @@
 # the koji builders have available.
 %bcond test 0
 
-%global giturl  https://github.com/Z3Prover/z3
-
 Name:           z3
-Version:        4.15.4
+Version:        4.15.8
 Release:        %autorelease
 Summary:        Satisfiability Modulo Theories (SMT) solver
 
+%global giturl  https://github.com/Z3Prover/z3
+%global majver  %{gsub %version ^(%d*%.%d*)%..*$ %1}
+
 License:        MIT
 URL:            https://github.com/Z3Prover/z3/wiki
 VCS :           git:%{giturl}.git
 Source:         %{giturl}/archive/%{name}-%{version}.tar.gz
 # Do not try to build or install native OCaml artifacts on bytecode-only arches
 Patch:          %{name}-ocaml.patch
+# Fix up the s390x docs so they look like other arches
+Patch:          %{name}-s390x-doc.patch
 
 # See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval
 ExcludeArch:    %{ix86}
@@ -74,37 +77,19 @@ Header files for building applications that use z3.
 # examples/tptp/tptp5.tab.c
 # examples/tptp/tptp5.tab.c
 # Other licenses are due to files installed by doxygen.
-# html/bc_s.png: GPL-1.0-or-later
-# html/bdwn.png: GPL-1.0-or-later
-# html/closed.png: GPL-1.0-or-later
-# html/doc.png: GPL-1.0-or-later
+# html/clipboard.js: MIT
+# html/cookie.js: MIT
 # html/doxygen.css: GPL-1.0-or-later
 # html/doxygen.svg: GPL-1.0-or-later
 # html/dynsections.js: MIT
-# html/folderclosed.png: GPL-1.0-or-later
-# html/folderopen.png: GPL-1.0-or-later
 # html/jquery.js: MIT
-# html/nav_f.png: GPL-1.0-or-later
-# html/nav_g.png: GPL-1.0-or-later
-# html/nav_h.png: GPL-1.0-or-later
-# html/open.png: GPL-1.0-or-later
+# html/navtree.css: GPL-1.0-or-later
 # html/search/search.css: GPL-1.0-or-later
 # html/search/search.js: MIT
-# html/search/search_l.png: GPL-1.0-or-later
-# html/search/search_m.png: GPL-1.0-or-later
-# html/search/search_r.png: GPL-1.0-or-later
-# html/splitbar.png: GPL-1.0-or-later
-# html/sync_off.png: GPL-1.0-or-later
-# html/sync_on.png: GPL-1.0-or-later
-# html/tab_a.png: GPL-1.0-or-later
-# html/tab_b.png: GPL-1.0-or-later
-# html/tab_h.png: GPL-1.0-or-later
-# html/tab_s.png: GPL-1.0-or-later
 # html/tabs.css: GPL-1.0-or-later
 License:        MIT AND GPL-3.0-or-later WITH Bison-exception-2.2 AND GPL-1.0-or-later
 Summary:        API documentation for Z3
-# FIXME: this should be noarch, but we end up with different numbers of inheritance
-# graphs on different architectures.  Why?
+BuildArch:      noarch
 
 %description doc
 API documentation for Z3.
@@ -149,7 +134,7 @@ Python 3 interface to z3.
 %prep
 %autosetup -N -n %{name}-%{name}-%{version}
 %ifnarch %{ocaml_native_compiler}
-%patch -P0 -p1
+%patch 0 -p1
 %endif
 
 %conf
@@ -167,9 +152,8 @@ sed \
   -i scripts/mk_util.py
 
 # Comply with the Java packaging guidelines and fill in the version for python
-majver=$(cut -d. -f-2 <<< %{version})
 sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so"),' \
-    -e "s/'so'/'so.$majver'/" \
+    -e "s/'so'/'so.%{majver}'/" \
     -i scripts/update_api.py
 
 # Turn off HTML timestamps for reproducible builds
@@ -192,6 +176,19 @@ export PYTHON=%{python3}
 
 %cmake_build
 
+# Remove meaningless memory addresses from the pydoc documentation
+# See https://github.com/python/cpython/issues/83572
+sed -ri 's/, handle [0-9a-fA-F]+//' \
+    %{_vpath_builddir}/doc/api/html/z3{,.z3{,num,poly,printer,rcf,util}}.html
+sed -ri 's/ at 0x[0-9a-fA-F]+//g' \
+    %{_vpath_builddir}/doc/api/html/z3.z3core.html
+# For unknown reasons, the s390x documentation build has fewer newlines than
+# the builds on other architectures.  Make the outputs match so the doc
+# package can be noarch.
+%ifarch s390x
+patch -p1 -T -d %{_vpath_builddir} < %{PATCH1}
+%endif
+
 # The cmake build system does not build the OCaml interface.  Do that manually.
 #
 # First, run the configure script to generate several files.