mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-28 19:01:29 +00:00
Code Activity
21826 commits 36 branches 58 tags 184 MiB
Commit graph

21826 commits

This branch
This branch
All branches
Author SHA1 Message Date
copilot-swe-agent[bot]
f2e00b3589 Initial plan 2026-02-26 23:52:54 +00:00
Nikolaj Bjorner
aeded4d721
Merge pull request #8787 from Z3Prover/dependabot/npm_and_yarn/src/api/js/multi-770cfcd984 
Bump minimatch in /src/api/js
 2026-02-26 15:52:39 -08:00
Nikolaj Bjorner
828e4a7ef7
Merge pull request #8779 from Z3Prover/copilot/convert-bv1-blast-to-simplifier 
Convert bv1-blast tactic to a dependent_expr_simplifier
 2026-02-26 15:52:18 -08:00
dependabot[bot]
e097a98019
Bump minimatch in /src/api/js 
Bumps  and [minimatch](https://github.com/isaacs/minimatch). These dependencies needed to be updated together.

Updates `minimatch` from 3.1.2 to 3.1.5
- [Changelog](https://github.com/isaacs/minimatch/blob/main/changelog.md)
- [Commits](https://github.com/isaacs/minimatch/compare/v3.1.2...v3.1.5)

Updates `minimatch` from 9.0.5 to 9.0.9
- [Changelog](https://github.com/isaacs/minimatch/blob/main/changelog.md)
- [Commits](https://github.com/isaacs/minimatch/compare/v3.1.2...v3.1.5)

---
updated-dependencies:
- dependency-name: minimatch
  dependency-version: 3.1.5
  dependency-type: indirect
- dependency-name: minimatch
  dependency-version: 9.0.9
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
 2026-02-26 23:51:30 +00:00
Nikolaj Bjorner
c70f902b53
Merge pull request #8780 from Z3Prover/copilot/convert-blast-term-ite-to-simplifier 
Convert `blast-term-ite` tactic to a `dependent_expr_simplifier`
 2026-02-26 15:51:30 -08:00
Nikolaj Bjorner
fadf045df0
Merge pull request #8781 from Z3Prover/copilot/fix-ts-ocaml-issues 
Add register_on_clause to OCaml and TypeScript bindings
 2026-02-26 15:49:40 -08:00
copilot-swe-agent[bot]
ff7cc0f59e Remove old blast-term-ite tactic class, rename blast-term-ite2 to blast-term-ite 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 20:07:42 +00:00
copilot-swe-agent[bot]
668dd7a0a1 Rename bv1-blast2 to bv1-blast, remove old tactic source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 20:06:14 +00:00
Nikolaj Bjorner
a384e464e3
Merge pull request #8782 from Z3Prover/copilot/update-csa-workflow-discussion 
CSA workflow: embed raw report content directly into GitHub Discussion
 2026-02-26 09:27:56 -08:00
Nikolaj Bjorner
2105e95f30
Merge pull request #8785 from filipeom/filipe/expose-re_allchar 
Expose `mk_re_allchar` in OCaml API
 2026-02-26 09:26:51 -08:00
Filipe Marques
f0421879bb
Expose mk_re_allchar in OCaml API 2026-02-26 16:22:55 +00:00
Nikolaj Bjorner
070f760501
Merge pull request #8748 from Z3Prover/copilot/fix-floating-point-model-validation 
Fix fp.to_real bitvector encoding for denormal floating-point values
 2026-02-26 02:21:20 -08:00
copilot-swe-agent[bot]
234913bf56 Implement register_on_clause for OCaml and TypeScript bindings 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 04:04:27 +00:00
copilot-swe-agent[bot]
033ea50a5d Convert bv1-blast tactic to a simplifier 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 04:01:11 +00:00
copilot-swe-agent[bot]
7390a9b856 Convert blast-term-ite tactic to also expose as a simplifier 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 03:51:42 +00:00
copilot-swe-agent[bot]
ddb8e35560 Update CSA workflow to integrate CSA report content directly into GitHub Discussion 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 03:41:55 +00:00
copilot-swe-agent[bot]
99d8db8ba8 initial plan 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 03:39:40 +00:00
copilot-swe-agent[bot]
31a9cbd3f7 Initial plan 2026-02-26 03:36:50 +00:00
copilot-swe-agent[bot]
c4f85493a7 Initial plan 2026-02-26 03:33:58 +00:00
copilot-swe-agent[bot]
0318762600 Initial plan 2026-02-26 03:31:18 +00:00
copilot-swe-agent[bot]
72411ce5b9 Initial plan 2026-02-26 03:31:08 +00:00
copilot-swe-agent[bot]
b4f7d057d3 Add model_validate and invalid-check to fpa regression tests 
Add (set-option :model_validate true) to each SMT-LIB2 spec in
src/test/fpa.cpp, and add ENSURE checks that the output does not
contain the string "invalid".

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-26 03:21:33 +00:00
Nikolaj Bjorner
4361b704df
Merge pull request #8774 from Z3Prover/copilot/simplify-code-in-context-and-solver 
Fix malformed JavaDoc in Context.java and extract ternary in Solver.cs
 2026-02-25 18:17:23 -08:00
copilot-swe-agent[bot]
add65451fd Add fpa regression test for fp.to_real denormal encoding fix 
Adds src/test/fpa.cpp with test_fp_to_real_denormal() exercising the
bug reported in the issue: denormal floating-point values in
(_ FloatingPoint 2 24) were getting wrong fp.to_real values because
mk_to_real was not subtracting the normalization shift lz from the
exponent.

Tests verify:
- The specific denormal from the bug report is NOT > 1.0
- Two other denormals have correct real values (0.5 and 0.125)
- A normal value is correctly identified as > 1.0

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-25 22:04:03 +00:00
copilot-swe-agent[bot]
af2e60c069 code-simplifier: fix JavaDoc formatting in Context.java and extract ternary in Solver.cs 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-25 21:49:23 +00:00
copilot-swe-agent[bot]
db98f1e2f7 Initial plan 2026-02-25 21:45:23 +00:00
Nikolaj Bjorner
fba1e4b648
Merge pull request #8737 from Z3Prover/copilot/fix-refutational-soundness-bug 
Fix soundness bug: RNE/RNA overflow to ±infinity in symbolic Real-to-FP conversion
 2026-02-25 13:34:59 -08:00
Nikolaj Bjorner
412c56ecc8
Merge pull request #8767 from Z3Prover/copilot/fix-ubv-to-int-bug 
Fix intblast: assert ubv_to_int(compound) = translation equality
 2026-02-25 13:32:40 -08:00
Nikolaj Bjorner
c51f45bf5e
Merge pull request #8766 from Z3Prover/copilot/fix-critical-bugs-from-discussion 
Fix critical static-analysis true positives: null deref, division by zero, dangling pointer
 2026-02-25 09:22:45 -08:00
Lev Nachmanson
a7ea22f24f remove an unnecessary template from levelwise 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-25 07:03:23 -10:00
Lev Nachmanson
66d19c4d3f
Merge pull request #8770 from Z3Prover/lws 
Optimizes the substitution of a non-nullified witness by an lc or a disc if they are added to the projection and do not vanish.
 2026-02-25 06:25:58 -10:00
Lev Nachmanson
0835420cc1 change the default of param lws_subs_witness_disc to true 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2026-02-24 15:24:35 -10:00
copilot-swe-agent[bot]
4860d57ae9 Fix intblast ubv_to_int bug: add bv2int axioms for compound expressions 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-25 00:46:13 +00:00
copilot-swe-agent[bot]
ae4cb5557a Fix true positive critical bugs from static analysis discussion #8764 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-25 00:41:59 +00:00
copilot-swe-agent[bot]
1b68ee5f30 Initial plan 2026-02-25 00:20:49 +00:00
Nikolaj Bjorner
5ccc2cd8c0 recompile 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-24 16:17:46 -08:00
Nikolaj Bjorner
b9d098fc0a
Merge pull request #8765 from Z3Prover/copilot/update-grep-search-methods 
api-coherence-checker: include Rust traits and trait implementations in search
 2026-02-24 16:17:02 -08:00
Nikolaj Bjorner
0064a2d70a
Merge branch 'master' into copilot/update-grep-search-methods 2026-02-24 16:16:50 -08:00
copilot-swe-agent[bot]
4a29c77aa2 Initial plan 2026-02-25 00:15:14 +00:00
Nikolaj Bjorner
48de0f8a5e updated compiled workflows 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2026-02-24 16:12:53 -08:00
Nikolaj Bjorner
6a4e8de5f3
Merge pull request #8761 from Z3Prover/copilot/add-compilation-database 
csa-analysis: add compilation database to CMake configure step
 2026-02-24 16:11:43 -08:00
copilot-swe-agent[bot]
bf934398d7 Update api-coherence-checker to search for Rust traits and trait implementations 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-25 00:10:31 +00:00
copilot-swe-agent[bot]
a0a44c5571 Initial plan 2026-02-25 00:08:53 +00:00
Nikolaj Bjorner
c580bcd4d1
Merge pull request #8762 from TempuraFramework/master 
Add missing Java API for `as-array`
 2026-02-24 13:51:33 -08:00
copilot-swe-agent[bot]
54b0746033 Add compilation database to csa-analysis workflow 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2026-02-24 20:05:15 +00:00
copilot-swe-agent[bot]
11cfaf6dfd Initial plan 2026-02-24 20:01:56 +00:00
Ruijie Fang
6b79297252 Add missing Java API method for as-array 2026-02-24 13:55:39 -06:00
Nikolaj Bjorner
c282ece605
Merge pull request #8760 from Z3Prover/copilot/add-workflow-for-z3-and-csa 
Add weekly Clang Static Analyzer (CSA) agentic workflow with Discussion reporting
 2026-02-24 11:48:11 -08:00
Nikolaj Bjorner
23d8bdd47c
Merge pull request #8758 from Z3Prover/copilot/fix-issues-except-rust 
Add missing solver/optimize API methods across Java, .NET, OCaml, Go, and TypeScript bindings
 2026-02-24 11:47:09 -08:00
Ruijie Fang
4f4e657449
Merge branch 'Z3Prover:master' into master 2026-02-24 13:39:36 -06:00