3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00

Commit graph

  • 9e0aa272a8
    Merge 9a0272528a into 76cceddb73 davedets 2026-06-18 19:45:09 -07:00
  • 9a0272528a Fix more inadvertent formatting changes. David Detlefs 2026-06-18 19:40:53 -07:00
  • d6d0d4e45a Fix inadvertent formatting changes. David Detlefs 2026-06-18 19:36:55 -07:00
  • 4bc4a9afae Want to push, got message saying remote is ahead. David Detlefs 2026-06-18 19:25:36 -07:00
  • 554a2cedab
    Merge branch 'Z3Prover:master' into master davedets 2026-06-18 19:24:37 -07:00
  • 75b81900d5 Fix "missing field initializer" warnings. David Detlefs 2026-06-18 19:22:05 -07:00
  • 76cceddb73
    Bump github/gh-aw-actions from 0.79.6 to 0.80.4 (#9902) master dependabot[bot] 2026-06-18 17:42:08 -06:00
  • 8409c27a11
    Bump actions/checkout from 6 to 7 (#9901) dependabot[bot] 2026-06-18 17:41:52 -06:00
  • a75c860899 lp: randomize the Gomory-cut gate to break period resonance lia_w Lev Nachmanson 2026-06-18 16:10:55 -07:00
  • 4196bca61d
    Merge a61693c129 into d9385e9713 Can Cebeci 2026-06-18 16:09:08 -07:00
  • a61693c129 Prevent special treatment of non-recursive siblings Can Cebeci 2026-06-18 15:55:32 -07:00
  • 262fe71e4e
    Bump github/gh-aw-actions from 0.79.6 to 0.80.4 dependabot[bot] 2026-06-18 22:13:34 +00:00
  • 5d3749662b
    Bump actions/checkout from 6 to 7 dependabot[bot] 2026-06-18 22:13:20 +00:00
  • c0888b9ecd debug qi term_enumeration Nikolaj Bjorner 2026-06-18 14:46:04 -07:00
  • 8f67109678
    Merge a90901b7c5 into d9385e9713 Nikolaj Bjorner 2026-06-18 20:01:22 +00:00
  • a90901b7c5
    Replace inline depth_guard struct with on_scope_exit in datatype_factory.cpp fix-benchmark-crashes copilot-swe-agent[bot] 2026-06-18 20:01:17 +00:00
  • d9385e9713 extend cases for process_formulas_on_stack Nikolaj Bjorner 2026-06-18 12:45:45 -07:00
  • 097372c779
    Merge branch 'master' into fix-benchmark-crashes Nikolaj Bjorner 2026-06-18 13:43:54 -06:00
  • 728ac39a59 flexible handling with quantifiers Nikolaj Bjorner 2026-06-18 12:43:27 -07:00
  • a3fb5058c6
    Merge branch 'master' into fix-benchmark-crashes Nikolaj Bjorner 2026-06-18 13:40:23 -06:00
  • 225ac56f5a extend cases for process_formulas_on_stack Nikolaj Bjorner 2026-06-18 12:39:39 -07:00
  • 99a8a922ec
    Use "override" keyword where needed. (#9892) davedets 2026-06-18 12:36:14 -07:00
  • 0f84ede6c1
    Merge f8ba42c5c4 into 3bf4d2b53d Copilot 2026-06-18 19:24:48 +00:00
  • f8ba42c5c4
    Clarify BV SMT2 regression assertion copilot/unsoundness-issue-gmp copilot-swe-agent[bot] 2026-06-18 19:24:44 +00:00
  • 4b32bab0ac Fix model generation bugs causing crashes in QF_ABV, UFBVLIA, and UFDT benchmarks Nikolaj Bjorner 2026-06-18 12:23:42 -07:00
  • 586a6b893d
    Fix GMP mod2k sign bug and add BV regression test copilot-swe-agent[bot] 2026-06-18 19:23:29 +00:00
  • 35fea6f4d3 lp: expose integer cut/cube period as lp.cut_period parameter Lev Nachmanson 2026-06-18 12:23:10 -07:00
  • 1d8fdbe3f2
    Merge a37003fa2d into 3bf4d2b53d Lev Nachmanson 2026-06-18 21:14:55 +02:00
  • af2d579a3f
    Merge e503ead008 into 3bf4d2b53d Copilot 2026-06-18 21:14:55 +02:00
  • 94212ca603
    Merge 1feb610daa into 3bf4d2b53d Clemens Eisenhofer 2026-06-18 21:14:55 +02:00
  • e615291680
    Merge 362c041502 into 3bf4d2b53d Nikolaj Bjorner 2026-06-18 21:14:55 +02:00
  • 3bf4d2b53d
    python: build a PyPI-publishable Pyodide (PEP 783) wheel (#9891) Alcides Fonseca 2026-06-18 20:05:03 +01:00
  • 531fd994de
    Initial plan copilot-swe-agent[bot] 2026-06-18 19:00:52 +00:00
  • b1d4f36c85 Merge branch 'master' of https://github.com/z3prover/z3 Nikolaj Bjorner 2026-06-18 11:07:49 -07:00
  • 8e6ed26fc2 integrate size measure for cost and avoid duplicates Nikolaj Bjorner 2026-06-18 10:16:54 -06:00
  • 8cb5f32ef7 Some of the overrides are only in debug builds; handle this. David Detlefs 2026-06-18 09:16:25 -07:00
  • 41471bbc3e add comment solver_parallel Nikolaj Bjorner 2026-06-17 17:44:54 -06:00
  • f2e6d05c56 disable hoisting ite over union derive Nikolaj Bjorner 2026-06-17 16:26:38 -06:00
  • 222a5a467b
    Fix MacOS CMake build: guard override with #ifdef Z3DEBUG in static_matrix.h, add clang warnings copilot/fix-macos-build-cmake copilot-swe-agent[bot] 2026-06-17 18:12:28 +00:00
  • 17b85cbe20
    Initial plan copilot-swe-agent[bot] 2026-06-17 18:04:16 +00:00
  • 29489c3bd8 make concatentation right associative Nikolaj Bjorner 2026-06-17 12:00:08 -06:00
  • e011aead11 perf Nikolaj Bjorner 2026-06-17 10:06:43 -06:00
  • f261c7732b fix perf Nikolaj Bjorner 2026-06-17 10:03:52 -06:00
  • 05c394aa6c bug fixes Nikolaj Bjorner 2026-06-17 09:39:08 -06:00
  • abaa46aa88 Oops: wasn't including compiler_warnings because I wasn't doing git add from base directory. David Detlefs 2026-06-17 08:37:23 -07:00
  • 360bad9a35 Remove tabs in macro; for some reason changes in compiler_warnings wasn't included. David Detlefs 2026-06-17 08:33:55 -07:00
  • 7ce5b687fa Fix "override"-related warnings. David Detlefs 2026-06-17 08:29:36 -07:00
  • 26feb16714 fix bugs Nikolaj Bjorner 2026-06-17 09:14:16 -06:00
  • 78818f9ae1 python: build a PyPI-publishable Pyodide (PEP 783) wheel Alcides Fonseca 2026-06-17 12:36:27 +01:00
  • b5a3d4fcb0 clean up but dangerous race condition is still present in the worker. an example: 1. Manager decides worker’s lease is stale. 2. It records/sends lease cancel. 3. Worker finishes naturally before observing 4. Worker releases/discards old lease. 5. The lease-cancel counter is still sitting on the worker limit. 6. Later, a naked m.inc() check sees that stale cancel and treats it as global cancellation. Ilana Shapiro 2026-06-16 21:50:52 -07:00
  • e88cac2fe1 restore smt_parallel to old/original version so we have a consistent baseline (even though it still includes newer bugs we've identified) Ilana Shapiro 2026-06-16 21:37:11 -07:00
  • 5c8cbaea3a Handle cancellation for parallel leases Ilana Shapiro 2026-06-16 20:15:10 -07:00
  • c10e7c2a6f attempt at lease policy patch Ilana Shapiro 2026-06-15 23:14:53 -07:00
  • 3a470de4ff
    Merge branch 'Z3Prover:master' into master davedets 2026-06-16 15:59:01 -07:00
  • 9091df56cb
    Fix instance of "flexible array member". (#9883) Nightly davedets 2026-06-16 15:09:18 -07:00
  • 0a3b87900c
    goal2sat: skip caching single-ref nodes without refcount perturbation copilot/fix-regression-test-failures copilot-swe-agent[bot] 2026-06-16 20:58:35 +00:00
  • 8eff8eb119 Fix "flexible array members" warning. David Detlefs 2026-06-16 13:42:46 -07:00
  • 56677318f9
    Merge branch 'Z3Prover:master' into master davedets 2026-06-16 13:36:46 -07:00
  • 4ffb324ed9
    Fix cache function to handle reference count check Nikolaj Bjorner 2026-06-16 14:16:14 -06:00
  • bcc3523b23
    Update seq_rewriter.cpp Nikolaj Bjorner 2026-06-16 14:14:49 -06:00
  • 69dc7cab01
    Update goal2sat.cpp Nikolaj Bjorner 2026-06-16 14:06:43 -06:00
  • 1d9c770d74
    Fix reference to recfun::util in lia2card_tactic.cpp Nikolaj Bjorner 2026-06-16 14:02:24 -06:00
  • 8c2a425e4b
    Smart constructors for regex ranges: canonical form at construction time (#9814) Copilot 2026-06-16 13:58:56 -06:00
  • 790e315387
    Merge branch 'master' into copilot/smart-constructors-regex-ranges Nikolaj Bjorner 2026-06-16 13:58:40 -06:00
  • 45da93d14b
    Merge branch 'Z3Prover:master' into master davedets 2026-06-16 11:57:15 -07:00
  • f4cdcce434
    Merge branch 'master' into goal2sat-skip-single-ref-cache Nikolaj Bjorner 2026-06-16 11:10:27 -07:00
  • 897c4475af
    goal2sat: drop unsafe ref_count≤1 cache-skip optimization; keep bit_blaster mk_eq improvement (#9882) Copilot 2026-06-16 12:09:20 -06:00
  • 0d4e5a7d5a
    fix: use resize instead of reserve in bit_blaster mk_eq for clarity copilot-swe-agent[bot] 2026-06-16 18:04:25 +00:00
  • b6f7a70a39
    fix: keep only bit_blaster mk_eq optimization from PR #9872 copilot-swe-agent[bot] 2026-06-16 18:02:42 +00:00
  • 9461368931
    Merge branch 'Z3Prover:master' into master davedets 2026-06-16 11:01:02 -07:00
  • ec7462024a
    Strengthen historical nlsat regression tests (#9857) Peter Chen J. 2026-06-17 01:36:13 +08:00
  • 3d691fe234
    Add versioned shared object names in Bazel rules (#9838) Shantanu Gontia 2026-06-16 23:05:21 +05:30
  • d457f9f5d3
    Bump markdown-it from 14.1.0 to 14.2.0 in /src/api/js (#9881) dependabot[bot] 2026-06-16 11:34:20 -06:00
  • 0270817b31 block lia2card on recursive functions Nikolaj Bjorner 2026-06-16 11:25:14 -06:00
  • bd4c12f821
    Bump markdown-it from 14.1.0 to 14.2.0 in /src/api/js dependabot[bot] 2026-06-16 17:17:32 +00:00
  • 66795ea322
    ci: validate Microsoft.Z3.dll PE Machine field is AnyCPU in nightly build validation (#9873) Copilot 2026-06-16 11:16:19 -06:00
  • b6c7ef2f68
    dotnet: force PlatformTarget=AnyCPU to fix arm64 host load failure (#9868) Copilot 2026-06-16 09:52:04 -06:00
  • c48a4aa56a
    Remove redundant check for reference count in cache Nikolaj Bjorner 2026-06-16 09:35:51 -06:00
  • eb775b2206
    Update bit_blaster_tpl_def.h Nikolaj Bjorner 2026-06-16 09:34:25 -06:00
  • ff2e0a3ab0
    Remove a few unneeded constructors (#9879) Nuno Lopes 2026-06-16 14:55:59 +01:00
  • 86de0cbd71
    Eliminate unused private fields and local variables. (#9875) davedets 2026-06-16 06:55:18 -07:00
  • 3fed9eadae remove a few more useless constructors Nuno Lopes 2026-06-16 12:18:04 +01:00
  • 82777c0092 fix #9815 properly Nuno Lopes 2026-06-16 10:00:45 +01:00
  • 108f302716
    Merge ab523fce54 into c67bb140dc Nikolaj Bjorner 2026-06-16 07:07:07 +00:00
  • ab523fce54 attempt at lease policy patch Ilana Shapiro 2026-06-15 23:14:53 -07:00
  • bf1755363c Merge branch 'derive-with-ranges' of https://github.com/z3prover/z3 into derive-with-ranges derive-with-ranges Margus Veanes 2026-06-15 23:00:42 -06:00
  • 61ba424ae6 misc edits of work in progress Margus Veanes 2026-06-15 23:00:25 -06:00
  • fc5e4d7557 check for lease expiration before checking for m.inc() Nikolaj Bjorner 2026-06-15 16:00:26 -06:00
  • 639530f42a Remove unused private fields and local vars. David Detlefs 2026-06-15 13:46:51 -07:00
  • b96f61654e
    Merge branch 'Z3Prover:master' into master davedets 2026-06-15 13:38:38 -07:00
  • 48ae786c4c catch exceptions from cube and backbone calls. They can throw Nikolaj Bjorner 2026-06-15 14:02:43 -06:00
  • e508cf3d8b Merge branch 'master' of https://github.com/z3prover/z3 Nikolaj Bjorner 2026-06-15 11:19:23 -07:00
  • 0648a8be97
    Add validate-dotnet-anycpu job to nightly-validation workflow (issue #9863) copilot-swe-agent[bot] 2026-06-15 18:11:56 +00:00
  • cc0cc84177
    Initial plan copilot-swe-agent[bot] 2026-06-15 18:08:39 +00:00
  • c67bb140dc
    Treat each transition-regex leaf as a single bisimulation state (#9871) Margus Veanes 2026-06-15 10:59:41 -07:00
  • 2b9b9a9623 log exceptions Nikolaj Bjorner 2026-06-15 10:28:52 -07:00
  • 622977814c fix(seq_regex_bisim): treat each transition-regex leaf as a single state Margus Veanes 2026-06-15 10:28:18 -07:00
  • 4237f9d86b log exceptions Nikolaj Bjorner 2026-06-15 10:03:46 -07:00
  • 969828b701 goal2sat: skip caching singly-referenced AST nodes Yusen Su 2024-09-23 00:12:46 -04:00
  • 178879e184
    Fix .NET wrapper PE Machine field: add PlatformTarget AnyCPU to prevent x64-only DLL copilot-swe-agent[bot] 2026-06-15 14:35:23 +00:00