diff --git a/sources b/sources index 949de7f..fcc522d 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (z3-5.1.0.tar.gz) = 03a854f720a56484ab99b8a5517150f1c9106400f54ad758cfa58e3ee2f95e349396a64d4f527a5bb9ee37f10ad9ecfa1916d1f5c921f04089deda409374491b +SHA512 (z3-4.16.0.tar.gz) = 7dbcdd04a72f46bc3b6cbac2453b2a43f5ae126287b878ffe37f0573f910a1130c474c5edfa622dab09957f106cf425ab0f7cdfd34d41658599ad50a81ae39dd diff --git a/z3-s390x-doc.patch b/z3-s390x-doc.patch new file mode 100644 index 0000000..ec9ae91 --- /dev/null +++ b/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:
+ a3, + _elems=<z3.z3core.Elementaries object> + ) +-
Z3_ast_map_keys(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_ast_map_keys( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_ast_map_reset( + a0, + a1, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_ast_map_size(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_ast_map_size( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_ast_map_to_string( + a0, + a1, +@@ -833,7 +841,11 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_get_app_decl(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_get_app_decl( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_get_app_num_args( + a0, + a1, +@@ -866,9 +878,17 @@ Data descriptors defined here:
+ a1, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_get_ast_hash(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_get_ast_hash( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_get_ast_id(a0, a1, _elems=<z3.z3core.Elementaries object>)
+-
Z3_get_ast_kind(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_get_ast_kind( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_get_bool_value( + a0, + a1, +@@ -1347,7 +1367,11 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_goal_dec_ref(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_goal_dec_ref( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_goal_depth(a0, a1, _elems=<z3.z3core.Elementaries object>)
+
Z3_goal_formula( + a0, +@@ -1355,7 +1379,11 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_goal_inc_ref(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_goal_inc_ref( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_goal_inconsistent( + a0, + a1, +@@ -1420,7 +1448,11 @@ Data descriptors defined here:
+ )
+
Z3_is_app(a0, a1, _elems=<z3.z3core.Elementaries object>)
+
Z3_is_as_array(a0, a1, _elems=<z3.z3core.Elementaries object>)
+-
Z3_is_char_sort(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_is_char_sort( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_is_eq_ast( + a0, + a1, +@@ -1532,7 +1564,12 @@ Data descriptors defined here:
+ _elems=<z3.z3core.Elementaries object> + )
+
Z3_mk_bool_sort(a0, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bound(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bound( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bv2int( + a0, + a1, +@@ -1546,7 +1583,12 @@ Data descriptors defined here:
+ _elems=<z3.z3core.Elementaries object> + )
+
Z3_mk_bv_sort(a0, a1, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvadd(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvadd( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bvadd_no_overflow( + a0, + a1, +@@ -1560,7 +1602,12 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_bvand(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvand( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bvashr( + a0, + a1, +@@ -1573,7 +1620,12 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_bvmul(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvmul( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bvmul_no_overflow( + a0, + a1, +@@ -1599,7 +1651,12 @@ Data descriptors defined here:
+ a1, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_bvnor(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvnor( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bvnot(a0, a1, _elems=<z3.z3core.Elementaries object>)
+
Z3_mk_bvor(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+
Z3_mk_bvredand(a0, a1, _elems=<z3.z3core.Elementaries object>)
+@@ -1616,11 +1673,36 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + ) +-
Z3_mk_bvsge(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvsgt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvshl(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvsle(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvslt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvsge( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_mk_bvsgt( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_mk_bvshl( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_mk_bvsle( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_mk_bvslt( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bvsmod( + a0, + a1, +@@ -1633,7 +1715,12 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_bvsub(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvsub( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bvsub_no_overflow( + a0, + a1, +@@ -1653,10 +1740,30 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_bvuge(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvugt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvule(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_bvult(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvuge( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_mk_bvugt( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_mk_bvule( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_mk_bvult( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_bvurem( + a0, + a1, +@@ -1669,7 +1776,12 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_bvxor(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_bvxor( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_char(a0, a1, _elems=<z3.z3core.Elementaries object>)
+
Z3_mk_char_from_bv( + a0, +@@ -1705,7 +1817,12 @@ Data descriptors defined here:
+ _elems=<z3.z3core.Elementaries object> + )
+
Z3_mk_config(_elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_const(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_const( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_const_array( + a0, + a1, +@@ -1765,7 +1882,11 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_empty_set(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_empty_set( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_enumeration_sort( + a0, + a1, +@@ -2056,7 +2177,10 @@ Data descriptors defined here:
+ a0, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_fpa_sort_half(a0, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_fpa_sort_half( ++ a0, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_fpa_sort_quadruple( + a0, + _elems=<z3.z3core.Elementaries object> +@@ -2197,7 +2321,12 @@ Data descriptors defined here:
+ _elems=<z3.z3core.Elementaries object> + )
+
Z3_mk_int2real(a0, a1, _elems=<z3.z3core.Elementaries object>)
+-
Z3_mk_int64(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_int64( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_int_sort(a0, _elems=<z3.z3core.Elementaries object>)
+
Z3_mk_int_symbol( + a0, +@@ -2333,7 +2462,12 @@ Data descriptors defined here:
+ a5, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_power(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_power( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_probe(a0, a1, _elems=<z3.z3core.Elementaries object>)
+
Z3_mk_quantifier( + a0, +@@ -2426,7 +2560,11 @@ Data descriptors defined here:
+ a3, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_re_option(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_re_option( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_re_plus(a0, a1, _elems=<z3.z3core.Elementaries object>)
+
Z3_mk_re_power( + a0, +@@ -2520,7 +2658,11 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_seq_empty(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_seq_empty( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_seq_extract( + a0, + a1, +@@ -2627,7 +2769,11 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_seq_to_re(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_seq_to_re( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_seq_unit(a0, a1, _elems=<z3.z3core.Elementaries object>)
+
Z3_mk_set_add( + a0, +@@ -2683,7 +2829,10 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_mk_simple_solver(a0, _elems=<z3.z3core.Elementaries object>)
++
Z3_mk_simple_solver( ++ a0, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_mk_simplifier( + a0, + a1, +@@ -3052,7 +3201,11 @@ Data descriptors defined here:
+ a2, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_optimize_pop(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_optimize_pop( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_optimize_push( + a0, + a1, +@@ -3288,8 +3441,18 @@ Data descriptors defined here:
+ a1, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_probe_eq(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_probe_ge(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_probe_eq( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_probe_ge( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_probe_get_descr( + a0, + a1, +@@ -3300,16 +3463,36 @@ Data descriptors defined here:
+ a1, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_probe_gt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_probe_gt( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_probe_inc_ref( + a0, + a1, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_probe_le(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+-
Z3_probe_lt(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_probe_le( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
++
Z3_probe_lt( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_probe_not(a0, a1, _elems=<z3.z3core.Elementaries object>)
+-
Z3_probe_or(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
++
Z3_probe_or( ++ a0, ++ a1, ++ a2, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_qe_lite(a0, a1, a2, _elems=<z3.z3core.Elementaries object>)
+
Z3_qe_model_project( + a0, +@@ -3605,7 +3788,11 @@ Data descriptors defined here:
+ a3, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_solver_check(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_solver_check( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_solver_check_assumptions( + a0, + a1, +@@ -3862,7 +4049,11 @@ Data descriptors defined here:
+ a3, + _elems=<z3.z3core.Elementaries object> + )
+-
Z3_solver_reset(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_solver_reset( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_solver_set_initial_value( + a0, + a1, +@@ -4118,7 +4309,11 @@ Data descriptors defined here:
+ _elems=<z3.z3core.Elementaries object> + )
+
Z3_to_app(a0, a1, _elems=<z3.z3core.Elementaries object>)
+-
Z3_to_func_decl(a0, a1, _elems=<z3.z3core.Elementaries object>)
++
Z3_to_func_decl( ++ a0, ++ a1, ++ _elems=<z3.z3core.Elementaries object> ++)
+
Z3_toggle_warning_messages( + a0, + _elems=<z3.z3core.Elementaries object> diff --git a/z3.spec b/z3.spec index 3c1df16..f014748 100644 --- a/z3.spec +++ b/z3.spec @@ -15,7 +15,7 @@ %bcond test 0 Name: z3 -Version: 5.1.0 +Version: 4.16.0 Release: %autorelease Summary: Satisfiability Modulo Theories (SMT) solver @@ -28,22 +28,13 @@ 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 @@ -57,6 +48,7 @@ BuildRequires: make BuildRequires: ninja-build BuildRequires: ocaml BuildRequires: ocaml-findlib +BuildRequires: ocaml-ocamldoc BuildRequires: ocaml-zarith-devel BuildRequires: python3-devel BuildRequires: %{py3_dist setuptools} @@ -148,6 +140,7 @@ 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. @@ -157,7 +150,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)\)\( \$(SLINK\)/\1 -Wl,--no-whole-archive\2/' \ + -e 's/\(libz3$(SO_EXT)\)\(\\n\)/\1 -Wl,--no-whole-archive\2/' \ -e "s/OCAML_FLAGS = ''/OCAML_FLAGS = '-g'/" \ -i scripts/mk_util.py @@ -169,16 +162,35 @@ 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 -p +%build export PYTHON=%{python3} -%build -a +%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 + # 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. # @@ -197,7 +209,10 @@ sed -i '/^api/s/ libz3\$(SO_EXT)//g' build/Makefile # Fourth, build the OCaml interface %make_build -C build ml -%install -a +%install +# Install the C++, python3, and Java interfaces +%cmake_install + %ifarch %{java_arches} # Move the Java interface to its correct location mkdir -p %{buildroot}%{_libdir}/z3 @@ -229,8 +244,8 @@ help2man -N -o %{buildroot}%{_mandir}/man1/z3.1 \ # Fix the pkgconfig file sed -i 's,//usr,,' %{buildroot}%{_libdir}/pkgconfig/z3.pc -%check %if %{with test} +%check cd build make test-z3 ./test-z3 /a @@ -244,7 +259,7 @@ cd - %files libs %license LICENSE.txt -%{_libdir}/libz3.so.5.1{,.*} +%{_libdir}/libz3.so.4.16{,.*} %files devel %{_includedir}/z3/ @@ -259,7 +274,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 @@ -270,7 +285,7 @@ cd - %ifarch %{ocaml_native_compiler} %{ocamldir}/Z3/*.cmxs %endif -%{ocamldir}/stublibs/dllz3ml.so +%{ocamldir}/stublibs/*.so %files -n ocaml-z3-devel %{ocamldir}/Z3/*.a