• d204413f2aca80615f9fe47023fd4178e7adf6ce remove update
• 85abbb8188b7d5b32784ac967f2b309ff4046622 include apt-get update for doc build
• e4bd40667514846397a7be251e9778ed5a3c526c update version of manylinux
• 25b0b1430c40d24f151756f84198b61d3091e272 move bound_manager to simplifiers, add bound manager to extract_eqs for solve-eqs #6532
• e5e16268cc4ed46f7f98cd3e96d72115af59993c Initialize m_istamp_id in lookahead::init (#6533)
• 8970a54eaa5241d76a5b3699d0c644110b42c7f1 expose parameters to control behavior for #5660
• 1c7ff72ae21c3da0f39c4d3c96e90764d6aeadce add tactic doc
• d415f073866b4dc729587d3ce8fe3e2166f7ac02 memory leak on proof justifications
• b700dbffce68682d53530208918a8f1bb0a450b6 fix #6528
• 2bd933d87f9fec351fdff9c2a85698d42d32529d Fix hwf.cpp for MinGW-w64 32-bit clang (#6529)
• c3e31149a5614e813909ef1041e007dad4f6abfd fix #6530
• a4d4e2e48300369a2670d7feb26780defc85faa9 track assertions
• 64ec8acd306ea6adb8e883860cce611665522f18 fix model reconstruction ordering for elim_unconstrained
• 30e0f78c16c23b4baf945f2872aff541cc2fc503 remove exit
• a4f2a1bb2e4ee9bcc2484f0e1088c8597ced6ad8 Bump json5 from 2.2.1 to 2.2.3 in /src/api/js (#6527)
• 49ee570b09047cbea94f7d26e3df10c86c9ce596 split into separate function
• 5899fe3cea8042d21203089f01d700fd22a1b7fb Add rewrite for array selects of chain of stores of a same value (#6526)
• 1ddef117a21de30909fd1166095caaa85c39da82 several fixes to proof logging in legacy solver
• 61b90e64b25629d14811921d0198079d96bf6b63 disable new simplifcation for multiplier until really understood
• fcea32344eafb4cbb4ca66161c1151f8f7c532aa add missing tactic descriptions, add rewrite for tamagochi
• 95cb06d8cff3c70388dfdf295e2f2347e1945ffa add quasi macro detection
• 25112e47b46691ef0007068858cae034b9d72055 bugfix to flatten-clases simplifier
• c07b6ab38faa03e5439a3b7c65f489bae1d53081 more tactic descriptions
• 0d8a472aacd6541200466d83cf8b06f538751b07 pass sign into literal definition for pbge
• 81ce57b5a84d8903d51b0a3b639da28d36448e15 #6429
• e0099150ca63f16cdb98ada543492985baf62c10 #6429
• 380c701cbe1a16380bf462e5d6ad5d97ebde28c7 restore debug clang/gcc build
• 21362c0b989456d7f842a639e08b63dcc3c7b63e make case-def and recfun-num-rounds re-parsable for logging
• ef101190056d5d856cf34135645916f01be6c20e #6429 fixes
• aa080a6b19cfcc10cd03c2a281ed0a98a27c09e2 update ignore-int handling #6429
• 8d0d6d8f04a22e5f9110a924b6063e85f74a66a4 Merge branch 'master' of https://github.com/z3prover/z3
• 6f95c77023ea3793b3a631798eff02e04901938d fix bugs in flatten_clauses simplifier, switch proof/fml
• e448191212c319f9388e0ddf6845b55de1348465 array rewriter: expand select of store with const array into an ite
• e508ef17f6d6d716f88906d7f7acb35bece9bc92 fix Alive bug #875: bit blaster not respecting soft memory limit
• a2cc504d4a85755f23df2f1d1b18dbff3fcaf0dc remove a couple more std::endl
• d30cb55bae24113468b3ae6f07d39536402b4891 don't flush stream when printing param vals
• d4490738bcddb5fa32581fb187a9bb2fa3a6fb16 Merge branch 'master' of https://github.com/z3prover/z3
• ea0d09b6c89c455271ecf16a1f7337fcaa395c9f add pointer to build parameters to README #6518
• dbf93c5fbdf458396c38993fdcac54f4e0803824 Fixing array select for lambda expressions in Python API (#6516)
• f6d411d54bbe80d5b305e9c2ae30b40c0ed358ad experimental feature to access congruence closure of SimpleSolver
• c0f1f338985898c059da924878715e5709f2eaa8 dampen second setup of theory_bv
• 5f6f2fc758bd68836ab2db1c9a3f580a25b9f75c rename bit_blaster class to bit_blaster_simplifier to avoid name clash
• 0d05e0649bb7e45eee1924ba158c0ba2a966b8d4 initialization order
• 2c3ecceb03a2b14722d7436d977e6566c4ba122f fix build
• 8002a51b82f703ce6dba5a429612e30bedb8b575 tiny fix to qprofdiff (#6497)
• 293627c889b4adef608d3204efcee1bb39826a7a fix #6513
• 07ab4d38b659d525b4363d660c4526a725fbc182 fix #6513
• 47324af210500af2d840595e8d1b493c5f7b1c90 be nicer when memout is reached in SMT internalize: return undef rather than crashing
• 7cc58c9cc32fb3fec283134ee14755aa76086bf2 Merge branch 'master' of https://github.com/z3prover/z3
• ec74a874232b6b23b17c741a91fff75f8d2fa6c7 fix #6510
• 3e8cbb66112aaa58710e8e23719ab864b51ad0fe #5884
• abef260d67907a9662293b4aefd63ade472c3f3e Merge branch 'master' of https://github.com/z3prover/z3
• bc19992543c4793ae90f286d4834c782e9b23548 add doc for ackermannize
• 8d332cc3a17ccdd6cf39490020ea7d7eeedf56a3 #6508 (#6509)
• 6fab4fec230820c6c73221a3e85164d6faedcfbd #6508
• b9c4f5d4fafcace3968eb3a5c5489a4c881628a0 #6506
• 8efaaaf24982ce810b8ea85fdf74eedc3dea29ad Fix #6503
• fe8034731d3f43fa9d0f8ebe5d72d085779752fe fix #6501
• f96130003687e5c72d9bbbf7485f0ecf7c5e1770 Merge branch 'master' of https://github.com/z3prover/z3
• 603597a22ebdfc90a1cdddf5ed0f41ef89bc00a8 deal with cancellation in qe for #6500
• e423fabf6a8808c36d906cdd62dda9c90773992d tactic
• 0768a2ead15d162e0e39c5791441cd16ccd73dd0 updated doc
• ecf25a4fe267cc7151a0f42ae0c7bbd8b6664b4b outline scheme
• 13920c4772683d179932507230755a7a19dc8b24 more doc
• d5316e017e9c0c9f44e4aa2453f908fde7ff4324 add tactic descriptions
• f01d9d29d2685b93b3cd9bb5a94ad35174843d7f Merge branch 'master' of https://github.com/z3prover/z3
• aed3d76a886ea1ef0a7c2db9504df893e388e591 add doc
• d47dd159d7019c103e5a78d9ec1c291919418c9f set encoding into gparams because this is the only entry point in zstring #6490
• c4b2acac24c1e660df99bbf4364f531826186b11 add missing error checking #6492
• dbb4bbe7dc8b494c7a3aff206672a7fcab69317c remove debug out
• 9054e729203931be474a9cdb15d6bc16e000cf01 fix #6467
• cd3d38caf79ccc0ecbf18f28044451b135f69cb2 sort out terminology/add explanations, add shortcut to C++, fix #6491
• 2d7a38e95e2c29ed32b8e75954ea6eac6535e5de fix #6488
• 7afcaa5364370dc20ba73b05304c138eb9dd7aed update doc
• e648e68d3608b39077dadfd252908e76c314f775 add doc
• e82c8e78ae7f9825d40ffaf9935a6364b793c2db Fix a compilation error with clang-cl (VS2022) (#6489)
• aded8e5bf475b6a645488b67bc49d33fd5a7a2c4 fix #6488
• 4598af70c823f741ed12186aa1273bf6febc7a45 fix #6488
• a3e68856802b4d4a440b6bc178277521917f0d0f fix #6488
• 039de6a2c80f6640cdfb6bb3db3add1f8c8e68a3 build issues
• cb8603177e7624b98ae23f5c0c56a8c0c964df4b fix build
• d308b8f5557d49da1f69290b68ec0ddc3bb19524 simplify code + remove unused file
• 6b60a3dbed4f7ed492afb4244eb59cd2edd4cf2a fix syntax
• 2520dcb04ba2661cb7ed8e433833338e25559f7f merge
• 2d43ccc4c6a4f63c2c6da58302a02c5610f98a30 Revert "fix crashes in elim-uncnstr2"
• 6a1b3f73446bc1c33bad3bd8a063c772bdac8f72 move debug output to before state update
• f7269bb60a3165d6a670f22aaa45b164b23906a7 update doc
• a9f52b0069bf31d316f3485731b13897551aee43 doc fixes
• 527fb18366f5b028b6144d0f84df43767cc45985 add doc for card2bv
• a302c2f15ee0e4d24ce9036050fffd8e827fe053 fix crashes in elim-uncnstr2
• ee307dd84f7e6b0953ba5e0903cd8d9a8abe5381 Merge branch 'master' of https://github.com/z3prover/z3
• 1434c7d394d36ab53627b42d85dde50f8921a1cf #6059
• 9ebacd87e2ee8a79adfe128021fbfd444db7857a fix buggy mask (typo in my last commit..)
• 96a2c0402657d2b836e23428a4c95c3ff8637070 fix bug reported by Nuno
• a96f5a9b425b6f5ba7e8ce1c1a75db6683c4bdc9 fix overflow in mpz::bitwise_not
• c6f9c09d70b7202ecb2b1492493e6d7bec392253 cleanup more in dependent_expr_state_tactic to reduce mem consumption
• ca6fed8b25331cd6a472d3296b4b28b73c0c993b minor code simplification
• 8981d32caf488cd4df4ed6ec7f14c390eba8ddb3 #6481
• 4a451b10d8ba9f8186789048b08379e19776a4d0 add custom coercion for floats. fix #6482
• c45c40e782d6c8c95771cc9ec8944600c78de760 doc
• 7e69dab8f69747680d7af1d825bfc68a634afbd8 distribute forall cpp code
• c33e58ee1a4e482319de25a06c651dde75ed3ac6 update distribute forall
• 80033e874499d18f9b650235dbd4e75c568aa447 cave in to supporting proofs (partially) in simplifiers, updated doc
• aaabbfb594fcfed4240c580e31db51cc3483e6ed remove comment that does not align with result
• d125d87aed403edaf2e971f4038e573eaba708c6 typo
• 1e06c7414acf11bd4ad85f777d4ed1f6d49e1c3e add doc
• 7df4e04a2c881479d661a2c9d3edea2913548118 add der description
• 90ba225ae3bd82aa9be438303f02d6a9e650a993 add more doc
• 5a5758baaa54eef5a65b58414d4cb082515a37fb add documentation to initial selection of tactics
• f1a65d964224cff059ac1aabfa8a47a90c594107 add documentation notes
• a2f5a5b50b47f64ee02db964058da05ce00a4656 remove memory alloc from statistics_report
• eb8c53c16431ddb6f3f07b5f102eab2a1a50769b simplify factory of dependent_expr_state_tactic
• de916f50d62b18b85194949fc213f7f7bb86ece5 add demodulator tactic based on demodulator-simplifier
• 87095950cb7ac8a5f5653b44d0a1bd8ac50f5636 fix #6477
• ead2a46a88972caa03e7013b43dd5f9e1dbb4a23 build
• b76ed6a47fc00d184fbceb518eeb5b18ea8ae93d proper fix to #6476
• 9b58135876826b569e7967aedade05e9430f9b52 try to fix linux builds
• 0f7bebcbed8fe33c6d5c3f9c653be57eb7e9adb8 try big M for linux build
• 1974c224ab74fb7957afba04fc3f13649a8929e8 add demodulator simplifier
• 9acbfa392361e785365498cfe18e3276d8fa10fc move it into substitution to handle dependencies
• 3d7bd40a87cee19d8b1135b3352a86b91f006a98 a round of cleanup
• d218083145db789b709c57d583b8b48f17267ab6 The demodulator doesn't produce proofs so remove code path that depends it does.
• 7fe67877489f2acda6f6fddbdcf0806877fba7e1 ufbv-rewriter is really a demodulator rewriter and does not reference ufbv
• e455897178b9bd64dcd01316df998b91c2948af9 fix #6476
• 79e6d4e32dc329b4be35d413feaa299ea5da3c4a tune and debug elim-unconstrained (v2 - for simplifiers infrastructure)
• 59fa8964cad87215cc8f6e24661224cc8566e2c3 minor code cleanup
• 3ebbb8472a4f57672528f69dc22850312dd9ba2d fix perf bugs in new value propagation
• 758c3b2c3ba02d8c6fb0d26180018fb9007549e2 fix filtering for recursive functions
• cf7bba62880c3f9a215d20e05b757a16a5da0a23 use ast_manager as an attribute
• 5073959ae02b1ff062ffd43a4d62af219db7ce34 add macro attribute
• 54a8d656179fc092cc62bf9652700e06821cc429 move flushes in display_statistics (#6472)
• a96b7d243afd01a130a804570cb6b193f546dd92 remove incorrect check for quantifier
• e5984dd3979ece320b465e5ed65538ae644e737b add cnf/nnf simplifier
• e3e2c21632bcc15ba2973d0208bd47c11b3a73ca Create cnf_nnf.h
• 847aec1d300b44dd6c28ec39179a71b96bfcfe5f update dependencies
• 529f116be084470af275715d7691143ee04c038e disable new code until pre-condition gets fixed
• 147fb0d9c16beb0a8c8dc31dc32d70c3216ccab2 fix tptp5 build
• 30c9cda61e49c13e602daf2ecc40c73496ca4f14 increment generation for literals created during E-matching
• f24ecde35c29b46706f736f5f29982d4016fb74a wip - fixes to simplifiers
• cfc8e19baf676102214ed97c71bb721ddc930a34 add more simplifiers, fix model reconstruction order for elim_unconstrained
• edb0fc394b8578d35661a5308eec919ae180d20c rewrite some simplifiers
• 23c53c6820b2d0c786dc416dab9a50473a7bbde3 fix build
• c1ff3d31920d6b5474fc4faa008bddb40c05a381 wip - adding quasi macro detection
• 7b9dfb8e1e439ac8194246f23f4a8708c17a4562 update dependencies for python build
• b084821a0cbf2dca5c14872be9686bc6e261ffe4 wip - dependent expr simpliifer
• bec3acd14618120a2606b35f606132f5063c5821 consolidate freeze functionality into dependent_expr_state
• 73a652cf4b60bc382b676da2b96a8b5bd359e342 some fixes to backtracking restore points in new solver
• dd1ca8f6bd1e2bc8dada167eb0056cfd4abc3dd1 move qhead to attribute on the state instead of the simplifier,
• ac023935a326c8ef33383422ccf406ccdf571062 introduce sat-smt-solver
• 82d9e4a4fc09e401995865487de22c905a3dbb3d update goal2sat interface to use explicit initialization
• 500626e814f680a42d5cf6c18b1024faec581bd2 add sat-smt-preprocess module
• 85f9c7eefaa721ea9eeb6484f310681db257967b replace restore_size_trail by more generic restore_vector
• 6454014119cd03f64754406e4f917ed1ddac4e92 enable incrementality for model reconstruction
• 4e9f21c2a1cf3aa53efe8d23361ce86a2aa7573c add rewriter and seq simplifiers
• a152f9cfd6470674fba04cffbb84e01348009fa6 port bit-blaster to simplifiers
• f0570fbc0ef7e6179f5a5ccff1701ebd11e88871 remove tactic exception dependency
• e95b0bd2cd7bdb15fdc8b6e52437fbe5c811d9e5 remove include of tactical
• 8184e7fe0a24cb06f2f56e9b3702c12764b4b12e keep track of qhead
• 5af6e1a046c803fbae472e84dc1f8e5c341b827d make max_bv_sharing a simplifier
• db74e23de1efe92170f3e6e9083516e6af652bc1 make card2bv a simplifier
• cb789f6ca8abb33fdc546452729732047ca337c0 add arithmetical macros
• eb812e47bea4a9aee8de58a7a1796d08ec8e064f cleanup
• b0247d8201cc7c1076c411618882034a9a5fe49b add exception handling for rewriter exceptions
• 1815812889c484b79d8a57e97834c0d8a8deb47a fix typo in name of tactic
• a64c7c5d19b0475b1872cf9118816d28c553155d add incremental version of value propagate
• decb3d3907eaa7949b59ffb7b63b39a743ed2887 stashed header file
• 34791295829f35b6a3a2f880bcaa4ece25cf7e14 remove unused structs
• caf204ab95dbf1c5f88b3ce89a478248c88865ba hoist macro-replacer as shared utility, update eliminate-predicates and model reconstruction
• 5fe2ff84e9cac0ecabe2a7d86cdf36691f69dce4 change functionality to not track ite terms for congruence closure
• 15dc7b78a0747619b3e4ab0c800a08ec001fcc38 Move merge_tf handling to euf_internalize
• eceeb295fc1f006b30c0932b3adad4173b65f327 fix #6457
• 4ac5e51e3ac7d986eee455f5cf4ccf9909046acf #6429
• f87e187b629891cf1ec3e6e43d29f87457520c63 #6429
• 0a671f2f44f7a041db0948b7c53719a0396e1c9c fix #6464
• 0a28bacd0f6d46a8ac61229fe8bd118b158b1bba remove debug out
• 9a2693bb72f8973f891618622fdfd0e78f831f41 tune euf-completion
• 22353c2d6cd90186133654796564384b5b60bfba new core perf - add merge_tf and enable_cgc distinction
• 11b712fee0d06a6457f901cc29eff7a819415543 switch to new configuration convention in solver object
• 6188c536ef852633571b34e74efe962b942f6ad7 add logging of propagations to smt core
• 5374142e3e1b0edee4d5ace5cdf2ba1d3ab82738 continue updates for adding proof-log to smt core
• c7781f346d5d723a8c9edfe6534d1a1b18067b2e move parameter sat.smt.proof to solver.proof.log
• cd0d52acec68ce1c23553da9edc255e4c4cf5215 using C++11 features to simplify for-loops
• 5c5673bc09435a0477b6e168731d0d67fc3f7f2c make sure parser context within solver object has its parameters updated
• 477b90228e57d619cd848c19feee646109c4a2c9 fix #6460: crash in mk_to_ieee_bv_i
• 0445d6f264a666ce38a96bf07ff980da2386ccee FPA->BV fix unused vars
• b9f34286a7fd23a89d7d8735daad67b2c2676f38 generalize macro head detection and elaboration
• fcaa85d7a8e48e78c739c40e7c16fb4898a83216 #6456 - elaborate on error message
• 86f37024033d419fd65844db4a3cdc077e57c024 prevent re-declaration of enumeration sort names
• c3c45f495a359975bb616375c3a7e0029f37c7ee add some comments to elim_predicates
• 251d49d13317998df7e353cdea889a71dbb3569b remove outdated comment
• 3f1093322501908e919fa62b90444aa3620fad60 remove VERBOSE 0
• 771157696b451ded4040de9ab42467dc483f8445 new simplifier/tactic
• d735faae4eaeb981694b8bf0229374a85f016305 add isolated hide/add model converter functions
• a81a5ec68c6479155a7fe82bba27b74765342e1c add virtual function requirement to dependent_expr_state
• dcc995f0e502b103ccb3f15b4012c0d6f2a8da4e code simplification
• 41b40c3a51d1239d08698d0f8fd05a2d740e97c1 remove dead code
• c2e9016d04b67cd9d33bb72be59960ccf0f4aa06 display model-add parameters in correct order
• ba68652c72d5b61157b87d88dadee2948397e343 add destructive equality resolution to existentials
• 7da91f4313980aebd98c21146962ef77cbd5a713 allow printing declarations with reverse variable order
• 59b7845c7dc765a9c19074c43d288daccd753d68 reset visited (fast mark) to not clash with occurs
• 6662afdd2632cb2c2f313796fdd0746c28a7a9cb perf improvements to solve-eqs and euf-completion
• 2c7799939e319ba48bc8e1d7a9d27d4bdbb13954 wip - tuning and fixes to euf-completion
• 98fc8c99db60f5ec8a79a4dbeaf029fca05befc3 add shortcut to equality mk utility
• 55ab7778f4b8e7653a0e9bb8d159962b70e9997a fix perf bug in new solve_eqs.
• d70dbdad501f3782e99d4d364fc7424f1bda6a6f wip euf-completion - debugging
• 255414f4a9558c2ce43fcfd097ef02c8e201e4db fix regression crash
• 9845c33236e944c3435b7303267d3acc5fc7b8e9 add shortcuts in rewriter, eliminate redundancies in dependent_expr tactic
• bfae8b216278d74cc69d5a415527380d7a50fd75 set flat_and_or to false in bv rewriter
• 041b5f9ef01be585c27796dda4f892e272b089b0 rename away solve_eqs2 to solve_eqs
• 48c0f8694facce9a645cf81beee2a9a7449450da euf-completion bug fix, streamline name to solve_eqs
• 3eeb59db34172f673d4ea54c1ec9ca191997fb5e fix #6451 missing occurrence marking when there is an unsafe equality already
• 95e07ffe8e96ed18fda51f0ccdabfbe5f32d8b68 disable unsound context equality solving
• 6297c001eed19b11f4871d764c2f93ed1d94d086 remove legacy solve_eqs_tactic entirely
• 3f2bbe558948f5c3cbaa5ca77e65c6d8687e8c46 harness del_object #6452
• 3d2bf13577547588cf22a197dbd020324596daa2 streamline statistics, fix bug in updating goals
• ce6cfeaa6873e7facf0fb00ce87c1d24381fd6b3 fix bug in euf-completion relating to missed normalization
• 3fa81d65270731290a4e03293d92eeaaa1a38469 bug fixes to elim-uncnstr2 tactic
• 38cde14e087e0470cce4d6134860007e3f8798fd wip missing updates
• 196788a0915d69b8599bd7a89dd4d644f324a537 bug fix for equality solving
• ce76e3138d9625601c738e7eab29cd0408116360 streamlining expr-inverter code
• 3d570aaa0af2f81fc19cf08af64d76d1c8ea9f22 add missing process_eq
• 0b83732b82a549b93e54ecf513c4992ba95df85f missing override specifier
• 343603f64341676d059411af62c4145c48f8268f fix build
• e33e66212c1a860c9bf5c48aa6f9926e3c0f2630 propagate values should not flatten and/or
• f4e17ecc653a11ccd4efe3117f030c05949414b7 add logging and diagnostics
• 9d09064ad08211bfb436b02bf08ee7cc0ee56ce1 add comments to elim_unconstrained and remove unused function
• efbe0a655414ba8e64c5a0b3c62e02730f622691 wip - updated version of elim_uncstr_tactic
• 689af3b4df2abcc0f45be9521066311e3654c980 add comments to elim_unconstr_tactic
• 15be80c9548f335527a39c011bdd19b03a0fe62d remove dependency on hash_compare
• 8da13ae24a2b8ab9948fb413f2d8510691ee7354 add statistics to verbose output of asserted formulas
• 9a656772b437e02ede9bc1e9850c112a325cb4cd fix #6446
• 4d86d739429e11faf4b8ec93f53c4c4ab7bd6b16 disable also tests for Windows x86, does not work with CI pipeline
• ff68df34510dc2e09030784e9e179f8ad8955131 update output of z3 doc
• 254f7b97ef2cb3f7503d791720509d7388dfaa02 cleanup state to clear model trail during calls.
• 823cd23ecc7f8b86079486a4c11c82badc7b5e73 building x64 windows tests during ci is too slow, skipping tests
• 3faca52c400f090062b69f8d6218a2cc5129d3ef re-enable new solve_eqs with bug fixes
• 9ef78fcfa7b6163b18827a208dd2b0a1cc3210b0 revert new solve-eqs
• 3a37cfca307bce55e3dd31859c5664572d9b83bc switch to solve_eqs2 tactic
• f769e2f1f66cc87266ab373bacdd12257df0c3d0 have bool rewriter use flat_and_or, and integrate hoist rewriter
• 238ea0a26433d3149361cd3fa8148266b426ef78 add shorthands for concatentation

This list of changes was auto generated.