• b5deba84263ebe3c9dc2aae73d7c11cafb572124 add EFSMT solving example (#5654)
• 3a9656bc59a8f9ad26ffdcff931c833d974b0e94 fixing issues with user propagator from python
• f2fcbc7cb734e34138221f2599c541c566b49d60 capture values not reference
• af2cc460a96b6db97c774ef0b8926c145f26d216 #5646
• dd1e0fc561196bbe097e45fe5876a00ca2d152c3 #5643
• 091079e58ca919b7c0e8fa768858c936991c1619 Added user propagator example (#5625)
• 87d4ce265901d5cfc33f9a617ec2104773c4c370 working on #5614
• a94e2e62af13cb23c14e97f7d4441327550040db build warnings
• 036b38a97fedc50f63c5b5735f76cd746b184c8f ubuntu 16 is no more
• a11ca1a1b7bbed703b78e186b484ab531b2ab026 Update wasm.yml
• 8e59b343382be25a2f5cb404cadedd3a3857e995 Update README.md
• 933bb4f1f029c1a59574d1dce38b55d03525e228 Update wasm.yml
• dfba177813766c3219a1d4da8342bba6b9214a27 Update wasm.yml
• f61e6abb352e233851ec78155bc8f51b702202f1 Update wasm.yml
• f83226df9c4fea049b43c09f9ffe8b1308e36774 Update wasm.yml
• fe0e1cce302ddc92d49db194d0c266e015eb08e4 Update wasm.yml
• e7a54db8b0eb29235bde703c6e361d67addecc24 Use emscripten to create a wasm build (#5634)
• d1fbf013eb56a894bf5812c265d59cded97cc03d Update azure-pipelines.yml
• 96671cfc73766568988ec876894c8f6f3bf5bebf Add and fix a few general compiler warnings. (#5628)
• 1d45a331631d6bcf5c774d2ab0e864ee94484a25 fix one typo and two misunderstandings for doxygen (#5633)
• d1592c6abf7fa3c9067e47eb40e6fa32d7dc0817 fix misspelled \brief for doxygen (#5632)
• 780761a29e856d2b20a562c40b3c235ee146f322 Create wasm.yml
• 4dad41416136ab421be54b4ee56fd17a9c6a20cd fix performance regression after adding user declared functions to model
• f5f35f87d08e8518c13bde189cd42ccd090a745e fix grouping for latest doxygen (#5626)
• 723b755ca76e1a05e3b0c55299bf1d689ea2604f Fix the command of install_name_tool -id. (#5622)
• eb8c8da8a739154e09856acb3bc66ac3951fadc1 ex handler
• 125eae06bdea90029fe95fc9c64374ea775779a1 #4869 load datatype parsing for HORN logic
• 61eb8d1908e406dd1f5d1505e4d4193a5f7c71e4 add ref for regression
• aa5b4b8c77a1d273d297336e21a43c8e2dd6bc0d strengthen contract for log_axiom_instantiation #5621
• bdecc256197583e02782fd1f4f7456c16165d3d5 strengthen contract for log_axiom_instantiation #5621
• efcad5ff358a9370e3ea5c57cb85bc59d21cc1af fixed nullability bug in the if-then-else info (#5620)
• 4cfc73779adec4dc4d37b16ebdcdea06c54e869c update build
• 075769c4c002fc1b9aac23db718a1e6064c3a573 try get_string contents again
• 45681b4c6e73ec4165895b2712954a9d71c25274 update API type annotation to make it OCaml friendly
• 3036b88f094fc5a468aa3ea04fb8fb5de0830563 support threading for TRACE mode
• 4b7c08d08d1fb028e6f40e23bfd20f63de933dc9 Update azure-pipelines.yml for Azure Pipelines
• 09bda6f21c4b49c8a71daf42c916afb78c120f81 Update azure-pipelines.yml for Azure Pipelines
• cd4481bca37e4f636fb9e252dc95f27187966616 Update azure-pipelines.yml for Azure Pipelines
• ec9498e1663b193ff6d601cfd13d3507c5e4bb83 Fix ocaml link and load (#5618) [ #4840 ]
• 066076557fa3dc7ade8324f559f61e6ff05b1420 Add post-install testing for ocaml binding. (#5617) [ #4840 ]
• 3a3cef8fcef58f31e9ec6495346eb065b816b155 #5615 - update documentation and use non-encoded versions for ASCII characters in get_lstring
• 7f41d6140f6b278b132739f492e62ff4c68e3dff use some suggestions from #5615
• 051616385f598196ad0b3d080086a5cba14c2fdd remove deprecated escape string from Julia bindings
• cd8d8bbb630dc8db8c01b8ec9987ca6640c42720 Fix runtime search path for shared-lib and add '-static' to the name of static-lib. (#5616)
• f05ac8a42950e6d1406f3394c5277d40aa21bb99 updated C++ API for escaped and unescaped strings #5615
• 05e7ed9637a7dc6eeb435094beaf2f386598c722 add API to access unescaped strings, update documentation of Z3_get_lstring, #5615
• 6eed885379370a1ec1912cef7e08b9504e37116b print bounded terms for better efficiency
• 13da6a02a60282de54cfa8790fcc10cf22f6d263 add handling of quantifiers #5612
• 839a0852fe6c677cd9148d2412d3e5ddc992a6cf Merge branch 'master' of https://github.com/z3prover/z3
• 86147d01ea5c2c1b288e37dbb3ffd5c218cddf1c #5605
• f9dde2e8a4709ba37341dc12a9b4a3d543769668 #5605
• 3557e0b0c52691c08836dfbc2bd37c2def221646 Added eq/fixed/final functions in C++ user propagator as methods (#5607)
• fc3a7018888c1f507d191d6c4799ea966bd8de70 push-pop
• d5e5dcfe451a2a2b2ba2097df66881c878f46a0f add nff and auto-relevant
• bc2020a39b9809b2573686ae813318623d3e318e #5604
• 115203e87cb746bead6cd269c7986c05332b3f87 fixes to sat.euf ematching #5573
• f78546cd7c4e45ec5eb46416728d6e7dfb54ede1 fixed bug of computing butlast of a sequence (#5602)
• fb9fa1b7d2e8bc6926e8286eb226d4d0d888e802 updated printer
• cb120c93f4f8ca0c62b5162486c30a893d4132e6 Regex range bug fix (#5601)
• 6302b864c807741223b0bf8ade4beb1da9e4f09d tweak GC in OCaml bindings (#5600)
• f60ed2ce928b43a40b3274036f78ffc85c36a75f #5591
• 7b341313d553e503acd1183106f27c04c0b34dd1 #5593
• fd77f0c1116d0fa0a62a804217137ba15ece8b12 fix #5594
• 96e117d78cfb3a391d77fe954629b34e6196b66d Update smt_context.cpp
• c15968aa9eb1a39d0452f317151987c8fe357134 fix #4901
• 9a76bf0aa24185229e8d900d1025a130a25dbba1 #5591
• 58fd4fc8602ed19e7c6c0ddfbead4629f457a7e2 Merge pull request #5550 from wintersteiger/cwinter_fpa_fixes
• 52032b9ef8a60b352027a05947c77d713bafb2d2 #5467
• b471ebdf1cf17b4178c2b76033a8ba82315b0944 Revert "Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it."
• 738783a26c760d33a3ef18c31d0d4484f0c2f1f8 Fix off-by-one in fp.div bit-blasting. Inspired by #4841 but doesn't quite fix it.
• c24f438e51cc9af302e400d36e1f1b73a4bb0d9a Fix for mk_to_fp_float; pertains to #4841
• 00e8ea79621c5029d6773e3164ded601161c0898 Make terms that are internalized on the fly relevant
• 8e69f76784a6fb6ef9418dfdf0d2c1aca11fb9b7 Add additional equality in theory_fpa
• f1acc4b78a8c80377c8f65a7a2758f8a59b1e5b5 Make fpa2bv debug symbol names optional
• 515a2a771e270f8c84a2d1f3e8a3c3909d33e8cd Whitespace
• e8d6d97ba378e4b80e4af4f7fc5296c02104d9a7 Refine fpa_decl_plugin::is_unique_value
• 12c32663c67e48d4397759bb12c0c20f8e7bde1b Fix error messsages
• c3549ec784149aeb1796b0deb4dbb0b2cc18d4b6 na
• 73102cffcbe2cc5dc491bbcf626c8b6939d46ac1 fix #5589
• 75702c36311f8adb2edcf92548a60387c87f8f9b na
• f7a2d08e74a7130c0bddc8d963b1e126d27cb20c Update README.md
• 88c3119d8d7cd164ef123103946b5b3dc5b404b2 Create android-build.yml (#5588)
• 0fc9f1d46a4b35744e2c9061ff86e01b36b34657 fix max/min length to handle concatenation
• f1b8376739f4c431c96dfea3bed0f01299cdce60 Rename 'user' to 'user_solver' #5586 (#5587)
• bfa960c2cee9ec4343d00f2e504508d757a36a1e fix internalize regression
• 6f5597117708748a219fbe8d89d242b3ed35b625 Newderiv (#5585)
• 146f4621c54d2755f75f51ab37dee42eff9f81e6 Updated regex derivative engine (#5567)
• c0c3e685e7801c7d670c11613f3cc8f4b293c724 disable all propagation until ematch incompleteness is fixed
• 94cc4ead7249af4b8a9fbca635484f5a3b428a99 remove arith_lhs simplification from preamble tactic
• 33f4e65fa919349501e7511669131f6742fc6b1b redo bindings/fingerprints
• 281fb67d88488dd70136615465902aa625d2cc6d unit propagate with fingerprints
• 8a85cfdb128b1426c3e6bb5be20dc987e64a2e37 fix #5579 -
• cbe7dd4a48780db2268ec52a60b880af3a21ea48 missing continue fixes unsound sat result from #5573
• ff723f15ffcf83eebede32d3bf2d25833b7f73cc Update z3++.h
• 62fd22f55595cbf08e6bcea366496d300618c465 disable macro finder tactic if there are recursive functions fix #5574
• 137e5c52633c5c8f6daf014cff3a59f715e3aaaa fix tmp_eq
• 67ae75bac715229378a7c26911e21b9e4aca6e6e fix tmp_eq
• da124e42759ab4fb93e69f9bb49899d3d21fb8a3 tune q-eval and q-ematch
• 92c1b600c3916c3c595366982ffbbe491a2f8eb5 tuning eval
• 2e176a0e02f164dbd27c0260b183f47eb15b045c count lazy bindings
• 3abecc34282107c5be45c9fb3e23aad6ac2b57b3 add extra commands to API parser
• 6c71baf77b91a0972276f462922f9308009bfd3d lifting iff to binary
• 1dcbd2d86cfe5e4dfb24e71dc74600470dd97873 Correct capitalization of package (#5569)
• d174f87c5e3c99bf4eb37ea72249ccf023ded36f #5532
• 18d1b368d1dde36e6119a008b9c52b271761983e #5532
• cabd5b10faa741edc566457c769b822f552609c0 #5532
• de20bffafe9e03795253b4a94041fdce37091505 import goodies from ps
• 708602dfbb3bbb6d0d225d202a4b129fd90fd703 fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas
• 2e965578270c91cc6bf5d83f7c4d5266ba3f6d2b fix #5560 - add a throttle on maximal size of bignums created for propagate-value lemmas
• 2c266a96c82647a171be2afae727b480bb4a63fe #5545
• 1352aa06f3e9683da2ed411d574474f64bf73ee7 #5532
• 0170f1f461b3967a5bdefbcec38d08d576875168 #5532
• fd799089b70aac85dcc0938284dc1333495ed76a fix build
• 6f31d83633560155d63d8411bf500e9b6fbb1531 fix #5541
• 426306376f8b4ef63468279633aa00360e7b517d CNF conversion refactoring (#5547)
• 91fb646f556730f73556857ea25f35dfcccbb547 Fix Z3Config.cmake.in when generating a static library (#5555)
• d36c3faf7622bd7344a4965b2e612aaabfe9b6cc #4880 add interpreted versions of to_bv functions for MBQI quantifier models
• 1fc7b63a80433ef02f72a94380d425bad8ab5e99 ...
• cef964fda3b1a5c753bbbc2d28b66bfcdd72c90d fixes for model converter default case
• fe3f139eb28faf1af17b8ca9d2ecc3060dc8a15e na
• c3c5c14eadc2c817cc6f1b24caace58375e90fbf prepare for min/max i
• 50375df8dc6e8b60b6c3306fdba0e4ccb296a4d5 enforce idempotency
• c58b2f4a9c35ce10f3306a598165e7d73e395654 Added character functions to API (#5549)
• 9aad331699b472c100ace108ebc248e2bb816572 #5546
• f13ccf8969ffa99b9913788d16bc2ed0a4497318 bv2char and char2bv with Clemens
• 34f878fb977bcc192e483176e5c4e96fece61058 make it easier to debug parallel
• 3e6ff768a58f072b888722e142eedcd65ea6dd30 fix regression bug in mam reported by Aseem
• 47fdd6c060f36653741649339070525cc42bc06d Added 16 bit string-encoding (#5540)
• e70f501932415eaf06dac8acf881572a83b7a6d0 handle potential extra nodes from q_solver
• c4d0ded7b7e8779e948e0f8faf65d0c9dfe7686d #5532
• 8c406c161e622950b893c6ccefc5f19a032552c5 #5532 add blocking condition for recursion.
• 93415740b6d6cb22561366c2e4a9a315de6d0585 left over bugs #5532
• be4df46f6f9f48034f35578aa5110df5de5992a8 #5532 remove unsound rewrite rule that was recently added
• 72f6271d8297d543d14fcf59a0d0d75788f66bd9 #5532
• 3764eb1959252238b24d198f846979fda231dced #5532
• 3021da87cf72b446bebc3d281545ac786f11f79c #5532
• 9c91698201948a17bc2ffa98f8f8a352f2d1f35b #5532
• 976c0a391c92b27486a2e5121631dce779d75fea revisit as-array evaluation
• 38b82fa742251c4179b3fa245dd2aa91f15e2ccd const rewriting revisited
• 051ede64e7102922601e53f24858978dd0a6d0e3 #5532
• 3de9162c7e8eb6a10322dfdae6a6a2b0f7e76b11 handle null more gracefully
• 9c5ef79701d26fa6c9413a5be4493982916d0638 #5532
• 18e4546404026a995f5eed0ff2da412c57c819e7 modernize parameter defaults
• cdcfbeb6d88a1b0274228e14842df1c5ae2b6314 #5532
• 0ddbbe9bd2cdf4ace9689f4dcf0f1527a432c196 #5532
• 5633af76cce9301f02a5a1bd6a6b97a35c4a3dbc #5532
• a566c7307df5c8d28cac2681e1746eefd5cb5fd9 #5532
• 87f5b9282f8539c29e150c799d1d83584a4120a7 #5532
• c4158ebc33848858523329cb1dcd069c2341537f #5532
• 20a259cfaad77a41c9d2eb3db5c4a68377a52356 throw less #5519
• af5c6e43b91aad0a2ae16ea3a1abf6cb574d3a09 #5528
• 55285b2193c6f73c17c53661a7e11f8e3df666e9 make it easier to iterate over arguments of an application
• e9a4a9a3909b0d2307fbcf16dcf028fb3da65232 merge
• edb26e7be739d41657f646f76cb7d1f064f85821 Merge branch 'master' of https://github.com/z3prover/z3
• 02acc38c28d20aff249e27bae2504539444bf225 add extra checks that user-supplied assumptions are asserted
• e05ef8ece9c527e1ea6fabb84f7ecbe5287e691f account for updating scoped state by goal2sat #5528
• f4abe3db0237e5439db74fcedcf39f731f642d29 #5528
• 9e306e3b6ecc78b70e2bcc86db1b9bc75c515d6a more useful diagnostics
• 968717a532baaa6b5bdf56a688a6380bc7791a0a follow on fix from #5528
• 6907d3071796f403ae8c6817905e197c1884fb26 #5528
• a74c01c8b98088ed096e7c046a8baa1906cf5f24 #5528
• cf9e55fa969692c5cdf8b7a7e19fd426064e3fb6 #5516
• ba68fba4193569a24263629b2af449e7fac5f6c2 build
• 0c53c139da18d0804003cbb4b6a841692e50d724 add to_string method to make it easier to use without <<
• 7ce4be8455d52e73c483f2a67358063cfd505de7 #5528
• a7bc4719c08f300f6c08367ec9175344a8d5df3b fix #5526
• 8bdc8d0e1a0ed8ebb34c0217a00cb9cd2da79c29 Update solver_subsumption_tactic.h
• a3ba4e136634b0c94806e6508b5f2002d020344a #5528
• f91c3d9fd667a9f1d4adf94bb24fa9e2f2f94fbf round-tripping escapes, again #5519
• 90f98d5791a1c21a8804a26524df405d77c85ced fix part of #5519
• 7c782a7ef862127cfa3aa4e6ec962abea0db696f #5518
• 1426390aecaee4b306ab2355b058e7d5b199f00a #5518
• ab2baa764c271d64a21b3c3c1c4c026276c1b2b7 #5518
• 34c8f598a55330c6927cdea1217a449de27a3ede #5518
• 07bbd026ac78b1219497a6791ab6b04bf741b606 #5518
• 0b063f7903f3f7b14fb42d59d8d15239fa67a69d #5518
• 535f4426550d8d1f764aad89b3386e60d27b0e9e #5518
• cd2701da0c83eb587a647b7b0e4f36761faa5fae fix the use of ctx in Q() (#5521) [ #4956 ]
• 148cb83b0d030fae6af99fb30f8da9a64004ba16 #5482 fix default case for model construction
• 9b5ec6d004bb401202d10eca14266f61f3e7b37b logging cleanup
• 1f4a7c5101c5be52a2efdc4648639fbfc46fad29 logging: don't call the returned function twice (one for log, one for return)
• 9a172939e0dcb7c2ff661776aae6067a32c02599 fix logging in Z3_fpa_get_[es]bits
• b1bc890992e9f601109cf3e9c27a57fdcfac0213 fix #5515
• e7fcbd95631385776842c8819d6553046b035aaa bail on first model validation failure
• 4f064ee5d6cddc1cc6f1749a6b9cd0ac4cc7aadb simplify based on comment from Jamie Sharp #5512
• e5a2f08cc9d22ac3807f5655a33a7db6105d9d9c fix logging of Z3_mk_lambda and Z3_mk_lambda_const
• e3a83dd0dd36db5133735313091728a408c77c97 Integrate fixes from #5512
• 992daa6d2e7addceae95fa5bb75b705f1af8b11d #5482
• e9a30385cfd0923658392ea44f2965e2ebae69a8 remove wtm and booth
• cd7a8260839e83e308753423e41fb757c7c66c41 bit_blaster unit tests for adder and multiplier (#5514)
• 8f306c6a8fec4b80e89d19cbec391f06d915ed6b handle constants
• 09696e989e56f83f9ea218434509809fb9158a12 add missing lambda defs per #5509
• 9790a8aa439ca9b94785f471143ce0cdda21fd95 #5507
• 828fc72754d42f77ac18b51ba53fc5ef12df1fa6 types
• d6848175eb0bce38a8cdeec04e967f61cadacffc re-add API for creating propagator from a context for "fresh"
• f7c1ed82733cc478fbefe9053749b5aa04ed4444 missing this
• 4d39af3d7b346ebf3c4216c17a11c52f9da546b4 #5507 missing init
• 07c26208fa9ecdc6b833875570427f3b654aa034 regressions from previous push
• 2daf569da63ed93801ff88c4fff1297313af764b update Bool rewriter to pull negations up
• e6264a80ffae5eff061ece2dcdf26506b3da9625 extend macro detection to negated equivalences #5496
• f03d756e086f81f2596157241e0decfb1c982299 missing rewrite exposed by #5498
• 17663acf75e294d9693cf7f9baa1b9d159d66494 #5482 other relevancy tracking
• e75b5e9513914550db9611bb63c76f402e782957 don't copy "true"
• 037c93b258b1ba3198fb85ecd1be86a7fd84b0e3 #5482
• 7bae29729799acd401fc567d2ba90ff0ed6b8101 #5482
• 26db68bf2c1c44ee04b8374c1a98f320754f9cd3 #5482
• e5b6cd36f0d5af78406ab4e664f0ed477d66c1a3 use datatype name instead of instantiation for cycle detection #5482
• e90ec457c3fa60ba88a64bc9192b4f1ee2198e31 #5482
• 5fa1b0b09fb3faecfa6dedf165e2e42bfedf8347 update project description #5503
• 23b995d3b59627308278960e7b75c25992cce703 #5499
• dd91cfb47e309e1f2b8a11581390cea4f22a82bf #5482
• 592c53e46dfc7992b300217f5d3e516724e26d91 char sort
• 170ef1dcca8de2c765bd16a57d294f2d13ebeb96 add character sort to Python API and allchar function to API for ease. #5500
• 4b3b4b95d97cbe12dd3be336c45897f0b5c7e700 missing
• 2a682e4b135fbc222669fa254a52609887c1c34d #5482
• 9c7d9f06ed3ce7cc80ee1017cf886d48821a9b5a #5497
• 1975e486eee4a4cbec311e01aa09be46f49112a5 finally expose some easier to use basics could be used in cases such as #5496
• aa0529895096d45238c1d2f25d89d883d30c1192 fix #5491
• 15e3e81cb56ec5826e188d3902acd2e3c7af4929 remove likely culprit for #5493
• d0e210849ffa520ad2d9cafed472aa4f7d0d706b #5454 again
• 9122ec9cd6de297e0d2830961add849b3a0886d8 comment out for now
• 93c3fc2bda9b11148a4e5555a2780c7594e5b86e try without semi-colon
• adcdd11afc19a50f7cb94eb6e2d709de0348873a #5454 again
• 2492278a4b88ab283283c74110c28a40066993cf Update test for java
• 1db9f9a3b5709f2aeb80ca8a8ee28eb810d13206 try vscode from github integration
• 810b9d003da8206bac428991a5b2faceb5f65202 move examples to python based build
• d980ee0533d1113398261f479b1e84ac60db6cb8 fix regression in FPNumRef sign
• b3db9a1cd5a8eb80345e1ced9e1c1a11c95aad30 #5488
• 5c9f4dc4d78187f582cee37ee5682536c92e9276 #5486 - improve type elaboration by epsilon to make common cases parse without type annotation
• 7f88cfe727ac3800b906f382ced2e705578873e4 build
• 1884ad5b2f119fa21ea5fb1295af0c0662687f8f expose method for updating python model for constants
• 34fc0276e9130b522a9322917d73897d7b9f7bf5 Update array_axioms.cpp
• 749d1ab3052e61ba6ad8bd1414e05c1f6ebb55b1 remove dependencies on stale component
• 3516c5272adf326370df136d48e92164f3ab3525 Update coverage github action (#5483)
• c8a83749ddd0db0a4b54c7f5a20a0fffdedfd27e #5484
• 904c6e21b11cafe451ac8d5bfeaeb99fb56705ad modify #5454
• 429e5ed0cd5377bdecabefd28a2530be870be246 #5454
• 3d13c0335f2fc30239b5438910ababf023bc56a0 #5454
• 6a3ba64afe51b841fdf8ceb5b3f82df2f5a13566 #5454
• fe4c48e14c4b20f1d07508122ecdb415dfa54753 reorder fields

This list of changes was auto generated.