Hello community,
here is the log from the commit of package z3 for openSUSE:Leap:15.2 checked in
at 2020-04-14 14:20:53
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Comparing /work/SRC/openSUSE:Leap:15.2/z3 (Old)
and /work/SRC/openSUSE:Leap:15.2/.z3.new.3248 (New)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3"
Tue Apr 14 14:20:53 2020 rev:18 rq:793498 version:4.8.7+git.20200407
Changes:
--------
--- /work/SRC/openSUSE:Leap:15.2/z3/z3.changes 2020-02-09 11:27:12.759360211
+0100
+++ /work/SRC/openSUSE:Leap:15.2/.z3.new.3248/z3.changes 2020-04-14
14:21:11.337283796 +0200
@@ -1,0 +2,27 @@
+Wed Apr 8 09:27:41 UTC 2020 - Martin Pluskal <mplus...@suse.com>
+
+- 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.EjyJMf/_old 2020-04-14 14:21:11.729284089 +0200
+++ /var/tmp/diff_new_pack.EjyJMf/_new 2020-04-14 14:21:11.729284089 +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.EjyJMf/_old 2020-04-14 14:21:11.777284124 +0200
+++ /var/tmp/diff_new_pack.EjyJMf/_new 2020-04-14 14:21:11.777284124 +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)
