Hello community,
here is the log from the commit of package z3 for openSUSE:Factory checked in at 2018-12-04 20:54:04
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Comparing /work/SRC/openSUSE:Factory/z3 (Old)
and /work/SRC/openSUSE:Factory/.z3.new.19453 (New)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3"
Tue Dec 4 20:54:04 2018 rev:15 rq:652428 version:4.8.3+git.20181121
Changes:
--------
--- /work/SRC/openSUSE:Factory/z3/z3.changes 2018-06-19 12:03:13.463010207 +0200
+++ /work/SRC/openSUSE:Factory/.z3.new.19453/z3.changes 2018-12-04 20:54:07.956866032 +0100
@@ -1,0 +2,978 @@
+Thu Nov 22 12:03:51 UTC 2018 - Martin Pluskal
+
+- Update to version 4.8.3+git.20181121:
+ * fix is-unit test in seq rewriter
+ * fixing #1948
+ * Improve intra-doc linking.
+ * fix #1959
+ * fix #1958
+ * add rc2 sample
+ * fix #1956
+ * add macz3 status
+ * add macz3 status
+ * test
+ * Fix broken link. It is Z3_add_rec_def, not Z3_mk_rec_def.
+ * Switch from using Z3_bool to using bool.
+ * tweaks to mk_nuget_release
+ * tweaks to mk_nuget_release
+ * increment version number to 4.8.4
+ * updated release notes
+ * have replayer handle oom natively
+ * build errors on shrink
+ * true is true, false is not true, it is false
+ * Remove usages of Z3_TRUE / Z3_FALSE.
+ * fix combinator signatures
+ * Improve intra-doc linking.
+ * Fix precondition in Z3_get_symbol_string doc comment.
+ * remove unsound rewrite
+ * Correct Z3_(fixedpoint|optimize)_from_file param doc.
+ * update dist scripts
+ * update unix-dist
+ * std::cout -> out
+ * investigate #1946
+ * fix windows build_dist setting
+ * fix #1945
+ * add empty/full to java #1944
+ * disable validation in builds
+ * fix debug build, add access to numerics from model
+ * make dotnet core optional for mk_win_dist
+ * fix #1934
+ * Fix missing word in doc comment.
+ * make dotnet core dist optional
+ * make dotnet core dist optional
+ * add support for keyfiles
+ * use netstandard1.4
+ * build generated files outside of src
+ * with Mathias on nuget package generation
+ * clean up dotnet core component
+ * update example build for dotnet core
+ * use old-fashined C for test_capi
+ * fix #1940
+ * remove spurious string
+ * start script on assembling platform binaries to wrap with nuget install
+ * update for nuget/core
+ * update for nuget/core
+ * update for nuget/core
+ * add TBD marker
+ * Choose runtime for .NET core DLL.
+ * update script to generate file directly instead of from makefile
+ * fix test build
+ * core
+ * fix #1937
+ * Fix problem in `mk_echo`.
+ * Fix some problems in `mk_echo`.
+ * Fix `echo` command for Windows.
+ * Build example for dotnetcore.
+ * more dotnet core
+ * more dotnet core
+ * more dotnet core
+ * adding dotnetcore handling
+ * add TBD for dotnet example
+ * Updated nuget package spec and directions
+ * recover error stream from dimacs
+ * fix #1922 - incorrect pretty printing of datatypes
+ * add multiline lisp style comments #1932
+ * fix #1927
+ * ignore propagation on units
+ * undefine min/max #1927
+ * Fix typos.
+ * Work around unexpected behaviour in generalizer
+ * Fix display_certificate in spacer
+ * Fix add external lemmas to solver even if use_bg_invs=false
+ * fixing mk-win-dist to include redist #1924
+ * use h_file not fullname in error message
+ * add exception handler for debugging #1925
+ * add stub for certificate #1926
+ * add error if library is not included #1924
+ * align variable names with dimacs input
+ * feat(api/ml): release runtime lock on some long-running functions
+ * add missing inline fix #1917
+ * fixed documentation of Z3_param_descrs_get_name
+ * fixed documentation of Z3_param_descrs_get_name
+ * fixing bugs uncovered by repro in #1914
+ * more consistent use of parallel mode when enabled, takes care of example test from #1898 that didn't trigger parallel mode
+ * fix model extraction for 0-ary recursive function declarations
+ * add missing override
+ * fixing python build errors
+ * deal with compiler warnings
+ * newline
+ * display'
+ * na
+ * na
+ * fix #1908
+ * prepare release notes
+ * add recfuns to python API
+ * add recfuns to model
+ * add recfun to API
+ * na
+ * fix #1901
+ * working with incremental depth
+ * fix #1897
+ * recfun
+ * more dotnet core prepration
+ * more dotnetcore preparation
+ * more prep for dotnet core
+ * more prep for dotnetcore
+ * avoid name clash
+ * prepare to retool
+ * fix build
+ * depth
+ * guard
+ * recfun
+ * updates to recfun_decl_plugin
+ * bypass warning size_t/unsigned
+ * remove case-pred and depth-limit classes
+ * Remove unused warning_displayer.
+ * Remove disable_error_msg_prefix.
+ * Improve format2ostream.
+ * Remove commented out string2ostream.
+ * fix crash exposed by examples/dotnet/Program.cs
+ * regressions in examples/dotnet/Program.cs
+ * fix symbol comparison
+ * remove dummy contracts
+ * remove dependencies on contracts
+ * Fix some spelling errors (mostly in comments).
+ * Fixed .NET Core API build.
+ * double happiness
+ * good luck!
+ * fix backtrack
+ * bump version, add double access
+ * fix location of research
+ * n/a
+ * iterative deepening per recursive function
+ * iterative deepening
+ * n/a
+ * fix #1889
+ * ctx
+ * handle case input format
+ * more refinements for recfun
+ * add self-contained section on where to retrieve binaries
+ * add instructions as gift for Klaus
+ * Fix some typos.
+ * Fix doxygen warnings.
+ * Use bool literals instead of 0/1.
+ * cleanup
+ * more integration
+ * Remove superfluous const from returned types
+ * Catch exceptions by const-reference
+ * Revert "Made Z3 compile for C++17 with MSVC"
+ * increment patch
+ * follow instructions from #1879
+ * Made it more legal C++17
+ * Fixes the git submodule error discussed in https://github.com/Z3Prover/z3/pull/1552
+ * add arguments to optimize_check fix #1866
+ * add arguments to optimize_check fix #1866
+ * add arguments to optimize_check fix #1866
+ * fix #1874 by removing nnf.skolemize option
+ * update parser
+ * remove qualifiers that downlevel compilers complain about
+ * pull rounding mode top-level to deal with build
+ * remove class from enum class, add default to avoid compiler warning
+ * dl_util: Use an unsigned to match other values.
+ * Typo fixes.
+ * add parameter to force sat-cleaning on initialization and on simplification phases
+ * Add a floating-point support to c++ api.
+ * Ignore current dir when searching for jni
+ * Normalized formatting
+ * Added packaging directions, removed linkresource flag
+ * fix java
+ * Added NuGet package icon
+ * build
+ * fix #1577 again
+ * fix #1864
+ * fix the value oflar_solver.m_status during pop()
+ * fix java bindings
+ * na
+ * fix #1577
+ * fix #1577
+ * fix memory leak when cuber isn't run to completion. Found by Daniel Selsam
+ * fixing #1847
+ * Z3str3: don't use arith_value::get_value in get_arith_value
+ * fix cubing semantics
+ * [NFC] Cleanup arith_eq_solver.(cpp|h)
+ * Refer to macOS rather than Mac OS / OSX.
+ * watch_list: Fix indentation.
+ * theory_lra: Remove unused variable.
+ * Avoid unnecessary copies in for-range loops.
+ * Use 'override' where possible.
++++ 781 more lines (skipped)
++++ between /work/SRC/openSUSE:Factory/z3/z3.changes
++++ and /work/SRC/openSUSE:Factory/.z3.new.19453/z3.changes
Old:
----
z3-4.7.1+git.20180614.tar.xz
New:
----
z3-4.8.3+git.20181121.tar.xz
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Other differences:
------------------
++++++ z3.spec ++++++
--- /var/tmp/diff_new_pack.thmv7o/_old 2018-12-04 20:54:08.632865280 +0100
+++ /var/tmp/diff_new_pack.thmv7o/_new 2018-12-04 20:54:08.632865280 +0100
@@ -12,14 +12,14 @@
# license that conforms to the Open Source Definition (Version 1.9)
# published by the Open Source Initiative.
-# Please submit bugfixes or comments via http://bugs.opensuse.org/
+# Please submit bugfixes or comments via https://bugs.opensuse.org/
#
-%define version_unconverted 4.7.1+git.20180614
+%define version_unconverted 4.8.3+git.20181121
%define sover 4_8
Name: z3
-Version: 4.7.1+git.20180614
+Version: 4.8.3+git.20181121
Release: 0
Summary: Theorem prover from Microsoft Research
License: MIT
++++++ _servicedata ++++++
--- /var/tmp/diff_new_pack.thmv7o/_old 2018-12-04 20:54:08.660865248 +0100
+++ /var/tmp/diff_new_pack.thmv7o/_new 2018-12-04 20:54:08.660865248 +0100
@@ -1,4 +1,4 @@
<servicedata>
<service name="tar_scm">
<param name="url">git://github.com/Z3Prover/z3.git</param>
- <param name="changesrevision">e94b97376c50b80fea4b8c8b01e8c29ee27d8f0f</param></service></servicedata>
\ No newline at end of file
+ <param name="changesrevision">7b2590c026a4fb3ec4f7be541e22d6cf78434e99</param></service></servicedata>
\ No newline at end of file
++++++ remove-timestamp.patch ++++++
--- /var/tmp/diff_new_pack.thmv7o/_old 2018-12-04 20:54:08.664865244 +0100
+++ /var/tmp/diff_new_pack.thmv7o/_new 2018-12-04 20:54:08.664865244 +0100
@@ -8,10 +8,12 @@
src/api/api_log.cpp | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
---- a/src/api/api_log.cpp
-+++ b/src/api/api_log.cpp
-@@ -50,7 +50,7 @@ extern "C" {
- res = Z3_FALSE;
+Index: z3-4.8.3+git.20181121/src/api/api_log.cpp
+===================================================================
+--- z3-4.8.3+git.20181121.orig/src/api/api_log.cpp
++++ z3-4.8.3+git.20181121/src/api/api_log.cpp
+@@ -49,7 +49,7 @@ extern "C" {
+ res = false;
}
else {
- *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n";
++++++ z3-4.7.1+git.20180614.tar.xz -> z3-4.8.3+git.20181121.tar.xz ++++++
++++ 164643 lines of diff (skipped)