• cfe02edda5721e4a1b9e97ce0d2b8404a9577e90 remove stale return
• fd1f5cdd0f455d60c4c9ed86bd702ca14560e3e9 fix callback type declarations for propagators
• eaa2fb76cada93ccddc5a619393f0d5a469b2f06 update release pipeline with x86 Nuget
• 86af723db7ecf47fd17e83f5de1110bbb13f284f remove left-over debug output
• 6d836e7e2f05a7e1a53bbc446735a49c625eb4a6 expose model update
• a9d70267242bf0e8200f221555a8b89d6b8bfd20 add note about transform
• 81a5e56c8960c3493cf63e721e192c9482d06766 publish to github
• 39df8ee372e23abfc765fa4c4b7451af760821d7 update win build
• 669a1d63daaafdf0d3f0b76f5fe09e593d25b536 na
• 29e288367eaeebd332686abdbc675cca2ac3fc58 pre-release pipeline
• 6010d751eda9a03dccf85a4490377f91a99b0ed8 fix #5903
• 41d1c340675961d6415362485594c0516a3af7b7 remove else case
• 1fa373d6c272223eab35c1a530936a39870a6989 old bug: unit of xor is false
• 4e0a2f596820cd4992aed569749e25fcfbaff307 Dispose of intermediate Z3Objects created in dotnet api. (#5901)
• bdf7de170394b920711d033cf14af97708f783a8 Care for root index being undefine while calling Z3_algebraic_get_i() (#5888) [ #5807 ]
• 6455ae4350a6f5e04872e8a5ded3f3d3199bcdcd Merge branch 'master' of https://github.com/z3prover/z3
• 0b230ee703de998aaca649058f8c812b719d3af8 move some functions to using var pattern #5900
• 6c4780a8459e515b39899caf85e912166b7850b1 Update cross-build.yml
• 3d87d86c2825437780167ae6ff8f5b203f15ee7f github action: add riscv64/aarch64/powerpc64 cross compile (#5897)
• a1517251dd05cf71777708e5f1574cb57aef93d2 call dispose on sorts #5900, missing charSort
• cd5e114ed3bfb32e3ed20861a6593a5d45948cc3 call dispose on sorts #5900
• cb9dcb799f4d2e6faf2a71f97c7dc0ca8336fd76 add regex power to API and for Java per request
• e1929ca9b979697747e823180c3611af7f0b9ac0 add regex power to API and for Java per request
• 706d7ea8936074cad3b49fb15da50a5deb8f386c native context uses legacy mk_context
• 313b87f3c68f849b1747e0f6eb5cf89ff8e8c9b5 doc: update readme (#5898)
• 545341e69999ceca585f3dacc08d5c6b6f096edc fix #5895
• c51ca86203e999dd86ce505d36e5d706ce0f67d6 add another constant folding case
• e839e18381b83c1171e34fa0955d6770564f379d minimal addition to rewrite bit-vector to character conversion using constant folding.
• 8f2ea90db12164458a2cff676901500cbbe7f831 Merge branch 'master' of https://github.com/Z3Prover/z3
• 081c62d006306ea7db52b3949dc0e21f55fc458b allow range comparison for bit-vectors and int/real
• 580012e19f4d7ed2227684e03c8b7183fb91498a fix #5894
• f26c12a9ad08643484cafde9664dcdc5effaec8e fix #5882. Use model true when inlining (#5892)
• 8e18a94558b8a58dfa49ccf86c422fc2c3d9700e Update README with info about Smalltalk bindings (#5893)
• 43f76368268ea14f19cd187c6999ed2cc475f332 remove some copies/moves
• 1d224d1bcdc067e8424eaa1df41a63f88b18e210 na
• c6f8ee33d4bdee9b56c65768304561c3c8989a19 na
• 3293aeb7c765228487fb95f9fc974a5e48af5ecb na
• e7ded9cdbd0bc78541996a16f2a4089cfd6602cc update to 2022
• 97c7ce63b535337fcd5c195ea2720546477c972e Clean up build warnings (#5884)
• e3568d5b47d976ebdd8f45f7816716549e28b3ef Handle additional cases in rule_properties::check_accessor (#5821)
• 882fc31aea9068f9b64ade2dccf429b113c9cf61 doc strings
• b0c0f4d1f4437e05d581049fba5e20b238c9f2b1 fix #5876
• 3e51b69a9ab0a333b819a08d73b16b2cd64f7a2c no fun!
• 2b71d8bc0878ecb35b9b34ccbed558c21c4410f4 doc macros
• 87e6f103c6883ea37da0198dc0a43e0b5db870d8 commenting
• 676ba78600192c4f7dca1e59f226cb44bde96a37 fix else case: it is first argument of const array
• 35d26bc28210f3177f47293d7f93c22d5a595d21 NativeModel: TryGetArrayValue (#5881)
• 248a3676affd9fefe886f1888decd49d508dd309 na
• e1e8d15827ecb727e38776d57b20ce7e7afd37ae stub out array serialization
• cd324a4734bef41e0520d53a3a917aca761754a0 na
• 8d1276fa60863c1d4cb726f5c0a6362bac12fdcc using directives
• 35fb95648b0aa7ba2304a5141ebe607c1122bd07 Updated user-propagator example (#5879)
• a08be497f7ae56bf5a5190eef353f5179b98f1e3 NativeContext, NativeSolver, NativeModel - updates for Pex (#5878)
• 811cd9d48d98963be64e730e5a61a4b310bfee3a add example
• ee18c5070c279f8a04e2a5dd63ece0b86c452ea3 add stubs for injective function axioms, add some parameter functions
• 757cf7622d549d5280748464366092aa198a5def sketch ArrayValue, add statistics
• 80506dfdfa80b4845f572c9773d7a7f6e3a95ef4 sketch ArrayValue, add statistics
• bf14aeb1bde040e8a5c7fb5100b8dcb3198af67a stub out nativesolver
• bbadd17d5637d38e8ccd0df7ea66a1e1c2eeec44 fix #5874
• 5f79a977fb6a0eef43835d4c098d6ac18ad67982 use conventions from Context
• c812d1e89086ca9c23cad8148f76c2a5985810a9 update native func interp
• 61d265477013d6671bad5c75776181f56f9f9fe1 quantifier
• deeb5e9921bf3eefb3413be29be778279f147f0e finish NativeModel
• c0826d58bf1d61783120dd1c73160709ca902e38 add stubs for native model and func interp
• deaad86d6a0e5e02abdf1164c7deee7855a765eb nit
• 2b6dadcbc661400ae0334e14b0e3c1f200988cf3 fix #5869
• 302c0d178c700dea0b29aa005f26a4971d90c00e fix #5867
• 412b05076ce3ebc28a1ef567c7d5841f51ad934a User-functions fix (#5868)
• 689e2d41de8776b2af3be8d78ba5b15c86ff531e remove a bunch of unneeded memory allocations
• 7f149a36d7da605835ae79d1dab64e2c99cf34b0 refining model update rules for del_rule #5865 #5866
• 30a2f2fd9d696ebd710e90dd7803652f42f806cb initial stab at NativeContext
• f2e712b0d6bbb19251020208c7fd31a74c0d232f throttle is_compatible to check variables at most once
• 7b4f1ed530b6c644d1cbd49aee3c9fca295151e6 missing initialization of m_user_propagator, disable unsound in-processing in pb_solver
• dc110f10a4ec887707ff5579870eb1512a2ec10b Update mk_util.py (#5864)
• 6be0a66b3898a248313bae792ce0df760e8fd85a fix #5863
• 6af170b058697e5fb18808728bb94de16c2027da fix #5861
• c2f1bdc099753b82abe36f04dee95b6b034db7e4 fix #5862
• 11030fc81dce9cf409cedc90d08786fca38594a8 disable unsound mk_seq_butlast
• ea0876b6d6ebe3f97171e88e9d06aaf42bdf5b45 add lambda definitions during ast translation #5820
• d06c51d51738f56ef754a567e6e474bd52afc4d1 na
• 061e94d723422b240e23743c8ef3f99739f1ac23 #5858
• e8d4804dbb726b8b13cc996cc33bd57d6acc893a Revert "use horn_subsume_model_converter in coi filter (#5844)" (#5859)
• 456b8ee68294acfb16eb624ff01f20b1edc9d547 nightly
• c47e5aff60ccc90df661800046ac4f52570c5be5 multi
• cfe9846f0cb75cdc76617b8f9643dbea50eca888 multi
• b84361805117c7fbe61c72c93253e75822d8c4c0 fix #5798
• 5c2624950baa5a69bb7ccce20b59486e7692ea6c #5849
• 1e463955c20eba19026941b439e295c4e74e0375 #4889 avoid double internalize of bvle
• b38b6daba36297e8a9268fc94af038400e58a51f add option to disable FPMATH
• f66b4f088062fcda727fcc5081479191d3a3a456 fir #5856
• 14ee02183c043c95d077d3ea8413ecfda4b45c93 nightly
• e800269cee9f49b9323b264969ff2ed9070947d2 na
• d0d4ab7955d7e5fe61c68da125fd20e3e3702278 #5820
• ff5d210e8168ba75b1058da3dac7c7a972d060f8 na
• c25d710958ea6993df5870c93429a12eae886611 try out arch arm64 on the mac
• 4d184fe65d5afdb58611b9c537d597f59564c926 skip expensive equality rewriting of Booleans
• 10b611b3bad0136251ca58ec2128a9c40009ba6b fix #5850
• 91045d3e4ae4f88f3eb4dbd4ee8e6197d15123ac two words
• 9a1a72867c99def51fdade411ebf2aa69dcdb797 Add str.<= and str.< to Java API
• 7091b1c856e6f85c3b9c0fc9cdb010f2d8ae38e7 add additional regex operators to API
• 2e00f2f32db7a05dbecbdb75ca7a1e1918a6a0a8 Propagator (#5845) [ #5818, #5835, #5829, #5843 ]
• 2e15e2aa4d01357223404ab4f9ab9d201a8fe9ab Add access to builtin special relations (Context::mkLinearOrder and Context::mkPartialOrder ) to Java API (#5832)
• 9cf50766a636050da7731bd58dcd01219cbe744b fix compiler warnings under clang (#5839)
• 09da87dc85560312fe5c6dbfa4929e82a420f8e8 use horn_subsume_model_converter in coi filter (#5844)
• 5bbb8fb8073371fc5b2958c2bd05181ce06a51ff add bail #5825
• 33985ebcf5487d04bd9bfc47e18fe737604fdf21 update expected
• 6202cd5394222e177b60cbe6782d7e6e81b162aa fix #5842
• aa6ec418e3ac14bffd232ab801aaf07edea20345 move idiv test to after cuts/branch
• 9a4d6cee6c9e7626f0c72f349d6c2b5b30df6551 overhead with push-ite on shared terms
• 3d26b501e78466f49abb889077d4e8f0d8e6b5f2 fix #5827 #5828
• d745d03afdfdf638d66093e2bfbacaf87187f35b switch to vs 2022
• 81e94b21541280cb7fbc3426419ed6c3a8f24dd4 na
• 07d02ea41578819dcd58b623fa979914a4dc4809 fix #5829
• 4f6fcf8ea78492e1d90398bcd3a663f8517f2a66 fix #5814
• 0059e880365518bd2d9938927b17079aa47a8c9a fix #5808
• 9958cab5cc737edf443340e5e08c094d91fc0c93 fix #5808
• 3f3d05856787dd6a6ae030a81800381c310a5969 extract also units from search state
• d4ea67a6e714914a5ce29790a260d5809d5ff91a Fix a few typos in README (#5782)
• 03ff3201b90a3aef32c99e9e2d367e7c44260e82 block recursive definitions with lambdas until they are properly supported #5813
• 1c10ce4070a29679244f7cc57fa1087d6a1d5cac #5815 - surface multi-arity arrays over python API
• 8a84cacfea8b47bdbc2e3be41aaee6c61a082fbf add tuple support for getitem #5815
• e9dad84b857c10c710605cc5294349737d4dcbfe update documentation comments
• 9d655cc658a2ec857f4fbc0c3d128cbe37b0b919 track all unhandled operators instead of latest
• 474949542e854b2286e09973d3357dbdcc024b45 Merge branch 'master' of https://github.com/z3prover/z3
• 05e28e43441c45356b70d5b9b0d117856744f1b4 fix #5812
• 6a412f7f043690d0032a1c6cf742bdd1692df7d5 allow to pass Booleans as arguments to arithmetic expressions
• 994c7ef52dcedd245498eb707a6ff3fdb01358cb format
• 1e0d49512ba480a4135302c2988e9089d330cfd6 call mux finder
• 4392b8871850ac797ed676f620f8798e903993fa return negated literal when expression is "not"
• 7ddfc542502937409665dc83c8a6027a04eb6353 shortcut negation
• f3fc6a50f317656314f0064b2a15c7de530550db formatting
• 6422b783b2ba984c20152bcceb600b015acc8deb fix mux extraction to check for top-level assertion
• 62bb234251916dd7ef95f5c101742c1c770415c2 expose extract roots as separate
• a326ad4cd9a345547708672b676435f2723fbe10 flag incomplete on lambdas #5803
• a189ca8b60eb06705fb5e1458ebdaa82be5ec98b truncation directive #5805
• 773e829c581ab99d9e24d8e3a28bc78ce7743f7a #5804
• 913b90f7aac8a585a40a0c74d7837be8dc2cb807 fix #5802
• 25516319573eaf1cd4da1ae20e039973c959a086 mul overflow #5797
• 5e81c1220c959fe74f5b4af7ab7b340b4a9d1845 #5797 probably still wrong wrt underflow.
• 9e5b6e0c9c8abb8c3ecb4f0d93bcc51146659218 #5778
• 4da930b4909bc19530a59d7494f79c9f78bbac8b #5794
• a6210413086c7889dac7752dddbe38e7b172f785 fix #5795
• 461e71017d87ac3d72157030ac278398416a7b4f fix #5792 again
• 53f72d9cbe310f2d2fbc509127fb369de957058b updated mini
• c6539deb6169afde2b569fba89a828f2f726691f fixing null check
• 435f79eab03535586c23cad7abdde94033daf812 tup
• 9294b2ceb2a649bc7dab3f7f999e45603bfb34e3 created
• 3de9d3777211918fdfbfd96dd4eef2661c701e08 fix overrides for created_eh
• bf6454dccc6f8b8d8d36ca1abc228b1d609f6a62 throw error if created-eh has not been registered
• ea6827505e6eb0a6a23ccc7ef9124bde1224515d add missing callback to m_created_eh
• f639a7e1bc565f7173b6cdf46979d8914baa74b3 add marker for top-level expression in rule.
• 61ab72b6a3224a9351c93b3174bebb353b1e4b03 fix #4869
• 3b8c0b7ae61fb06cf7e5d521268e5b4c2dfd06e8 fix #5791
• 20f9814939c1a9b000602b10ed6e21062689a8df fix #5789
• d02235fe08c85dbeb980a3147e279d25a74c3007 #5778
• 85f64566550cc6a73f89ff9f70d31ac60897483b Add missing constness (#5787)
• 996980974590c9db84ee2c1b84f447e1b263bb94 #5778
• a1f7676c81f3463b8c100c4928984fbf6ab59101 remove assertion - literals could be assigned but propagation incomplete
• 007af9cb8a81c47e56b41ca3d663e534e4e44913 fix #5784
• 17280846f8978ee8d4ef43882193f2b4bb0551fb added comments to explain #5781
• b1ff4bc24a73ec17f5a76a4d6cba488dbeb55e15 no normalize
• 75a81af426e9a713811475c3672fb8599ef3e32b fix #5786
• af9ae3598439d9027b1cffe0f233457e877825fa term
• c527fda0b6b2f074cc097823e57c8c83553a0906 term
• f1a302bba7ab478d2bf6ae5210e7179ebcb6b188 term
• 7a8c969033f69c58af364a0c2438bc2bb412954d ensure b_internalized
• a3d4e9a4e8be4e4d30717112eae8bcac1fa920d7 adding created to sat/smt
• c00591daaff8258a80e9415fc94b4d8869a650a9 finish is-fixed
• e5767bf2b8d209cd1a78b2ec54f8139963e4d60d na
• 0f03ef4ab08618fca0df2fb4c3436c618c00ddff for Clemens: ensure fixed values are propagated after registration
• 5b0389615beb53853a313309fcb3af62a22866b7 #5780
• 06feb71eb1244353bd955de4f9e857752de4d3bb fix bug in root setting exposed by incremental mode pb_solver
• 36cfb88f5f127863ee9fc897b8d61c4894d32cf3 add preliminary stub to handle closure types
• d777306bb6e4c89ebd9ccbc0a314c2071587a741 #5778
• fcc9f379e7384194c6a8faac7b5522014987cd34 #5778
• a15da8f9ba04b468dbc6313662cc841d5cc4a256 #5778
• 637ddf9397b87655c8d750fc21201b8eec582619 fix #5777
• 0dd5a5e576a5698c7d923333e0d1dbe9108c9845 #5777
• a48d3fdbb1c5e9513c9958d58254b64edc2fe3fa #5777
• ea93345b755c739c75265289016c19260f1ff2db #5777
• cd56d55e34a079273bcc5f8726e1be7e2f6f9164 #5753
• bc9c6ad93d07e6ae7c6ddd38a0862bae261bb363 #5753
• 1b5f7cd9e51dc6a9d5e8412b291ac73ca65aa374 na
• 17cfc1d0344e1986c563b9fd8b3dcaaf6129048d #5753
• 74824ac901622096bf90996fd46aa188b823b80b #5753
• d09abdf58e67bb2fe174f70ccfdbfb9d9c480181 fix #5771
• d5cc162fa788e143e04d45a5cddbe84c7e319583 bug in bounds
• 2363bfc1329d6fa18b55c68a710fa51223c6ed5b internalize arithmetic sub-terms #5753
• e816946ddcc6645168fbf896d907f91cd99cc561 handling unsimplified input
• b259f46f8502e8ee2da0fcf781d3f013f5d80b43 dependencies
• 4b6679e8e07537258e785be0eed85bbfb81225e2 #5753
• 366cd9b16ddc8b5808d1dbb2e65af394b8f02622 missing pb cases
• dfe2b27f9aa6d72583014fa301bd79d223fb254f #5773
• 0720998bacf1de33b02ea9e44bb47295d7b85943 #5753
• 10dc8d7313e5c5ff0e71b7d94e492b6f9a201f7a #5753
• 56d3718cde7260d54c34e1420ef11a3436671139 add simplification with qe-lite as an option #5767
• 08294d62e5cd7898d3876038264765bcc0c9d8e6 separate dependencies for qe_lite
• 2bcc8140319ab632028dd5517e9e52bd3f7477dc add macro to track closures declared in z3_api [ #5762 ]
• e5eaea46aa5b89b3a1e431e26f16d10519b1a098 ensure m_true is assigned #5753
• dbd5512d8c4f354b7f263cb600ba978b27228a9c ensure enode without recursion
• 055732423ca433f1332a0ac56f75e8476387d767 ensure enode without recursion
• 571a74c06109dda1e006646c7d7c2ca803234b14 counting function applications #5766
• 4cd818b57825e99bd9493fb9a54b8729f99c1e6d #5766
• d3bc11dd3a18408ec8fe45ef3bcf6bbc4ef9d691 bvs have to be expressions
• 21feefeac59d00f13278e33e2e70601d28082829 Add character access functions #5764
• 2b934b601dcb0422c1352c85312d96fd5f28d384 Add WebAssembly/TypeScript bindings (#5762)
• 9ac57fc510cfb7018563e9ce523d3b0f3bb4641f update version number for next release
• f1bf660adc6f40cfdbd1c35de58c49b5f9960a9c add case for abs (normally simplified, but not with default_tactic=smt).
• 671d071e5443a1778e3da15ff12278e1ddfba1fc #5753
• 010bccf3536d382bc1a5ffb95878bf228dde9ed7 Update wasm.yml
• bf3c213fd3edd1ac063e4e6caafa8962e2cd4e9a #5753
• 90fd3d82fce20d45ed2eececdf65545bab769503 enable propagation
• 9f9543ef698adc77252ed366e6d85cc71e4b8c89 Fix unused variable warnings. (#5760)
• 174889ad5ea8b1e1127aeec8a4121a5687ac9a2b id
• afbfea8ce6ce231149f037c1661d69c8326661d5 name the package
• 36ed1ffac22ed96167fa4c871405f2152bcfda11 update name of artifact
• 40761ebb0da47cd30aa0a4821164724a6fe9468b bug in script
• c2aff52dd758a686c36412582bf09d54d7c6fa24 os-info back to common
• d391043ffd7630041917ec6e41053862c8af676d only one arch at a time
• ef481073b2fe1093c558d4ac02e5e4daae6ca96d make static features avoid stack #5758
• 2c44454a17cbc8de596f0c416e1f5f153035fff1 self -> env
• d6ce05009be0c048dcaa367103b0d98e2d13d3dc try separate x86
• 6013d5da471edfca38ff2a08d3ff2139147ae9bc #5755
• 0bc8518cb5277e38b462c5a667945456ffb2e1b5 na
• 199daead50fcc7f36d8a13185168e52944c266f6 remove Z3_bool_opt #5757
• 7baa4f88b0cb4458461596d147e1f71853d77126 build failure
• 2be71cfc43c80a03b9bc680190b5fe8019ff8e47 #5753
• 6a3fe514f0a2c42a45fc33a0ae2b8b549b4125ad build
• 592b1d7f65506feb9a4c0ba5717a625ce8f4eede #5752
• d14f00d61abd697c5ae03dd1e8079f272d72ad45 with no last model
• dadda86bdc3202ed0b73603ba500c19c4363fd06 #5751
• 130a0c4aa0587ab679ec6fa5ea3b57f843f91373 resurrect infinitesimals from maximization function #5720
• d7c7fbb8f1b06e30bffcdc520666053b01a053d0 setting roots breaks relevancy propagation
• bd8de964f737dc0e7c3b8fa739771fbf643bc926 more fixes on relevancy
• 5ec7a66a453e55af5c71591871672637be2b3c11 change class name, add comment
• 964a5cd7612ac7aad555c71003fda2d924678761 lump java together
• e943bee625a71d41b7a991a6bc6d34bed4535853 apply delcypher's todo
• ef3dd32364da96a52e1d61ab9415dd366344ec60 some cleanup
• d1fb83103084cfcaa80ca8f8d687809a21f5e877 relevancy overhaul
• 4a1975053febec5a308c1610653c2427683f3c0a cleanup

This list of changes was auto generated.