Version 5.1.0

- Drop s390x doc workaround

sources

@@ -1 +1 @@
-SHA512 (z3-4.16.0.tar.gz) = 7dbcdd04a72f46bc3b6cbac2453b2a43f5ae126287b878ffe37f0573f910a1130c474c5edfa622dab09957f106cf425ab0f7cdfd34d41658599ad50a81ae39dd
+SHA512 (z3-5.1.0.tar.gz) = 03a854f720a56484ab99b8a5517150f1c9106400f54ad758cfa58e3ee2f95e349396a64d4f527a5bb9ee37f10ad9ecfa1916d1f5c921f04089deda409374491b

z3-s390x-doc.patch

@@ -1,505 +0,0 @@
---- 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

@@ -15,7 +15,7 @@
 %bcond test 0
 
 Name:           z3
-Version:        4.16.0
+Version:        5.1.0
 Release:        %autorelease
 Summary:        Satisfiability Modulo Theories (SMT) solver
 
@@ -28,13 +28,22 @@ 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}
+BuildSystem:    cmake
+BuildOption(conf): -G Ninja
+BuildOption(conf): -DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3
+BuildOption(conf): -DZ3_BUILD_DOCUMENTATION:BOOL=ON
+%ifarch %{java_arches}
+BuildOption(conf): -DZ3_BUILD_JAVA_BINDINGS:BOOL=ON
+%endif
+BuildOption(conf): -DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON
+BuildOption(conf): -DCMAKE_INSTALL_PYTHON_PKG_DIR=%{python3_sitelib}
+BuildOption(conf): -DZ3_INCLUDE_GIT_HASH:BOOL=OFF
+BuildOption(conf): -DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF
+BuildOption(conf): -DZ3_USE_LIB_GMP:BOOL=ON
 
-BuildRequires:  cmake
 BuildRequires:  doxygen
 BuildRequires:  gcc-c++
 BuildRequires:  gmp-devel
@@ -48,7 +57,6 @@ BuildRequires:  make
 BuildRequires:  ninja-build
 BuildRequires:  ocaml
 BuildRequires:  ocaml-findlib
-BuildRequires:  ocaml-ocamldoc
 BuildRequires:  ocaml-zarith-devel
 BuildRequires:  python3-devel
 BuildRequires:  %{py3_dist setuptools}
@@ -140,7 +148,6 @@ Python 3 interface to z3.
 %patch 0 -p1
 %endif
 
-%conf
 # Enable verbose builds, use Fedora CFLAGS, preserve timestamps when installing,
 # include the entire contents of the archives in the library, link the library
 # with the correct flags, and build the ocaml files with debuginfo.
@@ -150,7 +157,7 @@ sed \
   -e "s/\(['\"]\)cp\([^[:alnum:]]\)/\1cp -p\2/" \
   -e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive'/" \
   -e '/SLIBFLAGS/s|-shared|& %{build_ldflags} -Wl,--whole-archive|' \
-  -e 's/\(libz3$(SO_EXT)\)\(\\n\)/\1 -Wl,--no-whole-archive\2/' \
+  -e 's/\(libz3$(SO_EXT)\)\( \$(SLINK\)/\1 -Wl,--no-whole-archive\2/' \
   -e "s/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \
   -i scripts/mk_util.py
 
@@ -162,35 +169,16 @@ sed -e '/libz3java/s,\(System\.load\)Library("\(.*\)"),\1("%{_libdir}/z3/\2.so")
 # Turn off HTML timestamps for reproducible builds
 sed -i '/HTML_TIMESTAMP/s/YES/NO/' doc/z3api.cfg.in doc/z3code.dox
 
-%build
+%build -p
 export PYTHON=%{python3}
 
-%cmake -G Ninja \
-  -DCMAKE_INSTALL_INCLUDEDIR=%{_includedir}/z3 \
-  -DZ3_BUILD_DOCUMENTATION:BOOL=ON \
-%ifarch %{java_arches}
-  -DZ3_BUILD_JAVA_BINDINGS:BOOL=ON \
-%endif
-  -DZ3_BUILD_PYTHON_BINDINGS:BOOL=ON \
-  -DCMAKE_INSTALL_PYTHON_PKG_DIR=%{python3_sitelib} \
-  -DZ3_INCLUDE_GIT_HASH:BOOL=OFF \
-  -DZ3_INCLUDE_GIT_DESCRIBE:BOOL=OFF \
-  -DZ3_USE_LIB_GMP:BOOL=ON
-
-%cmake_build
-
+%build -a
 # 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.
 #
@@ -209,10 +197,7 @@ sed -i '/^api/s/ libz3\$(SO_EXT)//g' build/Makefile
 # Fourth, build the OCaml interface
 %make_build -C build ml
 
-%install
-# Install the C++, python3, and Java interfaces
-%cmake_install
-
+%install -a
 %ifarch %{java_arches}
 # Move the Java interface to its correct location
 mkdir -p %{buildroot}%{_libdir}/z3
@@ -244,8 +229,8 @@ help2man -N -o %{buildroot}%{_mandir}/man1/z3.1 \
 # Fix the pkgconfig file
 sed -i 's,//usr,,' %{buildroot}%{_libdir}/pkgconfig/z3.pc
 
-%if %{with test}
 %check
+%if %{with test}
 cd build
 make test-z3
 ./test-z3 /a
@@ -259,7 +244,7 @@ cd -
 
 %files libs
 %license LICENSE.txt
-%{_libdir}/libz3.so.4.16{,.*}
+%{_libdir}/libz3.so.5.1{,.*}
 
 %files devel
 %{_includedir}/z3/
@@ -274,7 +259,7 @@ cd -
 %ifarch %{java_arches}
 %files -n java-z3
 %{_libdir}/z3/
-%{_jnidir}/com.microsoft.z3*jar
+%{_jnidir}/com.microsoft.z3.jar
 %endif
 
 %files -n ocaml-z3
@@ -285,7 +270,7 @@ cd -
 %ifarch %{ocaml_native_compiler}
 %{ocamldir}/Z3/*.cmxs
 %endif
-%{ocamldir}/stublibs/*.so
+%{ocamldir}/stublibs/dllz3ml.so
 
 %files -n ocaml-z3-devel
 %{ocamldir}/Z3/*.a