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

Commit graph

  • 1a49d5288e
    Merge 4cb997c128 into 82a0d42970 Lev Nachmanson 2026-07-14 11:52:04 -07:00
  • 82a0d42970
    Improve hash mixing to eliminate bitvector-expression hash-table clustering (#10120) master Copilot 2026-07-14 11:51:49 -07:00
  • 76c3f405a7
    Merge 9264c9cc26 into c4cb5bbc15 Nikolaj Bjorner 2026-07-14 11:28:03 -07:00
  • c4cb5bbc15 update release.yml and tptp_frontend Nikolaj Bjorner 2026-07-14 11:16:47 -07:00
  • e2b9e3a6dc distribute quantifiers over Booleans Nikolaj Bjorner 2026-07-14 09:56:43 -07:00
  • 46b1c68f59
    Update nightly.yml Nightly Nikolaj Bjorner 2026-07-14 09:34:29 -07:00
  • 8f2713bdb1 Add array eta-reduction rewrite: (lambda (x*) (select a x*)) -> a Nikolaj Bjorner 2026-07-14 09:24:16 -07:00
  • 43ab391dbe
    Initial plan copilot/fix-z3py-spacer-crash copilot-swe-agent[bot] 2026-07-14 15:32:56 +00:00
  • 25e0e6f780
    fix(bazel): pin CMake library installs to lib (#10126) Simon Scatton 2026-07-14 17:30:48 +02:00
  • 98c8f2935e
    Nightly: prevent test.PyPI publish failure by rewriting unsupported macOS wheel tags (#10122) Copilot 2026-07-14 08:21:20 -07:00
  • 3df60813cd
    Nightly: clarify TestPyPI tag rewrite comment copilot-swe-agent[bot] 2026-07-14 14:58:10 +00:00
  • aa0b9ae02e
    Nightly: rewrite unsupported macOS wheel tags for test.PyPI copilot-swe-agent[bot] 2026-07-14 14:57:07 +00:00
  • 048de2605b fix(bazel): pin CMake library installs to lib Simon Scatton 2026-07-14 15:32:58 +02:00
  • 9aafc8714f
    Merge f00cf75ce2 into eae0530675 Copilot 2026-07-14 16:54:06 +09:00
  • b1053aa7a7
    Polish nightly test.PyPI workflow comment per review copilot-swe-agent[bot] 2026-07-14 03:19:26 +00:00
  • 4f4176d0c7
    Skip macOS wheels when publishing nightly artifacts to test.PyPI copilot-swe-agent[bot] 2026-07-14 03:18:15 +00:00
  • b87c6cf600
    Initial plan copilot-swe-agent[bot] 2026-07-14 02:56:59 +00:00
  • 00e5bf0b81
    Extend hash regression test with old/new quality comparison copilot-swe-agent[bot] 2026-07-14 02:16:59 +00:00
  • 4f6c7220ce
    Add unit-test comparison of old/new combine_hash behavior copilot-swe-agent[bot] 2026-07-14 02:14:41 +00:00
  • eae0530675 update version to 4.17.1 Nikolaj Bjorner 2026-07-13 18:56:19 -07:00
  • 627e19197c
    Update RELEASE_NOTES.md for v4.17.0 (PRs #9798–#10116) (#10121) Copilot 2026-07-13 18:43:58 -07:00
  • 55a5af1f93
    Add regression coverage for low-bit hash dispersion copilot-swe-agent[bot] 2026-07-14 01:42:41 +00:00
  • 0452362e9f
    Improve hash combining to avoid bitvector hash-table cliff copilot-swe-agent[bot] 2026-07-14 01:40:11 +00:00
  • eddbc43f03
    Initial plan copilot-swe-agent[bot] 2026-07-14 00:57:34 +00:00
  • 5c0443591d
    Align release macOS build targets with nightly’s 13.3 settings (#10118) Copilot 2026-07-13 17:51:57 -07:00
  • 9264c9cc26 Add symbolic-modulus congruence rule to nla_divisions quot-rem-lemmas Nikolaj Bjorner 2026-07-13 17:46:39 -07:00
  • cb3ff6e74f
    fix: align release macOS target with nightly copilot-swe-agent[bot] 2026-07-14 00:42:57 +00:00
  • 11a55c2f61
    Initial plan copilot-swe-agent[bot] 2026-07-14 00:40:26 +00:00
  • 72ee14f6d2
    Update RELEASE_NOTES.md with version 4.17.0 changes from discussion #10117 copilot-swe-agent[bot] 2026-07-14 00:34:17 +00:00
  • 26ad30bb76
    Fix invalid sequence models for seq.foldl results observed through seq.nth (#10111) Copilot 2026-07-13 17:33:39 -07:00
  • 424bcc545e
    Fix release-notes-updater: add copilot-requests: write permission (#10116) Copilot 2026-07-13 17:13:31 -07:00
  • cb693fd936
    Fix release-notes-updater: add copilot-requests: write permission for Copilot API auth copilot-swe-agent[bot] 2026-07-14 00:09:17 +00:00
  • 849c117091
    Initial plan copilot-swe-agent[bot] 2026-07-14 00:02:24 +00:00
  • 4cb997c128 lp: avoid heap allocation when relocating coefficients in static_matrix::remove_element Lev Nachmanson 2026-07-13 09:39:07 -07:00
  • aaaae5b4c2
    Polish foldl foldli regression test copilot-swe-agent[bot] 2026-07-13 21:43:06 +00:00
  • 2b5091dfff
    Parse fold regression results by line copilot-swe-agent[bot] 2026-07-13 21:42:29 +00:00
  • b7ff37565f
    Tighten fold regression test checks copilot-swe-agent[bot] 2026-07-13 21:41:47 +00:00
  • 8e742d2639
    Place foldl regression test at top level copilot-swe-agent[bot] 2026-07-13 21:41:07 +00:00
  • 500b756911
    Move foldl regression test invocation copilot-swe-agent[bot] 2026-07-13 21:40:20 +00:00
  • bc9d35567f
    Guard seq length propagation for foldl copilot-swe-agent[bot] 2026-07-13 21:39:40 +00:00
  • c75a034739
    Hoist seq length rewrite out of loop copilot-swe-agent[bot] 2026-07-13 20:23:15 +00:00
  • 710b4082d1
    Add constant-bound contradiction shortcut for string < constraints in theory_seq (#10112) Copilot 2026-07-13 12:56:57 -07:00
  • 7d1bdf041e
    Merge 1faba5c769 into 038b367d68 Copilot 2026-07-13 16:32:39 +00:00
  • 1faba5c769
    Fix missing std headers in singlethread WASM wrapper copilot/alternative-z3-solver-solutions copilot-swe-agent[bot] 2026-07-13 16:32:34 +00:00
  • 038b367d68
    Fix non-termination in mod rewriter for symbolic modulus (#10105) Copilot 2026-07-13 09:20:03 -07:00
  • b83573675e
    Merge a37003fa2d into 98e1f5ca2d Lev Nachmanson 2026-07-13 17:10:01 +02:00
  • 06a473004c
    Merge e503ead008 into 98e1f5ca2d Copilot 2026-07-13 17:10:01 +02:00
  • d8726d652e
    Add constant-bound conflict shortcut for string lt constraints copilot-swe-agent[bot] 2026-07-13 05:09:27 +00:00
  • 34964402b4 bugfix about child threads setting force_enable=false for parallel fmcad26_artifact Ilana Shapiro 2026-07-12 22:07:05 -07:00
  • be7e8d7820
    Add constant-bound shortcut for string comparison constraints copilot-swe-agent[bot] 2026-07-13 05:05:11 +00:00
  • 026971075b
    Fix sequence foldl nth model propagation copilot-swe-agent[bot] 2026-07-13 05:01:29 +00:00
  • dc8fcb93a6
    Enable macro-finder fallback for auto_config=false mbqi=false copilot/fix-unsat-with-asserts copilot-swe-agent[bot] 2026-07-13 04:59:52 +00:00
  • 98e1f5ca2d
    Fix assertion violation in bv2int_translator with smt.bv.solver=2 (#10109) Copilot 2026-07-12 21:56:12 -07:00
  • f662eed78d
    Fix bv2int_translator assertion: extend early-return for non-basic bool non-BV expressions in plugin mode copilot-swe-agent[bot] 2026-07-13 04:54:48 +00:00
  • 965942be79
    Java API: return EnumSort instead of DatatypeSort from Sort.create() (#10104) Copilot 2026-07-12 21:46:46 -07:00
  • da82c003c9
    Initial plan copilot-swe-agent[bot] 2026-07-13 04:37:57 +00:00
  • 3bfc2ca0b7
    Initial plan copilot-swe-agent[bot] 2026-07-13 04:35:26 +00:00
  • a4eeeceb52
    Initial plan copilot-swe-agent[bot] 2026-07-13 04:33:47 +00:00
  • 26476c495f
    Improve comment clarity in arith_rewriter mod fix copilot-swe-agent[bot] 2026-07-13 04:32:16 +00:00
  • b544f7e58c
    Fix non-termination in mod rewriter for symbolic modulus (issue #7403) copilot-swe-agent[bot] 2026-07-13 04:30:49 +00:00
  • 88d0d282d6
    Initial plan copilot-swe-agent[bot] 2026-07-13 04:21:19 +00:00
  • 7b26fe135a
    Add linear divisibility closure lemma for lp/nla solver (#7464) (#10107) Nikolaj Bjorner 2026-07-12 21:20:50 -07:00
  • 8c80fe9440
    Address code review: extract INIT_GLOBAL constant in browser-singlethread.ts and fix Web Worker README example copilot-swe-agent[bot] 2026-07-13 04:08:24 +00:00
  • 66b0f58e23
    Add single-threaded WASM build for z3-solver without SharedArrayBuffer copilot-swe-agent[bot] 2026-07-13 04:05:49 +00:00
  • 634b2886ba
    fix: declare type variables before use in solver display output (#10103) Copilot 2026-07-12 20:56:00 -07:00
  • ba1c44462b Add linear divisibility closure lemma for lp/nla solver (#7464) Nikolaj Bjorner 2026-07-12 20:54:36 -07:00
  • 4e48303776
    Fix Java API ClassCastException when getting EnumSort of constant copilot-swe-agent[bot] 2026-07-13 03:52:14 +00:00
  • b964e1a0e8
    Initial plan copilot-swe-agent[bot] 2026-07-13 03:49:21 +00:00
  • 6bff306066
    Initial plan copilot-swe-agent[bot] 2026-07-13 03:48:47 +00:00
  • 431f0223f0
    Initial plan copilot-swe-agent[bot] 2026-07-13 03:47:40 +00:00
  • 087eeaf33c
    Fix api_datalog test: reuse of Z3_context across set-logic calls (#10101) Copilot 2026-07-12 20:32:02 -07:00
  • 1e07ca76af
    fix: add dedicated lim_svector<sort*> m_type_vars to decl_collector and emit declare-type-var in display_decls copilot-swe-agent[bot] 2026-07-13 03:27:16 +00:00
  • 136a653ade
    cmake: prevent install_tactic.deps from triggering spurious rebuilds on reconfigure (#10102) Copilot 2026-07-12 20:07:41 -07:00
  • ad9300c75f
    Fix api_datalog test: use fresh contexts for each Z3_eval_smtlib2_string call copilot-swe-agent[bot] 2026-07-13 03:07:15 +00:00
  • eaf9236540
    fix: only write install_tactic.deps when content changes to avoid unnecessary rebuilds copilot-swe-agent[bot] 2026-07-13 03:04:29 +00:00
  • cc46f9a7cd
    Initial plan copilot-swe-agent[bot] 2026-07-13 03:01:46 +00:00
  • 638e7b7bce
    fix: simplify type variable collection condition in decl_collector::visit_sort copilot-swe-agent[bot] 2026-07-13 03:00:50 +00:00
  • 154f71102d
    fix: collect type variables (poly_family_id sorts) in decl_collector::visit_sort copilot-swe-agent[bot] 2026-07-13 02:59:45 +00:00
  • 9ea861ff98
    Initial plan copilot-swe-agent[bot] 2026-07-13 02:48:05 +00:00
  • 0b8335e776
    Set pi.avoid_skolems=false for TPTP solver runs (#10100) Copilot 2026-07-12 19:21:25 -07:00
  • 7b1cdf60f7
    Scope TPTP skolem parameter to solver copilot-swe-agent[bot] 2026-07-13 02:16:40 +00:00
  • d4e177c95e
    Set TPTP pi.avoid_skolems globally copilot-swe-agent[bot] 2026-07-13 02:15:08 +00:00
  • 0000e16851 expose avoid-skolems parameter to deal with TPTP problems Nikolaj Bjorner 2026-07-12 18:54:14 -07:00
  • 7d67dbfcfc
    Add QE regression for unsound check-sat-using qe result on quantified reals (#10097) Copilot 2026-07-12 18:53:15 -07:00
  • 4862a10ffd
    Spacer QE: avoid assertion on extended arithmetic model values and add #3845 regression (#10096) Copilot 2026-07-12 18:52:44 -07:00
  • d99b6e7b08
    Regenerate gh-aw lock workflows to remove stale model-multiplier runtime hook (#10099) Copilot 2026-07-12 18:30:19 -07:00
  • 50455f9b6d
    Delete z3.log copilot/fix-assertion-violation-again Nikolaj Bjorner 2026-07-12 18:29:16 -07:00
  • b1aa1e6ddc
    Add z3regex Python module to translate Python regex syntax into Z3 regular expressions (#10095) Copilot 2026-07-12 18:26:59 -07:00
  • 535bafc6d0
    Analysis of ASSERTION VIOLATION in qe_mbp.cpp - root cause identified copilot-swe-agent[bot] 2026-07-13 00:33:39 +00:00
  • d9ad23a188
    Ensure Nightly release source archive always matches the workflow commit (#10094) Copilot 2026-07-12 17:32:45 -07:00
  • c5e089124c
    Regenerate gh-aw lock workflows to remove missing merge script call copilot-swe-agent[bot] 2026-07-13 00:00:14 +00:00
  • 002546d83f
    Add sanity assertions in QE regression test setup copilot-swe-agent[bot] 2026-07-12 23:50:14 +00:00
  • 1f71d530f7
    Refine QE regression test assertions per review feedback copilot-swe-agent[bot] 2026-07-12 23:49:50 +00:00
  • bcee5ef4d4
    Add regression test for QE unsoundness issue #4175 copilot-swe-agent[bot] 2026-07-12 23:49:22 +00:00
  • 5cf1543118
    Fix Spacer QE numeral handling and add #3845 regression copilot-swe-agent[bot] 2026-07-12 23:48:30 +00:00
  • 1de3515ced
    Make Nightly tag SHA check robust copilot-swe-agent[bot] 2026-07-12 23:47:13 +00:00
  • f16b2dbee9
    Add z3regex Python regex translator module copilot-swe-agent[bot] 2026-07-12 23:46:30 +00:00
  • 2f11f6121a
    Tighten Nightly deletion and tag verification copilot-swe-agent[bot] 2026-07-12 23:46:18 +00:00
  • 606a06fa5f fix warnings Nikolaj Bjorner 2026-07-12 16:45:24 -07:00
  • 8624d910db
    Serialize nightly deploy and keep tag checks copilot-swe-agent[bot] 2026-07-12 23:45:16 +00:00