libz3-4_8-4.8.17-1.2 RPM for i586

From OpenSuSE Tumbleweed for i586

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.

Provides

• libz3-4_8
• libz3-4_8(x86-32)
• libz3.so.4.8

Requires

• /sbin/ldconfig
• /sbin/ldconfig
• libc.so.6
• libc.so.6(GLIBC_2.0)
• libc.so.6(GLIBC_2.1.1)
• libc.so.6(GLIBC_2.1.3)
• libc.so.6(GLIBC_2.3.2)
• libc.so.6(GLIBC_2.3.4)
• libc.so.6(GLIBC_2.32)
• libc.so.6(GLIBC_2.34)
• libc.so.6(GLIBC_2.4)
• libgcc_s.so.1
• libgcc_s.so.1(GCC_3.0)
• libgcc_s.so.1(GCC_3.3.1)
• libgcc_s.so.1(GCC_3.4)
• libgcc_s.so.1(GCC_7.0.0)
• libgcc_s.so.1(GLIBC_2.0)
• libgmp.so.10
• libm.so.6
• libm.so.6(GLIBC_2.0)
• libm.so.6(GLIBC_2.1)
• libm.so.6(GLIBC_2.29)
• libstdc++.so.6
• libstdc++.so.6(CXXABI_1.3)
• libstdc++.so.6(CXXABI_1.3.2)
• libstdc++.so.6(CXXABI_1.3.8)
• libstdc++.so.6(CXXABI_1.3.9)
• libstdc++.so.6(GLIBCXX_3.4)
• libstdc++.so.6(GLIBCXX_3.4.11)
• libstdc++.so.6(GLIBCXX_3.4.14)
• libstdc++.so.6(GLIBCXX_3.4.15)
• libstdc++.so.6(GLIBCXX_3.4.17)
• libstdc++.so.6(GLIBCXX_3.4.18)
• libstdc++.so.6(GLIBCXX_3.4.19)
• libstdc++.so.6(GLIBCXX_3.4.20)
• libstdc++.so.6(GLIBCXX_3.4.21)
• libstdc++.so.6(GLIBCXX_3.4.22)
• libstdc++.so.6(GLIBCXX_3.4.26)
• libstdc++.so.6(GLIBCXX_3.4.29)
• libstdc++.so.6(GLIBCXX_3.4.30)
• libstdc++.so.6(GLIBCXX_3.4.9)
• rpmlib(CompressedFileNames) <= 3.0.4-1
• rpmlib(FileDigests) <= 4.6.0-1
• rpmlib(PayloadFilesHavePrefix) <= 4.0-1
• rpmlib(PayloadIsZstd) <= 5.4.18-1

License

MIT

Changelog

* Fri May 06 2022 Ferdinand Thiessen <rpm@fthiessen.de>
  - Update to 4.8.17
    * fix breaking bug in python interface for user propagator pop
    * Various fixes for z3str3
    * Initial support for nested algebraic datatypes with sequences
    * Initiate map/fold operators on sequences
    * Initiate maxdiff/mindiff on arrays
  - Update to version 4.8.16
    * Initial support for Darwin Arm64 (for M1, M2, .. users)
    * Added functionality to user propagator decisions.
    * Added options for rc2 and maxres-bin to maxsat
    * Improved search for mutex constraints (at-most-1 constraints)
      among soft constraints for maxsat derived from approach used
      in rc2 sample.
    * Various other bugfixes
* Thu Apr 14 2022 Ferdinand Thiessen <rpm@fthiessen.de>
  - Update to 4.8.15:
    * Fix solution soundness bug on QF_ABV formula undetected by
      model validator
    * Various other bug fixes
* Tue Mar 15 2022 Shung-Hsi Yu <shung-hsi.yu@suse.com>
  - fix python3-z3 requirement
* Fri Jan 21 2022 Avinesh Kumar <avinesh.kumar@suse.com>
  - update to 4.8.14:
    * fixes Antimirov derivatives for intersections and unions required
    required for solving non-emptiness constraints.
    * includes x86 dll in nuget package for Windows.
    * exposes additional user propagator functionality
* Sun Nov 28 2021 Dirk Müller <dmueller@suse.com>
  - update to 4.8.13:
    The release integrates various bug fixes and tuning.
* Sat Oct 16 2021 Dirk Müller <dmueller@suse.com>
  - update to 4.8.12:
    Release provided to fix git tag discrepancy issues with 4.8.11
* Fri Jun 11 2021 Paolo Stivanin <info@paolostivanin.com>
  - update to 4.8.11:
    * fix soundness issues, invalid models, and crashes for options
    "tactic.default_tactic=smt sat.euf=true"
    * centos -> glibc
    * updated ref to esrp
    * undo cxx hoist
    * hoist c++ flags
