Hello community, here is the log from the commit of package z3 for openSUSE:Factory checked in at 2018-06-19 12:03:09 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Tue Jun 19 12:03:09 2018 rev:14 rq:617099 version:4.7.1+git.20180614 Changes: -------- --- /work/SRC/openSUSE:Factory/z3/z3.changes 2018-05-29 10:32:41.163591545 +0200 +++ /work/SRC/openSUSE:Factory/.z3.new/z3.changes 2018-06-19 12:03:13.463010207 +0200 @@ -1,0 +2,890 @@ +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 + * add set operations to python request by Francois + * fix #1662 + * fix #1661 + * fix memory leak from Arie + * fix ml build breakd #1659, #1660 + * fix #1655 + * fix #1653 + * remove stale file + * clean up python build files + * fix #1650 fix #1648 + * fix #1647 + * remove interp from documentation + * Set the SONAME field of libz3.so to libz3.so. + * remove interpolation from test_capi + * remove interpolation from test_capi + * deprecating interp + * fix #1638 + * fix #1645 + * remove interpolation and duality dependencies + * updated release notes for merge + * work around VS2012 compiler bug + * GLU -> GNU fix #1643 + * fix x86 warning + * Fix missing word in C++ API docs. + * Update OCaml docs for changes made elsewhere. + * Z3_TRUE/Z3_FALSE should be true/false, not 1/0. + * fix python build script dependencies + * dealing with compilers that don't take typename in non-template classes + * stale files + * merge with master + * fix bug reported in #1637 + * delay dereferencing justification + * release notes + * bumping version number by 1 for release tagging + * Use CMake's own mechanism for selecting language version if CMake version is new enough + * Add missing include The code should not have compiled previously, as smt::context was only forward declared at this point. + * Remove unnecessary (and confusing) parantheses around variable name in its declaration. Also fixes GCC warning [-Wparentheses]. + * Add comments + * Implement parallel python example + * As of GCC8, the throw by value, catch by reference idiom is enforced via -Wcatch-value + * NULL-initialize pointers to help GCC static analyzer Fixes: variable may be used uninitialized + * remove unused constructor that would construct lar_constraint in an partly initialized state. Fixes: variable may be used uninitialized + * fix #1621 + * fix #1625 + * fix #1621 + * fix #1625 + * updated sat state + * Big_int is no longer a part of OCaml's standard library and must be included via the num package: https://github.com/ocaml/num + * tune for unit test, delay initialize re-solver + * fix build + * add support for core extraction in parallel mode + * unreferenced variables + * fix osx build + * fix removal bug, tune all-interval usage + * disable slow validation code + * fix parenthesis + * use __builtin_prefetch for clang/gcc + * Fixed Segfault when failing to load datalog file + * The Permutation Matrix' `values` function attempted an incorrect conversion. This causes compilation with GCC 8 to fail. I suspect it worked previously due to SFINAE. + * fix if-def + * fix ema + * adding ema + * Revert "Specify encoding of source files in mk_util.py" + * update model conversion + * touch + * fix java + * fix #1607 by filtering exceptions when the context is canceled + * fixing compilation errors + * Specify encoding of source files in mk_util.py + * fix java + * fix dotnet example + * fix dotnet example + * create empty model + * fix #1609 + * fix build + * resolve + * resolve + * fix build issues + * fix build + * fix build errors + * fix build + * fix build + * fix build errors + * fix build errors + * try string in pragma + * pragma + * use C99 pragma + * merge + * n/a + * merge + * merge + * merge + * n/a + * fix #1604 + * fix local search initialization of units, encode offset in clauses + * testing memory defragmentation, prefetch, delay ate + * fix #1599. fix #1600 + * fix #1599. fix #1600 + * WMax conflict budget bug fix + * Revert "MSS based MaxSMT solver" + * Revert "implemented CLD" + * Revert "disjoint cores" + * Revert "WMax conflict budget bug fix" + * fix memory leak related to #1575 + * change order of concatentation for empty string, #1595 + * fix #1595 + * fix #1594 + * fix #1592 #1587 + * WMax conflict budget bug fix + * Z3 now will also try to find libz3 in PYTHONPATH + * Updated CMakelists.txt + * Added tactic for QF_FPLRA + * Fancy dots are not allowed here!! + * fix #1581 + * add warning message for optimization with quantifiers. Fix #1580 + * fix #1583 + * fix #1575, fix #1585 + * enable patterns on equality, add trace for variables for axiom profiling. + * add web assembly link + * add web assembly link + * fix #1576, hopefully + * fix #1579 + * Fixed corner-case in fp.to_ubv. + * remove extra file + * add params + * move parallel-tactic to solver level + * clean up parallel tactic + * adding smt parallel solving + * add backtracking conquer + * fix build + * fix build warnings + * adding the orphaned shorthand #1574 + * adding orphaned function declaration #1574 + * fix accounting for branches + * add filter cubes parameter + * parallel params + * updates + * fix regex automata leaked memory + * fix #1571 + * escape ascii above 127, issue #1571 + * fixes + * including all touched tautology literals each round + * Bugfixes for fpa2bv_converter. Fixes #1564. + * fix #1567 + * move some methods from header to cpp, format fixing, remove special characters + * fix cast in tests + * disambiguate calls to set + * disambiguate calls to set + * fix in occurs_check (early exit) + * replace by int64_t and uint64_t + * fixes + * style(datatype): use modern iteration + * chore(datatype): small fixes + * fix(datatypes): additional explanation in occurs_check + * fix(datatypes): update following @nikolajbjorner 's review + * fix(datatype): always use root nodes for the `parent` table + * chore(datatype): small improvements + * fix(datatype): only use pointer equality for enode_tbl + * perf(datatype): whole-graph implementation of occurs_check + * chore: add definition for `enode_tbl` + * perf(datatype): improve caching in occurs_check + * shorthands in enode to access args and partents + * remove comment + * Fixed bug in to_fp/to_fp_unsigned. Thanks to Florian Schanda for reporting this bug. + * add re.plus length enumeration; fix reordering warning + * flip literals in ATEs produced using RI + * Resolved merge conflict + * Bugfix for fp.to_sbv. Thanks to Florian Schanda for reporting this bug. + * Bugfix for unspecified semantics of some fp.* operators. + * Fixed overflow bug in fp.to_ubv. Thanks to Florian Schanda for reporting this bug. + * Fixed model completion for unspecified cases of floating-point functions. Thanks to Florian Schanda for reporting this bug. + * Fixed overflow problem in fp.to_?bv. Thanks to Florian Schanda for reporting this bug. + * Fixed MPF to_sbv. Thanks to Florian Schanda for reporting this bug. + * add tuple shortcut and example to C++ API + * fix collection error + * Fix buffering issue in print_success for declare-datatype + * disable bdd variable elimination + * fix bug in blocked clause elimination: it was ignoring unit literals + * bit-blaster + * increment version number due to ABI/API breaking change #1556 + * Remove int64, uint64 typedefs in favor of int64_t / uint64_t. ++++ 693 more lines (skipped) ++++ between /work/SRC/openSUSE:Factory/z3/z3.changes ++++ and /work/SRC/openSUSE:Factory/.z3.new/z3.changes Old: ---- z3-4.6.0+git.20180112.tar.xz New: ---- z3-4.7.1+git.20180614.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.Qwz2Fi/_old 2018-06-19 12:03:14.118985851 +0200 +++ /var/tmp/diff_new_pack.Qwz2Fi/_new 2018-06-19 12:03:14.122985703 +0200 @@ -16,10 +16,10 @@ # -%define version_unconverted 4.6.0+git.20180112 -%define sover 4_6 +%define version_unconverted 4.7.1+git.20180614 +%define sover 4_8 Name: z3 -Version: 4.6.0+git.20180112 +Version: 4.7.1+git.20180614 Release: 0 Summary: Theorem prover from Microsoft Research License: MIT @@ -78,7 +78,13 @@ -DBUILD_PYTHON_BINDINGS=true \ -DINSTALL_PYTHON_BINDINGS=true \ -DPYTHON_EXECUTABLE=%{_bindir}/python3 \ - -DENABLE_EXAMPLE_TARGETS=false + -DENABLE_EXAMPLE_TARGETS=false \ +%if 0%{?suse_version} >= 1550 + -DLINK_TIME_OPTIMIZATION=true +%else + -DLINK_TIME_OPTIMIZATION=false +%endif + %make_jobs %install ++++++ _servicedata ++++++ --- /var/tmp/diff_new_pack.Qwz2Fi/_old 2018-06-19 12:03:14.170983921 +0200 +++ /var/tmp/diff_new_pack.Qwz2Fi/_new 2018-06-19 12:03:14.174983772 +0200 @@ -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">e94b97376c50b80fea4b8c8b01e8c29ee27d8f0f</param></service></servicedata> \ No newline at end of file ++++++ z3-4.6.0+git.20180112.tar.xz -> z3-4.7.1+git.20180614.tar.xz ++++++ ++++ 146048 lines of diff (skipped)
