• 53a01a07bdf245353bd0288fc50efb2739d3d3be rename additional build options #2709
• 48554f0fb663830244855c896cd01dfdfdf5c696 rename additional build options #2709
• b50f8508f25bf396f590f4395fea0d19fefb576d rename additional build options #2709
• e9d9792524046d5290602e6702a43fd40e2c19c2 rename additional build options #2709
• 3ab9a1c88c1523e89f03b09efb20f5d744998e4a remove deprecated USE_OPENMP, rename API_LOG_SYNC to Z3_API_LOG_SYNC (tiny part of #2709)
• 3729458d14faf837b50dfb8406879d0a6d39d66c enable pypi
• dde8da853ef2ebdf74a19a75a7392fa54c63fd10 fix bug introduced when fixing #2721
• 9b72b60949656635c81899289c59e2110060174a block unsound itos solutions. #2721
• 29e1fb67d2db3727e7c80529ac8ebcdd70e10aa9 fix #2720, unsound preprocessing in elim_uncnstr_tactic where datatype properties of eliminated subterms is forgotten
• 05ad90c976be01b8dbd1e5025c819f405a3b49f5 fix for null symbol #2712
• 37382d22c41295b6df3ac962709ca1c70759e463 Updated references to Z3 icon
• dd4905e377fdd9142187bca571e5959b0f746b18 Publishing SNK file private key for reproducible builds
• 215edcf888b7645fd61642309e0a7da22f53f109 fix; disable rewrite. fix #2715
• fe0b3d6648b78ed165df5f79da25404f55b85962 na
• 3c6dceae7cc10a1ce6b263721e535e4b4fe3453e fix #2717
• d95b549ff84b799e298f2f7db232499340460f05 fix #2707
• f0b8da42ad3cb58d03ce0a66666953ba3545cf96 typo
• 2bf595cb8ff4c77b442c531dd0fc71f9796d4876 update release notes
• cbac8603873a3d4b3117ea9f5aef5fc150e31076 fix #2706
• b9bc6975e99ea9b06ca1ee19ed522409cf4076ae fix crash in BV internalizer due to unknown bv_neg symbol
• cb600a93299fee501d6f46a04f4ed75d6f751431 consolidate model.compact and model_compress #2704
• 1a9dfc5e8041b03150d877b1a7251eaff7374518 inherit weights
• 784e2721ddab50ece6e957cef0133ed30d27a782 print weight if it is different from default #2667
• 5f90e72d856674730522dfcfc3a7ad0da5b3187a ensure generation is increased #2667
• 12819640b7d39608f8dd6cece58d0d1b52ffe3b0 fix E instantiation
• 74cfcc4730882966a9d6eed9f00f5bb2634a5053 clang warnings
• 20598e3bd2745da2e6d79863e6e6c737a01321d5 address clang warnings
• 0c1b68b598ee3532f72fa030a326c617683b0d87 remove unused variable
• c73a87c19c552e571c350adfaee17d4b0623c0e9 remove assert
• 779183da061a056f2e0595545d24eccd99bd8633 fixing smtfd
• d23230ec159a215acdbc28be3df628ed98d33b61 fix declaration sorts of auxiliary functions
• dd827cae1cb90cbe597cd3f793b0bb2b1737f0e6 remove IS_GNU
• 4fabaf95aa7066a636ff82d6792c517277eb24f9 remove deprecated and bind1st and unused warnings
• 984db3047b8cf932b4c1fe488d495c2f83ad6223 deal with warnings
• 4527a99f64dde0ca650e285e91a6b173de30a2f8 fix #2675
• 1fec4bbe94f525a2c3f0d51eefe76e5a24814b36 fix output
• 0a8b924481f5b6c5f4239c9d45bf3acb86e45d0e remove print
• b76dee7a7a4f8f0c468fc34983fdf166caf941ec na
• 1e0c1cefd6e60d81dccaf4a222b2d8580cacbca9 add definitions for under-specified cases of arithmetic operators #2663 #2676 #2679
• 6cf7d8e523a05a23145ac45e00f3e5b78e189906 adding div0
• 1048abfd9f547cb368c76d7072ea57df3bd08592 Merge pull request #2683 from fpoli/fix-static-linking
• ac60269c3e98bcdacf53fafa5c956982bce6066c Merge branch 'master' into fix-static-linking
• 7eb6731ac267e09da8edb16628258a58d0207bdc Link pthread with --whole-archive option on Linux [ #2457 ]
• c181f898c2fecd7d2985d0753d0b99ad35860920 enable static linking pthreads, conditionally, #2683
• cef5a26361a46964a16ada7a1c236497c83541c3 update README on cmake
• 8a420c850bcbb69a1f13f781b29db8ae2bfb7db3 remove divergent ordering
• 23029daf5e91fa2fa28dc92c09980cbb1d42de9a investigating relevancy
• a78f8992258ec01a34ae186363d3f82c0c437d57 expand deep stores by lambdas to avoid expanding select/store axioms
• d866a93627bfed6cbdbe448ef6e3db2401ec446f na
• da061bbcc31cdb722a7d5ae92b8b71c37ab72e4d Add hurd support
• 16d4ccd396d7c049218d97c29060427b77a489c3 na
• 18b8089a1ee1b060ffb0cb728acd56f24333c70b Revert "remove unused random seed parameter on cmd_context"
• 4faaff5b7619703da5cb2d8c3df8e4a02861c2c3 Fix memory leak in bv2fpa_converter
• 2308d8af09627c974b90e4a14018f2ad8836deda Fix for partially interpreted floating-point functions. Relates to #2596, #2631.
• 1d4f8c01689f1660ff8e817e1c3292fe98edb4c4 Typos
• efa3c0f68e72833a4cc2854f8ef61c4ab58c5afd Fix compiler warnings
• 823bf317c5d420c971cecaab94dc43fdc20f0f49 fix #2664
• d0dac831435fadba9c72975d43fc712a00ff1f54 fix #2665
• e24481dacd5028f03a34ac4dacba0ebfa6979ce7 fix #2662
• 376d2c1ed42c2addb3c18a456e6da092c59375b5 add unit test based on #2658
• be99d3d450a4f5c70241d43a7b125f4b7adc635f z3str3: refactoring, move regex automata methods to theory_str_regex
• ed03c1d9e6333695dc9e6ed937d429951557a7f2 Removed incorrect include directories flag in ocaml META file
• 14c42c1d742346cebed2653d5e4d9cbf920307b8 na
• 64dd4e1c83746a21083082636582f445cc5b0baf fix #2659
• a8049c7feb302f6e651d78b56af69033aaca6d21 update nightly
• b9a407c25fb7cd9ea97ae3d6193d47d9a8074c13 z3str3: force eager axiom setup on new terms
• f91af026758dad6c8f92d430fef0669694fd2f41 z3str3: set up axioms on string terms that are added during the search
• 9ae1a6f06133d2e10c630d78893dba41fba2dcdc Add MSVC ARM64 job to Azure Pipelines
• 3feb1479c96bf4844892a5a070906581604f3e7d Improve platform detection, in particular MSVC ARM64
• 907ffde577c57b918b0a625e691b66dc54b6c7ab Drop explicit MSVC's DYNAMICBASE option setting in favour of defaults
• 837651e3187c616a9e0aff97945bac94f6cab884 Explicitly add EHsc to MSVC compiler flags
• 60dde9f3d53c2bdbc03e380939ba3b84ce87716e unit test for #2650
• 8125fb134f0e83a14cdfb5ace3129aded8afd90c na
• 3fcd9e64c7343f2096b417a094699534c076dc61 logging
• f4fd94747cbd41a6b8fcf579db5603c98e4ec9cb fix #2652
• e2a9cb80e27049da644cfdddf705a8e450d18743 remove unused random seed parameter on cmd_context
• 9847675095c37f15dc5867b7f9dcc2fc363f7482 fix #2647
• 76b3198282a4dc995c209d7f0f4809d8551b01f9 z3str3: fixes to str.indexof when axiomatizing constant expressions
• 0acbdffacff2afe7b12c48744ff4849fc0d86798 update mk_nuget_task
• bfc30440ac040d58fa05d76612fd766f512c0c5a update nightly
• 9fae4a16e6ba609874c7cf61853c763f8c6597c4 update nightly
• 4051fbd8b2dcae33eec2d8a750858444feb81242 update nuget packaging
• f086f01ae0d9b4934f99ef1a297522f67ca5b912 update nuget script
• 928e08f28feca1059166a225dffb23e80b500cdc update nightly runner
• af442cf28119c3453cd1ac3c36d39c877b471d79 update nightly runner
• 0756581a9971f7eabc12ca93bc7283ed03ddb1c0 add nuget stage to nightly
• 5c78f855ad95c3c23507a3492983969ed9f3bd85 re-add deletion for nightly
• aef0c19d3652ab601099218e93a25db5e9c78287 add pdb to distribution components
• e5504247e9533d10b9a53a842715447a415ac61b use propagation filter
• 423e084cda3c58b931bee7034e68b58516512106 remove unused var
• 11736f078e1469d51938689f88c2fd82a5d75e21 ensure statistics survive cancelation in tactics, fix propagation for smtfd
• 203ba12abc8a896e01641e87203562829b826143 moving to context reset model
• 724a42b6f28f1c25b2b05a21e5947f11015612be fix #2643
• 5eead52cc069662ca4e38689689d0ba9db911311 Fixed linkopts -lstdc++ for ocaml bindings
• c1fa8444606fd373c052c877f6e69fa205941ba8 format
• a82cee6984e15f8e595f6230618855ab0e306604 add information about supported packages in README, fix #2642
• 4ce6b53d95821a2cfcb46a579bc2561b2101689f fix #2640
• ca498e20d17457b4baa32578a94923cf8e3e105c move value factories to model
• 5122b2da7ebe7f38681306d14150676ccec9930b add solver.timeout as another entry point #2354
• ed149ea44950f75da7abcfdad021cef1ab1a86e8 working on core focused refinement loop
• 77c3f1fb822035ef4de04685cabcaa4da3f0a456 fix ocaml build by moving to Zarith methods
• 09523a4bca456aa1d7c4b510abff234586e9f8df temporary remove delete from nightly
• 5a1003f6ed10fc65a1cbcd2554f183714c413c7c remove platform dependent copy routine
• 66339b73f496874f59b05078f5c2aaad3ab0c8ec update setup.py to include redist x64 #2265
• 71d68b8fe082b5efb8cf9990e7275b3b97acbb62 fix #2445 fix #2519
• 224cc8f8ddf6eebe217c7368700b12dab2821e0a Fix case sensitive fs include Windows.h
• c93a265b0b3d6a6bd6dbb0c93615ab23d524f795 Install dlls in prefix/bin
• f18b4430c3e21746f022078026181cb932107e72 fix to_app crash
• a921b4ff4ad331a3b0800cdcb88d2125d9b95ab2 fix #2643 - fuzzers are here to get you @lorisdanton
• cc26d49060b74503fad2b31cadb6ff73d5725b79 preparations for dealing with #2596
• 5bdcc737ec477a9267ac2e1104126b8525a40d52 remove function name
• ce06cd0d7a09fd95c7631332d13c825cfce4b88a replace iterators by for, looking at @2596
• 8d942ed26c985a8b7258fdafb61fe08816e50653 sudo the install
• d0cf1458e3023ea62d1bf9e4288078662d944fe6 fix #2630
• a1b690032ad6689a43373837a4b0f27e8d03dfdf fix #2629
• a90529e3dc9333713fbc5233dd7397fd0b77fab3 add path to python
• 8c8a8cee7a5f03e8ac63aafeabfabcb9cd502e8e add build step to generate doc
• a1814bf3846d73042eed9becdb5c3b243181c9a9 doc.fix(ast/rewriter/poly_rewriter_params.pyg): typo som-of-monomials -> sum-of-monomials
• 31a6788859d4fc05d2b88080d58014c328aa7262 comment
• a990e7f02e0824d0458917f4e7989f478c3c627a add visitor example, fix double conversion
• 4fc64ab578ab75f96381ee60a15f879af3cde9ea z3str3: check for and re-internalize str.in.re terms
• 58bc2bff0b0a0b2595c0d224466947bdb1fc73f3 fix typo introducing unsoundness
• ca7d066c4e591c42b704c97eb27a06da5ad5b763 fix #2624
• ecba7b3cde4c1125ac1db63b7b7d63b299051b4a fix #1006
• fd1974845b01fbc4c66fd584e062d3888b23dec9 fix assert-and-track semantics for smt2 logging
• 908254752b851ccbf6bf31e51171b8e078378ebb simplify
• 26c34c91937e054af48145e548bb2d53bf782a99 fix #2623
• 6b7c0ce334d96438c80e01090d3504cfe91d9378 add feature description to RELEASE_NOTES
• d25c7e67ebb20f47017b14618faae75ea3489ef6 increase timeout for LTO
• 7a5ca960951e56b8dbf0828d40f723c93d4ba4af remove separate API for setting solver log, use parameter setting instead
• bc50b6bea2d52ae5964fe697e2cde15162ece3b9 fix a few warnings
• 4192c81fae01e90fd8110a00b14172be818f028b Merge branch 'master' of https://github.com/z3prover/z3
• 9eea5cb91a3936e9dd597349a47df1cb3592c461 make smt2 log scope aware
• 8bb2442a3fa401a65b0d5046c32c85800b71c1fb make smt2 log scope aware
• 4643fdaa4e909d99e5888e4a6574d066c7516482 remove a few str copies when throwing exceptions
• 01f085ab53f51e0792bf953d75887b05b7f8f692 build C++ API
• ce1f2e10c5ee436cfc0b7b1ea537499b294c76a5 build
• 16dc2788a7bfe29b87d505f092a20bc2315e2762 compiler warnings
• d7167715416d22dcc0b164392f12e3abc23673f6 unsafe pointer
• 228b952a50c355bb9ec93de390f91166b9e3b5f3 add also get-consequences
• be33bb7b48588cf53cd1e6d0450931f798773334 fix build
• 6ddce9d5befa1be4d0e0154163b1defc2ed5e0aa adding SMT2 log file for solver interaction #867
• f6f3ca150726cfc26a50752de5f0963ccf7d2ab5 adding SMT2 log file for solver interaction #867
• b6c13340bd94340d6ea898f53539e3359cda0642 bit-vector overflow/underflow operators exposed over C++ API
• 27765ee0f4309b22a5f141117a4aee11a342ac66 add stub for #2522
• 7e174f50c1b7c69c1d2ba626a8a6db196dad5060 use Z3_char_ptr
• f4b803de95361ab1e3b5d7d29a00bfd62401d383 expose mk_divides over API. Corresponds to a = b (mod m), #723
• f8469b65d1b57e62c62ebdd171562839346e5d06 enable default
• 66b38eac9f2c5ca8edfb2908da7203b1c599e990 add back dotnet after adding ;*.cs to path
• 5fa177a650242816d0972d95637edac43dbad82e remove --dotnet from Ubuntu due to 3.0 .Net core issues
• 02e71c7d23627fc19b2a91b3d537daa1bad65673 fix #2650, use datatype constructor producing smallest possible tree whenever possible
• b0bf2f1792d871cbecd96c50f8ae4f855cc75f3f z3str3: recognize two-argument re.loop
• 82c39f81a3589ed2f5cc016eb9ffb739ac169b0e fix str.at rewrite
• 9a516e5e4143da4ba84e514d7462bb1718c839a1 fix str.at rewrite
• a8e7074ddd9ae967b9ce0fac45ec0ffb21776e5a fix #2618
• 7c10fb83a04d29da286a15cd8d25ccaa87916ff7 fix #2615
• f9b6e4e24779968c10baf4dac952b075136abae0 batch length enforcement
• b53f66bf2fba12f6f02eb3614f15de7da842428b avoid access to invalid m_length
• a1cb3a21f6cecb10b2436a6f5f958ab53cd46417 fix test build
• 39edf73e786c657645d41a6433a799a3fb685bf1 fix #2613 fix #2612
• 016732aa5936452bf133adc3281da2a9d77cc200 move some tracing to verbose
• ea8ef3edf85e99c36d3e533f364f4d021c43051c edited error message string
• 0321312c8db1d3f0edbd23e6e48884fbb7d77d1d Changed to get_const_interp to match Java and C# bindings
• bba9d11fba618629c0c3953c3fbcbbe54b743e79 fix minor version back to 7
• 3e6080b265040c46920baba13d737eca61b19d50 na
• d4c60f57662fc03df540c0c6e2fd2a986fc6a828 Changed makefile generation for ml bindings to use OCAMLFIND variable
• 5b4cd6dde4a6820a5c6ce8aaff5e697341b07785 fix #2604
• c8908e81aab78ddc87d17282e647c9a2fc49fa47 fix #2609 fix #2610
• feff1f7f9691a65c98ebe7d160d86c2668b0bf15 fix #2609
• a635049e238f79ee5a1b7c7dae039cebb8e72505 fill in ad-hoc interpretation for division by 0. #2561
• 8a568d438fd0f440e1b900bbd87197bbbc65e341 na
• 6616b6a3662a19a9c079e3fa07dccf73a14571b2 only case expand for cases that contain defs. fixes #2601
• 88f0e4a64c9ac6ad3aa83e286f9ad843452bba1f fix #2592 #2593 #2597 #2573 - duplicates, also fix #2603
• fe7a7fe23fc9190f468766e76e9997ed065a130e z3str3: fail early on non-string sequence terms
• d70b63c8acf816e57adce30242c0c8a81be515f0 allow parsing commas from SMTLIB2 input
• 292e72ce0cee2caa5bab45ccdbb0a4817b308d2d fix #2590
• f29b03325387a1d62765cfd718ddf859462fb8ba z3str3: add is_var() similar to theory_seq's implementation
• 1c70bcee69110fff57f293f5f6049bf14b1c2123 z3str3: setup uninterpreted functions as though they were string variables
• 301209cda64867f41ac9e230dc64b4e508f84563 fix #2595
• 98c3887460993b049f1da990c205adc165d56da9 fix #2595
• a424ab918b16f12290dd16e4e17cba103e4429d0 remove setting timeout proc to null #2591
• deb45c09e891e99e364f5b6a131be4d0edf9435c fix #2586
• 79d4502771c184bea495eaad1a12286dc667bbf8 atomics for #2565
• 18fe28c0f0db547e52f96d7d7a2755a8becbaf7f fix perf bug exposed by Shelly Grossman
• 3dcfbb8347485a01413bc85b2491598eec163c9e fix #2585
• 2a1f05e7e8f493539e0edaae4aafb8a5e30400e0 remove Simplify rewrite resulting in flaky build breaks
• 20feecc7b0e8b30ae41e300386cea8b718e8e5ae z3.py
• 666a237cbcd4a25682556ec312b83fce685a8c82 z3.py
• 1b910c4ed29d0589db643e6382b66c16418d45e4 hash update
• d0fc463a0cb85d5ad0ae073f57a3f26949e74333 fix #2581
• 38ad66ce170050d114050c3ad4f8c8e843aea85e update hash #2579
• 1203af83eb5c8c106e9ce7799b889f8961f9eba0 expose cardinality declarations
• f7cc68aa6aabf4e997700c4599fcbe488c4c15c9 fix #2580
• 74aa47f45899b267842ed1dec65a57fbaa168b8b fix #2578
• 2dd9ea071d8471b4f6a48b5d731e4a73534a20f7 fix #2577
• 64d4e599c17523597120c022c6ec2ba0d2d821c1 re rewriter for loop
• 6041cb246f6a84bb6d6896649ef501625833f722 --lpthread -> -lpthread
• dee8a9f308f06b78a89ca829a5f4a6ca928e18a6 remove more unsound rewrites #2575
• f3f233cf14c877d2557b5403f028ed961c2fd5ba remove link experiment
• 6b117c0b2c969a809e3762145de23431768a76f2 move to zarith #2471
• 0b06a9b5d8beca9d0ee6037b23c78a684272f2a4 fix minor version numbering
• 3eac4a4aa1cb4b07a6d22438d6907ae13be02c4c clean up examples for unused variables
• a44cf7a9bab5a50f00108519321098187b1ad14f unused variable warnings
• 5919bc05311a4aaa6ed9f35ba32a35ce11cb8044 update for next version
• bdecd2298c84f00096c5fcc7b68e7129b00ecebf fix verion numbering
• dc625cb01df21066ad64dd90b4b29e386b06df23 remove unsound rewrite
• 22b6233e6230afd4360af75ef81d6303d601f608 increment version
• 48e996241eadcf31f92ac0181b4278f9b7ddf5cf fix initialization order
• 4101652747f631d54915459c942d85e5e1f21bc3 handle case where lower bound is above upper
• b506e4584547de1d323c6b373056ad501c93b81a align name of tactic in report
• cd0cd82eb7a018a9b7ec753f30887a2cc5ceb3b9 add rewrites for #2575
• 80636dd35ff714e63dfcc4d925f7e62b485d3e39 na
• 12034df11aabf6d9f416c5e4d8e2b408b4c37df6 add rewrites for #2575

This list of changes was auto generated.