Hello community, here is the log from the commit of package z3 for openSUSE:Factory checked in at 2019-06-19 21:01:58 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new.4811 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Wed Jun 19 21:01:58 2019 rev:16 rq:706047 version:4.8.4+git.20190224 Changes: -------- --- /work/SRC/openSUSE:Factory/z3/z3.changes 2018-12-04 20:54:07.956866032 +0100 +++ /work/SRC/openSUSE:Factory/.z3.new.4811/z3.changes 2019-06-19 21:02:02.986171209 +0200 @@ -1,0 +2,17 @@ +Mon Feb 25 09:59:16 UTC 2019 - [email protected] + +- Update to version 4.8.4+git.20190224: + * integrate some self-contained fixes from #2147 + * fix #2149 + * fix -Wsign-compare (len can never become negative anyway) + * remove debug code + * Fix translation of FPA numerals in ast_smt_pp. Fixes #2145. + * fix gc to not remove ternary clauses that are on assignment trail. This addresses issue with drat proofs that don't pass drat-trim due to deletion during gc, but use in conflicts + * stopwatch: fix debug build crash in sat solver + * fix VS build, take 2 + * stopwatches: fix a few places that would call start/stop multiple times + * and more... +- crop long changelogs +- use ExclusiveArch to avoid broken builds on other archs + +------------------------------------------------------------------- @@ -13,965 +30 @@ - * 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 ++++ 1908 more lines (skipped) ++++ between /work/SRC/openSUSE:Factory/z3/z3.changes ++++ and /work/SRC/openSUSE:Factory/.z3.new.4811/z3.changes Old: ---- z3-4.8.3+git.20181121.tar.xz New: ---- z3-4.8.4+git.20190224.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.ArQBZM/_old 2019-06-19 21:02:04.054172105 +0200 +++ /var/tmp/diff_new_pack.ArQBZM/_new 2019-06-19 21:02:04.058172109 +0200 @@ -1,7 +1,7 @@ # # spec file for package z3 # -# Copyright (c) 2018 SUSE LINUX GmbH, Nuernberg, Germany. +# Copyright (c) 2019 SUSE LINUX GmbH, Nuernberg, Germany. # # All modifications and additions to the file contributed by third parties # remain the property of their copyright owners, unless otherwise agreed @@ -16,10 +16,10 @@ # -%define version_unconverted 4.8.3+git.20181121 +%define version_unconverted 4.8.4+git.20190224 %define sover 4_8 Name: z3 -Version: 4.8.3+git.20181121 +Version: 4.8.4+git.20190224 Release: 0 Summary: Theorem prover from Microsoft Research License: MIT @@ -32,6 +32,7 @@ BuildRequires: gmp-devel BuildRequires: ninja BuildRequires: python3-devel +ExclusiveArch: %{ix86} x86_64 %description Z3 is a Satisfiability Modulo Theories (SMT) solver and integrates ++++++ _servicedata ++++++ --- /var/tmp/diff_new_pack.ArQBZM/_old 2019-06-19 21:02:04.114172155 +0200 +++ /var/tmp/diff_new_pack.ArQBZM/_new 2019-06-19 21:02:04.114172155 +0200 @@ -1,4 +1,4 @@ <servicedata> <service name="tar_scm"> <param name="url">git://github.com/Z3Prover/z3.git</param> - <param name="changesrevision">7b2590c026a4fb3ec4f7be541e22d6cf78434e99</param></service></servicedata> \ No newline at end of file + <param name="changesrevision">6ef3e5e3638fa5a3ba87bf3bc46f5eab81fbabfd</param></service></servicedata> \ No newline at end of file ++++++ z3-4.8.3+git.20181121.tar.xz -> z3-4.8.4+git.20190224.tar.xz ++++++ ++++ 37196 lines of diff (skipped)
