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 <[email protected]> + +- 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)
