Commit Graph

Select branches

Hide Pull Requests

17

18-sustained

18.0

18.1

18.2

19-sustained

19.0

19.1

19.2

20-sustained

20.0

20.1

20.2

21-sustained

21.0

21.1

21.2

22-sustained

22.0

22.1

22.2

23.0

23.1

23.2

24-sustained

24.0

24.1

24.2

25.0

25.1

a2c2-2020

contrib

dependabot/github_actions/docker/build-push-action-4.0.0

gpl-2016

gpl-2017

gpl-2018

lts-18

lts-19

lts-20

lts-21

master

ms-4.8.4

ms-4.8.5

ms-4.8.6

ms-4.8.8

ms-master

ms-z3-4.11.2

ms-z3-4.8.11

ms-z3-4.8.12

ms-z3-4.8.15

pure

qsat

spark-16.0

temp_duality_branch

unstable

#1

#2

#3

#4

#4

known-pure

z3-4.1.1

z3-4.3.0

z3-4.3.1

z3-4.3.2

z3-4.4.0

Mono Color

• 24563ee6bd Merge branch 'topic/kanig-1153-z3-4154' into 'master' master Johannes Kanig 2026-01-08 08:57:46 +00:00
• f1ba69ca2c Merging z3 4.15.4 into AdaCore master Johannes Kanig 2026-01-08 11:27:00 +09:00
• 745087e237 update release notes Nikolaj Bjorner 2025-10-29 07:39:33 -07:00
• c88295a7c7 fix C++ example and add polymorphic interface for C++ Nikolaj Bjorner 2025-10-29 03:08:49 -07:00
• 6efffa0054 renemable Centos AMD nightly Nikolaj Bjorner 2025-10-28 18:55:36 -07:00
• 1b9a636910 fix build break introduced when adding support for polymorphic datatypes Nikolaj Bjorner 2025-10-28 18:54:35 -07:00
• 88fcc05d6c Bump actions/upload-artifact from 4 to 5 (#7998) dependabot[bot] 2025-10-28 15:47:26 -07:00
• 488c712f5b Bump actions/download-artifact from 5 to 6 (#7999) dependabot[bot] 2025-10-28 15:47:15 -07:00
• 3570073c29 Add missing mkLastIndexOf method and CharSort case to Java API (#8002) Copilot 2025-10-28 15:46:48 -07:00
• b6e3a68839 update centos version Nikolaj Bjorner 2025-10-28 15:13:30 -07:00
• 766eaa3376 disable centos build until resolved Nikolaj Bjorner 2025-10-20 08:33:01 +02:00
• efd5d04af5 enable always add all coeffs in nlsat Lev Nachmanson 2025-10-24 17:47:16 -07:00
• 887ecc0c98 throttle grobner method more actively Lev Nachmanson 2025-10-22 21:36:22 -07:00
• 58e64ea826 try exponential delay in grobner Lev Nachmanson 2025-10-22 17:00:16 -07:00
• 2bf1cc7d61 Enabling Control Flow Guard (CFG) by default for MSVC on Windows, with options to disable CFG. (#7988) hwisungi 2025-10-22 05:18:25 -07:00
• 68a7d1e1b1 Bump actions/setup-node from 5 to 6 (#7994) dependabot[bot] 2025-10-21 21:17:35 +02:00
• 9a2867aeb7 Add a fast-path to _coerce_exprs. (#7995) Nelson Elhage 2025-10-21 12:16:54 -07:00
• 06ed96dbda add the "noexcept" keyword to value_score=(value_score&&) declaration Lev Nachmanson 2025-10-20 11:53:34 -07:00
• f2e7abbdc1 disable manylinux until segfault is resolved Nikolaj Bjorner 2025-10-20 08:28:08 +02:00
• aaaa32b4a0 build fixes Nikolaj Bjorner 2025-10-19 20:55:45 +02:00
• d65c0fbcd6 add explicit constructors for nightly mac build failure Nikolaj Bjorner 2025-10-19 20:14:20 +02:00
• fcc7e02167 Update arith_rewriter.cpp Nikolaj Bjorner 2025-10-18 13:32:49 +02:00
• 62ee7ccf65 Revert "Add finite_set_value_factory for creating finite set values in model …" (#7985) Nikolaj Bjorner 2025-10-16 13:18:35 +02:00
• 05ffc0a77b Add finite_set_value_factory for creating finite set values in model generation (#7981) Copilot 2025-10-16 13:16:54 +02:00
• a179286183 restore the method behavior Lev Nachmanson 2025-10-15 16:41:32 -07:00
• 1921260c42 restore single cell Lev Nachmanson 2025-10-14 17:43:48 -07:00
• 3b565bb284 trim parametric datatype test Nikolaj Bjorner 2025-10-15 21:39:39 +02:00
• 5163411f9b Update Z3_mk_datatype_sort API to accept array of sort parameters and add Z3_mk_polymorphic_datatype (#7966) Copilot 2025-10-15 20:51:21 +02:00
• e669fbe557 Bump github/codeql-action from 3 to 4 (#7971) dependabot[bot] 2025-10-14 18:08:27 +02:00
• 641741f3a8 parameter eval order Lev Nachmanson 2025-10-07 10:30:58 -07:00
• 8af9a20e01 parameter eval order Lev Nachmanson 2025-10-07 10:26:40 -07:00
• 6a9520bdc2 parameter eval order Lev Nachmanson 2025-10-07 10:21:09 -07:00
• 8ccf4cd8f7 parameter eval order Lev Nachmanson 2025-10-07 10:19:24 -07:00
• 40b980079b parameter eval order Lev Nachmanson 2025-10-07 10:14:02 -07:00
• a41549eee6 parameter eval order Lev Nachmanson 2025-10-07 10:06:43 -07:00
• 2b3068d85f parameter eval order Lev Nachmanson 2025-10-07 09:17:12 -07:00
• 3a2bbf4802 param eval order Lev Nachmanson 2025-10-07 09:13:21 -07:00
• 6e52b9584c param eval Lev Nachmanson 2025-10-07 09:04:24 -07:00
• 93ff8c76db parameter evaluation order Lev Nachmanson 2025-10-07 08:53:49 -07:00
• 00f1e6af7e parameter eval order Lev Nachmanson 2025-10-07 08:40:24 -07:00
• c154b9df90 param order evaluation Lev Nachmanson 2025-10-07 08:34:56 -07:00
• 77c70bf812 param order Lev Nachmanson 2025-10-06 15:51:53 -07:00
• 63bb367a10 param order Lev Nachmanson 2025-10-06 15:44:41 -07:00
• e9a2766e6c remove AI slop Nikolaj Bjorner 2025-10-06 13:53:24 -07:00
• 5a9663247b fix the order of parameter evaluation Lev Nachmanson 2025-10-06 13:42:38 -07:00
• 5ae858f66b fixing the order Lev Nachmanson 2025-10-06 13:35:37 -07:00
• aa5645b54b fixing the order Lev Nachmanson 2025-10-06 13:22:18 -07:00
• 542e015550 Remove unused variable 'first' in mpz.cpp Nikolaj Bjorner 2025-10-06 13:39:27 -07:00
• cd1ceb6efe [WIP] Add a mutex to warning.cpp to ensure that warning messages from different threads don't interfere (#7963) Copilot 2025-10-06 13:38:18 -07:00
• 3ce8aca411 Bump actions/checkout from 4 to 5 (#7954) dependabot[bot] 2025-10-04 01:22:52 -07:00
• c8bdbd2dc4 remove directory Nikolaj Bjorner 2025-10-03 11:58:57 -07:00
• e137aaa249 add user propagators to opt_solver Nikolaj Bjorner 2025-10-02 19:44:22 -07:00
• 0e6b3a922a Add commands for forcing preferences during search Nikolaj Bjorner 2025-10-02 10:47:10 -07:00
• 5d8fcaa3ee update clang format Nikolaj Bjorner 2025-10-02 10:39:37 -07:00
• 72c89e1a4e fix #7952 - make auto-selector detect large bit-vectors so it does't use the datalog engine for hopelessly large tables Nikolaj Bjorner 2025-09-30 15:58:48 -07:00
• 0881a71ed2 update format Nikolaj Bjorner 2025-09-30 15:42:01 -07:00
• 65c9a18c3a fix #7956 Nikolaj Bjorner 2025-09-30 15:41:40 -07:00
• 339f0cd5f9 Correctly distinguish between Lambda and Quantifier in Z3 Java API (#7955) Ruijie Fang 2025-09-30 11:55:14 -05:00
• 253a7245d0 add analysis Nikolaj Bjorner 2025-09-28 13:05:04 +03:00
• b5f79da76a add analysis Nikolaj Bjorner 2025-09-28 13:03:31 +03:00
• ae55b6fa1e add analysis Nikolaj Bjorner 2025-09-28 13:02:05 +03:00
• bda98d8da4 fix #7948 Nikolaj Bjorner 2025-09-28 12:45:42 +03:00
• b7eb21efed fix #7948 Nikolaj Bjorner 2025-09-28 12:44:56 +03:00
• 391880b6fc Add missing ::z3::sdiv to z3++.h (#7947) Wael Boutglay 2025-09-25 21:04:15 +02:00
• 6173a0d025 propagate value initialization to atoms Nikolaj Bjorner 2025-09-24 11:01:24 +03:00
• eae4de075b fix latent bug in factorization Nikolaj Bjorner 2025-09-23 10:47:24 +03:00
• 04ddade2dd remove stale comment Nikolaj Bjorner 2025-09-22 04:43:41 +03:00
• f5c28a0b76 household cleanup Nikolaj Bjorner 2025-09-22 03:58:04 +03:00
• e26f7b900c fix unsound axiom for lower-bounding Nikolaj Bjorner 2025-09-21 19:23:55 +03:00
• dcdae5a61c add smt debug output for nla_core Nikolaj Bjorner 2025-09-21 19:23:42 +03:00
• ce53e06e29 Par (#7945) Nikolaj Bjorner 2025-09-21 10:11:04 +03:00
• 2b5b985492 fix divergence regression Nikolaj Bjorner 2025-09-20 02:18:44 -07:00
• 9876e85a45 turn on max of sums transformation Nikolaj Bjorner 2025-09-20 00:55:37 -07:00
• 3256d1cc8b fix bug in unit test Nikolaj Bjorner 2025-09-20 00:44:49 -07:00
• 0e8648c7d7 fix compile of lp.cpp Nikolaj Bjorner 2025-09-20 00:33:23 -07:00
• a8ae52bfbf fix missing call change to cross-nested. Prepare for lower-bound and upper-bound cardinality constraints Nikolaj Bjorner 2025-09-19 18:57:50 -07:00
• 2517b5a40a port improvements from ilana branch to master regarding nla Nikolaj Bjorner 2025-09-19 12:28:20 -07:00
• 5d91294e90 update workflows Don Syme 2025-09-19 03:31:56 +01:00
• 59bd1cf4a0 updated clang format Nikolaj Bjorner 2025-09-18 15:13:20 -07:00
• b17df988ed Daily Test Coverage Improver: Add comprehensive API special relations tests (#7925) Don Syme 2025-09-18 17:20:14 +01:00
• 3fa34952f0 Daily Backlog Burner: Fix bad .dylib versioning in pip packages (#7914) Don Syme 2025-09-18 16:55:56 +01:00
• c43cb18e63 better rewriting Lev Nachmanson 2025-09-18 08:08:32 -07:00
• 37904b9e85 fix the parameter evaluation order Lev Nachmanson 2025-09-18 07:52:13 -07:00
• cda0a922b9 Daily Test Coverage Improver: Add comprehensive API polynomial tests (#7905) Don Syme 2025-09-18 04:47:22 +01:00
• 82ab6741a0 Daily Test Coverage Improver: Add comprehensive API pseudo-boolean constraint tests (#7898) Don Syme 2025-09-18 04:45:43 +01:00
• 222c64fa6f Remove Windows-only guard from hashtable unit tests (#7901) Don Syme 2025-09-18 04:23:01 +01:00
• 635d3b7017 Add .clang-format file for C++ code formatting (#7904) Don Syme 2025-09-18 04:22:27 +01:00
• 1b058f23e9 Daily Backlog Burner: Add include directory for easier Z3 integration (#7907) Don Syme 2025-09-18 04:21:56 +01:00
• 4e1a9d1ef7 Daily Test Coverage Improver: Add comprehensive API Datalog tests (#7921) Don Syme 2025-09-18 04:07:24 +01:00
• 7cb491dd6a update compiled workflows Don Syme 2025-09-17 23:49:55 +01:00
• d989bcaebe update compiled workflows Don Syme 2025-09-17 23:47:16 +01:00
• f300dfc425 recompile improvers Don Syme 2025-09-17 16:41:49 +01:00
• 2d0b9e6972 recompile improvers Don Syme 2025-09-17 15:50:33 +01:00
• aabdb407d1 latest improvers Don Syme 2025-09-17 13:49:00 +01:00
• 2364ea42ba update improvers Don Syme 2025-09-17 13:19:24 +01:00
• 7268136bb6 update workflows Don Syme 2025-09-17 11:33:24 +01:00
• db8206d265 improve improvers Don Syme 2025-09-17 11:03:23 +01:00
• 5b70f75d89 allow burner to create PRs Don Syme 2025-09-17 02:41:38 +01:00
• 81da4be228 backlog burner Don Syme 2025-09-17 02:20:48 +01:00
• ba4c9238c0 add daily backlog burner Don Syme 2025-09-17 02:03:48 +01:00