Hello community, here is the log from the commit of package z3 for openSUSE:Factory checked in at 2017-01-31 12:41:28 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Package is "z3" Changes: -------- --- /work/SRC/openSUSE:Factory/z3/z3.changes 2016-12-09 09:39:00.097871068 +0100 +++ /work/SRC/openSUSE:Factory/.z3.new/z3.changes 2017-02-03 20:08:03.397454691 +0100 @@ -1,0 +2,111 @@ +Fri Jan 27 13:44:56 UTC 2017 - mpluskal@suse.com + +- Update to version 4.5.0+git.20170126: + * streamline logging in arithmetic + * adding preferred sat, currently disabled, to wmax. Fixing issue #815 + * make a few functions static + * remove 2 outdated comments + * add a few more statics to avoid symbol clashes + * Re-added context creation locks in the Java API. Relates to #819. + * Bugfix for model construction. Fixes #828. + * adding range to C API. Issue #831 + * add range constructor to .NET API + * add regular expression operations to C and C++ API + * add regular expression features to C# API + * add missing complement + * add python API for newly exposed regex constructors + * exposing regular expression features to address issue #831 + * produce error message for cores with optimization. Issue #825 + * Whitespace + * Bugfix for special-case handling in fp.fma. + * fix bug in encoding of axioms for indexof. Issue #806 + * Bugfix for special-case handling in fp.fma. + * Build fix for C++ example + * add virtual destructors, fix operator code for API methods complement and intersection per note by Loris d'Antoni + * address #835 + * address #835 + * address warnings from #836 + * add virtual destructor to intermediary class in case this helps for #835 + * address other warnings per input from delcypher + * bail out on failure to properly project + * bail out on failure to properly project. issue #837 + * remove nested booleans during pre-processing. issue #837 + * add suggestions from #835 + * fix bug in handling of repeated soft constraints. #815 + * Add rewrite rule for property encoded in #812 + * Fix implementation of `scoped_timer` under Linux where it was incorrectly assumed that `pthread_cond_timedwait()` would exit due to a condition variable being signaled or a timeout occuring. + * handle model generation from issue #748. Deal with warnings from #836 + * Build fix for C/C++ example programs. + * Style, whitespace. + * ensure that FD logic understands pb from command context + * Making z3 python look in its installation directory for the z3 lib + * fix generation of wcnf + * Build fix for static binaries + shared examples + * Fix for parallel builds of the OCaml API. Relates to #797. + * Fix inconsistent emission of OCaml enumeration files. The ordering of emitted enum values is not consistent between python 2 or 3. The root cause of the problem was a dictionary's keys being iterated over which has no defined order. + * Refactor `mk_z3consts_ml()` code into `mk_z3consts_ml_internal()` and move that into `mk_genfile_common.py`. Then adapt `mk_util.py` and `mk_consts_files.py` to call into the code at its new location. + * Refactor `update_api.mk_ml()` so that the source and output directories can be different. This feature will be needed by the CMake build system to build the OCaml bindings. + * Fix issue with bd1f07f864a7f1790cec08a306ccc17507f7e5a8 pointed out by @nunolopes . + * remove sources for unused variable warnings + * fix debug build, unused variable warnings + * fix build again + * Add -fpic to armv7/armv8 build + * updated encodings + * remove redundant disjunction in compilation of at-most-1 constraints, log mutexes + * fix missing else reported in #855 + * improve parser error message over API, streamline names of statistics for arithmetic solver + * add restart.max parameter to control cancellation based on restart count + * initialize watch in assign_eh + * make get_consequence call skip check-sat if a model is already there + * enable incremental consequence finding with restart timeout + * Fixed initialization order warning. + * add operator for issue #860 + * allow disabling exceptions from C++. Issue #861 + * moderate exception behavior for issue #861 + * fix bug in antecedent collection for consequence finding: once an antecedent is set, it should not be cleared + * add at-least and pbge to API, fix for issue #864 + * remove polynomial factorization as suggested by issue #852 + * Removed polynomial factorization test cases. Relates to #852 and fixes #865. + * GCC compilation/keyword fix. Relates to #864 + * update CMakeList to remove polynomial-factorization + * Formatting, whitespace + * Added option to extend unsat cores with literals that (potentially) provide quantifier instances. + * Cleaned up #include<iostream> in api* objects. + * Formatting, whitespace, and Z3_API annotations. + * Bugfix for smt.core.extend_patterns + * Omit '.dll' from library name for DllImport. + * Mark void DummyContracts as Conditional to avoid compiling their arguments. + * Corner-case fix for smt::solver::pop_core + * Update README.md + * remove unused features related to weighted check-sat + * Added win64 build badge + * Separated win32/64 builds + * Added MAKEJOBS env var to mk_unix_dist.py + * Fix unsound handling of upper bounds in wmax, thanks to Patrick Trentin for report and careful repros #847 + * use stirngs for env variables + * fix crash with unary xor #870 + * fix memory leaks from cancellations + * update macro_util logging to uniform format + * build fix + * Added (include ...) SMT2 command. + * Added filenames to error messages for when we have more than one file. + * Enabled filenames in error messages during inclusion of files. + * Updated cmake build + * Windows build fix. + * Bugfix for macro finder. Fixes #832. + * fix bug in consequence extraction: the order of bcp is not fixed between restarts, so the order of unit literals may not be preserved. This is relatively rare, so we optimize for the case where we assume bcp preserves order (and maybe miss some consequences) + * Another fix for #847. Reset wmax theory solver state between lex calls, otherwise it uses stale constraints + * Added .NET 3.5 solution/project files + * x64 build fix for .NET 3.5 API + * Windows build fix. + * access parameters from Python API + * Added option to limit the distance of unsat core extension through patterns. + * fix test for int-value + * fix regression for z3num + * fix bug in sat-simplifier decreasing heap values of variables that are not in the heap + * fix part 1 of #875 + * add warning for scearios of #876 + * add format #879 + * rework sat.mus to use restart count for bounded minimization + +------------------------------------------------------------------- Old: ---- z3-4.5.0+git.20161129.tar.xz New: ---- z3-4.5.0+git.20170126.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.wyd1Jh/_old 2017-02-03 20:08:03.977373063 +0100 +++ /var/tmp/diff_new_pack.wyd1Jh/_new 2017-02-03 20:08:03.977373063 +0100 @@ -1,7 +1,7 @@ # # spec file for package z3 # -# Copyright (c) 2016 SUSE LINUX GmbH, Nuernberg, Germany. +# Copyright (c) 2017 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,11 +16,11 @@ # -%define version_unconverted 4.5.0+git.20161129 +%define version_unconverted 4.5.0+git.20170126 %define sover 4_5_1_0 Name: z3 -Version: 4.5.0+git.20161129 +Version: 4.5.0+git.20170126 Release: 0 Summary: Theorem prover from Microsoft Research License: MIT ++++++ _servicedata ++++++ --- /var/tmp/diff_new_pack.wyd1Jh/_old 2017-02-03 20:08:04.029365744 +0100 +++ /var/tmp/diff_new_pack.wyd1Jh/_new 2017-02-03 20:08:04.033365182 +0100 @@ -1,4 +1,4 @@ <servicedata> <service name="tar_scm"> <param name="url">git://github.com/Z3Prover/z3.git</param> - <param name="changesrevision">d9227b95ea4e3894f63907c38c4b3a79e249c429</param></service></servicedata> \ No newline at end of file + <param name="changesrevision">962979b09c991fc47a02e10afb07d68a353308ff</param></service></servicedata> \ No newline at end of file ++++++ z3-4.5.0+git.20161129.tar.xz -> z3-4.5.0+git.20170126.tar.xz ++++++ ++++ 16339 lines of diff (skipped)