• 7327023c887a469a70b973b7e5076c879ca68dc0 add variable replay, remove MacOS from Travis (#4681)
• af54a79acc9aba4a09fedcfce0488b1bdb2f3e3f fixing issue #4651 (#4666) [ #4662, #4667, #4665, #4661, #4668, #4676 ]
• d02b0cde7ad221f44aaa232b2e4a4fdc4fd66335 running updates to bv_solver (#4674)
• 4d1a2a2784b7bb2c62fd939b6e8c12763ef3241c update to xcode 9.2 for Travis
• 687a16a796e90ae82f15bc3db389636c4f0ae505 SMTFD is back (#4676)
• f370d8d9b4f1f617c12ede0865180a29116d6cb5 na
• 7fbaf71d4a3d622d3886365b80ba0743d8c9f42d na
• 65bc77d5666dccf0244fc9e3e2d264c1b8af48bf na
• fe43f8df8f2c5298bca4546430a9c27defb36ff8 na
• aa66be9406069ee59e54dd04f4cc93ef985c7500 na
• d83d0a83d6b12a1411f42cb3fbb560cbc638952b na
• e4b7b7bdf6f812767966eb0bea4421a1d4551437 na
• 95493f78f96a4d4a614129449f588a7d706aca99 na
• 4b2243473977ba38cbc2742dac9f9f3507331bd0 na
• 54a75d6a9117bea4c3accaf2685e75253a369eb9 remove SMTFD
• 7c2fe46eb72ebaed1614af71cd0ae58dd724de8f build fix
• daf7e9e3ef9b5c9584b516673e505e17511d2bdf file
• 116390833b5ec5b43a46d26be92064e517cabd8c prepare for theory plugins
• 141edef0d64796fd387ec2f8efe796a7329c48e2 butterfly effect on fp?
• 527bf72d42527054d7cc1e3f18e061fd7cb5d2d8 Remove duplicate binary condition. Fixes #4668.
• ecddaeae66378180423d93928992dfe53bba25c8 na
• 74a2bf15882c7c7dbf717ae9749dc711267a7adf Merge branch 'master' of https://github.com/z3prover/z3
• 03e92f3f20b09a05ed2ae6cba14be4f221d75388 with bounded
• d4e92d4aca1df34ef2d56e425a27134395a214c0 move theory_var_list into id_var_list and utilities from smt-enode into it, prepare for theory variables in egraph
• fa9cf0fa0c3163e2f4c9683048acdb39e25f8ded mk-var during copy
• ed7d9693664b7f5e7704892e6a081f69285701e9 elaborate on smt/drat format outline, expose euf mode as config
• 4d41db3028f97748758427dcf74406658082ab81 adding euf
• 314bd9277b9012c36871a56c28fa56a7e14192a2 avoid duplicate class names frame in sat_scc and sat_smt
• bee3077640ae4de245b7563fc047fadacf5e1ab4 free memory in egraph
• a003af494b00a1ac09d86a72fd2babacaa99651d release nodes
• bbe027f6a14d90f45c5a52453c6696cce9a4a23c na
• 25106866b52eea709561024c9bfca0a59e3ee867 fix dotnet build
• 9f0b3032630806adc8ce26a88264705cfedc3c1a na
• 727ea43b16caa39dff5a4d993acd69426222b3c3 remove lazy push from theory_lra
• 9b5dc0ca26e14f0c30a36370222a2eb938a98323 fix misc issues around #4661 introduced when adding lazy push/pop to selected theories
• b992f59aad9fe4a574a8af43fe79deccbc74bc3b expose name inclusion as optional
• dbe2c9b30594995f83262ad769a82bebd0c8db18 encoding options #4665
• e8826bb20f90c21e3cb4f196d4fa67b00d005691 fix #4651
• 4682b48d3acff55781b62e5298997cbc458ebab3 na
• 86310a1a2779c063981efd163852268ba13f4caf updated sat_smt
• e9a4e486ae6b486e29ebf2ff4e3e6365441354a6 dbg
• a35d00e4c4b6df2d3dedc2a4357275c68ff2d651 remove pragma
• 996905a2c1dcc1ac432af5647a03fe6afb5c1a67 fix warnings
• 35e3d8425cf01afd6a2254e83a4cbcd4939bdbbd move fpa
• 11c90cc142385864c3421a73c7fe86241f0ce9b4 move parameters from ast/rewriter to params
• 507b4c7848793ec6018e1d48c5e84f6a1a2956ac path
• 49838057a4d07e86d0bd0e54ac01ced4c2853dd5 virtual method
• 98084d7da7f903c3ba56da1a483c65a986806495 add depend
• 7c592d4543303456d0056d4acc67de07cba0369a add depend
• f6b242e58147a42c1d1a992b3a15229daa07a9e1 update cmake
• 455d53ef27ad79cbc4941064aed48c762b2c4d9f missing cmakelists
• e2bdf54d5ef227e9f48200be613b4bb634856462 update include
• 79fc3f2375a9b6ef85c12f3ca1a21495f97aaef2 warnings /errors
• b9cbb08858d18e71c5e184a1a5ead2cc99f8d2e4 shuffle dependencies
• 4e6476c90a556ee8c49d5a659088cc22ca9544ba fix cmake build
• 60f8884dbdf655ca259d41b294d2ba51b087db1d sr
• b8fb744935a50ed0b845a0d79fde2750f15e77e1 reset caches
• 739b5376e3c89ac2b350a7fcca61f3761919de10 dbg build
• 93ee2a68a46bdfd2998776fcc752655532fb1f20 persist fields
• 86c11b9349bcae61708b2f969aef8f2fe691767f order
• b03d1c805331af4cf334cd8e3f5819bbad2fad68 deps
• ba21ffa31b9343e34af969fc7c36efde17afc9dd missing file
• 0440cfeea73408ca34eba192b2970cf812eb2628 add smt params dependency
• 4244ce4aade3b4b5e1e8bd477ac364baed86bafb adding ack/model
• 7f0b5bc129988225c831314202608a26a18170f9 Allow to skip System.loadLibrary() calls from Java Native class (#4667)
• 6706b0dfcdc7c99662567a75c59862be981026f1 na
• 872fd5e9ffb5c464218ed2a026608e535d6cbff9 fix #4662
• c6135a40d538daffa1dc9495df2103a66259c8e7 virtual
• 4ab35a9bb5a29fc6a904cdebd09f3678f654b8a1 euf model
• e6e635b2e8edc016d4f7aebe6b3e378ea40c7a10 remove unneeded pragma
• 21e13bc5f96c5acc2fc627b7c0b0ca99d7e2f866 re-add pb extraction
• 526d76b4471c78a950af3dcab0cabfe361677053 re-add pb extraction
• 9c77fbc2a9128420dd5366b9d9a1ff572520e72b use virtual destructors
• 1a36d44450701282e7f66c905433cfd4878f0693 na
• c21a2fcf9f98f5b7d1c1a5db034714880b7bfa34 sat solver setup
• 78b88f761ca21f0287eb6563092b706d15c7b71b updated rewrite rules to propagate nullability over nonground regexes (#4663)
• ab10616b7788c36b4256729459ee8a817d85d88f fix build
• ecd3315a742ee63c36b0e757216d1989ac6c16be add sat-euf
• a7b51d04cd2af233f704f75406f2a90ec8d9c52f remove unused file
• 22aee4d08dc5fe6cbb656b04d13f20560d416c63 fix issue in #4655
• c722962124946eb197f9ddab0cf718f85c2a4712 fix regressions in python API for user-propagator
• e46ad45968ccbfb65fcb78cbe843eb73effbcd39 na
• 6beec7b642706cdcb830594151131869b6ddc683 na
• dc1783aafab3d654f9ef0c636ae8915438b3b5cb na
• 3dedc13481bc92a26c57ef87e594c6d33cc1ff87 na
• 65e6d942ac013ef9e3c88022d79de051f089f717 euf
• 96587bf70814b66f16bb582700f3f94dc0de113a na
• 85b4fc18658ed500bd2c8f5d587a2b409d6c8f47 void
• 43d932301dc266f3500b5d20325728b4ed6caefa apply operator
• 84475ff142c5a4ed51d9a056b89046a6e8b13ac8 fix #4637
• 666e835e089f2cd4b71e4eb4cecfd8228b174b6e na
• af389db2b28c54c1a298fd0a3aefb26e2e0da210 build break
• 03276b12b1896b05c2fd29c0417247e4d76e2aeb na
• 96f10b8c1cb83f3434bc12cf03560a6d2d2953ce user propagator
• 5e5ef50dbc02a2496bbb4611917f4a6f35db63b5 re info extension (#4659)
• a58b8ceced87178efaa53262c4c410625e7b2642 na
• db65381f3324cef4164438c8dafff099acf897fb extended calculation of info for regexes (#4656) [ #4658 ]
• 2d5b7497455359a7b431e9ef7a0c6a94bb4985de extend solver callbacks with methods
• 1e29ba76d0ad995e3e1fb5aa9450ae1505227dad renamed compl method (compl is a reserved c++ keyword) to complement
• 4dd9249a95d11e4fc42aab054d57058e3492871f trying to remove invisible control characters
• 8285162c3cbf43827dc5d1ca9b20e2f9b80e01c3 fixed type bug: bool to lbool
• 7b478c840650984af0870bbe96df9291b422af79 fixed loop lower bound bug in loop info and default nullable value in invalid_info
• 6b11af7ec678ed24b0e2270ae32d705705a7007d Merge branch 're-info-extension' of https://github.com/veanes/z3 into re-info-extension
• 3fb226dcd6feaa9cb36c56ac4366db3cef6fe61c added missing return statements, reordered def of compl to match declaration order of methods
• 1099c519ab222dca9a5e68412e6f1f6528d79e48 took care of PR comments and fixed some info calculation bugs
• 93bc1bc9834b292478379e25d5878a4d7cbccfec extended calculation of info for regexes, updated tracing of state_graph with regex info
• 080be7a2afc85a0ff8c239a05fa6ac0220547f61 merge
• 22b5daf85e8a01731145b1d97aa5688f17f4f7c1 fix rlimit for clang-10 (#4658)
• 48792581ebbce36727c9e2c8485cec479a3d2f5d took care of PR comments and fixed some info calculation bugs
• 738d091b58ff5bd47eae1f9fc7c9d831e548f7bc extended calculation of info for regexes, updated tracing of state_graph with regex info
• ecb43ccca20eeb40031995fca0f1bc190d8157e2 update smt logging format to follow SAT solver
• 77088745d05e41f2d00522abd70aa25bfce13b9d missing override specifiers per #4654
• eef05e00afe1c3696a654d82420fc7312f4f8bf7 user propagator
• ba4a218fc09cd17d4681c0e7b7048dd61b908793 user propagator fixes
• de65c61ebc3504bca6bdbe0a4a055e767577e0a1 renamed re to rex and added custom pretty printing for info (#4650)
• 79aa3457c12ece00011ecb7ae681846775ecdc01 prop
• 5aaa7e0022f125030b8cfc0e3b6eeb193562188a fix #4648
• ed258ca01902fb9ca48e9464cf32fbd56c1a7a76 approximate min-length for complements
• 4857d60c99d45865d35d277bba5b72d8d5f16445 user propagator over the API
• c50e869e5ac2a92c848616802c9d4d09d6ede73b computing and memoizing info for regexes (#4647)
• 747a8ff72a4154c5df5100a41f1bea7b9c83c8e1 initial sketch of python bindings
• 0c93c7aa08ca189f38dde19f105e81362641bb2d adding user propagation to API
• 578ddf3e9dd6dd686bc057bd1c3d2cdf776d359d na
• 152c95f72a4d0e26bd8d5f2cfaf9d34eb616cb61 adding user-propagator ability
• c13e3ce693e9a57a16d747b1fec40fd46d20b8d9 fix #4640
• df8b14d77c1cbf50412923bb356611a86ec074d9 fix #4641
• 26114845257bdff6653fe0488a989debaa044666 fix #4642
• 33d96c1a37712452ce242396be5a2c799e2511bf fix #4643
• e591b321bb4587b22171de95292177d7cca28430 set guard/cf and dynamic base in release
• f0308436b5b6df00f12aef7f54e6f35948a87f84 use lazy scopes to avoid push/pop overhead
• 558233dd8e48a2bd62d53a0bb9e8fd84ff463522 build fixes, add lazy push/pop state to avoid overhead on unused theories
• ca3ec22b7a87476c0b37a7a32c52cb48a128dbdc handle better cancellation for parallel, switch between cube mode and base level mode in smt.threads, expose parameters to control theory_bv and phase caching
• fae206b738cbbd82069f440f22b00810d5794a15 add command-line help descriptions on tactics
• c0a07f922970aa1c4c27e972f6e2885f9ca12350 tidy
• c4a03dcf7c4a2eb8d29bf9d3bb7b92277fb3b553 remove temporary comment
• 363b416473519fc5c7b51e9492c6b1ebe8b912a8 pp support for regex expressions in more-or-less standard syntax (#4638) [ #4636, #4637, #4588 ]
• 1233cb4621939cbc86af6b575102c6d12c496573 added missing const declarations that caused build failure on some platforms
• 0d9dc032d74aa5752764c17a25d55a32d53aad08 Merge branch 'regex-pp-compact' of https://github.com/veanes/z3 into regex-pp-compact
• 1567587b979b445cc2091ce32a4711a23efa54d7 fixed bug in seq_unit
• e80b143e71fba78e2cd2e940c5de65be906c56c0 updated detection of when parenthesis can be omitted to cover empty and epsilon
• ae413365e9f98af9a2e3559ff80b07056fe22581 further PR comment fixes
• 5f9a3269105601a91627efc560f8752d2e8803fc took care of comments for related PR
• 2c33bd6fafeded0c2c9dbfc8b76e1b872cc44ad1 pp support for regex expressions is more-or-less standard syntax
• bfae1c420586b545be8058927cacfe8266a51bea fixed bug in seq_unit
• 9729db16a23beffc1eede4217067f8b395e77fa7 always reduce macro expansions in model evaluation #4588
• 5b663aad7086168da889c0f35e209510f1a7ad97 updated detection of when parenthesis can be omitted to cover empty and epsilon
• be6f7bb4d7641d0feb12e0ed42b38ec6be380332 further PR comment fixes
• 094e41d21d93fff2c8098374d91d9fae468c3e80 build
• 7d391d44a29b999fda150b992f5b59de2d83a410 #4637
• 024ccf1b53d50b3804ef9d5fe38031d782af83a0 took care of comments for related PR
• a892e4793bdc384be545fd7b982389db27b0c664 typo
• 2c02264a94d2377ebf5f64162813b7e379446619 Regex solver updates (#4636)
• 3ab75bdf3bb937be8d3309c4cbf1060fa6f53972 pp support for regex expressions is more-or-less standard syntax
• 9df6c10ad87ae37c7deba1e7428496dbd5ab0022 handle small powers in theory_lra #4616
• c63ad2e834f3ca101d83556c03fe534c1888d3d9 enable ranges for bit-vectors
• 72d140334fff2d285956b8419b552d727619156a fixes for #4634
• c41abf2241deb5e1d4d23429d9b0b35a420e5cf7 fix #4624 #4633 #4632 #4631
• 84390575e2fc888e23baafa5928f191764a30497 fix #4624
• 11d5b508be5c7e2ee3d81fcd656f9784b9119d35 fix #4625
• 40455632230caa1e9b73e6fd92223b168398d7c8 fix #4626
• 5ecc59b6bc5611060b77bd76f6c632574482e956 fix #4627
• a5e4e520fb5712be29107c67304a28d83254919b fix #4628 - not really a bug, but style nit. uf1 and uf2 need both to be called
• be3c3dacb3f85124d09aa2fefed43eae35eb91a9 add bound refinement propagation
• 7fc4653e4783db45c862979154ccf383d267ef47 fix #4623
• 9f7e80c4405c3034647629aec3b90cd8a14bcde8 trace also declarations in assumptions
• 1f48eabea5cfe0ce10f7c9d319e3390cefae1eac allow Boolean arguments to bit-wise logical operators #4618
• e5693b8a981456ed77d5e539aae62327bdbaad3b added support for saving state graph in dot format (#4621)
• 3852d4516dbff75a0d00caeffc4f2f400ce7cb90 modular Axiom Profiler (#4619)
• 934f87a3366b9dc3bbde10ff185968f4c845a920 dgml output generation for regex state graphs (#4620)
• a51e40a6cd4f2f2897dbbbbac96ceda7fa07f0c1 gc perf fix
• f4ec63f39c249299eaca857bf594b568268e2a9e z3str3: add auxiliary str.substr axioms (#4617)
• 4fa2e237048503b2e65920a115738d86839cb19e overload bit-wise operators to work for Booleans for convenience #4618
• db009e28059b9bba89ef0ea771e24191fd95a4ac overload bit-wise operators to work for Booleans for convenience #4618
• 7ae706844d0bd1b47351bb1d90e8d87265f4494a revert breaking change
• 7eb05dd952a2f5de1d4be09436a97651c85dba18 ensure lengths are registered for disequality fixe #4613
• b82dff531e4ed23eb4b227366a6c1ee9e6dec299 Use Z3_ option prefix in cmake with Java bindings build command (#4612)
• 7fa5b31fe1e3fdc2b12cdbb46173b1f66b29d761 adding back dropped return statement (#4611)
• 06f34bd42bb1297af7b2461924d96b05744649b6 tidy
• 8137143adae3db2c8551a5f6bc8624778b0914a9 string to regex approximation used to strengthen membership constraints (#4610)
• fb035c063494bde126dbbd26c2007bc6ac310e1b fixed a but with insertion of a null vertex
• 566a0d540ae972ef3cf71b44348d0ca263c1b770 simplify has-fixed-length
• 97ed1cd07d732612f640f29479b0045c2bc53a1f don't rewrite empty/non-empty checking predicates
• 615e2cf37c9a8544f2b0711d89791c617f1ae817 don't rewrite empty/non-empty checking predicates
• b4f994b5c8fb319ec7fd114230ed6430d252fef6 fix loop
• 4392c03b57bb9c46afb055b1b25e73563dc8f813 better behavior on disequality and branch selection
• 02084dc95ba833ec94af8ba5ef2df132badd1fc0 misc
• 3f862cb2eeacccd75988b5c69b7dd6a2ad7d86f4 better behavior on disequality and branch selection (#4605)
• e0d46691166cc1450934bf606c3f79807e2c0589 na
• ac64a370d77d22328f1e39f5061592677a776a4d change default
• 6cfbda0f088bcfa708634e7df672fb0930046b67 remove automata references
• 976e4c91b0f151483e3cf047e294fb5e58ef7580 Integrate new regex solver (#4602)
• 293b0b8cc25400bbb37e6ab6a4bd6ce6fcfde080 fix build
• 3a26dccc8ad89d316a33c571c1f5cae7ff602add fix build
• e0a9848e018b7daec5cc21c333a6513242d1ea15 fixing build
• 69b4a819a6b216256a1ac3a518f0d4909e3b8bd4 rewrite to_int comparisons
• f6cbe3a016c1ce016a0db4272864ca9a3d67ceba propagate on variables
• 40393528370035349e9189481abde49d2f055a54 add ability to touch variables for bound propagation
• a74ef394ec98ee42daf1c69f251e036561f64ef6 some more rewrites
• 59d8895d1583496f53205ea4dc81b1b91295fbb3 add accessors for implied values to API
• 4628cb8e794521ed37b49ce7177a1cb34f496a06 check for negation, not complement
• 42b42dd89ac6ecdc02d943fb686d52428e98b409 use bounded pp for cubes
• f7b2407a118ae50086c7f50ae5d190e31a672ac5 for #4588
• 8857a67e4f15607f0dc6f2311d62dae48ab55ec5 fix model return after shutdown, reported in #4532
• b71a64365d78618ae64083a99af2d1d6b90993d2 sketch fixed-length heuristic
• 5664b570a33785f8b3b87d7646a06f274d4c319e Seq rewriter integration (#4599)
• afdfc5e8a60e2ee3cde83d78132773ff894f0258 z3str3: fix incorrect automaton polarity in intersection check, and clean up code (#4595)
• 6910c0d5ebb000e1975ca53850dc70d0c4311aaa Revert "Seq rewriter integration (#4597)" (#4598)
• e90f01006c176b981f9c77f8cb00f9f278e895d1 Seq rewriter integration (#4597)
• 2fb914d2a20a4ade2a4c8f7b71e5d0c5f67eb583 z3str3: construct correct counterexamples for string-integer in model construction (#4562)
• d591bf62c1f3c719912daf557898fb262aedf146 add to readme #4575
• 9624df942f2300c59639cc7cce7322b1a16fd226 na
• a08082e392a344839af5600753da5632c23c437d fix #4594
• ae502bc2c42d1be9fc582b366dcd3235ec62a13b simplify a few of the several axiom trace commands
• c7704ef9af37ffaf619311ea827bbcc00795fee8 pass algebraic manager to arith-plugin mk-numeral because rational check may overwrite the argument using the current manager deals with crash as part of #4532
• ac39ddb43fd6a7126cdae85585ee94d7f5d81626 flush gmc for sat-preprocessor model bug #4532
• e8ef9a85a4681ee82f53d838e03bfb0f012f83c9 fix #4327
• 4be6927460626f46df937d152657b27baca56581 unused variable warning
• 78afa2527cf22fcbaf122b0d8e2572f07cef581c unused variable warning
• 4d586c2c13b1a7af9c77c15c774c832cfe6edae0 remove stale references to gac/csc
• 105f97d3eeadf17fab6e77835ed77734eba37354 #4582 again
• 2133ba06a7ac71e5121e68bcd55fc6583fc19555 prepare for theory variables othe rthan seq/re
• f789573d1264def464b37ddf69a674c42adbc12a prepare for alternative axiom
• 2d4839f89e9848b6dc305d5336f47c618692f141 #4582 again
• 1059f6d3b8a37c7d55ddec780e7b540e3367d039 #4582 again
• 963daab268cdbe61c26eb47db743904329f9e606 #4582 again
• e63992c8bd99ce0fbc1c76575646387f8411c216 fix #4589
• 780346c7ca86a6f8ab9ac6fe4ecb032cc8b5c52b address model generation bugs raised in #4518 and #4324
• e1d2b88a82e150ae2f4edda3fd5546de6d251e4f access polynomial expressions from algebraic numerals
• a6a041ec5db6b1566985bf3c72dd20b78092ae1d setting defaults in AUFLIRA and AUFLIA to conservative ite-lifting. Fixing conservative setting to be after constructor in asserted_formulas. fixes #4586
• 71a32f5bb2db4b124dd785473d74ebd48346441c remove unused
• 45855fce06e12e8ad09af99547e8ff081099bbfe fix
• dd5e2e8930fc1b91c4faa850168d5d7763bdd34b check for 0
• 640cf1809d9c5b30522fe0506abc5cb13becb5a4 Merge pull request #4585 from iscottb122/dotnet_fp_significand [ #4584 ]
• b6867d69c2d985cf09ea87451dc4bf66e347157c Return significand bits correctly (dotnet API). Fixes #4584
• ed58175e1b9f7f2e44bfbf5bed503551c435cc85 issue #4582
• aab50ff3f53da7315548e9fb59dbb913573442c1 fixing bugs reported in #4518
• b1824fea1042e37f701bf9f778ce060ff9019234 fix lifetimes for crashes in #4525
• f17ead21f92ca2c48b4e8478cb752ecfca5da78e fix #4578
• 1d8d85add9e1f9b9478fab3194e82c2f0d77df44 fix #4575 - correction set resolution only works with uniform weights
• ebce0b3612664fe34a13bed9d1db8f1a4c41afb9 fix #4577

This list of changes was auto generated.