Hello community, here is the log from the commit of package z3 for openSUSE:Factory checked in at 2017-12-22 12:21:02 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Fri Dec 22 12:21:02 2017 rev:11 rq:559146 version:4.5.0+git.20171213 Changes: -------- --- /work/SRC/openSUSE:Factory/z3/z3.changes 2017-10-19 19:32:34.383651616 +0200 +++ /work/SRC/openSUSE:Factory/.z3.new/z3.changes 2017-12-22 12:21:38.275607183 +0100 @@ -1,0 +2,228 @@ +Thu Dec 14 12:20:44 UTC 2017 - [email protected] + +- Update to version 4.5.0+git.20171213: + * generalize model finder code to be independent of conjunction elimination + * Turned assertion failure into proper error message. + * fix incorrect clause in argumentsValid subterm of substr reduction + * add shortcuts for concatenation and equality propagation + * fix build of obj_ref_hashtable + * fix setup for non-linear real arithmetic per QF_UFNRA regresssions + * add obj_ref_map to make it easier to maintain reference counts with a map of objects + * remove deprecated functions from ML API. #1393 + * [Release Notes] Note that C++11 is required to build Z3 and is also required by the C++ API bindings. + * [CMake] Use C++11 when building C++ API example. + * fix #1390 + * 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 + * fix #1326 + * more C fixes to model example + * re-add model example + * disable model example pending C compliance or C99 or whatever adjustment + * remove ast.h reference + * missing files + * [CMake] Try to unbreak the C example build with older GCC versions by forcing the language version to be C99. + * move min_cut, fix #1321 + * ifndef/define match + * fix build errors + * fix build, fix #1322 + * more build errors in debug mode + * missing file + * move more proof utils + * move proof utils under ast + * Add example of using Z3's new model construction C API. This API was requested in #1223. + * rename repeated class apart + * unused warnings + * backward comp + * fix build issues + * move spacer_marshal to under parsers/smt2 + * create proofs folder, move proof-post-order utility to proofs directory, fix regression with proofs + * account for review + * fixing regressions introduced when reducing astm proof dependencies + * add parameter to specify the file into which dot proofs are to be printed + * add some colors to the proof output + * add a basic printer into graphviz (http://graphviz.org/) for proofs + * patch build failure + * streamlining proof generation (initial step of removing ast-manager dependency). Detect error in model creation when declaring constant with non-zero arity. See #1223 + * fix #1319, fix #1320 + * fix #1316, segmentation fault when numeric value is not internalized + * disable eager clear of check-sat-result to fix #1318 + * remove debug code + * remove redundant and wrong range type, in extension to changes made for #1223 + * additional array functions exposed over API, ping #1223 + * add special case handling for string constant backpropagation in theory_str + * Update README.md + * gift for Nuno + * fix scope accounting for dom simplifier + * nnf: let's try a different version of compatible frames wo/ copying + * Backward compatibility + * frame, again + * moving out construction of expr_ref + * trying to fix mac build + * add macro for _Exit under WINDOWS + * Backwards compatibility + * Whitespace + * [TravisCI] Don't run Python regression tests under ASan for now. The script that runs them doesn't propagate LD_PRELOAD and so the tests fail. + * [TravisCI] Try to unbreak running Python regression tests under ASan. + * [TravisCI] Add ASan/UBSan configuration that runs unit tests. + * [TravisCI] Add `RUN_API_EXAMPLES` option so that we can disable building/running examples in some configurations. + * More LSan workarounds. + * [TravisCI] Try again to not show suppressions by default + * [TravisCI] Swap `run_quiet` and `run_non_native_binding`. In the previous order `grep` inside `run_quiet` would get ASan LD_PRELOAD'ed which would sometimes fail. + * [TravisCI] Try to fix case in `run_quiet` where the script would fail with. + * [TravisCI] Don't print sanitizer suppressions by default because that breaks Z3's regression tests. + * Workaround `regressions/smt2/error.smt2` test timing out. + * [ASan] Ignore Clang OpenMP leaks for now. + * [TravisCI] Fix typo + * [TravisCI] Fix `Z3_BUILD_TYPE` variable that was not propagated into the Docker image as an environment variable. + * [UBSan] Remove a bunch of suppressions. + * [TravisCI] Try to run the Python and .NET examples under ASan. + * [LSan] Remove suppression files. The were fixed on rebase + * [LSan] Don't run `c_maxsat_example` with LeakSanitizer because it contains leaks that the Z3 developers don't intend to fix. + * [LSan] Suppress another leak until I can figure out what is going on. + * [LSan] Add suppression for part of #1297. + * [TravisCI] Fix typo in created directory for suppression files + * [TravisCI] For ASan/LSan use larger context so we get larger stack traces if needed. + * [TravisCI] Make ASan/UBSan configuration a debug build. + * [TravisCI] Add ASan configuration + * [CMake] When building C/C++ API examples use the same build type as Z3 if doing a single configuration build. + * [TravisCI] Fix getting proper stack traces for ASan/LSan. The `llvm-symbolizer` tool needs to be installed and ASan/LSan needs to be told where to find it. + * [UBSan] Update UBSan suppression file to suppress all undefined behaviour I have observed running in CI. + * [TravisCI] Don't run the python binding system tests when building with UBSan. + * [TravisCI] Fix undefined SCRIPT_DIR variable + * [TravisCI] Add a UBSan configuration + * [TravisCI] Don't run the non-native example when building with UBSan. + * [TravisCI][CMake] Add `Z3_C_EXAMPLES_FORCE_CXX_LINKER` CMake option and propagate its value into the C API examples. + * [TravisCI] Add ASan/LSan/UBSan suppression files and use them in CI. + * adding explicit assignment for auto-generated function. + * make vector friendly to gcc < 5 + * add move constructor to ref_vector + * add move constructor to watch_list + * vector: make expand_vector() less prone to mem leaks by calling the destructors after move + * add move constructor to obj_ref + * nnf: remove ast incref + * add move constructor to rational + * fix build of unit tests + * add move constructor to mpf + * remove noexcept since MSVC 2012 doest support it ++++ 31 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.20171009.tar.xz New: ---- z3-4.5.0+git.20171213.tar.xz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.4SFQuc/_old 2017-12-22 12:21:38.971573248 +0100 +++ /var/tmp/diff_new_pack.4SFQuc/_new 2017-12-22 12:21:38.975573053 +0100 @@ -16,11 +16,11 @@ # -%define version_unconverted 4.5.0+git.20171009 -%define sover 4_5 +%define version_unconverted 4.5.0+git.20171213 +%define sover 4_6 Name: z3 -Version: 4.5.0+git.20171009 +Version: 4.5.0+git.20171213 Release: 0 Summary: Theorem prover from Microsoft Research License: MIT ++++++ _servicedata ++++++ --- /var/tmp/diff_new_pack.4SFQuc/_old 2017-12-22 12:21:39.015571103 +0100 +++ /var/tmp/diff_new_pack.4SFQuc/_new 2017-12-22 12:21:39.015571103 +0100 @@ -1,4 +1,4 @@ <servicedata> <service name="tar_scm"> <param name="url">git://github.com/Z3Prover/z3.git</param> - <param name="changesrevision">cae414e575299d976899b764041195ff36f484e9</param></service></servicedata> \ No newline at end of file + <param name="changesrevision">387e984bd39a8a6ed636b0210bce6fef79b51bc5</param></service></servicedata> \ No newline at end of file ++++++ z3-4.5.0+git.20171009.tar.xz -> z3-4.5.0+git.20171213.tar.xz ++++++ ++++ 26618 lines of diff (skipped)