* Fri Jan 29 2021 Dirk Müller <dmueller@suse.com>
  - update to 4.8.10:
    - rewritten arithmetic solver replacing legacy arithmetic solver and on by default
* Thu Sep 17 2020 Dirk Mueller <dmueller@suse.com>
  - update to 4.8.9:
    significant improvements to regular expression solving expose user theory
    plugin. It is a leaner user theory plugin that was once available.
    It allows for registering callbacks that react to when bit-vector and Boolean variables
    receive fixed values.
    - many
    - the new arithmetic theory is turned on by default. It _does_ introduce
    regressions on several scenarios, but has its own advantages. Users can
    turn on the old solver by setting smt.arith.solver=2.
    Depending on feedback, we may turn toggle this default setting again back to smt.arith.solver=2.
  - remove remove-timestamp.patch, 5a42a000e938a295feb1a7070dd74b192796db4e.patch (upstream)
* Fri Jul 17 2020 Mark Stopka <mstopka@opensuse.org>
  - Backport pkg-config support from upstream
    * add 5a42a000e938a295feb1a7070dd74b192796db4e.patch
* Thu Jul 16 2020 Guillaume GARDET <guillaume.gardet@opensuse.org>
  - Drop ExclusiveArch as it does build properly on other archs
* Tue May 26 2020 Martin Pluskal <mpluskal@suse.com>
  - Update to version 4.8.8:
    * Various small changes
  - Switch to released tarball from git snapshot
* Wed Apr 08 2020 Martin Pluskal <mpluskal@suse.com>
  - Update to version 4.8.7+git.20200407:
    * work on random_updates
    * fill columns to fill in random update as in theory_arith_aux.h
    * block selected configurations from HORN tactic
    * set arith.solver=6 by default
    * revert the default arith.solver=2
    * simplify patch_blocker()
    * redirect to the new solver
    * fix the patch of real vars
    * change lar_terms to use column indices
    * change lar_terms to use column indices
    * fix #3713: too much caching in dom-simplify for OR expressions
    * fix #3739 - dependencies may be valid even if they are null
    * [spacer] fix ugly bug in ground refutation generation (i.e., cex)
    * Replace is_null with is_non_empty_string in spacer params
    * [spacer] fixedpoint.get_answer() returns ground refutation for SAT
    * reduce_invertible: fix mk_diagonal for BV 0 switch from -x to ~x
    * minor code simplification in bv rewriter
    * reduce_invertible: recognize (* x -1) as the same as (- x)
    * roll back in maximize_term if the integrality is broken
    * remove output from normalize bounds
    * and plenty of other chanes
  - Use cmake_build macro
* Thu Jan 30 2020 jslaby@suse.com
  - Update to version 4.8.7+git.20200129:
    * change in the test lp.cpp and in a trace statement
    * Add explicit instantiation of update_inf_cost_for_column_tableau.
    * fix build
    * speed up freedom interval computation
    * return l_undef in get_phase() if lpvar is not available
    * add filter to gcd test
    * fix #2898
    * correct handling of int terms in theory_lra
    * fix the debug build
    * and much more
* Thu Oct 10 2019 jslaby@suse.com
  - Update to version 4.8.6+git.20191009:
    * fix assert-and-track semantics for smt2 logging
    * remove separate API for setting solver log, use parameter setting instead
    * make smt2 log scope aware
    * remove a few str copies when throwing exceptions
    * adding SMT2 log file for solver interaction #867
    * bit-vector overflow/underflow operators exposed over C++ API
    * use Z3_char_ptr
    * expose mk_divides over API. Corresponds to a = b (mod m), #723
    * and many more...
* Mon Feb 25 2019 jslaby@suse.com
  - Update to version 4.8.4+git.20190224:
    * integrate some self-contained fixes from #2147
    * fix #2149
    * fix -Wsign-compare (len can never become negative anyway)
    * remove debug code
    * Fix translation of FPA numerals in ast_smt_pp. Fixes #2145.
    * fix gc to not remove ternary clauses that are on assignment trail. This addresses issue with drat proofs that don't pass drat-trim due to deletion during gc, but use in conflicts
    * stopwatch: fix debug build crash in sat solver
    * fix VS build, take 2
    * stopwatches: fix a few places that would call start/stop multiple times
    * and more...
  - crop long changelogs
  - use ExclusiveArch to avoid broken builds on other archs

Files

/usr/lib/libz3.so.4.8
/usr/lib/libz3.so.4.8.17.0

Generated by rpm2html 1.8.1

Fabrice Bellet, Thu Jun 16 23:15:40 2022