Hello community, here is the log from the commit of package z3 for openSUSE:Leap:15.2 checked in at 2020-01-17 12:05:46 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Leap:15.2/z3 (Old) and /work/SRC/openSUSE:Leap:15.2/.z3.new.26092 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Fri Jan 17 12:05:46 2020 rev:16 rq:764888 version:4.8.6+git.20191009 Changes: -------- --- /work/SRC/openSUSE:Leap:15.2/z3/z3.changes 2020-01-15 16:32:40.948890272 +0100 +++ /work/SRC/openSUSE:Leap:15.2/.z3.new.26092/z3.changes 2020-01-17 12:05:50.508620325 +0100 @@ -1,0 +2,70 @@ +Thu Oct 10 08:15:48 UTC 2019 - [email protected] + +- Update to version 4.8.6+git.20191009: + * fix assert-and-track semantics for smt2 logging + * remove separate API for setting solver log, use parameter setting instead + * make smt2 log scope aware + * remove a few str copies when throwing exceptions + * adding SMT2 log file for solver interaction #867 + * bit-vector overflow/underflow operators exposed over C++ API + * use Z3_char_ptr + * expose mk_divides over API. Corresponds to a = b (mod m), #723 + * and many more... + +------------------------------------------------------------------- +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 + +------------------------------------------------------------------- +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 + * and more... + +------------------------------------------------------------------- +Fri Jun 15 08:24:41 UTC 2018 - [email protected] + +- Update to version 4.7.1+git.20180614: + * fix memory leak in relation_manager, use for loops + * fix #1665 + * remove trial with mfsr flag + * enable non-expression bodies of quantifiers to fix #1667 + * fix bugs exposed by Nuno's PB example + * z3.py: add overflow checks to PB API + * gcc mode + * int64_t + * deal with shift exponent error + * deal with shift exponent error + * try flags to fix gcc build + * int64_t + * try new gcd + * and more... + +------------------------------------------------------------------- +Fri May 18 14:04:41 UTC 2018 - [email protected] + +- Use python3 exclusively +- Do not call contrib/cmake/bootstrap.py - it is obsolete + +------------------------------------------------------------------- @@ -22,31 +92 @@ - * Remove unnecessary copy of coeff in iteration. - * Remove ignored const qualifiers. - * Fix code formatting: Incorrect indentation. - * fix #1429 - * print_stat_f: Remove implicit conversion of float to double. - * Typo fixes. - * set default rewriter behavior in incremental mode to distribute multiplication over addition #1373 - * removing axiom exposing unsoundness, replace by weaker axiom - * add shorthand for translating models #1407 - * add __copy__, __deepcopy__ as alias to translate on same context #1427. Add generalized Gaussian elimination as an option to first-pass NL solver - * fix build of test - * adding pre-processing to nlsat for equations - * fix get-objectives error #1419 message (get-objectives) - * initialize additional assumptions after setup_context is called the first time - * alternate strategies for QF_NIA - * remove custom exception, perhaps this handles exception issue - * add virtual destructor to see if this helps ASan error - * Allowing slices and negative index in assertions - * add Python facility for int2bv, fix #1398 - * Documentation fixes. - * Bumped version number. - * Updated release notes - * add back missing initialization of lo - * fix nlsat regression - * avoid crash on nl - * fix crashes in nlsat - * fix crashes in nlsat - * remove comment out - * add integer branch and bound to nlsat - * small improvements to QF_NIA tactic - * fixes compilation flags for OCaml plugins + * and more... @@ -74,212 +114 @@ - * disable C++11 dependency to fix the travis build - * deal with ambiguity - * circumvent build errors introduced when using the ast_vector_tpl iterator - * include path - * include special functionality in parsers for solvers and opt for additional file formats - * include special functionality in parsers for solvers and opt for additional file formats - * fix issues found in parsing examples - * remove assertion that gets violated on exception path (declaration of datatypes are not getting removed) - * fix lack of warning/error for unbounded objectives in context of quantifiers #1382 - * fix test build - * fix test build - * set version, fix build of test files - * fix java - * fix dotnet example - * fix example file to be smt2 format - * fix maxsat compilation for maxsat example - * fix maxsat compilation for maxsat example - * fix c example, remove more smtlib1 printing - * remove SMTLIB1 printing - * Update version - * add parser error - * increase minor version, update java/.net apis - * fix error messaging for parsers - * remove smtlib1 dependencies - * fix #1371 - * remove std::cout - * save model from level 0, fix #1380 - * fix #1377 - * fix #1377 - * fix #1375 - * fix #1376 - * fix #1368 - * fix different bug reported on #1366 - * fix break - * fix #1366 - * expose extra symbols for logic ALL, requested in #1364 - * fix #1365. Filter MBQI instantiations for as-array terms that lead the array theory to return unknown and therefore block further instantiations. as-array terms are at this point almost always created from internal model values so quantifier instantiations with these have little value, other than instantiations of other paraameters that may indepdendently help - * remove redundant argument #1364 - * fix argument validation to new overflow/underflow functions #1364 - * add bit-vector over/underflow checks to Python API, #1364 - * fix #1233 - * debugging #1233 - * adding instrumentation to debug #1233 - * avoid rationals for addition in checked_int64 - * Fixed bug check in bv2fpa converter. Fixes #1291. - * avoid a warning - * add bvsmod - * additional bit-vector operators over C++ API - * fix occurs function used in qe_lite #1241 - * fix crash - * fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI - * fix infinite loop in traversing equivalence class, #1274, still requires addressing MBQI - * fix #1358 - * fix slicer for unsoundness. #1304 - * fix java build problem with bool arrays - * clean up bv_numeral code and fix bug in how they are initialized - * add method to create bit-vectors directly from an array of Booleans - * include information whether rule is reachable in del_rule model converter for simpler model presentation #1241 - * insert total relations in model converter. #1291 - * [CMake] When invoking `mk_api_doc.py` pass the build directory. - * fix rewriter loop reported in #1354 - * make .NET and Java bindings for optimization use Expr instead of ArithExpr to accomodate bit-vector optimization - * Fixed MSYS/MinGW build. Fixes #1335. - * Improved support for MSYS/MINGW. Fixes #969. - * API doc build fix. Related to #1350. - * Fixed API doc build - * Fixed Windows build of C example. - * Fixed bug in fp.to_ieee_bv with rewriter.hi_fp_unspecified=true. Reported in #1349. - * Fixed error handlers in Python API. - * Fixed C example build. - * Fixed C example build. - * Fixed default library path order in Python API. - * Fixed library path order in Python API. - * Fixed problems arising from unfortunate object destruction order in the Python API. Fixes #989. - * fix #877 by bypassing exception generation during label collection - * fix #889 - * remove a few unneded mem allocations - * fix proof mode related segfaults #1241 - * remove asserts for proof generation to enable mode switch in spacer virtual solver - * fix segfault reported as part of #1241 - * fix build - * fix model converter bug in coi-filter #1241 - * MSYS offers a MINGW shell as well. (uses different os.uname()) - * fix order of instantiation for recursive functions, #1274 - * internalize free var before iterating eqc in theory_str - * Added support for MSYS2 - * fix virtual method override - * fix build break with virtual method override - * fix stack overflow - * add proofs dependency to solver - * add solver pool abstraction for Spacer - * fix #1330. Interpolation transformation needs to handle TRANSITIVITY_STAR - * fix #1326 ++++ 122 more lines (skipped) ++++ between /work/SRC/openSUSE:Leap:15.2/z3/z3.changes ++++ and /work/SRC/openSUSE:Leap:15.2/.z3.new.26092/z3.changes Old: ---- z3-4.6.0+git.20180112.tar.xz New: ---- z3-4.8.6+git.20191009.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.9u61WM/_old 2020-01-17 12:05:51.292620670 +0100 +++ /var/tmp/diff_new_pack.9u61WM/_new 2020-01-17 12:05:51.296620672 +0100 @@ -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 @@ -12,23 +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.6.0+git.20180112 -%define sover 4_6 -%if 0%{?suse_version} >= 1500 -# Use python3 n SLE/Leap 15.0 and Tumbleweed -%define _python python3 -%define _python_sitelib %{python3_sitelib} -%else -%define _python python -%define _python_sitelib %{python_sitelib} -# USe python2 on older distros -%endif +%define version_unconverted 4.8.6+git.20191009 +%define sover 4_8 Name: z3 -Version: 4.6.0+git.20180112 +Version: 4.8.6+git.20191009 Release: 0 Summary: Theorem prover from Microsoft Research License: MIT @@ -36,12 +27,12 @@ URL: https://github.com/Z3Prover/z3/wiki Source0: %{name}-%{version}.tar.xz Patch0: remove-timestamp.patch -BuildRequires: %{_python}-devel BuildRequires: cmake BuildRequires: gcc-c++ BuildRequires: gmp-devel BuildRequires: ninja -BuildRequires: xz +BuildRequires: python3-devel +ExclusiveArch: %{ix86} x86_64 %description Z3 is a Satisfiability Modulo Theories (SMT) solver and integrates @@ -68,14 +59,12 @@ %description devel Development files for the Z3 library. -%package -n %{_python}-%{name} +%package -n python3-%{name} Summary: Python bindings for Z3 Group: Development/Languages/Python Requires: %{name} = %{version} -Provides: %{name}-%{_python} = %{version} -Obsoletes: %{name}-%{_python} < %{version} -%description -n %{_python}-%{name} +%description -n python3-%{name} Python bindings for the Z3 library. %prep @@ -84,14 +73,19 @@ %build %define __builder ninja -%{_python} contrib/cmake/bootstrap.py create %cmake \ -DBUILD_LIBZ3_SHARED=true \ -DUSE_LIB_GMP=true \ -DBUILD_PYTHON_BINDINGS=true \ -DINSTALL_PYTHON_BINDINGS=true \ - -DPYTHON_EXECUTABLE=%{_bindir}/%{_python} \ - -DENABLE_EXAMPLE_TARGETS=false + -DPYTHON_EXECUTABLE=%{_bindir}/python3 \ + -DENABLE_EXAMPLE_TARGETS=false \ +%if 0%{?suse_version} >= 1550 + -DLINK_TIME_OPTIMIZATION=true +%else + -DLINK_TIME_OPTIMIZATION=false +%endif + %make_jobs %install @@ -101,26 +95,23 @@ %postun -n libz3-%{sover} -p /sbin/ldconfig %files -%defattr(-,root,root) %license LICENSE.txt %doc README.md RELEASE_NOTES %{_bindir}/z3 %files -n libz3-%{sover} -%defattr(-,root,root) %{_libdir}/libz3.so.* %files devel -%defattr(-,root,root) %{_includedir}/z3*.h %{_libdir}/libz3.so %dir %{_libdir}/cmake/z3/ %{_libdir}/cmake/z3/Z3Config.cmake +%{_libdir}/cmake/z3/Z3ConfigVersion.cmake %{_libdir}/cmake/z3/Z3Targets* -%files -n %{_python}-%{name} -%defattr(-,root,root) -%dir %{_python_sitelib}/%{name} -%{_python_sitelib}/%{name}/*py +%files -n python3-%{name} +%dir %{python3_sitelib}/%{name} +%{python3_sitelib}/%{name}/*py %changelog ++++++ _servicedata ++++++ --- /var/tmp/diff_new_pack.9u61WM/_old 2020-01-17 12:05:51.324620685 +0100 +++ /var/tmp/diff_new_pack.9u61WM/_new 2020-01-17 12:05:51.324620685 +0100 @@ -1,4 +1,4 @@ <servicedata> <service name="tar_scm"> <param name="url">git://github.com/Z3Prover/z3.git</param> - <param name="changesrevision">450f3c9b459d128135abb5bbd4fa0508fe26bfae</param></service></servicedata> \ No newline at end of file + <param name="changesrevision">ecba7b3cde4c1125ac1db63b7b7d63b299051b4a</param></service></servicedata> \ No newline at end of file ++++++ remove-timestamp.patch ++++++ --- /var/tmp/diff_new_pack.9u61WM/_old 2020-01-17 12:05:51.332620688 +0100 +++ /var/tmp/diff_new_pack.9u61WM/_new 2020-01-17 12:05:51.336620690 +0100 @@ -1,21 +1,27 @@ +From 22ff49d575f0e11dfb2b251ae68f5cf8bdd2c069 Mon Sep 17 00:00:00 2001 From: Jiri Slaby <[email protected]> -Subject: Remove timestamp +Date: Thu, 10 Oct 2019 10:19:23 +0200 +Subject: [PATCH] Remove timestamp Nobody wants timestamps, it's bogus as it causes irreproducible builds. Remove that crap from api_log. - --- - src/api/api_log.cpp | 2 +- + src/api/api_log.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) +diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp +index e82ec3fd1..1efa09b95 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp -@@ -50,7 +50,7 @@ extern "C" { - res = Z3_FALSE; - } - else { -- *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n"; -+ *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << "\"\n"; - g_z3_log->flush(); - g_z3_log_enabled = true; - } +@@ -54,7 +54,7 @@ extern "C" { + res = false; + } + else { +- *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n"; ++ *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << "\"\n"; + g_z3_log->flush(); + g_z3_log_enabled = true; + } +-- +2.21.0 + ++++++ z3-4.6.0+git.20180112.tar.xz -> z3-4.8.6+git.20191009.tar.xz ++++++ ++++ 352924 lines of diff (skipped)
