• 4b51fe466db6f47b43dec4baa6bbf697688a7172 fix #2562
• 69abe1687e14bbbf5cabe0aebd0909fd7f2b59cf backjump to level of clause to ensure that new atoms created by projection are assigned as assumptions fix #2557
• 0f20175bdd716fc852395ae7ad54d169de3af42b fix #2556, sign of of inequality is not restricted to -1, 0, 1, but can be -2, -3 etc
• 0c972b8bee766c92f48a56b172fba3a33cd359a2 tidy
• da805f6016a846e45c7c2c2a0560759f95fee6fa address perf bottleneck exposed by #2552
• fffc539b40345a08a4edbd6b29b59db227cc3b5f fix #2549
• 098725aa1cdfb15e36911001a32a6ce8495da274 fix #2553
• 67c47775140921bf9b9136a0d8b169b1e077cac1 fix #2548 fix #2530
• 5d9ed5b0a94807946ac3218fc24ecdfed288aa84 Allow for __truediv__ and __rtruediv__ even when not using Python3
• 1b83c677ea9e8683c3ba33ab8e7b33589055b309 spacer: fixes lim_num_generalizer
• 63840806d84c4205952fe97a572b4cbf398ad273 fix #2546, retrieve model in optsmt lex before iterating
• 0481adb87c853947e5afbc3ddd708e387e111906 fix #2547
• 0d3fed9a6ad844c0b65130b2013e7372dd16d92f spacer: lemma generalizer for small numbers
• 78a1f53ac969ba8357ffa4009427f6873bbaee67 fix #2544
• b1cdb3e4518d17e2c4dde22a55eb581f5926ba69 add mbqi to smtfd. For Nuno, of course
• c22a17f43075ff0182631040409b6d5f340918df smtfd
• d3da161803d9c7906f49ca41b26a68fb8eef9237 smtfd
• 5ba4d8d0f1c577caaa899a02eff179b9b4c12fb4 na
• d44081db7d736945d450b0ecb93ec39602fc4bd5 fix clang compilation errors
• 3b1a73b9e80c17102e691d5d9e711e242e40ceb7 add smt to project.py dependencies
• 85fb6f59de2ba0628d1fe8b9686e45a2e414783b disable ackermannize on goal
• ff3cff06b28ed5a1dafe3f64038826b8f808ce3c deal with ite
• c476c4a86aa1a73374a9aab9757820ed67a1fe93 smtfd solver that uses lazy iteration around fd to produce theory lemmas
• e881c4af3fbf8141604e1cce24fca05e73ae0992 Support repr_html for jupyter
• 228d68f165be5742d8bd757e06784f25a67e035a enhance ackermannize for constant arguments
• 18ba14cff81be7a846cdc793f7d012e3a86fdfab Z3str3: fix empty-string contradictions (#2538)
• bc723fbe89a1fe4d41d7257002a586335683dc46 fix #2539
• 8ec6219010d8b488de0ad84aa33233680d59a976 na
• a92c82d895723fd2a8fed319639b815b5ebb9324 na
• f645f8d6853355e198903a4dae7fe3f36430a93b fix #2537
• 29f0897afca47db69c5c97bfe7cf5d00290b9637 tweaking nlqsat
• 5fbfc0f9f75088ff2a0a08dbbc319de2e551832b minor code simplification
• 8f4e7f49618f3893c2ef228fcd3aefbdfa1b6a7b fix #2533
• 9fce5e124f801b1dcedf6038348ce6bf6ccd6635 fix build
• 87a96d7bd48f8d287d245a322669f75bba6c6539 fix mutexes hanging due to access to free'd memory
• cb7532668698d1e10295730f944f952209634d65 minor code simplification
• 68e4ed3c9c039716a53849b2e85fb4818f43b71e fix #2531
• 000e485794992c2e30a2052ce5be65f1e55e331d add array selects to basic ackerman reduction improves performance significantly for #2525 as it now uses the SAT solver core instead of SMT core
• 7823117776d6727b06e08e3f7918582670ba7de6 Restore expected behavior to stopwatch
• e816d1672456b785a2f45be35b9edcb666f796ee fix #2527
• 4c0db00a7b37d277e3a703794fad31e52adfc455 fix push/pop bug for ite-elimination, thanks to Nao Hirokawa for reporting it
• de43e051022235a8125c8e57d244bf6821486f4c fix overflow bug exposed by #2476
• a8bfab32735449e8553cd39a14ee2db57b82aeca add model.inline_def option to make #2517 happy
• 35fa24a82a1bc4a9c3abe911c77d554c0b80c2f6 initialize best model
• 20dc59e02d5cf6c0a1b2a2a76aab6ed196d05241 fix #2523
• 2e6908bd9e395fb333e3125e3b477f361de4d76f fix #2509, fix issue with model inheritance exposed by #2483
• 271cd2ac6b8bffe6bd69edd432d7b73b3aa3631e disable expensive model validation
• f048cb27ba8b4ceafd752fd08d7758f3223180eb revert the revert
• 75a40d8f8eadda99a4e7a6f8de7541a78739ad50 reorder fields, rename overload name clash
• 64f4c9794deaa84d8d888a2195d73bcca3ed9950 fix regressions during string fixes
• 0d9cd7bc2bfc5e34ea6e2e108d42f2b6f1f528da addressing misc. string bugs
• a337a5137487d0e6ed0cfe134e9acb2240391e71 fixes for #2513
• de69b01e925edb27f1594a5355334194bb738d80 Lev's fixes
• f90db2ba1c813de705ddfba8b269c231c5752bb1 add back compression to ensure local functions are inlined #2517
• c15764e06d65037c1dd1ad359f2d4222214897db remove verbose=0 instances #2507
• ffc696e63424d18b6bb989844bac4c84ea8dfa12 exclude built-in functions from model
• eea041383d171b09964d443553096faf75ce5b4f fix #2502
• e08abb3213be4b1eabc4fcd3d519273f14de529c fix #2504
• 2f60bcbfcbff5245d2780ab33e4b67468c7068f9 Clean up NaN return values in Z3_get_numeral_double
• 423fb73d34be6441b876caad9a6fbc2a2d853a45 Fix for fp.rem. Pertains to #2381.
• f22d6e399d3badaf09888ba54266942e33bae5e3 Fix floats in Z3_get_numeral_*string.
• 79cd1f0edcfb05655854781448728ffdade145f4 Fixed Z3_get_numeral_double. Fixes #2501.
• 258b798a6b4276b4206bfbe358fa89b627fd2eeb test-z3: Improve help output. Provide help when no args.
• f02170feb4e1aeb2bb74b35f7d2486d9f4b501bc Clean up whitespace.
• fcc7bd35e5359391e4d78d61fa41dbe07a8f23f7 fix #2489
• 3074e2b80c32640e18198115f399a74fcfc1cd2c fix #2487
• d64dc939b273c069bef7133d7342a65bf237e001 Add note about minimized unsat cores to C API docs.
• 9949f165257721a456a53543df36d69099021ce5 Fix release note typos.
• e2122c0d3d1302e3e71af083d2aada558e04b8e0 Fix whitespace issues in *.pyg.
• 0734c5f3f30df9b87258a9dd7910c3539cfa33a1 fix is-array-sort test again
• 892aa126605d8cf9a1696af1add6cb30435fb1e0 Fix for fp.rem. Fixes #2381.
• 0edd587e5a7bf5c0fa890383254533e0c11c69cc Fix typos in examples.
• ec5b148eccfb5359d974d441f5c206e502427c28 Add python packaging build and deployment with Azure
• eec550e645150a6b29719009e71ed048b7331e2a fix python build break
• 2b2f016f968e449392bb98632d28c0276619f0d1 python for accessing lambda, switch to theory branching for QF_LRA
• 520ea65f32699b7370e4cd01813d046fc1bfc15e move towards theory phase selection, implement getitem on lambda
• 0eafeb9342bdc2dccda646f3d78ab8964d5ea7a9 Fix confusing tabs mixed in with spaces in C examples.
• 0093157bb90ed056940c354ba7075d4514443be3 Handle dynamic sort of Nth()'s return value in the Python API
• e89bb37156b6a614e5f0add9f41aff9a88950259 More see also content in C API docs.
• 375c0ff9a9bc594bad2e14ec0c1141203600489a Implement get_proof() in bmc and spacer engines
• 876cfb4dc968f33e7319dd19aa679ae71a918ba1 optimization of phase
• 75962173ff2e1c1b51b99fa42ac88f2d0f2c7998 fix #2481
• 9fa9aa09ff12d81ae0c2bcbf5225d305eda242e2 fix #2468, adding assignment phase heuristic
• 42e21458bab35aa86e815cbb2f8199cfd71824df fix #2479
• ce84e0f24082be575c62cd95334053f9739978e3 remove strategic solver header file
• fc41a61b6e03c03760f8f87c4aef30ffed78c24f expose strategic solver factory prototype at level of solver module
• 1ae0a9813251cb7fb9a966664fd8f15902d7f958 fix #2466
• 52acbf1f1467ec2dd5968541a7951631d4bd0107 bug in qe_lite
• e2d91ce1fcdded463bb2c9ae21317641e406eddb distribute concat over bvxor and bvor, #2470
• 8579a004d0283cadca06292ca48fb4f3c9a03e53 distribute concat over bvxor and bvor, #2470
• e9504536858874a1829c5b82514c6c8fb07d4210 force propagation for smt cubing
• bbfac99b22949b5ac1d7892e74036fefb49d1ba7 fix #2469
• 0af249d651656048d569239edfe0e1d2f8d46723 'na
• f90439fdc524e8b05651dace685b3c27591c063f docs: Fix a number of identifier formatting issues.
• 077f518241c97bd4cd34c660a09171043e61b63f Fix -Wreorder warning.
• ce7f9c3f3d3dedc69a7e46e365f783952eaf4026 Remove unused variable.
• d977c151f6d0ab32503ccb8fcb3c6eca529725a2 Merge pull request #2462 from waywardmonkeys/fix-typo
• 6be36f18c604441743bd0f0ffb826f7b6adadfaa Fix typo.
• bc3b0f6e332bce68e4533677f84e3e18271f5fa5 introduce fresh term when none is available in context or model to fix #2456
• 01920abf46a2558e5cf9f08260547b723a47bdd5 introduce fresh term when none is available in context or model to fix #2456
• 59f69bbe0dc81e6aef2a9fa9aa9b0cfffd1ce2b9 introduce fresh term when none is available in context or model to fix #2456
• c7dc420b3be3ad72e7576e36785955e170b48427 let me guess, ASAN doesn't like 0-byte memcpy
• 90415a18d330d3a6066e589aaf20f1c2cc9435f6 fix build of test
• d7ac8dbc7d8661375bfd354419b53588359ee84c fix #2458
• 3147d2351d50a4eca7d97b380f86038ef31e98da fix #2460
• 4431a534b3f719d6e51898a95b67bb01c026e73a fix #2450 - track assumptions across lazy explanations and variable equalities
• db5af3088b54f3afb388e730789142b9630aca8b logging for #2450
• 1d488d07fa52d0dd95ee797a3f8b335f579d04f4 nlsat
• 2d5714a5d4b854ea2bcb48f7749954a7a356f985 fixing #2443 #2445 #2447 #2448
• 584eee2cf4350d325992ae35eebcfaaa4606b867 fixing #2448 and #2445 and #2443
• c4480337c4d4dc71f3c16207c60619dee3e72075 fixing #2448 and #2445 and #2443
• 3d1c40ce23f776a6162fd00c9fa2c8c368fc850b fixing #2448
• 95eb0a052113b4c36e3c88c7ae81e054cc89887a remove an unnecessary call m_mpq_lar_core_solver.m_r_solver.track_column_feasibility(j)
• 294dcf7b1c40edd50e9f30e86b3bf681dafd9c13 Merge pull request #2455 from levnach/fix
• e9e950062aa48e65cf23c40baf09df756294fb96 fix the build
• db5ac5afa8087d5176a40cc66e88800e16954e05 fix a bug in lar_solver in queryaing if a column is int
• 9d6728aa718b003adda909a7147533f18ea222fe fix unsound rewrite
• 0a29002c2f551504f80a25071d28c5cb8042e88e return unknown if m_array_weak was used and result is satisfiable
• 3f032e85e0339ca73718db431d91849d1fe8c530 remove include of thread
• bec38f268b51940adec2e38686b32e0287fb105c remove debug code
• 7f073a0585168821adbc8a4603a8e5964542a60f fix #2452 fix #2451
• b7a27ca4bd25792208a77dae7e6023fce2a01291 Merge pull request #2454 from RichardBradley/java_sudoku_example_fix
• 04e0b767c300aec525493d4ab1a8dd5d8e3407f9 Fix sudoku Java example
• a2b18a37ec2a8c2a031956ae8b4bddf4340719e8 fix #2449
• e1fd167e01d74353431c683b9533c75b2074e087 remove stale assertions due to lambda #2446
• 74631265b9eba8b4801c0bd7acf3557efd228869 remove stale assertions due to lambda #2446
• 902c683b92ce332a072cf75a644023f39de29c02 expose _get_ctx for scope semantics of newer versions of python #2441
• 2bd8d3b4852765cdd92abd7db6331fc5bac8fb5d fixes for input4/5 #2416
• 06ee09a11325470730d522f2b0fbf0914a2894a3 Update README.md
• 07472d25637be307bdd6d23ec2568ba3b88e3ef1 Update README.md
• 728139599c469c992b7c4853ab3c9d92358fafd8 unfinalize
• 42a1926cbb14a44dbbb7e25ff2d3afda806f5502 update readme
• 6b5961ac1eaff2fa0123d6634b7d53d96da13f22 update readme
• 00a4f6ad3d3819d0e3e78e9a507b72135e3e5cdb throw
• 1d223b0403721c60b1e34214d9ac0920b0bfba4f setting ctx to null after close
• 2eea7709e06c357fb84798ae52a6690231e74e7b Merge pull request #2438 from agurfinkel/issue_2430
• 53aded3198738e64f2e8f1cf3db44d0bb4db5535 fix #2416 exposed bugs: unsat-core extraction in combination with chronological backracking, equivalence elimination in combination with PB constraints
• 92db639caf755a0403990c0c0f6fa70d3a8b2ff4 Use refutation to compute ground sat answer
• 8a0d79251e6cf169e5ac7c24993bf94057efa85d make sorting of soft constraints the same across implementations of std::sort
• e6df7b73aa09847d82f05798690eb85b37125225 fix #2434
• ca25e482e53f739aa374f531d9c4b0c86df7551c temporarily disable elim_pure
• c75a57731f0b7f484b3e70ab9062c509e1959e4c fix #2433
• 859512d937594d3b597c956a7c476e46f3af9f8b fix #2431
• e17b43617c90aa6e136b1bce93b2fa4ec972e8c5 na
• 604e6b2705afc9bbd37593032b5763ad23a40ae2 fix #2418, change types in sat_solver to avoid cast
• 809b0ebca76e6ea9c03c4bc362ce4295526f6e3d revert fix to #2417
• 3a90de1cbe280c98046f6191d3ad2ee933346e52 fix #2419
• e65a5d0f4739ec7a89ec4500f5ab00ca9ca96de8 fix #2420
• 019d78e2194277fb38e8635ed33960cecfa812f2 fix #2422
• 1a70fce92eb127480a79eaf8af7dc19d089cfd5b add back nvars
• 185b01dd35b6e0897963e0fa0f0821836d18fb75 fix #2416
• c2264c73f21057903ca1921c3c47e54d38616f49 debug mutex
• df04d7f108e694ff808bb5aac81ab045b481cf1e Merge pull request #2428 from danielschemmel/warnings
• 77d5b381ead4711c3d73c8be9256382230e82712 Order initialization to avoid -Wreorder
• 5e5c231712dc57bff527eb22d67d0136218251c3 Remove unused variables
• 364fbda92542789b9810cc8d9a594de047b07059 expose reorder config
• aff4b3022ad9a4c65364c82c2da3bcbd62052189 fix #2417
• a9a26e5f2eeb909bafc09a3f24bd8cc57eaf6825 review comments by Elffers
• e593b5b2c83dd6d4281cc806a6106f60336c7147 fix #2415
• 43a19cadf6c80ea0b31a7638b5b7939b69b264c6 avoid reorder regression. affects performance of SAT and also noticably for #2405
• 41ca9560126c2a19549b10eb7974683a6d4d0ccc expose import model converter over Python, document it, add partial order axioms for lex, disable linear order axioms, prepare ground for re-adding clauses from reconstruction stack
• 7ed5ca05e353ba6aeb14ab43b877c3294fee2e4c fix #2408
• d07f2d45e740b10ba96ee4e98bd04f3562febe14 fix #2409
• 1fca76b0a12ac1a543d9f397c38539b90e640029 relax restriction on infinitesimal for rdl, #2410
• 5820b16800d91794a4ff3921986cb86585e5f7ba mark assumption literals to be skolem to hide them from models #2406
• 4b6a7371dd378270e2983682d9385d8276bf1ec7 insert fresh
• fb124d6e9301fea1cb1b2c3c9d78ee1c966c1e68 Merge pull request #2393 from Nils-Becker/master
• 4deb9d2af27426fe18381af2994bbc60f5513a3a use array interpretations whenever possible for #2378. Also strengthen equality test for lambda
• 3ca32efd184dab9fb027eab7b9514d00574da5d0 na
• 2d4e9a0f67983e8dca9a84666d0ff5f31fb5cb09 update managed APIs for lambda-based array models #2400
• 659be6940ba4108b82ed9af3f2734e9c95e9aa21 fix #2395
• 26c1c744aa067885da6a4884233c00600dd354e5 fix #2396
• 0bca2aabff43bd913c56f073222cec6e100ce241 remove invocation of debugger
• 559af09b0756fb68629dc9463e7ff27994566d5f fix index cases
• 84990ffa277002d0b8737af95bb890c0d7ab6191 fixing #2378
• be72accaf523916fd79faa02e8f003b6825086ec na
• 1538b31dd931e4b8314dc18a8b9d1e317dee8866 na
• d861b912897b7ad25cc82844c7d997a0cc8feebd augment axiomatization for substr to fix #2366
• 79e4b84507984c3d7bbf8f0c911ea18dd8da805f augment axiomatization for substr to fix #2366
• 1ba6d16c612ede7ab789146cb96a6c132a241fe0 augment axiomatization for substr to fix #2366
• 308647efd96ea302b20d6f8a4534293ce71dcae3 Merge branch 'master' of https://github.com/Z3Prover/z3
• 335072eda2fd56974dc3fc969329f748523bec1f extract logging into separate function
• cfb4d289b8b2e210c1bf6d4ae07dbefe193ea363 fix #2325
• c7fb1e4c9f21a5141881b19847343b85103fe1b2 fix spelling of target folder
• 9474833c989797de64fe47faba4a726b8cdc8ea6 fix #2391
• adb91ae93cd0b299a0aa1151020623a64c47da7c compile 0 case regardless of numerical value
• 77df8ebd12e903cd9326079a46e0d4452e494e36 try to copy artifacts
• 8d9a631c5da252a31588d61fb50476b39666b80a try to copy artifacts
• 1d859a98e571245ddfc0cbb682fb6e18ebd53993 updating comment
• 7a48524213f5935efa6579cbfacb9af60de775dd count subterm references correctly
• b226f3a77cf63ed92539165b54b48889f8ad2289 cleaning up includes
• 035101f399ba3112affd341eb7a8636ca5da13dc Merge branch 'master' of https://github.com/Z3Prover/z3 into HEAD
• 23d01f5974cf6d97455f00d562fbf46da7ce218e fixing rewrite logging (https://bitbucket.org/viperproject/axiom-profiler/issues/13/version-486-of-z3-not-compatible-with)
• 09328d5bec5ca3f68967c00595571c95014c05a6 remove unknown option /RELEASE in python build
• ee94f8f5ce89651dd5e659f3e876b535f41ad73c update release script
• 5de35d46eb30f46f02bfcb29c05b292482eca51a fix #2390
• a13ac6a759519368c0235b0818a2d7709de917b8 Merge pull request #2389 from agurfinkel/issue_2357
• 7cb956a0e2370e00e6cc065dffbba01adebac5bb Uses non-flattening rewriter in profos
• 88aa689a70819f464ce5edf02e807b357d1b393a fix #2387, add ite-hoist rewriting, allow assumptions to be compound expressions
• cd93cdd819155da8b6fc98127f63512e042e6d08 na
• 6bbe8e2619c83e6a0403931aee06fdeabe5c738b add some static
• 6e637348826f0725ba8a01c455448023ca2889e4 Merge pull request #2368 from waywardmonkeys/fix-typo
• 164039a47c6712e9cfb8ba4533d60886b64228ed Merge pull request #2383 from mcfi/patch-2
• dd253cdd47d81b110815ed026a70f3c996c9ed5c Merge pull request #2382 from mcfi/patch-1
• 962d0dda78ffddc51cbd476ea65a06aade92dfc2 Pass /RELEASE to MSVC linker
• f8a9f6cce091ac5bca849dfe19221c75ac50e9e2 Remove unreferenced formal parameter name
• 6d244ed2aa311d07e8c8aaca9051308d0107ce03 internalize reflect
• b86432e2a33938b8ecd2d3a347534bc23f4aecdf na
• c744b19bcedb7436ca94338b2e82bae5a83dba77 resort to only supporting ground non-linear division for nra_tactic/nra_probe #2372 #2376
• 8e2ad4e461a4469d345a7b93b17f6acb23e64d38 #2379 and #2380
• 1517ca907e560efed482e5ea3a24359baacc7edd Another fix for fp.rem.
• 77827498bd90d38636ad4bd5071ffa34b37e241b Added checkpoints to lia2card tactic.
• df4065536fa51e81a664f506751a4ea547a20e6e Cleaned up FP predicates in the Python API. Fixes #2323.
• e0dc05c97edc559ae0d5ce841120bb55ad8e479b Fixed final alignment step of fp.rem. Fixes #2369 and does not break #2289.
• 807095a3448d90db993a81b955ed7d78f2f3112d fix #2375
• 1202554dbcaa67b18e507206ee6f0e6f2a5c95d5 Merge branch 'master' of https://github.com/z3prover/z3
• db87f2aab055ab189a6c47cd9e2c4216fc65cf3f separate rewriter used by smt context from asserted formulas to avoid term substitution, exposed by #2370
• c4e0f8ce8fb1f4540275b1cb811f1281f1af173d Python: Fix doc comment typo.
• 60c504f4ef64eaf085b1fec2773704cd1102c611 make a few helpers static
• e5dffeace4b04b757aaa5f78e4e749034029fef0 fix #2365
• 90098633ef05563fe5f125fc9a8d4ed5d80c9533 remove target from nightl'
• 218edbe9c68c7906971e1660510a6e7afe933ca6 ensure also negative lt are constrained #2360
• 85b0722df0a53a828d546c9756905d09315427a7 ensure also negative lt are constrained
• 1f0d162b7fc4ebd368bdaf159d3a414f33f0a334 fix segfault #2360
• 6f08c0788fba30a2bb3f9f9e505e8b785c7b282d put back delete step in nightly
• 6e994f92794f72abdda28dcd7e9bebb7d6f0543e temporarily disable delete
• 8a129a3e6f85fa337eb7e55504ddf543828068dd try replace for nightly to address #2362
• 335543b37419ef01c4315c835aebb734895a0815 adding comparison #2360
• db274ebe01ba81195b30b848d77386ffa2fff865 relax condition for distributing extract over ite #2359
• b8734273c80884b27acd4d97b4eaf4cca21aab37 pydoc regression
• 1e21ea464511cbd9d955fba00f73ebf2577f5a99 fix cleanup bug exposed by reordering simplifcations
• e8080d2307cb7a7b82a5eb1663b09d28ca13680e revert normalizing ordering on equality as it breaks others and doesn't necessarily lead to simplification
• 2a1f8ac2d89a13d52275e952b2f1e3c2d07be5c6 revert normalizing ordering on equality as it breaks others and doesn't necessarily lead to simplification
• 5dfc40bf50efbb8781a62cd33150271c90494286 python regression
• b4290d4b3d7c021965e9ce7ee636caac0f9cac74 python regression
• e0a44894cf480908ddc8110b1761e682af4e4644 purge smt.timeout, use timeout instead to control solver timing #2354
• 63a952f254d7f3f19cbd426690ff7b560da26ea2 setting ast to null on destructor to deal with #2350
• 333b32b0d2c829e771f2e9c9d632f00632220b44 disable adding redundant ite clauses as lemma. Add as non-redundant
• cbe52e298bfd29f83c25a390f90d846e75c9090c remove tracing, fix doctext
• 1ae0769af502f18432dafc44ee7dcdd420c1cbe4 update doctest

This list of changes was auto generated.