z3-4.8.10
4.8.10 release
Changes:
- 517d907 Update release.yml for Azure Pipelines
- af914f1 change to macos latest
- c5432db merge
- 3a572ed fix build
- 48058e7 fix #4951
- 3f2349f update release notes
- 9dcf44b fix git_utils.cmake (#4954)
- fa4869e fix #4949 - and/or get rewritten depending on parameters for rewriter
- 3a2ed69 fix #4952
- 80f429c nuget
See More
- 27ea232 fix #4955
- dc43826 fix #4955
- 3bc18ab na
- ec5d08a update release script
- 80033a5 na
- 95d98ea throttle equality propagation to shared expressions
- 7c34a54 try different command-line
- 64ba2a9 fix gc of pb constraints
- 01418a0 better staging of mbi based on generation
- 990aecc change gc strategy for user-push/pop
- b87405c tune user-pop
- 3ed490d tune backtracking
- 91c54f6 na
- 8abb644 add xml file to the mix #4578
- d1dab32 fix build
- fc3a642 fix #4948
- 0aac7e5 fix #4942
- 0e429ca enable new core for incremental mode
- 2ead209 indentation and updated links to default landing pages
- bcbda45 updates to doc
- 396bfa0 fix grouping error
- 223bffd fix #4920
- 1a71dfa play nicebox #4918
- 96ab9ed fix #4923
- ffd57be #4923 - eq2bv
- 690bc51 fix #4927
- bb56443 more #4932
- 43eb862 fix #4932
- 3d39f37 fix #4930
- e902e1e fix #4931
- c36355c fix #4933
- 0173359 debugging/testing mbi
- 4ca6d69 use updated C++ features
- ac7d07c fix #4937
- 60ef60d euf solver updates
- 7bf691e fix bug in tracking qhead
- 4db41c0 remove some dead code from fpa2bv converter
- 5da71dc na
- 523578e working on new solver core
- f519c58 Add groovy R.U.Stan option to retrieve models even when they don't exist #4924
- 799de71 limit recursion depth of push_not() to 8 (#4917)
- 374ae52 testing mbi
- d8eba2d scripts/update_api: Replace Z3_LIBRARY_DIRS with Z3_LIB_DIRS (#4915)
- 372e5ca fixes in new solver
- 21c626e fix bound miss-computation, include sporadic nra check for #4913
- 8546cf9 on #4702
- 2679ae5 fix #4912
- 6284f6f Update nightly.yaml for Azure Pipelines
- 9d22cf4 add signing to nightly
- 1c3b768 update ubuntu version number
- 0ed33af Update nightly.yaml for Azure Pipelines
- 8692fcd Update nightly.yaml for Azure Pipelines
- d72f6c8 Update nightly.yaml for Azure Pipelines
- 010d578 sym file
- 021bd8a sym file
- f26662d na
- 3576b66 na
- 0c94d6d na
- d67f9fb na
- 835dd94 nightly
- 3121c39 nightly
- d0fbeb1 Update nightly.yaml for Azure Pipelines
- a728561 add destination to custom command
- a164087 remove cheap-eqs option as there is already propagate_eqs
- 5866d6e custom
- 84a7f3f quote?
- 5a20413 na
- 715b1fd try snupkg parameter
- 9e54cd6 wrap remove/move
- 2c313dd wrap remove/move
- d94244b shutil.remove -> os.remove
- 726853d add stages
- b108f51 add stages
- 6c42e80 shutil.remove -> os.remove
- 6b312a5 move/remove
- 9e86c87 move/remove
- cd77a4d fix #4909
- 8e0a2c9 fix #4910
- 8cb1dd2 mk-nuget-task where is the icon?
- 259a8ff fix #4907
- dd05c68 update license to nuget 4.9 URL
- 359d66b Update nightly.yaml for Azure Pipelines
- 76a4bf5 Update nightly.yaml for Azure Pipelines
- 64a92f7 new nightly
- c100a18 use ReleaseVersion macro
- 3cd49d5 Update nightly.yaml for Azure Pipelines
- 5ce3c18 Update nightly.yaml for Azure Pipelines
- e8b506a update for nuget
- 4039785 initial steps for including symbols
- c022a3e fix reset break
- 28a6da4 fix #4902
- 8521d2c check engine configuration for unsupported engines #4898
- 7ce1c38 'na
- e1f71d4 fix #4904
- 26af694 add overloads to != and == based on #4906
- fa5567f fix #4905
- 727095c fix #4899
- 11477f1 fixes in new solver
- 26b4ab2 Update .gitignore
- 692bed7 fix sign bug in internalization of literals
- 0ef8ebe fix #4895
- 7fe8298 fix #4873
- f71204c fix #4879
- 0643e7c fix #4886
- dda4d66 fix #4888
- 8cb30d0 na
- 89fb55a fix #4890
- 89a6c7a fix #4883
- 4d7062d fix in nla_ordered_lemma
- 621e992 fix arith_solver=6 regression over solver=2
- fae9481 fix #4875
- 97683bd fix #4876
- 8ce08d5 na
- 43ddb08 fix #4874
- 9b9d906 fix #4871
- c49d39a perf for #4655
- f5f980f add rewrite rule
- 430b4ea fix #4870
- 9f6a0a8 fix #4389 fix #4859
- 409414c #4655
- 289cc9d add rewrites for replace_all
- 7089610 set arith.cheap_eqsTO True
- bb3faf5 Update azure-pipelines.yml for Azure Pipelines
- 982da8d fix #4868
- 6c9bdc9 fix #4848
- 27dac3e fix #4844
- b90143c set the defalt for cheap_eqs=False, do not run
- 4c1fcba fix #4865
- 746dd74 fix #4856
- c3c7aad na
- 2e5eb2d Tree fix (#4864)
- 0c93c7a Fix finding .git directory in CMake when z3 is a submodule of some other repository (#4850)
- b0cecf7 Make multi-index arrays not so bad (#4857)
- 4d55f83 misc
- b0fd25f z3str3: don't compute intersection difficulty against a null automaton (#4846)
- 6d427d9 fix #4839
- 12198d1 fix #4794
- 9156e35 log
- 3bca1fb Java type generics (#4832)
- bb24b3f fix #4836
- 260f759 fix #4835
- 67bbdc7 fix initialization order
- 5c2f07d max lex less chatty
- eacef5f deal with warnings over unused variables and procedures
- 64af898 fix #4834, regression after delay-propagating disequality axioms
- b7e1b1e get rid of threads in the scoped_timer thread pool prior to forking, on non-Windows (#4833)
- 05c5f72 fix #4829
- 17f0409 fix #4831
- 6e14d3f fix #4795
- df09cb7 fix relevancy test
- 35900ee avoid crash from #4772
- 67a8492 more graceful proof checks
- 6771e44 fix #4825 #4824
- 1619311 fix #4826
- f58618a fix java compile
- b5a6c6b attempt at more graceful timeout handling #4821
- d6a5ef4 add recfuns to Java #4820
- 6aba325 z3str3: reject certain unhandled expressions (#4818)
- c27a325 na
- b769c00 fix error messages for #4816
- 291502f this->
- 1008b2d fix #4812
- 193ca57 fix #4811
- 65464f5 include order
- 797f50e DRAT debugging updates
- 6d0b89a fix #4810
- 065e065 fix crash when parsing datalog format
- 299e178 fix #4808
- d6106f2 disable gcd test
- 1b768c9 fix #4805
- 1269776 remove experimental option. Fix #4806
- ac1b3fc fix delay blasting and relevancy
- 9f34af5 update justifications only at level 0
- ee04bfd fix equality propagation
- a475e7c Add gcd test to bv-rewriter
- 6506d33 Add GCD test
- b7b7970 guard table erasure for representative
- 40159a3 fix single-thread build
- 0fa88ef scoped_timer: wait for timer thread before main thread continues (#4803)
- e16acd0 move std::function initializer to beginning of class
- f6f594e fix missing equality propagation in new bv solver
- 36e40a2 add logging for rewriter.flat
- 85a2079 fix relevancy tracking in new solver
- 36e9412 fix #4796
- 98db260 relax unhandled condition
- 49a0266 na
- 9fa17a4 bug fixes in nullability check
- c15001b #4532
- 71ac40c fix #4793
- cb4e519 #4740
- 7f869e5 fix #4792
- d61f30f force flat for solver 2, fix #4789
- 5d10cb7 fix #4791 - diff is left associative
- 72e57f5 update release similar to nightly
- 7e68d54 na
- aced115 model validation
- 16db8bf add model validation
- b5aab7e fix clone
- 9704733 fix #4790
- fdd3e6c Update nightly.yaml for Azure Pipelines
- 8c60e7b Update nightly.yaml for Azure Pipelines
- 41cc037 change manylinux to ubuntu-latest
- 4810b4c add a comment in nla_order
- fc5e5a2 add a comment in nla_order
- fdedeed additional sign related fix for #4740 #4740 (comment)
- 5ace60c enforce guard option
- 672e392 guard
- be50f38 enforce sign coherence #4740
- 638ef9e enforce sign coherence #4740
- e955bd0 push equality for #4740
- 3c9ada5 tune hoist-rewriter
- 768e2c1 tune hoist-rewriter
- 4d26aab fix bug in rewriting of power
- f78980c fix rewriting of power
- 7d205f1 TB08-009 fix z3 build on windows (#4782)
- 864eaf8 remove unsound rewrite #4778
- e2c1436 fix #4775
- 89ffb45 fixes to bv/dual-solver,
- a4354c9 na
- 752f08c check_feasible is called after column is added for fixed variable
- 2ead7c7 use value function in lar_solver
- eadf755 Fix bonus subtraction in fp.rem. Fixes #4564. Fixes most of #2381.
- 372bb4b Fix reference counting in Z3_mk_fpa_to_ieee_bv
- 30fd01b api: avoid copying param_refs whenever possible
- d0d06c2 rename
- 620204b use value function in lar_solver (#4771)
- 5335097 use get_value/get_ivalue API instead of self-rolled from arith_solver
- ee12e3f add init_model, global m_delta, get_value, get_ivalue to push model maintainance into lar_solver #4740
- ab199de debug arith/mbi
- fb6e7e1 test mbi
- a764d52 'clean
- d64bc79 wrong assert, compiler warnings
- c03c395 Add missing assertion. Fixes #4642.
- 1730bc7 fix #4763: shell not finishing before hard timeout
- 0e1def5 fix #4736
- f354671 add parameter for scenario from #4743
- ceedd7e #4721
- c07cfc0 include path to thread and guard by SINGLE_THREAD
- ac4bcb9 update logging for lemmas
- 91511f7 fix #4744
This list of changes was auto generated.