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

Commit graph

  • 2dac76d19a Handle overflow predicates in new core bit-vector internalization Lev Nachmanson 2026-02-27 13:07:39 -10:00
  • 6ec40153cc fix #7677: treat FC_CONTINUE from check_nla as FEASIBLE in maximize Lev Nachmanson 2026-02-27 12:29:14 -10:00
  • ffe29b1433 Fix #7951: add cancellation checks to polynomial gcd_prs and HNF computation Lev Nachmanson 2026-02-27 10:09:51 -10:00
  • d906a0cc2d fix bug reported by Maria Novoszel Nikolaj Bjorner 2026-02-27 12:02:49 -08:00
  • 5ff5b075b2
    Merge pull request #8789 from Z3Prover/succ_int_mult Lev Nachmanson 2026-02-27 09:45:26 -10:00
  • 21c23e78db Fix #7507: simplify (>= product_of_consecutive_ints 0) to true Lev Nachmanson 2026-02-26 12:36:28 -10:00
  • fda8b4175f
    Merge pull request #8793 from Z3Prover/copilot/fix-missing-api-functions Nikolaj Bjorner 2026-02-27 03:14:18 -08:00
  • a4ccb6390d Integrate rw_table into th_rewriter_cfg and expand populate_rules() copilot/add-abstract-machine-evaluator copilot-swe-agent[bot] 2026-02-27 04:36:28 +00:00
  • 57c9987d25 Add abstract machine for pattern-based term rewriting (rw_rule) copilot-swe-agent[bot] 2026-02-27 03:23:39 +00:00
  • 282db840de Add missing API functions to Go, OCaml, and TypeScript bindings copilot-swe-agent[bot] 2026-02-27 02:55:37 +00:00
  • f223360b33 Initial plan copilot-swe-agent[bot] 2026-02-27 02:55:29 +00:00
  • 3f6acc45ed Initial plan copilot-swe-agent[bot] 2026-02-27 02:48:36 +00:00
  • 5d48cb8344 fix: replace 33 bare except clauses with except Exception haosenwang1018 2026-02-27 02:02:04 +00:00
  • ea873672c3
    Merge pull request #8788 from Z3Prover/copilot/simplify-fpa-test-code Nikolaj Bjorner 2026-02-26 16:29:42 -08:00
  • cf0ffa2673 refactor: extract run_fp_test helper in fpa.cpp copilot-swe-agent[bot] 2026-02-26 23:54:17 +00:00
  • f2e00b3589 Initial plan copilot-swe-agent[bot] 2026-02-26 23:52:54 +00:00
  • aeded4d721
    Merge pull request #8787 from Z3Prover/dependabot/npm_and_yarn/src/api/js/multi-770cfcd984 Nikolaj Bjorner 2026-02-26 15:52:39 -08:00
  • 828e4a7ef7
    Merge pull request #8779 from Z3Prover/copilot/convert-bv1-blast-to-simplifier Nikolaj Bjorner 2026-02-26 15:52:18 -08:00
  • e097a98019
    Bump minimatch in /src/api/js dependabot[bot] 2026-02-26 23:51:30 +00:00
  • c70f902b53
    Merge pull request #8780 from Z3Prover/copilot/convert-blast-term-ite-to-simplifier Nikolaj Bjorner 2026-02-26 15:51:30 -08:00
  • fadf045df0
    Merge pull request #8781 from Z3Prover/copilot/fix-ts-ocaml-issues Nikolaj Bjorner 2026-02-26 15:49:40 -08:00
  • ff7cc0f59e Remove old blast-term-ite tactic class, rename blast-term-ite2 to blast-term-ite copilot-swe-agent[bot] 2026-02-26 20:07:42 +00:00
  • 668dd7a0a1 Rename bv1-blast2 to bv1-blast, remove old tactic source copilot-swe-agent[bot] 2026-02-26 20:06:14 +00:00
  • a384e464e3
    Merge pull request #8782 from Z3Prover/copilot/update-csa-workflow-discussion Nikolaj Bjorner 2026-02-26 09:27:56 -08:00
  • 2105e95f30
    Merge pull request #8785 from filipeom/filipe/expose-re_allchar Nikolaj Bjorner 2026-02-26 09:26:51 -08:00
  • f0421879bb
    Expose mk_re_allchar in OCaml API Filipe Marques 2026-02-26 16:22:55 +00:00
  • 070f760501
    Merge pull request #8748 from Z3Prover/copilot/fix-floating-point-model-validation Nikolaj Bjorner 2026-02-26 02:21:20 -08:00
  • 234913bf56 Implement register_on_clause for OCaml and TypeScript bindings copilot-swe-agent[bot] 2026-02-26 04:04:27 +00:00
  • 033ea50a5d Convert bv1-blast tactic to a simplifier copilot-swe-agent[bot] 2026-02-26 04:01:11 +00:00
  • 7390a9b856 Convert blast-term-ite tactic to also expose as a simplifier copilot-swe-agent[bot] 2026-02-26 03:51:42 +00:00
  • ddb8e35560 Update CSA workflow to integrate CSA report content directly into GitHub Discussion copilot-swe-agent[bot] 2026-02-26 03:41:55 +00:00
  • 99d8db8ba8 initial plan copilot-swe-agent[bot] 2026-02-26 03:39:40 +00:00
  • 31a9cbd3f7 Initial plan copilot-swe-agent[bot] 2026-02-26 03:36:50 +00:00
  • c4f85493a7 Initial plan copilot-swe-agent[bot] 2026-02-26 03:33:58 +00:00
  • 0318762600 Initial plan copilot-swe-agent[bot] 2026-02-26 03:31:18 +00:00
  • 72411ce5b9 Initial plan copilot-swe-agent[bot] 2026-02-26 03:31:08 +00:00
  • b4f7d057d3 Add model_validate and invalid-check to fpa regression tests copilot-swe-agent[bot] 2026-02-26 03:21:33 +00:00
  • dcee8d5a94 fix: replace 33 bare except clauses with except Exception haosenwang1018 2026-02-26 02:23:58 +00:00
  • 4361b704df
    Merge pull request #8774 from Z3Prover/copilot/simplify-code-in-context-and-solver Nikolaj Bjorner 2026-02-25 18:17:23 -08:00
  • add65451fd Add fpa regression test for fp.to_real denormal encoding fix copilot-swe-agent[bot] 2026-02-25 22:04:03 +00:00
  • af2e60c069 code-simplifier: fix JavaDoc formatting in Context.java and extract ternary in Solver.cs copilot-swe-agent[bot] 2026-02-25 21:49:23 +00:00
  • db98f1e2f7 Initial plan copilot-swe-agent[bot] 2026-02-25 21:45:23 +00:00
  • fba1e4b648
    Merge pull request #8737 from Z3Prover/copilot/fix-refutational-soundness-bug Nikolaj Bjorner 2026-02-25 13:34:59 -08:00
  • 412c56ecc8
    Merge pull request #8767 from Z3Prover/copilot/fix-ubv-to-int-bug Nikolaj Bjorner 2026-02-25 13:32:40 -08:00
  • c51f45bf5e
    Merge pull request #8766 from Z3Prover/copilot/fix-critical-bugs-from-discussion Nikolaj Bjorner 2026-02-25 09:22:45 -08:00
  • a7ea22f24f remove an unnecessary template from levelwise Lev Nachmanson 2026-02-25 07:03:23 -10:00
  • 66d19c4d3f
    Merge pull request #8770 from Z3Prover/lws Lev Nachmanson 2026-02-25 06:25:58 -10:00
  • 0835420cc1 change the default of param lws_subs_witness_disc to true Lev Nachmanson 2026-02-24 15:24:35 -10:00
  • 4860d57ae9 Fix intblast ubv_to_int bug: add bv2int axioms for compound expressions copilot-swe-agent[bot] 2026-02-25 00:46:13 +00:00
  • ae4cb5557a Fix true positive critical bugs from static analysis discussion #8764 copilot-swe-agent[bot] 2026-02-25 00:41:59 +00:00
  • 1b68ee5f30 Initial plan copilot-swe-agent[bot] 2026-02-25 00:20:49 +00:00
  • 5ccc2cd8c0 recompile Nikolaj Bjorner 2026-02-24 16:17:46 -08:00
  • b9d098fc0a
    Merge pull request #8765 from Z3Prover/copilot/update-grep-search-methods Nikolaj Bjorner 2026-02-24 16:17:02 -08:00
  • 0064a2d70a
    Merge branch 'master' into copilot/update-grep-search-methods Nikolaj Bjorner 2026-02-24 16:16:50 -08:00
  • 4a29c77aa2 Initial plan copilot-swe-agent[bot] 2026-02-25 00:15:14 +00:00
  • 48de0f8a5e updated compiled workflows Nikolaj Bjorner 2026-02-24 16:12:53 -08:00
  • 6a4e8de5f3
    Merge pull request #8761 from Z3Prover/copilot/add-compilation-database Nikolaj Bjorner 2026-02-24 16:11:43 -08:00
  • bf934398d7 Update api-coherence-checker to search for Rust traits and trait implementations copilot-swe-agent[bot] 2026-02-25 00:10:31 +00:00
  • a0a44c5571 Initial plan copilot-swe-agent[bot] 2026-02-25 00:08:53 +00:00
  • c580bcd4d1
    Merge pull request #8762 from TempuraFramework/master Nikolaj Bjorner 2026-02-24 13:51:33 -08:00
  • 54b0746033 Add compilation database to csa-analysis workflow copilot-swe-agent[bot] 2026-02-24 20:05:15 +00:00
  • 11cfaf6dfd Initial plan copilot-swe-agent[bot] 2026-02-24 20:01:56 +00:00
  • 6b79297252 Add missing Java API method for as-array Ruijie Fang 2026-02-24 13:55:39 -06:00
  • c282ece605
    Merge pull request #8760 from Z3Prover/copilot/add-workflow-for-z3-and-csa Nikolaj Bjorner 2026-02-24 11:48:11 -08:00
  • 23d8bdd47c
    Merge pull request #8758 from Z3Prover/copilot/fix-issues-except-rust Nikolaj Bjorner 2026-02-24 11:47:09 -08:00
  • 4f4e657449
    Merge branch 'Z3Prover:master' into master Ruijie Fang 2026-02-24 13:39:36 -06:00
  • cdd5582a5b Add Clang Static Analyzer (CSA) agentic workflow with Discussion reporting copilot-swe-agent[bot] 2026-02-24 19:30:15 +00:00
  • 6fe956c2f6 Initial plan copilot-swe-agent[bot] 2026-02-24 19:25:21 +00:00
  • 0074de0fce improve non-zero witness substitution logic Lev Nachmanson 2026-02-24 09:19:13 -10:00
  • cfb3a01756
    Update Solver.cs Nikolaj Bjorner 2026-02-24 09:58:12 -08:00
  • ce04a24348 Improve TypeScript Optimize documentation for handle index clarity copilot-swe-agent[bot] 2026-02-24 17:28:45 +00:00
  • 9802b32a3e Add missing API methods: dimacs, translate, proof, addSimplifier, getLower/getUpper, etc. copilot-swe-agent[bot] 2026-02-24 17:22:17 +00:00
  • 8e5f1840a9
    Merge pull request #8755 from Z3Prover/copilot/simplify-go-propagator-callbacks Nikolaj Bjorner 2026-02-24 09:10:21 -08:00
  • 819144f374
    Merge pull request #8756 from Z3Prover/copilot/create-agentic-workflow-backlog Nikolaj Bjorner 2026-02-24 09:08:28 -08:00
  • 08addfa654 Initial plan copilot-swe-agent[bot] 2026-02-24 17:03:50 +00:00
  • 4ebf453365 Add issue-backlog-processor agentic workflow copilot-swe-agent[bot] 2026-02-24 16:54:49 +00:00
  • d2f6dd0d5a Initial plan copilot-swe-agent[bot] 2026-02-24 16:49:41 +00:00
  • 575f4a8911 Simplify Go user propagator callbacks with withCallback helper copilot-swe-agent[bot] 2026-02-24 16:48:05 +00:00
  • 023b29ff0e Initial plan copilot-swe-agent[bot] 2026-02-24 16:44:52 +00:00
  • e0161b2e2e
    Merge pull request #8746 from Z3Prover/copilot/simplify-go-return-logic Nikolaj Bjorner 2026-02-24 08:44:24 -08:00
  • 13cf90ea09
    Merge pull request #8753 from Z3Prover/copilot/update-api-coherence-checker-workflow Nikolaj Bjorner 2026-02-24 08:43:14 -08:00
  • aaa62efc90
    Merge pull request #8725 from Z3Prover/copilot/convert-factor-to-simplifier Nikolaj Bjorner 2026-02-24 08:42:30 -08:00
  • 1f5bc9ba0c Add Rust bindings (prove-rs/z3.rs) to API coherence checker workflow copilot-swe-agent[bot] 2026-02-24 16:36:54 +00:00
  • cac5e83948 Initial plan copilot-swe-agent[bot] 2026-02-24 16:30:20 +00:00
  • de3cf18899 Fix fp.to_real encoding for denormal floating-point values copilot-swe-agent[bot] 2026-02-24 05:22:54 +00:00
  • 9e96ee91dc Fix regression: use setup_solver_terms() instead of setup_solver_poly() in nra_solver check() copilot/fix-z3-regression-unknown-to-sat copilot-swe-agent[bot] 2026-02-24 05:11:31 +00:00
  • f0612ab7e0 Initial plan copilot/fix-invalid-model-generation copilot-swe-agent[bot] 2026-02-24 04:44:45 +00:00
  • 243275c638 Initial plan copilot-swe-agent[bot] 2026-02-24 04:44:27 +00:00
  • da54b16b7d Initial plan copilot-swe-agent[bot] 2026-02-24 04:43:57 +00:00
  • 3feac95119 Simplify boolean return in goOnBindingCb copilot-swe-agent[bot] 2026-02-24 04:42:49 +00:00
  • f8e97957f8 Initial plan copilot-swe-agent[bot] 2026-02-24 04:41:56 +00:00
  • 8ec15639e0
    Merge pull request #8726 from Z3Prover/copilot/convert-cofactor-term-ite-to-simplifier Nikolaj Bjorner 2026-02-23 20:40:23 -08:00
  • 441fbe25fa
    Merge pull request #8742 from Z3Prover/dependabot/github_actions/actions/setup-go-6 Nikolaj Bjorner 2026-02-23 20:33:03 -08:00
  • fe5c15e1fc
    Merge pull request #8743 from Z3Prover/dependabot/github_actions/github/gh-aw-0.49.5 Nikolaj Bjorner 2026-02-23 20:32:37 -08:00
  • 87a8ccfa0e
    Merge pull request #8744 from Z3Prover/dependabot/github_actions/actions/upload-artifact-6 Nikolaj Bjorner 2026-02-23 20:32:11 -08:00
  • 55753ba36f
    Merge pull request #8745 from Z3Prover/dependabot/github_actions/actions/download-artifact-7 Nikolaj Bjorner 2026-02-23 20:31:58 -08:00
  • 6df2aeedb9
    Merge pull request #8741 from Z3Prover/dependabot/github_actions/actions/checkout-6.0.2 Nikolaj Bjorner 2026-02-23 20:30:33 -08:00
  • a61de6023a
    Bump actions/download-artifact from 4 to 7 dependabot[bot] 2026-02-23 23:24:27 +00:00
  • 2fed3b67ba
    Bump actions/upload-artifact from 4 to 6 dependabot[bot] 2026-02-23 23:24:03 +00:00
  • c3a97b5a03
    Bump github/gh-aw from 0.45.6 to 0.49.5 dependabot[bot] 2026-02-23 23:23:44 +00:00