z3-4.8.7
4.8.7 release
Changes:
- 30e7c22 upgrade pip
- f170e65 add importlib_metatada
- c62380a update names of config vars
- 3669543 rename additional build options #2709
- 429fc7c rename additional build options #2709
- 2673235 rename additional build options #2709
- f7a6f3f fix #2718
- c7248a6 rename additional build options #2709
- dc4adcb doc
- 4522e7a rename additional build options #2709
See More
- 53a01a0 rename additional build options #2709
- 48554f0 rename additional build options #2709
- b50f850 rename additional build options #2709
- e9d9792 rename additional build options #2709
- 3ab9a1c remove deprecated USE_OPENMP, rename API_LOG_SYNC to Z3_API_LOG_SYNC (tiny part of #2709)
- 3729458 enable pypi
- dde8da8 fix bug introduced when fixing #2721
- 9b72b60 block unsound itos solutions. #2721
- 29e1fb6 fix #2720, unsound preprocessing in elim_uncnstr_tactic where datatype properties of eliminated subterms is forgotten
- 05ad90c fix for null symbol #2712
- 37382d2 Updated references to Z3 icon
- dd4905e Publishing SNK file private key for reproducible builds
- 215edcf fix; disable rewrite. fix #2715
- fe0b3d6 na
- 3c6dcea fix #2717
- d95b549 fix #2707
- f0b8da4 typo
- 2bf595c update release notes
- cbac860 fix #2706
- b9bc697 fix crash in BV internalizer due to unknown bv_neg symbol
- cb600a9 consolidate model.compact and model_compress #2704
- 1a9dfc5 inherit weights
- 784e272 print weight if it is different from default #2667
- 5f90e72 ensure generation is increased #2667
- 1281964 fix E instantiation
- 74cfcc4 clang warnings
- 20598e3 address clang warnings
- 0c1b68b remove unused variable
- c73a87c remove assert
- 779183d fixing smtfd
- d23230e fix declaration sorts of auxiliary functions
- dd827ca remove IS_GNU
- 4fabaf9 remove deprecated and bind1st and unused warnings
- 984db30 deal with warnings
- 4527a99 fix #2675
- 1fec4bb fix output
- 0a8b924 remove print
- b76dee7 na
- 1e0c1ce add definitions for under-specified cases of arithmetic operators #2663 #2676 #2679
- 6cf7d8e adding div0
- 1048abf Merge pull request #2683 from fpoli/fix-static-linking
- ac60269 Merge branch 'master' into fix-static-linking
- 7eb6731 Link pthread with --whole-archive option on Linux [ #2457 ]
- c181f89 enable static linking pthreads, conditionally, #2683
- cef5a26 update README on cmake
- 8a420c8 remove divergent ordering
- 23029da investigating relevancy
- a78f899 expand deep stores by lambdas to avoid expanding select/store axioms
- d866a93 na
- da061bb Add hurd support
- 16d4ccd na
- 18b8089 Revert "remove unused random seed parameter on cmd_context"
- 4faaff5 Fix memory leak in bv2fpa_converter
- 2308d8a Fix for partially interpreted floating-point functions. Relates to #2596, #2631.
- 1d4f8c0 Typos
- efa3c0f Fix compiler warnings
- 823bf31 fix #2664
- d0dac83 fix #2665
- e24481d fix #2662
- 376d2c1 add unit test based on #2658
- be99d3d z3str3: refactoring, move regex automata methods to theory_str_regex
- ed03c1d Removed incorrect include directories flag in ocaml META file
- 14c42c1 na
- 64dd4e1 fix #2659
- a8049c7 update nightly
- b9a407c z3str3: force eager axiom setup on new terms
- f91af02 z3str3: set up axioms on string terms that are added during the search
- 9ae1a6f Add MSVC ARM64 job to Azure Pipelines
- 3feb147 Improve platform detection, in particular MSVC ARM64
- 907ffde Drop explicit MSVC's DYNAMICBASE option setting in favour of defaults
- 837651e Explicitly add EHsc to MSVC compiler flags
- 60dde9f unit test for #2650
- 8125fb1 na
- 3fcd9e6 logging
- f4fd947 fix #2652
- e2a9cb8 remove unused random seed parameter on cmd_context
- 9847675 fix #2647
- 76b3198 z3str3: fixes to str.indexof when axiomatizing constant expressions
- 0acbdff update mk_nuget_task
- bfc3044 update nightly
- 9fae4a1 update nightly
- 4051fbd update nuget packaging
- f086f01 update nuget script
- 928e08f update nightly runner
- af442cf update nightly runner
- 0756581 add nuget stage to nightly
- 5c78f85 re-add deletion for nightly
- aef0c19 add pdb to distribution components
- e550424 use propagation filter
- 423e084 remove unused var
- 11736f0 ensure statistics survive cancelation in tactics, fix propagation for smtfd
- 203ba12 moving to context reset model
- 724a42b fix #2643
- 5eead52 Fixed linkopts -lstdc++ for ocaml bindings
- c1fa844 format
- a82cee6 add information about supported packages in README, fix #2642
- 4ce6b53 fix #2640
- ca498e2 move value factories to model
- 5122b2d add solver.timeout as another entry point #2354
- ed149ea working on core focused refinement loop
- 77c3f1f fix ocaml build by moving to Zarith methods
- 09523a4 temporary remove delete from nightly
- 5a1003f remove platform dependent copy routine
- 66339b7 update setup.py to include redist x64 #2265
- 71d68b8 fix #2445 fix #2519
- 224cc8f Fix case sensitive fs include Windows.h
- c93a265 Install dlls in prefix/bin
- f18b443 fix to_app crash
- a921b4f fix #2643 - fuzzers are here to get you @lorisdanton
- cc26d49 preparations for dealing with #2596
- 5bdcc73 remove function name
- ce06cd0 replace iterators by for, looking at @2596
- 8d942ed sudo the install
- d0cf145 fix #2630
- a1b6900 fix #2629
- a90529e add path to python
- 8c8a8ce add build step to generate doc
- a1814bf doc.fix(ast/rewriter/poly_rewriter_params.pyg): typo som-of-monomials -> sum-of-monomials
- 31a6788 comment
- a990e7f add visitor example, fix double conversion
- 4fc64ab z3str3: check for and re-internalize str.in.re terms
- 58bc2bf fix typo introducing unsoundness
- ca7d066 fix #2624
- ecba7b3 fix #1006
- fd19748 fix assert-and-track semantics for smt2 logging
- 9082547 simplify
- 26c34c9 fix #2623
- 6b7c0ce add feature description to RELEASE_NOTES
- d25c7e6 increase timeout for LTO
- 7a5ca96 remove separate API for setting solver log, use parameter setting instead
- bc50b6b fix a few warnings
- 4192c81 Merge branch 'master' of https://github.com/z3prover/z3
- 9eea5cb make smt2 log scope aware
- 8bb2442 make smt2 log scope aware
- 4643fda remove a few str copies when throwing exceptions
- 01f085a build C++ API
- ce1f2e1 build
- 16dc278 compiler warnings
- d716771 unsafe pointer
- 228b952 add also get-consequences
- be33bb7 fix build
- 6ddce9d adding SMT2 log file for solver interaction #867
- f6f3ca1 adding SMT2 log file for solver interaction #867
- b6c1334 bit-vector overflow/underflow operators exposed over C++ API
- 27765ee add stub for #2522
- 7e174f5 use Z3_char_ptr
- f4b803d expose mk_divides over API. Corresponds to a = b (mod m), #723
- f8469b6 enable default
- 66b38ea add back dotnet after adding ;*.cs to path
- 5fa177a remove --dotnet from Ubuntu due to 3.0 .Net core issues
- 02e71c7 fix #2650, use datatype constructor producing smallest possible tree whenever possible
- b0bf2f1 z3str3: recognize two-argument re.loop
- 82c39f8 fix str.at rewrite
- 9a516e5 fix str.at rewrite
- a8e7074 fix #2618
- 7c10fb8 fix #2615
- f9b6e4e batch length enforcement
- b53f66b avoid access to invalid m_length
- a1cb3a2 fix test build
- 39edf73 fix #2613 fix #2612
- 016732a move some tracing to verbose
- ea8ef3e edited error message string
- 0321312 Changed to get_const_interp to match Java and C# bindings
- bba9d11 fix minor version back to 7
- 3e6080b na
- d4c60f5 Changed makefile generation for ml bindings to use OCAMLFIND variable
- 5b4cd6d fix #2604
- c8908e8 fix #2609 fix #2610
- feff1f7 fix #2609
- a635049 fill in ad-hoc interpretation for division by 0. #2561
- 8a568d4 na
- 6616b6a only case expand for cases that contain defs. fixes #2601
- 88f0e4a fix #2592 #2593 #2597 #2573 - duplicates, also fix #2603
- fe7a7fe z3str3: fail early on non-string sequence terms
- d70b63c allow parsing commas from SMTLIB2 input
- 292e72c fix #2590
- f29b033 z3str3: add is_var() similar to theory_seq's implementation
- 1c70bce z3str3: setup uninterpreted functions as though they were string variables
- 301209c fix #2595
- 98c3887 fix #2595
- a424ab9 remove setting timeout proc to null #2591
- deb45c0 fix #2586
- 79d4502 atomics for #2565
- 18fe28c fix perf bug exposed by Shelly Grossman
- 3dcfbb8 fix #2585
- 2a1f05e remove Simplify rewrite resulting in flaky build breaks
- 20feecc z3.py
- 666a237 z3.py
- 1b910c4 hash update
- d0fc463 fix #2581
- 38ad66c update hash #2579
- 1203af8 expose cardinality declarations
- f7cc68a fix #2580
- 74aa47f fix #2578
- 2dd9ea0 fix #2577
- 64d4e59 re rewriter for loop
- 6041cb2 --lpthread -> -lpthread
- dee8a9f remove more unsound rewrites #2575
- f3f233c remove link experiment
- 6b117c0 move to zarith #2471
- 0b06a9b fix minor version numbering
- 3eac4a4 clean up examples for unused variables
- a44cf7a unused variable warnings
- 5919bc0 update for next version
- bdecd22 fix verion numbering
- dc625cb remove unsound rewrite
- 22b6233 increment version
- 48e9962 fix initialization order
- 4101652 handle case where lower bound is above upper
- b506e45 align name of tactic in report
- cd0cd82 add rewrites for #2575
- 80636dd na
- 12034df add rewrites for #2575
This list of changes was auto generated.