Hello community, here is the log from the commit of package z3 for openSUSE:Factory checked in at 2017-10-19 19:32:31 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Thu Oct 19 19:32:31 2017 rev:10 rq:534438 version:4.5.0+git.20171009 Changes: -------- --- /work/SRC/openSUSE:Factory/z3/z3.changes 2017-08-04 11:57:57.743633606 +0200 +++ /work/SRC/openSUSE:Factory/.z3.new/z3.changes 2017-10-19 19:32:34.383651616 +0200 @@ -1,0 +2,526 @@ +Tue Oct 10 12:14:38 UTC 2017 - [email protected] + +- Update to version 4.5.0+git.20171009: + * allowing non-literal assumptions + * adding escape characters to reason-unknown #1043 + * add colon to assertion stack levels #1046 + * remove throw in reason-unknown #1043 + * add pb built in ops for logic ALL #1045 + * enable get-unsat-assumptions command per request in #1048 + * Fix Expr.update in java API returning superclass + * Remove tab + * put temporaries on trail + * Tabs + * Fixed signed/unsigned comparison warnings + * add string accessors to managed APIs #1051 + * expose operator kinds for internal functions using their sequence variants. Issue #1051 + * fix regression in str + * fix reference count issue with pinning to expr_ref + * add shorthand for enumerating constants in a model + * print success after reset assertions #1057 + * add documentation per #1058 + * add documentation per #1058 + * Added __deepcopy__ operators to ref-counted objects in the Python API + * [Doxygen] Fix bug where some header files were not being scanned. + * [Doxygen] Fix some Doxygen warnings for `z3_optimization.h` + * [Doxygen] Fixed mismatched `@{` and `@}` declaration which prevented the `capi` group from being declared properly. For example this prevented from `Z3_mk_solver()` from appearing in the `capi` group. + * print success #1068 + * filter assumptions by membership in initial list #1065 + * revert change to 1065 + * print_core as a function + * [Doxygen] Rewrite documentation of `Z3_mk_solver()` and `Z3_mk_simple_solver()` to try to make it clearer what the differences are between these APIs. + * apply correction by ddcc #1069 + * escaping names in get-assignment #1061 + * [CMake] Move CMake files into their intended location so the `contrib/cmake/bootstrap.py` script no longer needs to be executed. + * [CMake] Remove bootstrap check. Now that the CMake files are in their correct location we don't need it anymore. + * [CMake] Modify `contrib/cmake/bootstrap.py` to do nothing except print a warning. + * [CMake] Remove documentation on "Bootstrapping". It is no longer relevant. + * properly quote symbols #1061 + * Add translate method for FuncDecl in java api + * Fix docstrings for FuncDecl.translate + * fix unsoundness bug in axiomatization of str.at. #1067 + * port FuncDecl copy to dotnet, continuation of #1073 + * fix build warning + * add sequence recognizers + * add concat recognizer + * Fix Z3_PRINT_SMTLIB_FULL not working as expected + * Fixed AST translation functions in .NET and Java APIs. Fixes #1073. + * use less memory #1078 + * fix build + * address issues raised in #998 + * address issues raised in #998 + * revert internalize logic for re until debugged + * typo + * fix bug in qe-lite reported in #1086: bookkeeping of unconstrained variables only works for quantifier-free formulas + * disable tweak to seq until there are cycles to test further + * Whitespace, typo. + * Whitespace + * Reverted fix for quoted echo strings when smtlib2_compliant=false. Kindly reported by Armael Gueneau. Fixes #1062. + * Fix for the fix for #1062. + * Fix bug #1079, integrality testing seems to have been wrong + * fix build break + * fix assertion, start addressing #1087 by using size_t + * add is_hypothesis() method + * ensure that variable names are properly quoted + * expose iterators in expr_map + * api to accumulate stopwatches + * expose iterator api of obj_hashtable + * remove debug code + * factored out is_variable_proc to a header file + * improve comments + * make qe_lite prefer simpler definitions + * typo in a comment + * api for accessing dl_rule name + * preserve dl rule names during xforms + * disable dt2bv for quantified variables as enum2bv does not handle them. #1092 + * refine test for non-fd to be more inclusive while addressing #1092 + * [CMake] Fix dependencies for generating `install_tactic.cpp`. + * [CMake] Fix dependencies for generating `gparams_register_modules.cpp`. + * [CMake] Fix dependencies for generating `mem_initializer.cpp`. + * (mev) renamed variable to clarify that it is unused + * (mev) bug fix in expanding array equalities + * (mev) call expand_value only at the end + * add note to Context documentation about scoped uses of contexts #1077 + * (mev) only reduce function interpretation + * [CMake] Fix CMake warning about CMP0042 on macOS + * add a template instantination + * #1101 + * [CMake] typos in cmake + * fix missing initialization + * propagate rule names during xform + * another fix for #1101 + * add separate get-objectives command #1107 + * adding change notes to release notes for a future release + * make the option soup dependencies more user-friendly, #1109 + * [CMake] Fix missing sanitization in `z3_add_cxx_flag flag()` function which caused CMake 2.8.12 to hit an error when handling the `-std=c++11` flag. + * [CMake] Unbreak detection of pthreads for CMake versions < 3.4 + * [CMake] Remove use of `INSTALL_PREFIX` argument to `configure_package_config_file()`. This argument wasn't available until CMake 3.1 and we don't appear to be really using it anyway. + * [CMake] Unbreak the configure step for CMake 2.8.12 + * [CMake] Fix detection of git description and hash for CMake 2.8.12 + * Added rlimit increments in theory_arith to avoid non-termination issues via F*. + * Adjusted rlimit increments in theory_arith to avoid non-termination issues + * Unbreak Z3 C++ API exception support for GCC < 5.0. This was broken by 0b1d5645097d41eec4c43946407e08d57b41ad64 . + * [CMake] Add missing python example files. + * Fix Python API examples so they work with Python 3 as well as Python 2. + * [CMake] Teach CMake to build the `maxsat` example as an external project. The project can be built by building the new `c_maxsat_example` target. + * fix bitrot in maxsat example reference management #1116 + * ensure that auxiliary PB booleans are recognized during rewriting. Fixes segementation fault #1113, but does not address performance issues with quantifiers and optimization combinations + * fix maybe non initialized warning + * fix run of lp_solver for mps files + * Fixed x86/x64 issues in theory_str + * Fixed backwards compatibility problem in maxsat example + * use worklist algorithm to avoid stack overflow #1125 + * fix unsoundness bug instroduced when fixing #1125 + * [TravisCI] Implement TravisCI build and testing infrastructure for Linux + * cleanup for warning message + * use iterators, update build icon for osx + * revert icon update + * icon update, take 2 + * icon update, take 3 + * icon update, take 4 + * clean up warnings in theory_str + * fix compiler warnings + * fix compiler warnings + * fix compiler warnings + * fix compiler warnings + * deal with warning messages + * fix trace/debug build for unreferenced variables + * fix theory_str warnings: rename get_value() to get_arith_value() + * adding doc #1132 + * Add --guardcf flag to mk_make.py to optionally enable Control Flow Guard. + * update documentation according to #1058 + * detect overlapping signatures #1134 + * revert update to #1134 + * fix check for finite sorts #1122 + * avoid complaining about division by 0 as unhandled in theory-lra + * doc fixes + * [CMake] Change the `WARNINGS_AS_ERRORS` option from BOOL to STRING to allow a new mode `SERIOUS_ONLY`. + * [TravisCI] Add `Z3_WARNINGS_AS_ERRORS` environment variable to control the `WARNINGS_AS_ERRORS` CMake option. + * proper theory_arith integration in theory_str::get_arith_value() + * add get_num_scopes to python solver api + * Fix typo that prevented uses of `bvsmod_i` being parsed. + * Fix minor typo in C API documentation + * Fixed bug in sat model converter. Fixes #1148. + * improved get_arith_value() in theory_str + * remove disabled code block in get_arith_value() + * add e_internalized() check in theory_str::get_arith_value() + * Improved collect-statistics tactic + * Fixed inconsistent state upon solver interruption. Partially fixes #951. + * Bugfix for fp.fma. One piece of puzzle #872. + * pretty printer: fix typo with ReSort sort name + * fixes to #1155 and partial introduction of SMTLIB 2.6 datatype format + * fixes to #1155 and partial introduction of SMTLIB 2.6 datatype format + * fix compiler warnings + * fix uninitialized warning + * fix regression reported in #1159 + * Fix for fp.fma encoding. Relates to #872. + * Fixed normalization shift in MPF rounder. Relates to #872. + * fix bug exposed when running test-z3.exe /a in debug mode, #1159. Add assertions to heap interaction + * [TravisCI] Fix running unit tests. + * Adding ENABLE_CFI flag to CMake. + * fix for #1161 + * ensure that assertions within the unit tests are exercised in all build modes, remove special handling of SASSERT for release mode #1163 + * address ASAN bug report #1160 + * address #1167 + * fixes #1168 + * fixes #1171 + * fixes #1172 + * fixes #1169 + * attempt at addressing #989 by referencing _lib directly instead of over lib() in function calls + * unexpressing interpolants #1172 + * add suspenders for #989 + * updated suspenders for #989 + * another round of fix for #989 to avoid problems with doxygen generation (TravisCI build failure) + * Cleaned up mpf rounder. Rewrote mpf fma. Relates to #872. + * fix #1173 + * revert first fix for #1173, replace by handling single arity chainables + * remove arity check + * fixing a build error + * add dummy initialization to unused variables to avoid compiler warnings + * Bugfix for fp.fma. Fixes #872. + * Fixed sign bug in mpf fp.fma. Relates to #872. + * Fixed renormalization in fp.fma. Relates to #872. + * fix #1177 + * fixes #1176 + * fixes #1180 + * fixes #1179 + * Fixed renormalization in fp.mul. Relates to #872. + * make proof_checker less verbose + * extra flags to control quant_hoist + * mark mk_true() and mk_false() const + * option to control array_der in qe_lite + * move semantics for ref + * Injected 3 missing bits of precision into fp.rem. Relates to #872. + * Simplified bit-vector bounds in fp.rem. Relates to #872. + * fix build break based on new assertion in smt-eq-justification + * Fixed bug in fpa2bv converter. Fixes #1178. + * make include paths uniformly use path relative to src. #534 ++++ 329 more lines (skipped) ++++ between /work/SRC/openSUSE:Factory/z3/z3.changes ++++ and /work/SRC/openSUSE:Factory/.z3.new/z3.changes Old: ---- z3-4.5.0+git.20170523.tar.xz New: ---- z3-4.5.0+git.20171009.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.UEOrYy/_old 2017-10-19 19:32:35.039620924 +0200 +++ /var/tmp/diff_new_pack.UEOrYy/_new 2017-10-19 19:32:35.039620924 +0200 @@ -16,11 +16,11 @@ # -%define version_unconverted 4.5.0+git.20170523 +%define version_unconverted 4.5.0+git.20171009 %define sover 4_5 Name: z3 -Version: 4.5.0+git.20170523 +Version: 4.5.0+git.20171009 Release: 0 Summary: Theorem prover from Microsoft Research License: MIT ++++++ _servicedata ++++++ --- /var/tmp/diff_new_pack.UEOrYy/_old 2017-10-19 19:32:35.079619053 +0200 +++ /var/tmp/diff_new_pack.UEOrYy/_new 2017-10-19 19:32:35.079619053 +0200 @@ -1,4 +1,4 @@ <servicedata> <service name="tar_scm"> <param name="url">git://github.com/Z3Prover/z3.git</param> - <param name="changesrevision">f3a0b7e0cd891c53badfc8c44d5fc2939a61a79d</param></service></servicedata> \ No newline at end of file + <param name="changesrevision">cae414e575299d976899b764041195ff36f484e9</param></service></servicedata> \ No newline at end of file ++++++ z3-4.5.0+git.20170523.tar.xz -> z3-4.5.0+git.20171009.tar.xz ++++++ ++++ 131057 lines of diff (skipped)
