z3-4.8.8
4.8.8 release
Changes:
- ad55a1f Update release.yml for Azure Pipelines
- 42e6cbc publish also ubuntu build
- 9a44ed8 enable pip
- 2804b40 disable nuget publish for now
- b42ea38 Automatically push release pipeline packages to nuget.org (#4249)
- cceae2e old solver as default
- 2e714fc expose uninterpreted op versions for ad-hoc parsing
- e459cf4 na
- 54f38d0 fix #4235
- 6a61e8d fix #4234
See More
- da9b037 fix #4233
- fc6bdb9 fix #4232
- aa3749f fix #4231
- eda2eb5 fix #4245
- 0acaf1c fix #4218
- 1f15033 z3str3: remove legacy code (#4215)
- 691759c fix #4227
- 603b555 port progation from cons branch
- 2d08baf fix #4219
- 1a642b4 na
- 93004a9 fix #4225
- bbaedbc fix #4224
- 6f6c8d7 fix #4216
- f2449df introduce ul_pair associated_with_row
- d20259b remove stdout
- 82236d4 some simplifications in theory_bv
- 911d23a fix #4210
- 7b1aee4 fix #4203
- 2104624 updated release notes
- 3985943 na
- a34c5a9 bail out on big rational numbers in nla monotone lemmas
- b81ab94 pipeline with release mode (#4206)
- be998c3 Allow different parsing strategies (#4205)
- 39fb44f fix #4200
- 2a93ac3 fix #4200
- 6f48c9c na
- 3473dec na
- 6a540e8 add Julia to pipeline (#4199)
- d3e4dd6 relax condition on theory disequality propagation fix #4194
- fcab7e4 fix #4195
- 91a190a disable multi-threading for validation code, masks #4196
- 5e4276b fix #4197
- dc9221e limit iterations on equality solver based on experimenting with #4178
- 37f6364 fix #4103
- 09d881c na
- 75859ef model anomaly fix #4171
- 4067c84 prepare for stronger rewrites
- 6e4a059 build warning
- 0f1815c fix #4181
- f30d63a better rewriting for ule
- f3dd58d fix #4187
- 47fa6ba fix #4191
- 8be266c micro tuning for #4192
- f313ab9 correct newly introduced rewrite
- ec8866c na
- f0d33dd some simplifications based on #4178
- 2695221 [Julia bindings] Changes for libcxxwrap 0.7 (#4184)
- 6088da5 fix #4176
- c94a9e8 na
- 8dd522d fix #4057 fix #4061
- dcb75c4 fix #4174
- 166be6c add constructor preservation axiom to update-field
- f859063 fix #4164
- 5b6255e small updates
- 397bf2d move windows dependencies down
- 16bc5b8 build warning
- 9757413 fix #4163
- cb5c2d3 fix unit test build
- 893265c fix #4166
- e9119a6 fix #4168
- dbfa3dd [spacer] implement spacer::is_clause() (#4170)
- 799b613 avoid repeated internalization of lambda #4169
- 7ae2047 remove assignments to lambdas, exposed by #4169
- 9c52d4e debugging #4169
- 68f1f1e fix #4162
- 9f6a733 add hook for induction
- fd911a5 build warning
- 0e77074 another revision of purify_arith, fix #4144
- 3fc001b simplifications noticed by trying #4147
- 7cfd16c correct ordered lemmas
- 56690d1 remove incorrect order lemmas
- b0ffad9 Merge pull request #4092 from mtrberzi/regex-compl-inter
- 0fb6a7c Merge pull request #4101 from mtrberzi/int-to-str-leading-zeroes
- 4d54b41 #4153
- e67112f NYI control paths
- ee1d393 files to make build easier
- 7e34925 Improve UX for unreachable/unimplemented errors (#4094)
- a11dc5d shuffle checks for enable_edge around fix #4159
- 71e9bf1 initialize local variable
- 4defe9b reorder
- 8dde1bf compiler warnings
- 00d35c2 initialization order
- a1928a2 update expected
- 97fe2c8 remove an assert
- 35e3df4 cosmitic changes in int_branch.cpp
- d5162d9 add an assert
- aa0f5db fixes
- f8037ff always call find_feasible_solution in move_nbasic_columns_to_bounds()
- ba40a57 better branching with usage_in_terms()
- 3bbf147 na
- ccce599 fix #4143
- fa1197a fix #4155
- 815fedd fix #4156
- fa88dab fix #4135
- b571e43 fix #4146
- c5550e4 build
- 1dc8b59 fix #4154
- 1f9e022 fix #4131
- e3f712b build
- 19409a2 value sweep
- 38e0968 fix #4128
- 4f46292 fix #4116
- 3a63c37 fix #4127
- 8996e81 fix #4120
- 4938ea7 fix #4123
- 1c2aa10 fix #4125
- a0de244 pleay nice with alignment
- d818233 unused variable warnings
- 5434f3e fix #4105
- f119398 fix #4102
- decd69a move to util
- 6d4bd37 fix #4104
- fc1321f fix #4104
- d37ebb8 na
- f7a7b9e fix #4108
- 7358881 fix #4112
- c2e0491 fix #4113
- 0499b6b some fixes in branching
- 029edcf fix #4114
- 51c3778 fix #4106
- 530f772 fixes in branching
- 236edad fix #4111
- dc852a6 fix #4110
- d309429 fix #4107
- 16d34b9 fix #4100
- 626d018 fix #4098
- f919380 add recfun rewriting, remove quantifier based recfun
- 7f1b147 remove
- 9f378bb #4099
- a884201 remove using insert_if_not_there2
- 9ea1cf3 na
- 1a5d663 z3str3: disallow leading zeroes in int-to-string conversion
- d21911c z3str3: fix support for re.complement and re.intersection
- 785c9a1 fix #4049
- 6ab8346 fix #4082
- a3844af fix #4081
- c3b33aa fix #4090 fix #4088 fix #4085
- 470e87a update rewite modality
- 851c38f fix #4086
- 2793c3a more replace rewrites #4084
- 03ba268 more replace rewrites #4084
- 7597396 fix #4080
- 6ff61d1 fix #4062
- eb2d7d3 fix #4079
- 64cb5ca remove spurious output
- 04fec3f fix #4076
- cc8cd2c na
- 9c3f019 fix #4069
- 8c5993d max term
- 8921ed5 fix a bug in Horner heuristic
- 8f29766 fix #4073
- 50d5811 Fix the Julia bindings paragraph in README (#4068)
- 0829023 add docs (#4072)
- 8fe3caa throttle digit constraints
- c7878e3 fix #4060
- 886f4cb fix #4029 - propagate digit literals on all units if they haven't already been propagated
- f94abf6 fix #3978
- caa5b09 fix #4050 - have to delay model compression because it may use internal symbols that have to be transformed. model compression is used prior to displaying certificate
- 95a78b2 updates to seq and bug fixes (#4056) [ #4037, #4044, #4040, #4045, #4036, #4025, #3200, #4053, #4052 ]
- 53c14bd Use Position Independent Code flag on Static library builds (#4043)
- 5ec04f7 forgot to remove unneeded class field
- 220bc7f fix #4048: incorrect bvurem rewrite when divisor=0
- dd064a5 delay digit axioms until solving itos succeeds
- e3e6959 fix #4026
- c8b9eba fix #4028
- ad8eb8f #4024
- e1fa04b disable breaking change to model generation
- eded7d0 fix #4006
- f76c642 another memory managment leak fix. Relates to different leak exposed by #3997
- 4495789 more checks for #4013
- fcc34a0 fix #4019
- 339a256 fix #4021
- 79b776f na
- 19e0285 move deep internalization out of theory_seq
- b92b6c0 add missing digit axioms
- 99c90d2 fix crash
- 0fe2d3d more seq overhaul
- a9c4984 more seq overhaul
- 7673547 fix #3999
- bcbe802 remove buggy bv-trailing
- 3e9479d a lot of seq churn
- b8bf608 na
- a83f72b some fixes
- 501aa79 split into seq_axioms and seq_skolem
- d5eef9d na
- 040d4b8 fix #3994 remove bogus option
- 767dff4 fix #3903
- 19f655c fix #3930
- dd3e574 fix #3983
- 1f23ae8 fix the test build
- 95cb828 make lar_solver pretty printer const on the solver
- 5208b64 expose only necessary methods of lar_solver
- 6d8e540 return an empty model when the status of the solver is neither FEASIBLE nor OPTIMAL
- cb4ceea fix #3985
- 206c3e2 fix #3979
- dde0c51 warnings
- f67077b warnings
- d465938 add lower bounds on lengths if they are not present
- e6174c8 bail out of mb branching if lengths are not available
- 40b4ca7 fix #3950
- 357ec2f fix #3948 - cache has to be reset also when processing 'and' because it could be processed in an incompatible context by the caller
- 2e1e9c9 na
- 3845e08 fix #3878
- d0f9405 fix #3966
- 068f65c fix #3967 regression from using rewriter mode that splits strings
- 79a2b52 fix #3971
- 1ec9779 fix #3972 regression from changing the way assumptions are initialized
- 25252af fix #3975
- cce27ff fix #3976
- 164a73f fixing #3933 - remove unclear code normalizing itos
- b04c974 na
- 835b57b fix #3961 fix #3940
- 7ed9996 fix #3962
- 5f81913 fix #3951
- 5e0c34c fix #3953
- 2a0537a fix #3954
- b8c069c fix #3955
- f564c32 fix #3957
- d7d6877 fix #3958
- 387964f fix #3960 fix #3959
- 0f69783 spelling
- fe7146d fix #3913 - change assumption tracking to be granular based on disabled guards
- e102779 more to #3926
- 7caae3f small improvements in tableau in rows and bound propagation
- 9079393 small changes in one_iteration_tableau_rows
- 9223f61 build
- 9f42338 fix #3926
- 299a6f4 fix #3939
- d3db2af fix #3941
- b4e7730 fix #3938
- 6a56954 fix #3943
- 5dafd1f fix #3945
- 5c4f775 fix #3935
- 01c12c9 na
- 84a4d98 fix #3936
- 75a460c fix #3932
- 9b609af fix #3924
- 51eaf84 fix #3931
- c85113a fix #3928
- db9d6d1 fix #3836 remove unused and buggy hoist_cmul
This list of changes was auto generated.