Hello community, here is the log from the commit of package z3 for openSUSE:Factory checked in at 2017-03-21 22:51:14 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Tue Mar 21 22:51:14 2017 rev:8 rq:481464 version:4.5.0+git.20170313 Changes: -------- --- /work/SRC/openSUSE:Factory/z3/z3.changes 2017-03-12 20:00:50.068632304 +0100 +++ /work/SRC/openSUSE:Factory/.z3.new/z3.changes 2017-03-21 22:51:14.620408877 +0100 @@ -1,0 +2,81 @@ +Mon Mar 13 15:30:57 UTC 2017 - jsl...@suse.com + +- Z3Config.cmake is not needed anymore +- Update to version 4.5.0+git.20170313: + * Fixed utf-8 version string handling for python2. Resolved #787 + * Set soname version correctly in cmake build + * cmake build: set SOVERSION to include the minor version number + * fix overflow exposed in #880 + * Thread labels through tactic system + * Add basic Sine Qua Non filtering + * adding parallel threads + * Fix off-by-one bug in array indexing in the OCaml bindings + * refine parsat + * add const & + * Introduce and use labels_vec + * ensure that parallel threads are only invoked when thread count > 1 + * add name + * delete comment + * delete unused args + * reindent + * use insert_if_not_there + * fix issues with running parallel solver: random strategy should not be a default on all solvers. Also reuse base solver + * fix bug in propagation of parameters to combined solvers + * bypass combined solver when logic is set to QF_BV or QF_FD + * bypass combined solver when logic is set to QF_FD + * move exchange par + * enable pb theory always as pb terms can be introduced during transformations. Issue #884 + * use is_uninterp + * correctly pretty-print + * add and use new is_pattern recognizer + * add par_or tactic to C++ API. #873 + * fix bug in lexicographic handling in maxres: previous assumptions were not committed in corner cases + * Fixed signed/unsigned warnings + * Fixed model-converter segfault in ::check_sat. Relates to #881 + * Fixed model-converter segfault in ::check_sat. Relates to #881 + * add itos/stoi conversion to API. Issue #895 + * fix model generation for non-linear expressions, reported by Martin Suda and Giles Reger + * expose numerator/denominators for Martin and Giles + * add missing mod/rem/is_int functionality to C++ API + * make parameters accessible from expressions. Issue #896 + * add par_and_then + * use non _ method from z3printer module so to be resilient against how _ is handled as indicator of private functions + * add recursive function graphs to model, adapt rewriter to bypass branches whose evaluation is redundant + * add octal escape to seq_decl_plugin + * C-style octal escapes, including 1- and 2-digit escapes + * add _re.unroll internal operator to seq_decl_plugin + * expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911 + * expose bounds as vector expressions instead of containing ad-hoc expressions. Issue #911 + * remove unreferenced label + * fix type on exception message + * fix unhandled finite domain sort rewrite case. Issue #918 + * Java API for getting the objective value as a triple + * Sane indentation + removing extra spaces for Optimize.java + * Class Optimize#Handle should be static, + * fixed bug where `mk_make.py --build=...` would fail to handle absolute paths correctly. + * Free allocated char arrays in JNI API + * [CMake] For single configuration generators only allow `CMAKE_BUILD_TYPE` to be one of the pre-defined build configurations that we support. + * add boolean operators to zstring and fix ostream + * Tabs, whitespace + * fix bug for bit-vector optimization. Issue #919 + * fix bug for bit-vector optimization. Issue #928 + * ensure evaluation of array equalities is enabled for external facing evaluator. Issue #917 + * check that formulas are in lira before invoking qsat. Issue #919 + * add notes to README based on feedback in #916 + * remove scratch notes from readme + * include recursive functions to models. Issue #898 + * remove print breaking build + * fixing build break, adding fixedpoint object to C++ API + * adding fixedpoint object to C++ API + * fixing build break, addressing #935 + * z3py: With tactical should not try to use context as a parameter + * move restore relevancy until after literals have been replayed + * [CMake] Support including Git hash and description into the build. CMake will automatically pick up changes in git's HEAD so that the necessary code is rebuilt when the build system is invoked. + * [CMake] Implement generation of `Z3Config.cmake` and `Z3Target.cmake` file for the build and install tree. + * [CMake] Python examples should only be copied over if python bindings are being built. + * [CMake] Build `c_example`, `cpp_example` and `z3_tptp5` as external projects. + * [CMake] Fix typo handling OpenMP flags. + * [CMake] Fix examples linking against libz3 when it is built as a static library on Linux. + * [CMake] On Windows when building the examples copy the Z3 library into the directory of the example executable so that it works "out of the box". + +------------------------------------------------------------------- Old: ---- Z3Config.cmake z3-4.5.0+git.20170126.tar.xz New: ---- z3-4.5.0+git.20170313.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.TjrsJD/_old 2017-03-21 22:51:15.432294100 +0100 +++ /var/tmp/diff_new_pack.TjrsJD/_new 2017-03-21 22:51:15.436293535 +0100 @@ -16,18 +16,17 @@ # -%define version_unconverted 4.5.0+git.20170126 -%define sover 4_5_1_0 +%define version_unconverted 4.5.0+git.20170313 +%define sover 4_5 Name: z3 -Version: 4.5.0+git.20170126 +Version: 4.5.0+git.20170313 Release: 0 Summary: Theorem prover from Microsoft Research License: MIT Group: Productivity/Scientific/Other Url: https://github.com/Z3Prover/z3/wiki Source0: %{name}-%{version}.tar.xz -Source1: Z3Config.cmake Patch0: remove-timestamp.patch BuildRequires: cmake BuildRequires: gcc-c++ @@ -91,9 +90,6 @@ %install %cmake_install -install -d %{buildroot}%{_libdir}/cmake/Z3 -sed 's|@PREFIX@|%{_prefix}|g; s|@LIB@|%{_lib}|g' %{SOURCE1} > %{buildroot}%{_libdir}/cmake/Z3/Z3Config.cmake - %post -n libz3-%{sover} -p /sbin/ldconfig %postun -n libz3-%{sover} -p /sbin/ldconfig @@ -110,8 +106,9 @@ %defattr(-,root,root) %{_includedir}/z3*.h %{_libdir}/libz3.so -%dir %{_libdir}/cmake/Z3/ -%{_libdir}/cmake/Z3/Z3Config.cmake +%dir %{_libdir}/cmake/z3/ +%{_libdir}/cmake/z3/Z3Config.cmake +%{_libdir}/cmake/z3/Z3Targets* %files -n python-%{name} %defattr(-,root,root) ++++++ _servicedata ++++++ --- /var/tmp/diff_new_pack.TjrsJD/_old 2017-03-21 22:51:15.496285054 +0100 +++ /var/tmp/diff_new_pack.TjrsJD/_new 2017-03-21 22:51:15.496285054 +0100 @@ -1,4 +1,4 @@ <servicedata> <service name="tar_scm"> <param name="url">git://github.com/Z3Prover/z3.git</param> - <param name="changesrevision">962979b09c991fc47a02e10afb07d68a353308ff</param></service></servicedata> \ No newline at end of file + <param name="changesrevision">28493622c25e033a2db48bb99a4fba7d12e2fb7e</param></service></servicedata> \ No newline at end of file ++++++ z3-4.5.0+git.20170126.tar.xz -> z3-4.5.0+git.20170313.tar.xz ++++++ ++++ 4395 lines of diff (skipped)
