baserev update by copy to link target

• Files Changed
• Browse Source

In the current spec file python3-z3 has a requirement on z3, but that is not
correct, python3-z3 requires the shared library in lib-z3, fix incorrect
dependency by updating spec file.

• Files Changed
• Browse Source

- 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

• Files Changed
• Browse Source

- update to 4.8.13:
  The release integrates various bug fixes and tuning.

• Files Changed
• Browse Source

- update to 4.8.12:
  Release provided to fix git tag discrepancy issues with 4.8.11

• Files Changed
• Browse Source

baserev update by copy to link target

• Files Changed
• Browse Source

- 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

• Files Changed
• Browse Source

baserev update by copy to link target

• Files Changed
• Browse Source

- update to 4.8.10:
  - rewritten arithmetic solver replacing legacy arithmetic solver and on by default

• Files Changed
• Browse Source

baserev update by copy to link target

• Files Changed
• Browse Source

- 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)

• Files Changed
• Browse Source

baserev update by copy to link target

• Files Changed
• Browse Source

fix chlog

• Files Changed
• Browse Source

Backport pkg-config support from upstream

• Files Changed
• Browse Source

baserev update by copy to link target

• Files Changed
• Browse Source

- Drop ExclusiveArch as it does build properly on other archs

• Files Changed
• Browse Source

baserev update by copy to link target

• Files Changed
• Browse Source

- Update to version 4.8.8:
  * Various small changes
- Switch to released tarball from git snapshot

• Files Changed
• Browse Source

baserev update by copy to link target

• Files Changed
• Browse Source

- 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

• Files Changed
• Browse Source