Hello community, here is the log from the commit of package z3 for openSUSE:Factory checked in at 2020-04-08 19:57:07 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new.3248 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Wed Apr 8 19:57:07 2020 rev:20 rq:792407 version:4.8.7+git.20200407 Changes: -------- --- /work/SRC/openSUSE:Factory/z3/z3.changes 2020-02-07 15:53:36.439484398 +0100 +++ /work/SRC/openSUSE:Factory/.z3.new.3248/z3.changes 2020-04-08 19:57:25.089155588 +0200 @@ -1,0 +2,27 @@ +Wed Apr 8 09:27:41 UTC 2020 - Martin Pluskal <[email protected]> + +- Update to version 4.8.7+git.20200407: + * work on random_updates + * fill columns to fill in random update as in theory_arith_aux.h + * block selected configurations from HORN tactic + * set arith.solver=6 by default + * revert the default arith.solver=2 + * simplify patch_blocker() + * redirect to the new solver + * fix the patch of real vars + * change lar_terms to use column indices + * change lar_terms to use column indices + * fix #3713: too much caching in dom-simplify for OR expressions + * fix #3739 - dependencies may be valid even if they are null + * [spacer] fix ugly bug in ground refutation generation (i.e., cex) + * Replace is_null with is_non_empty_string in spacer params + * [spacer] fixedpoint.get_answer() returns ground refutation for SAT + * reduce_invertible: fix mk_diagonal for BV 0 switch from -x to ~x + * minor code simplification in bv rewriter + * reduce_invertible: recognize (* x -1) as the same as (- x) + * roll back in maximize_term if the integrality is broken + * remove output from normalize bounds + * and plenty of other chanes +- Use cmake_build macro + +------------------------------------------------------------------- Old: ---- z3-4.8.7+git.20200129.tar.xz New: ---- z3-4.8.7+git.20200407.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.mSbGJE/_old 2020-04-08 19:57:26.725156782 +0200 +++ /var/tmp/diff_new_pack.mSbGJE/_new 2020-04-08 19:57:26.725156782 +0200 @@ -16,10 +16,10 @@ # -%define version_unconverted 4.8.7+git.20200129 +%define version_unconverted 4.8.7+git.20200407 %define sover 4_8 Name: z3 -Version: 4.8.7+git.20200129 +Version: 4.8.7+git.20200407 Release: 0 Summary: Theorem prover from Microsoft Research License: MIT @@ -86,7 +86,7 @@ -DZ3_LINK_TIME_OPTIMIZATION=false %endif -%make_jobs +%cmake_build %install %cmake_install ++++++ _servicedata ++++++ --- /var/tmp/diff_new_pack.mSbGJE/_old 2020-04-08 19:57:26.765156812 +0200 +++ /var/tmp/diff_new_pack.mSbGJE/_new 2020-04-08 19:57:26.769156815 +0200 @@ -1,4 +1,4 @@ <servicedata> <service name="tar_scm"> <param name="url">git://github.com/Z3Prover/z3.git</param> - <param name="changesrevision">9694dc0c749962efa3d46e7af3ef60747bfa19e3</param></service></servicedata> \ No newline at end of file + <param name="changesrevision">5c9fd90031a94fe598c18f9dbeba22dd6b5565f0</param></service></servicedata> \ No newline at end of file ++++++ z3-4.8.7+git.20200129.tar.xz -> z3-4.8.7+git.20200407.tar.xz ++++++ ++++ 51554 lines of diff (skipped)
