• 27ea23289ef39989c46da9a052a1ac41adede6d9 fix #4955
• dc4382604b934295087610734b65b05725534aff fix #4955
• 3bc18ab0d1ffbcd14b28fc5c51c4855310ae3b9d na
• ec5d08ac0045e1d8eec350d52ca6ecee813f2f61 update release script
• 80033a5527efd323b582b654fa786429e5994f08 na
• 95d98ea8ced65d9c9e34b034a7a8f3ac4c6bd400 throttle equality propagation to shared expressions
• 7c34a54e8ad2be4bd125d6484c56726ca41dde78 try different command-line
• 64ba2a9fc9919cfddcc963d0b951e6f793ebc7be fix gc of pb constraints
• 01418a06a30a5fb14f8a146d4fef7bec7ad7c699 better staging of mbi based on generation
• 990aecceb7c55523c03bcc08885d5c824a3624ce change gc strategy for user-push/pop
• b87405cc9274b10f486de02e8f34c806fb579635 tune user-pop
• 3ed490d4edb298f85c8f0444ec869215ff140314 tune backtracking
• 91c54f6c392db45e880160cfbad6992bacee1f81 na
• 8abb644378ebaf1a9699e1b2fdd32075bcfcea4e add xml file to the mix #4578
• d1dab327cd6de125392bab4d74d4ec34a9e01477 fix build
• fc3a642876cddfca38840d5e1b41cfb657e98a28 fix #4948
• 0aac7e54a91de423088f0f321b9eef1bbac87118 fix #4942
• 0e429cab33818d590eb3484c554912d8a8fe6dc2 enable new core for incremental mode
• 2ead209d406f0fc0ef964d37119e27a8f64a64e2 indentation and updated links to default landing pages
• bcbda45298d7e9df4116e67518802cf009f07291 updates to doc
• 396bfa05f3eaceceef25eb0769d50769f11e3064 fix grouping error
• 223bffd035dac5dfe9f87cb101cb55410907ee63 fix #4920
• 1a71dfac6f7a9bcce9736ab983bf27fda0f819c7 play nicebox #4918
• 96ab9edbfd5c5c9a9e56631296ff41de9cb4b821 fix #4923
• ffd57bef2427ca525bc74b16f3c4bfa3bd01c442 #4923 - eq2bv
• 690bc51b7fffff5a7d647eafb536f62c8aaa9e07 fix #4927
• bb56443e71c3c29c7fe03696a7b915560365d371 more #4932
• 43eb8623742e90a1361cac5ab64c2b87b39466df fix #4932
• 3d39f37e63c6a17f7aabe7f3c4a96ca99a778e33 fix #4930
• e902e1ef13301124555e4cc8dc72d565621e7d6a fix #4931
• c36355c1e5d43f66b1775791aed96929706c75ca fix #4933
• 0173359a507dec8c58ce71735ad7172386e4e33b debugging/testing mbi
• 4ca6d6951fcdc9af2d91bacbb8dd481bd17c59a0 use updated C++ features
• ac7d07ca58aece8690a4983da84818a94b72a16d fix #4937
• 60ef60dff8371e9b5cc92632e0221fa96091e937 euf solver updates
• 7bf691e1f95ddee202a5d07b23da61544caf7122 fix bug in tracking qhead
• 4db41c02ccf6c8a1d52015718928a695aa99acf9 remove some dead code from fpa2bv converter
• 5da71dc8478ef581d38de56a54e9a904bd670d19 na
• 523578e3f6ad5e869b3e2747169e667c9beadbee working on new solver core
• f519c58acec47c11c64eab4a145f8735fa63a6e6 Add groovy R.U.Stan option to retrieve models even when they don't exist #4924
• 799de71a9f2c9523c1a1e99169b8faa40a288961 limit recursion depth of push_not() to 8 (#4917)
• 374ae52d70b33d438190c15b905cafd411e731d5 testing mbi
• d8eba2d72f41c4494102d3f039f9db360db99319 scripts/update_api: Replace Z3_LIBRARY_DIRS with Z3_LIB_DIRS (#4915)
• 372e5ca56996dc3ed8de8b3ef0318d4706d323e0 fixes in new solver
• 21c626e3eebc100e78e7e27bf0ad5f1d603bbae8 fix bound miss-computation, include sporadic nra check for #4913
• 8546cf97d7a63e0800bfca4fec84e76eb7598a98 on #4702
• 2679ae517b7a331bd0005970a4f40db0723073d5 fix #4912
• 6284f6fb0322d72b010001df35442efcf97b527e Update nightly.yaml for Azure Pipelines
• 9d22cf4d4f347747f2b1818eba9b898734ef8530 add signing to nightly
• 1c3b768ed0fe2fd00f5ac6bb132c9f171ac2e255 update ubuntu version number
• 0ed33af279e6dd26922b24e032cb035984610b64 Update nightly.yaml for Azure Pipelines
• 8692fcdf3b5b0ec0b098b1831003a56b06904409 Update nightly.yaml for Azure Pipelines
• d72f6c80dfa59fd2ce44a27fa8e740657dff87ad Update nightly.yaml for Azure Pipelines
• 010d578e8f411da002067493aea394759fc66832 sym file
• 021bd8a994c63368a45c1819cbf7399ea5332ece sym file
• f26662d079f51989f7578115315b9e2f3b7f108d na
• 3576b66e325bf74f890ea0793b0bd3cd002a3366 na
• 0c94d6dab6539afcc0be9c777e29c6400010dc1b na
• d67f9fb3f1a26cfd5ad94135d24072cecc063359 na
• 835dd9414f8466f77f1fecadbac380dfe142ee21 nightly
• 3121c39a14d42323976e6b0357c22d0e0644bd10 nightly
• d0fbeb11c9a65109587a209156fa8bef0b9714d7 Update nightly.yaml for Azure Pipelines
• a72856111b88f7aeef12c1ea88ffa679a81ee05d add destination to custom command
• a164087384e686bb6c082f38f2ae752949352e59 remove cheap-eqs option as there is already propagate_eqs
• 5866d6ee3fc406b762dad9e6cb98e1c455a98c8e custom
• 84a7f3fcd0778e78db160f2f3e90ad9d3a169a16 quote?
• 5a20413d04ef8a4c77641431ec833bbef95a448c na
• 715b1fd39360632de5ceec5546315e43ad8ab528 try snupkg parameter
• 9e54cd63dcd5964699bbbfd3faf3a6e1b8b3746e wrap remove/move
• 2c313ddb7a30c36084456e2d706f5e786291fdda wrap remove/move
• d94244b23637e9323dcb054da8839143e3d4dc80 shutil.remove -> os.remove
• 726853de4e2b26f220db64affb3837638991e6a0 add stages
• b108f5163d9f669a2ed4dbb8392ef2c122763929 add stages
• 6c42e8068c6608edeb4496f4ddee28cf6b6e6c37 shutil.remove -> os.remove
• 6b312a58a35ae96427b93e5d8816641ae9e21a5a move/remove
• 9e86c8761e328734f02979314b0f6cded019b633 move/remove
• cd77a4d9a5e31b839faa66a51415980aae7b75c8 fix #4909
• 8e0a2c9e77edf0e8afc87a1f95abce23417df349 fix #4910
• 8cb1dd29b503288ed952c173b33ed51bdb92a407 mk-nuget-task where is the icon?
• 259a8ff786270a35596144ad3bda2f78c25bcd77 fix #4907
• dd05c683e01e809d87514d83dc96e6d2dbba143f update license to nuget 4.9 URL
• 359d66b5791814c3531b76ac51cc1334e70038ae Update nightly.yaml for Azure Pipelines
• 76a4bf5fa0df29cf2cb46eef41d81e8aa62eb6c2 Update nightly.yaml for Azure Pipelines
• 64a92f720bd4b02163ea381c51a0b790f6cf5472 new nightly
• c100a18b37c7de58585540f2bb70fbf409fbfdef use ReleaseVersion macro
• 3cd49d56c23ad65572ebbcba8851cc45939b28dc Update nightly.yaml for Azure Pipelines
• 5ce3c18fd04cffe135d1b30bda95fec9cb19b926 Update nightly.yaml for Azure Pipelines
• e8b506a1728110f128b0d18ec1de7133171873d6 update for nuget
• 4039785bb611c41766d453dded505cd1aa643550 initial steps for including symbols
• c022a3e5736d9f277077c61fbf05052098834e34 fix reset break
• 28a6da4532c952a7077d233421aa498f5ca2ff59 fix #4902
• 8521d2caaaa2ab2b305978d133da86cf8368d95e check engine configuration for unsupported engines #4898
• 7ce1c38544afea8e46b42ba8d7f4d46001489b8a 'na
• e1f71d4932846c0775e0931ae45aa37b09e1c16a fix #4904
• 26af694d2c9e3e1ef7a6e605c025626c7a751f4d add overloads to != and == based on #4906
• fa5567fa1fb3c0c687b495d6f67257e17c573424 fix #4905
• 727095c563a866457406d96f7bb016b0d3c8af68 fix #4899
• 11477f1ed14d0af2e613ba58cef1ce3f1851b5a1 fixes in new solver
• 26b4ab20dbe6f79abf6d7bf7987d1d19d66e670d Update .gitignore
• 692bed79912c6f1718a993073e73d37cd98f4bb2 fix sign bug in internalization of literals
• 0ef8ebe89ffd28bf1ceb71ef5ede47a768dc2490 fix #4895
• 7fe829847938627ad880d3781fc81ac8dfd96cb3 fix #4873
• f71204c2220acf60a511b3eb2c5a83c941c13e36 fix #4879
• 0643e7c0fca2b16dae9a4799471bc50e66a333a1 fix #4886
• dda4d66325d9cfa219ce79e1eb959bcf131597af fix #4888
• 8cb30d05055b3c8abf0eda90bc04e97a18a0d08b na
• 89fb55a86422b24e922033f803c4cb78eacf6e65 fix #4890
• 89a6c7a349602c5feb2138627b1194cb587da2cc fix #4883
• 4d7062d2a12e47b3506fc105e791a67867d70f1f fix in nla_ordered_lemma
• 621e99284b02f6804a283a19ad696a8675a80623 fix arith_solver=6 regression over solver=2
• fae9481308040ba84fe0e081e142cb9cd3e86cb9 fix #4875
• 97683bd48a00d51d0c8deeaff1adaaeae41400de fix #4876
• 8ce08d57a015fc165a580c8341b210e33f2697f3 na
• 43ddb083327fcee316c345a4f9ab7f48e5f18fed fix #4874
• 9b9d9067025057aeb1aa911b756cb60e5f08d57b fix #4871
• c49d39af81a2a05a7cdb450175aed7a0c2ce72a9 perf for #4655
• f5f980fa381f16ee92b284c4fb87435cbbf6bfbf add rewrite rule
• 430b4ea25229830593c00199ca5175e1f4987cdd fix #4870
• 9f6a0a868af38f4a7baa0766bae32de7af4d8754 fix #4389 fix #4859
• 409414c5b386d9f25702f47b3d04d688c004f43e #4655
• 289cc9de7926aab1249c0508846f8f9ecbd2be7c add rewrites for replace_all
• 7089610bbd45fc51651ba8caac925cabb479092f set arith.cheap_eqsTO True
• bb3faf527c77c9662869bbb447e1c1ed62d8d992 Update azure-pipelines.yml for Azure Pipelines
• 982da8db0561d32f0fe7cddcdaf5e92729f5a6c0 fix #4868
• 6c9bdc949e90bdfb4605aa7f88a637d121ac710b fix #4848
• 27dac3e1a03b13fbe33b6787bbadf22b2302ba49 fix #4844
• b90143cc0eaa11f5c77863129468be8f51584ac3 set the defalt for cheap_eqs=False, do not run
• 4c1fcbaa62e487c62b7cd47d2123885007b335f6 fix #4865
• 746dd745ad373c7b304b8e87f432b7f258ee06b8 fix #4856
• c3c7aad1a87eab6f7ba9d955300c42ab30984cea na
• 2e5eb2dde23fa599cf59dbfdfbf9e229cd191f29 Tree fix (#4864)
• 0c93c7ae03b8515fe99521e6ce35c1528bb799e7 Fix finding .git directory in CMake when z3 is a submodule of some other repository (#4850)
• b0cecf774731f2cbae45ac697d4733723690ac04 Make multi-index arrays not so bad (#4857)
• 4d55f836540ac4ea5fa4943fed79809ffcfa6601 misc
• b0fd25f04190cb54fbfae69cec8b8369a96c5300 z3str3: don't compute intersection difficulty against a null automaton (#4846)
• 6d427d9dae4f374107297b5bf0dd0fa5651c0d1b fix #4839
• 12198d13ac75459d870d9caf5a793896765abd2d fix #4794
• 9156e355d86a2fd00883b5c7b2d3f0eccc941a5f log
• 3bca1fbcd82d0dd8afec741d8759a72f8490f1e2 Java type generics (#4832)
• bb24b3f2bec212931f4518d8b8ae771594f6e277 fix #4836
• 260f759177926056c1b460a92ed93f46bd041c9a fix #4835
• 67bbdc752498e6d2a618c2762b9431c92b581e7a fix initialization order
• 5c2f07df09585d6437b85ebac7db9ed3c2f73924 max lex less chatty
• eacef5f3f9af67521137bf955b092114c749dc49 deal with warnings over unused variables and procedures
• 64af8981ba40262b369fbb55ab99da7ea4e88b20 fix #4834, regression after delay-propagating disequality axioms
• b7e1b1e118b1f29a9937f054f8a56c468475ab28 get rid of threads in the scoped_timer thread pool prior to forking, on non-Windows (#4833)
• 05c5f72ca1dd6a2e8b31ebc38cfe8a6c9004955b fix #4829
• 17f04099a50f3d74b12aeae04d5dcda47ef67a00 fix #4831
• 6e14d3fbd305d4a85c5735340d634d61d0ed0159 fix #4795
• df09cb7c95d1a858aa862bd1d1d7088b89f37937 fix relevancy test
• 35900ee8eaf890edba32ccc877830073dd9b914f avoid crash from #4772
• 67a8492bd0b8d70ed1518633611bc8b412180be7 more graceful proof checks
• 6771e44d93a4d7331c2f7642c2ae2b1118624fd9 fix #4825 #4824
• 1619311ff7ae7213ec0389b1ad94b60a58b38d15 fix #4826
• f58618aa04aa36f407848b1dfe060630882caea2 fix java compile
• b5a6c6bc6603759855ae95ab6e1d819f35c148d5 attempt at more graceful timeout handling #4821
• d6a5ef43434a1ac0a51f9712c215bb710a6ac5a5 add recfuns to Java #4820
• 6aba325ceada29b81b05921b8f9890da20084aa1 z3str3: reject certain unhandled expressions (#4818)
• c27a3250174f7ab899cfda0fc5c008adebde6fcb na
• b769c0054b4c58564155c93a9f1dedc0b2835ad3 fix error messages for #4816
• 291502f8e490d6119f78decfb5bc43dad97b8630 this->
• 1008b2d4cb05821359f4c8a483fb6c48845e7e08 fix #4812
• 193ca5744473050214c5312da76b44c212c73c63 fix #4811
• 65464f5944901bdac4db4bab70ca4b8363c9d270 include order
• 797f50e6998d43934c83baeda0170c3bed6e0c8f DRAT debugging updates
• 6d0b89a989827599dfa986bc51dafeae77e7fed7 fix #4810
• 065e0652a3e15638d99935c6c95d7d6e9b52fcba fix crash when parsing datalog format
• 299e1788b8fe309fc98b3bff9da5c64914e87316 fix #4808
• d6106f26ff6e61a93b4100bc68966d0bbbddc9d6 disable gcd test
• 1b768c9b3aebf77e41a90a53036e299ffa06a2ba fix #4805
• 12697767778532b237c03fe7415935b72c7ef1a2 remove experimental option. Fix #4806
• ac1b3fc6f2690101d706d39ea09529241c559a28 fix delay blasting and relevancy
• 9f34af5e1885ef311c5744df51275efb7a63d704 update justifications only at level 0
• ee04bfd1748f95f9f44e6f2b2ea0487cf375bfc8 fix equality propagation
• a475e7cf5a14a20724d57e297dd65d04656b5b00 Add gcd test to bv-rewriter
• 6506d33b35edb78a521bcf536809ac8ceeecb9fb Add GCD test
• b7b7970c4ae164bf17c315e190158bc4f040a32c guard table erasure for representative
• 40159a3a96b3a50622e00424a345538466dcdf2f fix single-thread build
• 0fa88efc2b6340180148c3b3307ece1447a9fb7b scoped_timer: wait for timer thread before main thread continues (#4803)
• e16acd0965bcb679e54c451eba61a4a8ed474a03 move std::function initializer to beginning of class
• f6f594e21dc9e7ea085e3e903795d64c8bd6eaed fix missing equality propagation in new bv solver
• 36e40a296f81dc3a374a4bb72bfbb7a0bf9a7c2e add logging for rewriter.flat
• 85a20791dbc84e5fbe09198c1be72f3c365807f2 fix relevancy tracking in new solver
• 36e94122524ec7833758c1c6e10b188d128e333a fix #4796
• 98db260a93bf882155756da3ea61e2f7b65be270 relax unhandled condition
• 49a0266c6af355e2f32c317e6d1b8a2ef366af8e na
• 9fa17a432a51cd864d543b041e6985e8a028dcfb bug fixes in nullability check
• c15001bf699a7777b9d62ceff02f15301eb1df5d #4532
• 71ac40ca238648e5a42726c01090f42260ead7b6 fix #4793
• cb4e5197faa4b0af421edc7cc7b547bde820067f #4740
• 7f869e513b05990cee3fc80eed43494002d7dea5 fix #4792
• d61f30fdc68480658095a62693ff5eb92d75a8b3 force flat for solver 2, fix #4789
• 5d10cb7af4f264c40e102071b3f4d788bfb5d5b6 fix #4791 - diff is left associative
• 72e57f550d46f120946d253e314e96c81ebfa604 update release similar to nightly
• 7e68d546bad299d26beb8cde4627af61b9fb3651 na
• aced115b7014d1571eb8ce5a5b38af5e0e059dcc model validation
• 16db8bf49e5dfd1ecb65431a97972ed471b80b06 add model validation
• b5aab7ec2a0113d8976ebe578c67d48a21bb92ff fix clone
• 9704733693a0672a6d6db0f3576f0dfe8fc4f2d0 fix #4790
• fdd3e6c4c2f18576513517e4714f76852ead94d7 Update nightly.yaml for Azure Pipelines
• 8c60e7b8f415c0fe6d5fa1b3d1c6f2279ffa93a8 Update nightly.yaml for Azure Pipelines
• 41cc0372042a1b750d025b442b9c43965ed4b606 change manylinux to ubuntu-latest
• 4810b4cac29ce1ae255fdc3bc1a0718ce7b4b673 add a comment in nla_order
• fc5e5a20980b45b0c766edff1e1408396836420d add a comment in nla_order
• fdedeed7aeeaa499224cc1e36e2b4088e4293a6b additional sign related fix for #4740 https://github.com/Z3Prover/z3/issues/4740#issuecomment-721508240
• 5ace60c812a1178dc0e60c4a1099a15fd10c432b enforce guard option
• 672e39238636fdcdad52e00d09dc3e9422289a2a guard
• be50f389031b0b90c3aeb843f776d135413a9295 enforce sign coherence #4740
• 638ef9ed03cb0070f9b01a479cb29ab762c8690a enforce sign coherence #4740
• e955bd09e52d3277555af3e2f8a0933bfaa2f36a push equality for #4740
• 3c9ada54b64e5516e0cf869c5de7881686df8fd0 tune hoist-rewriter
• 768e2c1d0d3bf9127796665ef9b9c864f4c0caa3 tune hoist-rewriter
• 4d26aabd83a607c0187ce332b96c92608f0bf840 fix bug in rewriting of power
• f78980c81c5092c8f8b67be8933b8350a91d07ec fix rewriting of power
• 7d205f1cf0c7a6bb990302e4b3c880cabf21a0f3 TB08-009 fix z3 build on windows (#4782)
• 864eaf8bf893103ede09be06878e1e7cb51996a9 remove unsound rewrite #4778
• e2c1436cc8e17cbe93b18dc83d3af573dfea115e fix #4775
• 89ffb45c4f94a7d6a857d3c24563727a12f11f0b fixes to bv/dual-solver,
• a4354c960cfdb71fa1ff8e2fbc903c7a4a7e0113 na
• 752f08c9d6ca9eeefc6837db5b0a57583edd1326 check_feasible is called after column is added for fixed variable
• 2ead7c77ee3785e27a0cb026ac904fca2b96267d use value function in lar_solver
• eadf7556282854d629826786a861fe06b69989cb Fix bonus subtraction in fp.rem. Fixes #4564. Fixes most of #2381.
• 372bb4b25afeb3d727060a7063470e4a11b78983 Fix reference counting in Z3_mk_fpa_to_ieee_bv
• 30fd01b526df65aa09e7d1785bc5fb333b12a680 api: avoid copying param_refs whenever possible
• d0d06c288a76236ea6fb32b3858e7414e7d5f4c5 rename
• 620204bbb464341d2f33e7502d92313f0acf8e43 use value function in lar_solver (#4771)
• 533509776839b79a22610254107a216d0853a9e3 use get_value/get_ivalue API instead of self-rolled from arith_solver
• ee12e3fb52a6bd7d45a359135bf1a16ba4d78d76 add init_model, global m_delta, get_value, get_ivalue to push model maintainance into lar_solver #4740
• ab199dedf9f6bf21bd16c9e5869e7eb71575a58b debug arith/mbi
• fb6e7e146bdec63b34fec628f548653ab51bb6b3 test mbi
• a764d528a1f31f75c8db76cd706fd08620366149 'clean
• d64bc795f0f2a5e6ecdca17c1f5143a348a5d5be wrong assert, compiler warnings
• c03c395267dee98032f8d68124eecd72ceec50ca Add missing assertion. Fixes #4642.
• 1730bc7c7ff2e42d88a4316d872392ac9307f727 fix #4763: shell not finishing before hard timeout
• 0e1def5bd6950e7e967348335e04be5905e99626 fix #4736
• f354671465a3bce85d4e3a484a6aeb8a96fe3676 add parameter for scenario from #4743
• ceedd7e84dde6f6259bef70784aafe91513fe08e #4721
• c07cfc0e6971f8696a7ed553155885f64196fa4a include path to thread and guard by SINGLE_THREAD
• ac4bcb9034839d6f95b6f091f74ab10cc2b510c9 update logging for lemmas
• 91511f73a036559bdb49089e3ea1c0406dba30ac fix #4744

This list of changes was auto generated.