• da9b037f2a6777c2f29170c388d564f3b3a34227 fix #4233
• fc6bdb970866280608b5ed6a6311dd9782e538c7 fix #4232
• aa3749f678a83f717681600cf4c6c996acc6a18e fix #4231
• eda2eb512454a4ae305b5147fe6cbb8fdb177f39 fix #4245
• 0acaf1ca0f3f3669fffb331dafc8839bed17debe fix #4218
• 1f15033ca257b609c639291f1be835b26f03b422 z3str3: remove legacy code (#4215)
• 691759c9e2c193b872027e4e74c50428f2c8e8ba fix #4227
• 603b5552fac7a514f3a05cd02c791389acd29973 port progation from cons branch
• 2d08baf3d577ad972450cbe92d3457156265f2f6 fix #4219
• 1a642b4311226d1495ff821e618548cd73a3d114 na
• 93004a9d49effe79852fb19e48f545be56f37a73 fix #4225
• bbaedbcccc61b36f53791b874eba2771ed3d2dca fix #4224
• 6f6c8d76eb3f9a4aa258d3c3d3a1176dcdc465b9 fix #4216
• f2449df06eeb666cd545b6fdd7e54f7bf31495e6 introduce ul_pair associated_with_row
• d20259b57aea956e44e0fa4ed9f226e924aee5ef remove stdout
• 82236d44c6c4a997e538b1ccfc5c521be9cf668c some simplifications in theory_bv
• 911d23af1a488fc3ac703915a0366fdcc1f6af5c fix #4210
• 7b1aee48dda022f85b8cc5898be8f5c51f3375c5 fix #4203
• 2104624dfa2c8f3e47bb53514705f658ae1a4a64 updated release notes
• 3985943eecb107ec89ca539ec3d7766552b67835 na
• a34c5a9450ed6b5d562c846e7c173ea7187fcfbc bail out on big rational numbers in nla monotone lemmas
• b81ab94db7e9a5fa9de9bc6aa2b69c4995ffc824 pipeline with release mode (#4206)
• be998c308c1094aea98c544ca84f1a1346a7d248 Allow different parsing strategies (#4205)
• 39fb44fe097ae995c81ee2a5b022bf9f4fe2dbbf fix #4200
• 2a93ac3d81774c8e9b922ea8c9f7578985a5d4e6 fix #4200
• 6f48c9ce5128b10bc3947d291611fa795a261e7b na
• 3473decb747e11909cf68f5eef20aebce3f8a25b na
• 6a540e8429716b3816155f7a14faf3e455461828 add Julia to pipeline (#4199)
• d3e4dd69f8c20f7a0ff1e81b03250732aa150604 relax condition on theory disequality propagation fix #4194
• fcab7e4f9cef2de79447942ad2365566cb9a69f1 fix #4195
• 91a190a7854afee414bc58f84f4ebbc2ea83de59 disable multi-threading for validation code, masks #4196
• 5e4276b0bdc42ec3cd4ee234c758ae5d6b786448 fix #4197
• dc9221e4bd87d9fdfdce4921d685724cd48b2f62 limit iterations on equality solver based on experimenting with #4178
• 37f6364547a473ab84008848ef25d0d07cc27e50 fix #4103
• 09d881cce51bd87b39975b58cdc565c0009f911a na
• 75859ef4e42a3aa66ecc2b0639e5effe5d9e9a01 model anomaly fix #4171
• 4067c84611257d5bbf98277b7f507e44cd6dc771 prepare for stronger rewrites
• 6e4a059c75ffb7a46d9ac16abbb6d6d6ce46cb6e build warning
• 0f1815ca0417a0f89c0ed10dfba25605e3f19c03 fix #4181
• f30d63a8f2d4ef92d7168b2e7881be92348709c1 better rewriting for ule
• f3dd58d7adf60977d1a55a793e487a49767db730 fix #4187
• 47fa6ba7a60e63cd5635da7b899f1e78be82dd09 fix #4191
• 8be266c18c8982e4ef485ba01bd41f35bb6ab6a5 micro tuning for #4192
• f313ab9e4c4c7fd8e81dfd070b8e70e35de95d47 correct newly introduced rewrite
• ec8866c91a6bb9ae3f42db1476099e91d071db7c na
• f0d33ddddbe6d23517c15cfad7957ee23ed2a875 some simplifications based on #4178
• 269522127b0c9d68b45f794d6a0963c4de4dabbe [Julia bindings] Changes for libcxxwrap 0.7 (#4184)
• 6088da5159959c099c7b295015cef8aa4887638a fix #4176
• c94a9e8dddb9b6ec2b9ab772a6ade28264c12023 na
• 8dd522d80527cb226a0d4511c2e3a387d3e3686d fix #4057 fix #4061
• dcb75c4b31a3633b2e9317d9acfe10108c3773d9 fix #4174
• 166be6c3b90ce30c58ea68b21cfd6ade5b5a0b59 add constructor preservation axiom to update-field
• f8590634bde708ed7793210218d3f758243c89fe fix #4164
• 5b6255e3d14a7f8e11861c21e75f2ed32adeef86 small updates
• 397bf2dec6d42cdaefb7630e4f7432e77fc8cfc4 move windows dependencies down
• 16bc5b8432d7e003ae176f9396897e1609762dcf build warning
• 97574134e0b57e2ff382a2810e6e52400e220248 fix #4163
• cb5c2d3a98b9696e6f6962d38759083a5ef97f1a fix unit test build
• 893265ce945b0a5c5f318498659ad055f3a1715d fix #4166
• e9119a6eb5d4f57ea65ac69414aae59e331639cd fix #4168
• dbfa3dd7f1aebbdf1216feb176099852196c9445 [spacer] implement spacer::is_clause() (#4170)
• 799b6131f26668e1e0317aa8c86fc4b6e6bd05d8 avoid repeated internalization of lambda #4169
• 7ae20476c2054d0069386a3b8ea179eaa559d3cc remove assignments to lambdas, exposed by #4169
• 9c52d4e615993f0db9b285aeb6810d7739c26c07 debugging #4169
• 68f1f1e62f627786a105fd8fe482c6fe766a276e fix #4162
• 9f6a733ff6a9be7668d0177be9be50d34444cc06 add hook for induction
• fd911a5563547e416385fb21347c4bb7d87ae186 build warning
• 0e77074e842f4eb975eac92f28dbe1754d75cc7f another revision of purify_arith, fix #4144
• 3fc001baeafa6bf57be781e59bc1d9276ef3ca0c simplifications noticed by trying #4147
• 7cfd16c7f948aad0cfb3707695c62ac8f3d3b5fc correct ordered lemmas
• 56690d16da2bec23e902e97cbe9af681db936c46 remove incorrect order lemmas
• b0ffad95b0fb62d7cf5dff15290aebfa038f2784 Merge pull request #4092 from mtrberzi/regex-compl-inter
• 0fb6a7c5d83455f078e13d3d8da5486df34eebc4 Merge pull request #4101 from mtrberzi/int-to-str-leading-zeroes
• 4d54b4109f2eb79de9a12075cd9fe067adac4337 #4153
• e67112f289aba5e8e6640cd7d8373a2e592ea8d6 NYI control paths
• ee1d393150775e3c26cbafc195a0222ca925e83f files to make build easier
• 7e349250353cd4a7634d2286d76220c5cd3e67d8 Improve UX for unreachable/unimplemented errors (#4094)
• a11dc5d3b57e33888c6e9822aaea10ae888f7053 shuffle checks for enable_edge around fix #4159
• 71e9bf10530280ec4335525ca2fb17f49addf4ed initialize local variable
• 4defe9b6ab1811144c1e44402b7067ee441c0caa reorder
• 8dde1bf86df40d11ecabd2dc96bf4d94fb3162a1 compiler warnings
• 00d35c2777d628d5cc71b3777023d9c302ec9f02 initialization order
• a1928a243860f49786fae11b84592c1f6c8351f2 update expected
• 97fe2c86098564d65e33821eff532ff000354dcd remove an assert
• 35e3df49e2f9e12ec6970551d479d57531f309e6 cosmitic changes in int_branch.cpp
• d5162d92ad3e488f4265505918a7c0ceccbc2ddc add an assert
• aa0f5db5116cfd9624f93ef1f6249c8c4b1f93dd fixes
• f8037ffda4d96bf7b61f4597416209768b9c2d74 always call find_feasible_solution in move_nbasic_columns_to_bounds()
• ba40a5752fe0bc1cd80256ccd9f8ebe917aa9f8a better branching with usage_in_terms()
• 3bbf1474f30cb6e162d81d9c6b85dc63c3c453cf na
• ccce599bad86a05782437bccef799ce85a09b725 fix #4143
• fa1197a78f0469ca7eeacc904c95d6bbbf695369 fix #4155
• 815feddd1ad51a47f532740c1a8a68efb1ce1596 fix #4156
• fa88dabd10023c86b176394df36ec2f33df42214 fix #4135
• b571e43f85f29fc55c9b3a98e8aed9c9ac49eec0 fix #4146
• c5550e43859cab305e67abfe11091774455c6123 build
• 1dc8b597b413c3aeac60e082978c67e480bf844c fix #4154
• 1f9e0221681cf7ece832be52ce269869b6f31389 fix #4131
• e3f712b3cfc4588f794ccefa126191977c2f3620 build
• 19409a25a6ab92b182d9e9e82da64f265ff57372 value sweep
• 38e0968845314db449efcd23d68833bd389703eb fix #4128
• 4f462925a006716ca2803b49a5fa05560a91ac57 fix #4116
• 3a63c3751e5414324bf0f1903b98fa793d1d3217 fix #4127
• 8996e8129e4ddaced0b150ea5146163e7405264d fix #4120
• 4938ea7be615627e8994d59c25930cc1d5092974 fix #4123
• 1c2aa1076bd3347f10c5bb94e8a469ca795a13e5 fix #4125
• a0de244487c53ab632c3e90725d4041c6393fcf8 pleay nice with alignment
• d818233063682d8ee83f14496f516774063ad1e8 unused variable warnings
• 5434f3e31df037f930ca1aa6b44f568d3a6df7ce fix #4105
• f1193986c9cdeef45c135e65af3c0f6fcc61b083 fix #4102
• decd69ac738d3407e0796c3f26ab663cb231b324 move to util
• 6d4bd37e15214803192a380dc5af46576d9a1eb5 fix #4104
• fc1321f8b3559d0182b55b57ad3df4f9ea2ac11c fix #4104
• d37ebb830980ed5e9c57c6e6ccfb09b09dea5660 na
• f7a7b9e1f4678b16903c8d711acdd66649aeb602 fix #4108
• 735888145e6c350cf9a089e7d0cdd924671a7853 fix #4112
• c2e0491456e23360f156fe537f90e613e4f19ae0 fix #4113
• 0499b6b64a239cf4824a067e671e0d1269d84264 some fixes in branching
• 029edcfabd47493a6db7f4e56db24c326dc5e69d fix #4114
• 51c3778354b3b960edf076b927af99c36208a661 fix #4106
• 530f77281c7d488b43d1e1c0352562f15ce06cda fixes in branching
• 236edad8dc0106785ab933fcad49eea86c53df04 fix #4111
• dc852a6f839dc71fba31045e325e639704869251 fix #4110
• d3094291d3d4fd8807a8e2bdc1a664a7a9c62aef fix #4107
• 16d34b9fcc2da4f6d62e1f719e0bb3cfc742c814 fix #4100
• 626d0186c8c40c2aec1ad0e00f34f8ea8c3e7fa1 fix #4098
• f9193809ea04f0c1bce4f33427ce38ff494c497d add recfun rewriting, remove quantifier based recfun
• 7f1b147cba3bc9d4c0d95397946184d8e956d1c7 remove
• 9f378bb1b985c9d670271ba11613bed7b05e71fe #4099
• a884201d623e6bb901502c9c7693c34324f526d1 remove using insert_if_not_there2
• 9ea1cf3c5ce9baac66ae6e97e8a3a45604c1fc34 na
• 1a5d663138af2025302f680a6b66a3c32d516984 z3str3: disallow leading zeroes in int-to-string conversion
• d21911c0732630b4196037ba03f80bb0a3986e33 z3str3: fix support for re.complement and re.intersection
• 785c9a18cab28b9adfc71ec981f7452fd65279fd fix #4049
• 6ab83466d9e4e229ba22160140ac9ab9ff1fa627 fix #4082
• a3844af94bf381f3e854425f09358e818a5ac664 fix #4081
• c3b33aae8a75ba8424f8eb8711fd2acc3bc8e38a fix #4090 fix #4088 fix #4085
• 470e87afe9bd07605123f4da60a472c328f7d340 update rewite modality
• 851c38f64aea74947d5eb169f67d00aace8ed95c fix #4086
• 2793c3af2c2cae7e6e780e829fa6fbc15317aead more replace rewrites #4084
• 03ba26821947edc61163d1975d8b6675b1118cbf more replace rewrites #4084
• 7597396dd092b118bfead628cc55dc3f10b1125a fix #4080
• 6ff61d1f802f15a9747b5082f745991438649047 fix #4062
• eb2d7d3e81c9f83a41e51d6de027d966e2ac21f1 fix #4079
• 64cb5cad81e6ab0099262143e833028b53b714ed remove spurious output
• 04fec3f6a009fa8620da10ae8f7ca34bd1b4c53f fix #4076
• cc8cd2cc2f8ffd9206fea56f9aa3fb53bd6069a6 na
• 9c3f0190f4b74e8b34b73ad64d086888fddeb9a0 fix #4069
• 8c5993d9a6fffd4ee62df9c32c2b74698445831e max term
• 8921ed56b5beecf26cc4a24f6dc16c6ab9282b94 fix a bug in Horner heuristic
• 8f297666fe91a6088819da77999e12da0a598ccb fix #4073
• 50d58114cf37e1b20b03b078d505249cfda73a9d Fix the Julia bindings paragraph in README (#4068)
• 08290230dbf4eace6156803d35e64f89dd84687a add docs (#4072)
• 8fe3caa1010f9fb3c7e35612f0c18264a047da60 throttle digit constraints
• c7878e384cb07a4040e383790af638987d5d7d3d fix #4060
• 886f4cbee08f3e6f4fc06379a94d9471ce7ec86e fix #4029 - propagate digit literals on all units if they haven't already been propagated
• f94abf6512168bcd4a46f1255406b11d81a1909f fix #3978
• caa5b0904622d6711cbf1ff328e346f5818eed8b 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
• 95a78b245004a823415118a9015b58787ac18ab9 updates to seq and bug fixes (#4056) [ #4037, #4044, #4040, #4045, #4036, #4025, #3200, #4053, #4052 ]
• 53c14bd55482ac884885ba48304b7e6859da679c Use Position Independent Code flag on Static library builds (#4043)
• 5ec04f7fd27bbf8905ee1d9c7924a86b8c556fcf forgot to remove unneeded class field
• 220bc7fcd93a23e620ef96e9b87bd1ead0f7db4e fix #4048: incorrect bvurem rewrite when divisor=0
• dd064a5554c41148318f23223c7177a250c2ccfe delay digit axioms until solving itos succeeds
• e3e6959b70c8b6f85b4465dfc982bf15a2d7791b fix #4026
• c8b9eba0695b3a429436fd856d1bc4b0fb76c1d7 fix #4028
• ad8eb8fdcb9e0d9f19fb19d9ee7a14f3cbce0112 #4024
• e1fa04b365ee068026b168cb363193b722c43c46 disable breaking change to model generation
• eded7d023d85b947d3e68e2c8f27d1ddb9b66447 fix #4006
• f76c6424f204051de117e1053a019bf78e90b3ba another memory managment leak fix. Relates to different leak exposed by #3997
• 44957894eae6b75a5eaba484a49a1d79b191af06 more checks for #4013
• fcc34a07b2ada3fde8f124172e20031de778ba50 fix #4019
• 339a2568b20b54a24ea324ab88b9e23a3da28e7d fix #4021
• 79b776fee52621aec4a5a042060eab7a81b7853f na
• 19e0285b835931a26edb4fb56892ea897822f477 move deep internalization out of theory_seq
• b92b6c0fc67d1cae534bc6f2f21f8c4b118adec0 add missing digit axioms
• 99c90d2419e0e3c40e467080d40f13952a81b7a6 fix crash
• 0fe2d3d8b7165f5f117b4214853bb2583af0053c more seq overhaul
• a9c4984a16b14544f4efa7775c886bb20a844268 more seq overhaul
• 76735476d4abc5e0f119d9bf416e4dc92048ff93 fix #3999
• bcbe802b27e06404b2e82d65f645ccbe4327e2a5 remove buggy bv-trailing
• 3e9479d01a8c709138e051ad1932697db9a9913e a lot of seq churn
• b8bf6087ffeff104941a61d9d13b698daf1a75ef na
• a83f72b65715d46f9434502af5322dd13e1e04e5 some fixes
• 501aa7927dba13a90e3fc9526c01a9d06e1704e3 split into seq_axioms and seq_skolem
• d5eef9dd8b69a2eda4accdbf53f148f85d630b0e na
• 040d4b8d24779ccdff27772bb4b87b80752b13a4 fix #3994 remove bogus option
• 767dff4a5ac8219095dd48d1eebbfe77d348a356 fix #3903
• 19f655c69391fd5899474e3b2083ac140d16aacb fix #3930
• dd3e574f8161871a957316beb01a6cf3d763b98c fix #3983
• 1f23ae8aae2f84ac250c0a993995df7c2c530825 fix the test build
• 95cb82832474de4cd9b3c92601798a7c6027186d make lar_solver pretty printer const on the solver
• 5208b64a6ba4589a2b19c0e45c97a51774955a72 expose only necessary methods of lar_solver
• 6d8e5400fd508ae297e28813395bd3957161e7f4 return an empty model when the status of the solver is neither FEASIBLE nor OPTIMAL
• cb4ceeab3ac10c10f6e681e6cb79b9bdf48d785c fix #3985
• 206c3e2c381fcf5dd4921e374d4cc5f89fdccf14 fix #3979
• dde0c514fa0105dacea55ce5a9bb01b6e0638952 warnings
• f67077b7ffe2702b062b9723c5192bfda7b834b1 warnings
• d465938496acee3de07a5b27fada0b500b16c92c add lower bounds on lengths if they are not present
• e6174c89f312fc6ff29cedc247dbc5daad54bc73 bail out of mb branching if lengths are not available
• 40b4ca7f861868fb02b10937855240721e0d5b3f fix #3950
• 357ec2fd0149616a71e883007633017d7344793f fix #3948 - cache has to be reset also when processing 'and' because it could be processed in an incompatible context by the caller
• 2e1e9c90821658cdabaa05606b1021ef2e968559 na
• 3845e0859c90f91bb886ed9c52aa93f5c429a3b5 fix #3878
• d0f94055e7aa24f35315b74d228ad57fc3a9c21d fix #3966
• 068f65c8ac7dcb89e71f7535f5c4f6a89b345c01 fix #3967 regression from using rewriter mode that splits strings
• 79a2b52de06d6e70dfc9ea12a1498e3da1df04e9 fix #3971
• 1ec977930a534b83a40d658991b42ca35617021e fix #3972 regression from changing the way assumptions are initialized
• 25252af1fcd30e925480e731cbb4afc0a442e0b2 fix #3975
• cce27ff65ffc7c071e2c29cad6f4dd2bfb07239b fix #3976
• 164a73febb5fcf0eaa47ce7bf6b49832119a5573 fixing #3933 - remove unclear code normalizing itos
• b04c97458daa2d8dc3a460df6a5fdc5936188447 na
• 835b57b77584e0ec22a0976806b392447283763f fix #3961 fix #3940
• 7ed9996fc05aa42621b583fc7e3938ea3b465c05 fix #3962
• 5f819132920b10c78a3a703957b20b0e6f4e9900 fix #3951
• 5e0c34cae2f8d7c96029b28e748615ce1caeef25 fix #3953
• 2a0537af695c99b5d4eef821021ca88e5f4eacdf fix #3954
• b8c069c6b771c9344dca6388221d407ded9040b1 fix #3955
• f564c325d37153b959d181e6bd1db70869702daa fix #3957
• d7d687703195a36fe0725278f5c05b6defa0dd2c fix #3958
• 387964f5089a169c74420ad5a52e11a4237e84a2 fix #3960 fix #3959
• 0f697830fcb3212126f9d885b4d0148d926bbcbf spelling
• fe7146d93be8690f77e69ba6eacb391bd080539e fix #3913 - change assumption tracking to be granular based on disabled guards
• e1027790ae9e5e99ab98351c3a4953ae49661f5e more to #3926
• 7caae3f5d235c8f7c4da1764ff3503566fbb0deb small improvements in tableau in rows and bound propagation
• 90793931b1a5f9c7879da952c8a00ab610bd530d small changes in one_iteration_tableau_rows
• 9223f611ba6748c5e36d67c2e7d7dcc28ad4b4ff build
• 9f42338de86f1da7560fbfd14c355874b3ef6dc0 fix #3926
• 299a6f4aeea2c413c427f8ebcd3726a7096e7209 fix #3939
• d3db2af81d6a9d6fb811c21a0660da8003329720 fix #3941
• b4e77300344733d16e5835bcb7df8b5ae33a6b79 fix #3938
• 6a5695463ff171403701178ad4825781f3d2ea56 fix #3943
• 5dafd1fe25d62cc99eee24a1637903d0c3515082 fix #3945
• 5c4f775b1b2b7a9f4b03d2340b36deacd55bea8a fix #3935
• 01c12c951ccc12e33f00e5b52c1d59d54f139380 na
• 84a4d9850b6aa7eed17c02a3d6b6b0332e328c59 fix #3936
• 75a460cc156ee1d15ea4e20523dc52be66ed016d fix #3932
• 9b609af8fc5e582280e0a8791b1c565239d21d3c fix #3924
• 51eaf84eed2e4c0c3c93eebcca31bf1edf085893 fix #3931
• c85113acdbd2394dc40d545a514b4bad12da1ea4 fix #3928
• db9d6d12fc1dfa4cf7240f9e88c64dfb6dfa21e7 fix #3836 remove unused and buggy hoist_cmul

This list of changes was auto generated.