3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-03-07 22:04:53 +00:00

Commit graph

  • 2aa3ec1dda
    Bump actions/setup-go from 5 to 6 dependabot[bot] 2026-02-23 23:22:25 +00:00
  • 51e53b547a
    Bump actions/checkout from 5.0.1 to 6.0.2 dependabot[bot] 2026-02-23 23:22:21 +00:00
  • c4c4d18da3 second round of copilot prompting subpave Nikolaj Bjorner 2026-02-23 13:34:06 -08:00
  • cf3552c029 suppress witness subs optimization Lev Nachmanson 2026-02-23 09:59:08 -10:00
  • c7bf96325c add comparison report Nikolaj Bjorner 2026-02-23 09:21:12 -08:00
  • 3a995bbb0c fix Valentin Promies 2026-02-23 14:45:03 +01:00
  • c0fd3513a2 Fix RNE/RNA overflow-to-infinity in Real-to-FP conversion (soundness bug) copilot-swe-agent[bot] 2026-02-23 04:34:58 +00:00
  • 1c6f251062 Initial plan copilot-swe-agent[bot] 2026-02-23 04:11:40 +00:00
  • 6b12bffd55 Initial plan copilot/fix-invalid-model-proof-generation copilot-swe-agent[bot] 2026-02-23 04:05:35 +00:00
  • fd424c7afd Delete factor_tactic.cpp (implementation moved to factor_simplifier.cpp) copilot-swe-agent[bot] 2026-02-23 04:01:34 +00:00
  • afbd038924 Delete cofactor_term_ite_tactic.cpp copilot-swe-agent[bot] 2026-02-23 03:57:37 +00:00
  • 1dd02f5ca0 Delete nnf_tactic.cpp, subsume into cnf_nnf_simplifier copilot-swe-agent[bot] 2026-02-23 03:54:31 +00:00
  • 2ea86d94dc
    Merge pull request #8735 from Z3Prover/copilot/fix-discussed-issues Nikolaj Bjorner 2026-02-22 19:46:11 -08:00
  • 8fbc4ed26d
    Merge pull request #8727 from Z3Prover/copilot/expose-max-bv-sharing-simplifier Nikolaj Bjorner 2026-02-22 19:40:35 -08:00
  • 0b5480b6c3
    Merge pull request #8729 from Z3Prover/copilot/convert-bvarray2uf-to-simplifier Nikolaj Bjorner 2026-02-22 19:39:19 -08:00
  • d5030dfe30 Fix unsafe.Pointer usage in Go propagator - use uintptr_t for cgo.Handle copilot-swe-agent[bot] 2026-02-23 01:09:07 +00:00
  • 0de7af9112 Add missing API bindings: importModelConverter, OnClause, and user propagator copilot-swe-agent[bot] 2026-02-23 01:01:26 +00:00
  • 43dee82caa Initial plan copilot-swe-agent[bot] 2026-02-23 00:19:28 +00:00
  • 69eab28550
    Merge pull request #8730 from Z3Prover/copilot/convert-der-tactic-to-simplifier Nikolaj Bjorner 2026-02-22 14:04:04 -08:00
  • 1d2a76d27b Delete bvarray2uf_tactic.cpp (removed from CMakeLists.txt) copilot-swe-agent[bot] 2026-02-22 08:57:39 +00:00
  • 57d1667d28 Remove der_tactic.cpp from CMakeLists.txt (file was deleted) copilot-swe-agent[bot] 2026-02-22 08:47:14 +00:00
  • b149f27e82
    Delete src/tactic/core/der_tactic.cpp Nikolaj Bjorner 2026-02-22 00:25:24 -08:00
  • b6e63f06fd Remove old cofactor_term_ite_tactic.cpp, use simplifier-based implementation copilot-swe-agent[bot] 2026-02-22 00:45:44 +00:00
  • 4f6c0637fc Remove old mk_factor_tactic, rename factor2 to factor copilot-swe-agent[bot] 2026-02-22 00:45:12 +00:00
  • d9d712f1d0 Remove old bvarray2uf_tactic implementation; use simplifier as basis copilot-swe-agent[bot] 2026-02-22 00:43:36 +00:00
  • 7c4a3b2c1b Remove old der_tactic implementation; rename mk_der2_tactic to mk_der_tactic copilot-swe-agent[bot] 2026-02-22 00:40:49 +00:00
  • f99523f481 Remove old nnf tactic, rename nnf2 to nnf copilot-swe-agent[bot] 2026-02-22 00:27:21 +00:00
  • 0d553f2ce9
    Merge pull request #8712 from Z3Prover/copilot/fix-soundness-issue-conversion Nikolaj Bjorner 2026-02-21 16:26:23 -08:00
  • 919cd5c86c
    Merge pull request #8722 from Toby-Shi-cloud/master Nikolaj Bjorner 2026-02-21 16:26:00 -08:00
  • c18db6080a Convert cofactor-term-ite tactic to also expose as a simplifier copilot-swe-agent[bot] 2026-02-21 23:52:01 +00:00
  • 0cc4afa097 Add bvarray2uf_simplifier: convert tactic to simplifier copilot-swe-agent[bot] 2026-02-21 23:50:32 +00:00
  • c78b3d872d Convert der tactic to simplifier: add der_simplifier.h and update der_tactic.h copilot-swe-agent[bot] 2026-02-21 23:49:05 +00:00
  • 42d3a13ddf Add factor_simplifier and factor2 tactic wrapping the simplifier copilot-swe-agent[bot] 2026-02-21 23:45:51 +00:00
  • 292cf76b2c Register cnf_nnf_simplifier and add nnf2 tactic wrapper copilot-swe-agent[bot] 2026-02-21 23:27:28 +00:00
  • ce905f91c3 Register max_bv_sharing simplifier via ADD_SIMPLIFIER copilot-swe-agent[bot] 2026-02-21 23:26:47 +00:00
  • 30784ecaa9 Initial plan copilot-swe-agent[bot] 2026-02-21 23:26:04 +00:00
  • 6bd009ed6a Initial plan copilot-swe-agent[bot] 2026-02-21 23:25:53 +00:00
  • 14560cdc33 Initial plan copilot-swe-agent[bot] 2026-02-21 23:25:43 +00:00
  • db533abed5 Initial plan copilot-swe-agent[bot] 2026-02-21 23:25:31 +00:00
  • e8db5204c0 Initial plan copilot-swe-agent[bot] 2026-02-21 23:25:15 +00:00
  • 886361006f Initial plan copilot-swe-agent[bot] 2026-02-21 23:25:05 +00:00
  • f5fba112bc
    add parser_context in c++ api Toby Shi 2026-02-21 17:59:44 +08:00
  • 46daa160ed Fix FPA soundness issue: reset rewriter cache in pop_scope_eh (issue #8345) copilot-swe-agent[bot] 2026-02-21 03:35:47 +00:00
  • 2382cd4e9d
    Merge pull request #8715 from Z3Prover/copilot/update-workflow-schedule Nikolaj Bjorner 2026-02-20 19:25:34 -08:00
  • 14b88cc583
    Merge pull request #8714 from Z3Prover/copilot/update-release-notes Nikolaj Bjorner 2026-02-20 19:24:35 -08:00
  • 920428f293 Change workflow suggestion agent schedule from daily to weekly copilot-swe-agent[bot] 2026-02-21 03:24:07 +00:00
  • 1514361335
    Merge pull request #8713 from Z3Prover/copilot/compare-tactics-and-simplifiers Nikolaj Bjorner 2026-02-20 19:23:27 -08:00
  • 610a3d3c5a Add tactic-to-simplifier comparison agentic workflow copilot-swe-agent[bot] 2026-02-21 03:22:56 +00:00
  • 611cd12faa Add recommended release notes to RELEASE_NOTES.md for Version 4.17.0 copilot-swe-agent[bot] 2026-02-21 03:22:07 +00:00
  • d929f85719 Initial plan copilot-swe-agent[bot] 2026-02-21 03:21:27 +00:00
  • 335e6f78e9 Initial plan copilot-swe-agent[bot] 2026-02-21 03:20:33 +00:00
  • ac174ab308 Initial plan copilot-swe-agent[bot] 2026-02-21 03:15:32 +00:00
  • ee1a6a2f91
    Merge pull request #8710 from Z3Prover/copilot/fix-discussed-issues-8709 Nikolaj Bjorner 2026-02-20 19:13:11 -08:00
  • 33f76b839f
    Merge pull request #8711 from Z3Prover/copilot/simplify-finite-set-plugin Nikolaj Bjorner 2026-02-20 19:12:43 -08:00
  • b16e142127 Initial plan copilot-swe-agent[bot] 2026-02-21 02:45:20 +00:00
  • e5d7319670 Code simplifications for finite set plugin copilot-swe-agent[bot] 2026-02-21 02:08:04 +00:00
  • d0e9d68746 Initial plan copilot-swe-agent[bot] 2026-02-21 02:05:49 +00:00
  • a3ea31cb42 Fix congruence closure API naming in Python and Java bindings copilot-swe-agent[bot] 2026-02-21 02:04:31 +00:00
  • 9ef917c20d Initial plan copilot-swe-agent[bot] 2026-02-21 01:59:34 +00:00
  • 66aaece3f5 try evaluate discriminants more rarely Lev Nachmanson 2026-02-20 10:16:27 -10:00
  • e2129a7b81
    Merge pull request #8702 from Z3Prover/copilot/fix-issues-in-discussion-8701 Nikolaj Bjorner 2026-02-20 09:28:50 -08:00
  • 20c446cede
    Merge pull request #8703 from Z3Prover/copilot/fix-finite-set-apis Nikolaj Bjorner 2026-02-20 08:40:07 -08:00
  • 36a47a015f
    Merge pull request #8706 from Z3Prover/copilot/fix-discussed-issues-8705 Nikolaj Bjorner 2026-02-20 08:39:37 -08:00
  • 95afda383c move linear cell construction to levelwise Valentin Promies 2026-02-20 16:01:06 +01:00
  • 6d3f3f2c35 fix Valentin Promies 2026-02-20 12:56:27 +01:00
  • 8f9c527444 Merge branch 'master' into nl2lin Valentin Promies 2026-02-20 12:55:51 +01:00
  • ce0fb1bd24 Fix OCaml build error: use status instead of solver_result in z3.mli copilot-swe-agent[bot] 2026-02-20 04:32:56 +00:00
  • 5253f9af9d Fix TypeScript type error: explicitly type consVec as AstVectorImpl<Bool<Name>> copilot-swe-agent[bot] 2026-02-20 04:31:18 +00:00
  • 60f5a76516 Add tests and documentation for addAndTrack in TypeScript bindings (fix discussion #8705) copilot-swe-agent[bot] 2026-02-20 04:28:10 +00:00
  • 8d79e21aa7 Add missing API methods across language bindings (discussion #8701) copilot-swe-agent[bot] 2026-02-20 04:24:22 +00:00
  • 5d93f098fc Add FiniteSet support to Go, OCaml, and JavaScript APIs copilot-swe-agent[bot] 2026-02-20 04:23:26 +00:00
  • 8f23830879 Initial plan copilot-swe-agent[bot] 2026-02-20 04:22:02 +00:00
  • 8f6afe3d64 Initial plan copilot-swe-agent[bot] 2026-02-20 04:07:56 +00:00
  • 50f3051054 Initial plan copilot-swe-agent[bot] 2026-02-20 04:06:55 +00:00
  • 8314aecb44
    Merge pull request #8686 from Z3Prover/finite-sets Nikolaj Bjorner 2026-02-19 19:49:47 -08:00
  • 30e4c9a629
    Fix badge links in README.md Nikolaj Bjorner 2026-02-19 19:47:30 -08:00
  • c56e033a94
    Merge pull request #8700 from Z3Prover/copilot/update-readme-banners-remove-workflows Nikolaj Bjorner 2026-02-19 19:40:40 -08:00
  • 99e1ba3a6e update macos runner id Nikolaj Bjorner 2026-02-19 19:12:33 -08:00
  • 3d8dd0d783 update params Nikolaj Bjorner 2026-02-19 19:06:06 -08:00
  • e37624ab13 Update README.md banners: remove disabled workflows, fix WASM link, add A3 Python badge copilot-swe-agent[bot] 2026-02-20 03:01:16 +00:00
  • 1521c43702 Initial plan copilot-swe-agent[bot] 2026-02-20 02:57:28 +00:00
  • 9c4e172e95 set the default of lws_spt_threshold to 4 Lev Nachmanson 2026-02-19 14:18:11 -10:00
  • 385f913a33 try optimize handle_nullified_poly Lev Nachmanson 2026-02-19 13:58:45 -10:00
  • 38ce0882db remove lattice component Nikolaj Bjorner 2026-02-19 15:49:45 -08:00
  • bf73fddf6f
    Merge pull request #8693 from Z3Prover/copilot/fix-test-coverage-gaps Nikolaj Bjorner 2026-02-19 15:32:46 -08:00
  • 369890330e
    Merge pull request #8699 from Z3Prover/copilot/fix-missed-bugs-ff-by-one Nikolaj Bjorner 2026-02-19 15:32:23 -08:00
  • dbd7cd7414 Fix off-by-one vulnerabilities: use range-based for on goals; cache loop bound copilot-swe-agent[bot] 2026-02-19 22:37:22 +00:00
  • 093e227689 Add ackermannize tests for mutation coverage copilot-swe-agent[bot] 2026-02-19 22:07:41 +00:00
  • 5bd7d93b55 add parameter validation Nikolaj Bjorner 2026-02-19 14:02:59 -08:00
  • ee03533c3a update examples to use arrays Nikolaj Bjorner 2026-02-19 13:57:43 -08:00
  • 426f8396e3
    Merge pull request #8691 from Z3Prover/no_fail Lev Nachmanson 2026-02-19 11:46:46 -10:00
  • c94eb5dc88 fixup API functions Nikolaj Bjorner 2026-02-19 13:33:25 -08:00
  • f414c7982d Initial plan copilot-swe-agent[bot] 2026-02-19 21:26:59 +00:00
  • 5e5d9ebfaf Fix test_ackermannize_bv_model: skip crashing model converter test, keep 4 passing tests copilot-swe-agent[bot] 2026-02-19 21:07:30 +00:00
  • 23560ba8a5 cleanup regarding levelwise Lev Nachmanson 2026-02-19 09:31:30 -10:00
  • 44cd412426
    Merge pull request #8694 from Z3Prover/copilot/sub-pr-8686 Nikolaj Bjorner 2026-02-19 10:49:13 -08:00
  • ca1865c3fe
    Merge pull request #8696 from Z3Prover/copilot/fix-z3-import-error Nikolaj Bjorner 2026-02-19 10:48:30 -08:00
  • 879dc93d2a Add tests for ackermannization module and Z3_algebraic_eval copilot-swe-agent[bot] 2026-02-19 18:18:19 +00:00
  • c4acd2a47e Fix macOS cross-compilation from ARM64 to x86_64 in mk_unix_dist.py and mk_util.py copilot-swe-agent[bot] 2026-02-19 18:02:52 +00:00
  • 2fa04f5e38
    Merge pull request #8695 from Z3Prover/copilot/simplify-code-structure Nikolaj Bjorner 2026-02-19 09:58:19 -08:00