Hello community, here is the log from the commit of package z3 for openSUSE:Factory checked in at 2016-09-13 22:22:30 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Changes: -------- New Changes file: --- /dev/null 2016-07-07 10:01:34.856033756 +0200 +++ /work/SRC/openSUSE:Factory/.z3.new/z3.changes 2016-09-13 22:22:31.000000000 +0200 @@ -0,0 +1,47 @@ +------------------------------------------------------------------- +Wed Jul 20 04:21:40 UTC 2016 - [email protected] + +- Update descriptions + +------------------------------------------------------------------- +Mon Jul 18 09:54:52 UTC 2016 - [email protected] + +- Update to version 4.4.1+git.20160717: + * fix bugs exposed in #677. to_int(x) has the semantics that to_int(x) <= x, and to_int(x) is the largest integer satisfying this inequality. The encoding in purify_arith had it the other way x <= to_int(x) contrary to how to_int(x) is handled elsewhere. Another bug in theory_arith for mixed-integer linear case was also exposed. Fractional bounds on expressions of the form to_int(x), and more generally on integer rows were not rounded prior to internalization + * garbage collect all api::object references when calling del_context. Request issue #679 + * add proper garbage collection to ast_manager. Issue #679 + * remove unfinished ite-macro finder, tune ast GC to ensure nodes are roots only once + * fix rounding mode for pseudo-boolean constraint creation, Issue #683 + * add object z3 objects to target context during translation, to fix build regression failure on z3test.py + * add tptp5 example to cmake, adding output SZS directives for Geoff + * fix ubuntu build failure + * mark also ast in parameters as GC roots. Issue #676 +- Use cmake macros +- Some spec file polishing with spec-cleaner + +------------------------------------------------------------------- +Mon Jul 18 08:39:50 UTC 2016 - [email protected] + +- update to 20160717 + * a lot of changes, see the repo +- remove CMake-Provide-a-way-to-customise-the-install-directo.patch +- add remove-timestamp.patch + +------------------------------------------------------------------- +Thu Mar 10 10:12:17 UTC 2016 - [email protected] + +- disable build of examples (unused) + +------------------------------------------------------------------- +Wed Mar 9 13:46:58 UTC 2016 - [email protected] + +- update to 20160309 +- remove: 0001-cmake-add-base-files.patch (not needed anymore) +- add CMake-Provide-a-way-to-customise-the-install-directo.patch +- correct packaging + +------------------------------------------------------------------- +Mon Oct 12 13:45:04 UTC 2015 - [email protected] + +- initial package + New: ---- _service remove-timestamp.patch z3-4.4.1+git.20160717.tar.xz z3.changes z3.spec ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ # # spec file for package z3 # # Copyright (c) 2016 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 # upon. The license for this file, and modifications and additions to the # file, is the same license as for the pristine package itself (unless the # license for the pristine package is not an Open Source License, in which # case the license is the MIT License). An "Open Source License" is a # 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/ # %define version_unconverted 4.4.1+git.20160717 Name: z3 Version: 4.4.1+git.20160717 Release: 0 Summary: Theorem prover from Microsoft Research License: MIT Group: Productivity/Scientific/Other Url: https://github.com/Z3Prover/z3/wiki Source0: %{name}-%{version}.tar.xz Patch0: remove-timestamp.patch BuildRequires: cmake BuildRequires: gcc-c++ BuildRequires: gmp-devel BuildRequires: make BuildRequires: python BuildRequires: xz BuildRoot: %{_tmppath}/%{name}-%{version}-build %description Z3 is a Satisfiability Modulo Theories (SMT) solver and integrates several decision procedures: Linear real and integer arithmetic, fixed-size bit vectors, uninterpreted functions, extensional arrays, quantifiers and model generation. %package -n libz3-4_4_2_1 Summary: Library for the Z3 SMT theorem prover Group: System/Libraries %description -n libz3-4_4_2_1 Z3 is a Satisfiability Modulo Theories (SMT) solver and integrates several decision procedures. This subpackage contains the Z3 runtime library needed for Z3 and other projects. %package devel Summary: Development files for Z3 Group: Development/Languages/C and C++ Requires: %{name} = %{version} %description devel Developmnet files for the Z3 library. %package python Summary: Python bindings for Z3 Group: Development/Languages/Python Requires: %{name} = %{version} %description python Python bindings for the Z3 library. %prep %setup -q %patch0 -p1 %build python contrib/cmake/bootstrap.py create %cmake \ -DBUILD_LIBZ3_SHARED=true \ -DUSE_LIB_GMP=true \ -DBUILD_PYTHON_BINDINGS=true \ -DINSTALL_PYTHON_BINDINGS=true \ -DCMAKE_EXE_LINKER_FLAGS="" \ -DCMAKE_SHARED_LINKER_FLAGS="" \ -DENABLE_EXAMPLE_TARGETS=false \ -DCMAKE_BUILD_TYPE=RelWithDebInfo make %{?_smp_mflags} %install %cmake_install %post -n libz3-4_4_2_1 -p /sbin/ldconfig %postun -n libz3-4_4_2_1 -p /sbin/ldconfig %files %defattr(-,root,root) %doc LICENSE.txt README.md RELEASE_NOTES %{_bindir}/z3 %files -n libz3-4_4_2_1 %defattr(-,root,root) %{_libdir}/libz3.so.* %files devel %defattr(-,root,root) %{_includedir}/z3*.h %{_libdir}/libz3.so %files python %defattr(-,root,root) %{python_sitelib}/*py %changelog ++++++ _service ++++++ <services> <service mode="localonly" name="tar_scm"> <param name="url">git://github.com/Z3Prover/z3.git</param> <param name="scm">git</param> <param name="changesgenerate">enable</param> <param name="filename">z3</param> <param name="versionformat">4.4.1+git.%cd</param> </service> <service mode="localonly" name="recompress"> <param name="file">*.tar</param> <param name="compression">xz</param> </service> <service mode="localonly" name="set_version"/> </services> ++++++ remove-timestamp.patch ++++++ From: Jiri Slaby <[email protected]> Subject: 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 +- 1 file changed, 1 insertion(+), 1 deletion(-) --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -36,7 +36,7 @@ extern "C" { g_z3_log = 0; return Z3_FALSE; } - *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(); return Z3_TRUE; }
