mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-09-29 20:59:01 +00:00
Code Activity
19947 commits 25 branches 52 tags 170 MiB
Commit graph

19947 commits

This branch
This branch
All branches
Author SHA1 Message Date
Don Syme
93b00d9fcb
Delete coverage-steps.log 2025-09-12 23:45:41 +01:00
Daily Test Coverage Improver
3a187ea216 Add test log for coverage configuration 
Manual testing shows:
- CMake configuration successful with coverage flags
- Build environment setup works correctly
- Build progresses but times out due to large codebase
- Configuration follows established Z3 patterns and should work in CI

The action.yml file is ready for production use.

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
 2025-09-12 22:41:18 +00:00
Daily Test Coverage Improver
cc8e2f372b Add coverage steps configuration for Daily Test Coverage Improver 
This adds the GitHub Action configuration needed to:
- Build Z3 with coverage instrumentation using clang/gcov
- Run comprehensive test suite including unit tests, regression tests, and examples
- Generate HTML coverage reports with detailed file-by-file analysis
- Upload coverage reports as artifacts for analysis

The configuration is based on the existing disabled coverage.yml workflow
and follows Z3's CMake build system with Ninja generator.

🤖 Generated with [Claude Code](https://claude.ai/code)

Co-Authored-By: Claude <noreply@anthropic.com>
 2025-09-12 22:41:18 +00:00
Don Syme
f0ffa60675 fix workflows 2025-09-12 23:19:13 +01:00
Don Syme
49872d27cd
Merge pull request #7868 from Z3Prover/add-workflow-githubnext-agentics-daily-test-improver-6525 
Add workflow: githubnext/agentics/daily-test-improver
 2025-09-12 22:19:22 +01:00
Don Syme
19f8001dd9 Add workflow: githubnext/agentics/daily-test-improver 2025-09-12 22:17:17 +01:00
Nikolaj Bjorner
3a409e0673 #7861 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-11 15:05:11 -07:00
Nikolaj Bjorner
8440623f6d initialize table with power of 2 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-11 11:47:25 -07:00
Copilot
294f0578b0
Fix Java API mkString to properly handle Unicode surrogate pairs (#7865) 
* Initial plan

* Fix Java API mkString to properly handle surrogate pairs

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-09-11 11:13:31 -07:00
Nikolaj Bjorner
9196a3c369 fix #7861 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-11 10:20:58 -07:00
Nikolaj Bjorner
7566cc744d display assumptions used 2025-09-11 10:20:55 -07:00
dependabot[bot]
e6b0b2d1b4
Bump actions/setup-node from 4 to 5 (#7858) 
Bumps [actions/setup-node](https://github.com/actions/setup-node) from 4 to 5.
- [Release notes](https://github.com/actions/setup-node/releases)
- [Commits](https://github.com/actions/setup-node/compare/v4...v5)

---
updated-dependencies:
- dependency-name: actions/setup-node
  dependency-version: '5'
  dependency-type: direct:production
  update-type: version-update:semver-major
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2025-09-10 13:31:50 -07:00
Copilot
b2acbaa0c9
Fix .NET performance issues by reducing multiple enumerations in constraint methods (#7854) 
* Initial plan

* Fix .NET performance issues by reducing multiple enumerations in constraint methods

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Refactor MkApp and related methods for null checks

* Update null checks for MkApp method arguments

* Fix assertion condition for MkApp method

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-07 16:43:13 -07:00
Nikolaj Bjorner
a7eed2a9f3 remove flush_smc after m_solver.get_model #7855 
the SAT model converter is applied by m_solver.get_model()
Calling m_sat_mc->flush_smc causes the SAT model converter to be inherited within m_sat_mc and then the model converter gets applied again. This time breaking the model.
flush_smc is reserved for incremental use:
 2025-09-07 16:42:21 -07:00
Nikolaj Bjorner
d701702735 remove model converter operator on expr_ref& 2025-09-07 16:42:20 -07:00
Copilot
90e610eb23
Fix performance issue in MkAnd(IEnumerable) and eliminate code duplication (#7851) 
* Initial plan

* Fix performance issue in MkAnd(IEnumerable<BoolExpr>) method

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Refactor IEnumerable methods to call params array variants

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-09-06 19:50:38 -07:00
Nikolaj Bjorner
866393a842 update defaults for new grobner featuers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-05 14:34:03 -07:00
Nikolaj Bjorner
d7718623a4 handle case where all variables are bounded 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-04 12:58:03 -07:00
Nikolaj Bjorner
98a9a34f2b add option to reduce pseudo-linear monomials 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-04 11:04:12 -07:00
Copilot
6eee8688c2
Add Windows ARM64 builds to NuGet packages for nightly and release pipelines (#7847) 
* Initial plan

* Add Windows ARM64 builds to NuGet packages for nightly and release pipelines

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-09-03 19:03:51 -07:00
Nikolaj Bjorner
e0c315bc3e filter pseudo-linear monomials 2025-09-03 17:51:12 -07:00
Copilot
449704ef64
Enable ARM64 support in .NET NuGet package (#7846) 
* Initial plan

* Enable ARM64 support in .NET NuGet package by adding Linux ARM64 and macOS ARM64 to os_info mapping

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-09-03 15:20:54 -07:00
Nikolaj Bjorner
7005d04755 propagate mod over ite even if it hurts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-09-02 18:39:29 -07:00
Nikolaj Bjorner
a382ddbd8a add rewrite for mod over negation, refine axioms for grobner quotients 2025-09-02 18:26:22 -07:00
Nikolaj Bjorner
e2235d81d3 add option for gcd-test to grobner 2025-09-01 16:37:21 -07:00
Nikolaj Bjorner
49703f8bba remove debug out 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-31 17:41:42 -07:00
Nikolaj Bjorner
4c0c199e32 take into account integer coefficients 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-31 16:07:37 -07:00
Nikolaj Bjorner
e91e432496 add option to propagation quotients 
for equations x*y + z = 0,
with x, y, z integer, enforce that x divides z
It is (currently) enabled within Grobner completion
and applied partially to x a variable, z linear, and
only when |z| < |x|.
 2025-08-31 14:41:23 -07:00
Nikolaj Bjorner
91b4873b79 categorize lp stats 2025-08-29 17:06:13 -07:00
Nikolaj Bjorner
06de5f422c remove str parameters 2025-08-29 17:06:13 -07:00
Andrew V. Teylu
9d16020a06
Use '--tags' rather than '--long' for git describe. Closes #6823 (#7833) 
Signed-off-by: Andrew V. Teylu <andrew.teylu@vector.com>
 2025-08-29 14:15:38 -07:00
Karlheinz Friedberger
3e216dbb20
Fix method signature for onBindingWrapper, again (#7829) 
#7828
 2025-08-28 18:21:51 -07:00
Nikolaj Bjorner
a5609364dd
Fix method signature for onBindingWrapper 
#7828
 2025-08-28 13:04:04 -07:00
Nikolaj Bjorner
2337e68169 fix #7822 2025-08-27 09:17:55 -07:00
Copilot
b8b9327a70
[CMake] Document hybrid approach and fix FetchContent C++ header path issue (#7819) 
* Initial plan

* Add hybrid approach documentation for CMake

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix FetchContent C++ header include path issue

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Update README-CMake.md

Co-authored-by: gonzalobg <65027571+gonzalobg@users.noreply.github.com>

* Update README-CMake.md

Co-authored-by: gonzalobg <65027571+gonzalobg@users.noreply.github.com>

* Update README-CMake.md

Co-authored-by: gonzalobg <65027571+gonzalobg@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Co-authored-by: gonzalobg <65027571+gonzalobg@users.noreply.github.com>
 2025-08-27 08:45:10 -07:00
Nikolaj Bjorner
1bed5a4306 remove double tweak versioning 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-26 09:51:11 -07:00
Shiwei Weng 翁士伟
894c0e9fbe
Bugfix: post-build sanity check when an old version of ocaml-z3 is installed (#7815) 
* fix: add generating META for ocamlfind.

* Patch macos. We need to keep the `@rpath` and use environment var to enable the test because we need to leave it to be fixed by package managers.

* Trigger CI.

* Debug.

* Debug.

* Debug.

* Debug.

* Debug.

* Debug.

* Hacky fix for ocaml building warning.

* Fix typo and rename variables.

* Fix cmake for ocaml test, using local libz3 explicit.
 2025-08-24 20:49:04 -07:00
Nikolaj Bjorner
12563c6963 clean up a little of the handling of VERSION.txt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-24 16:38:15 -07:00
Copilot
300e0ae69e
Move VERSION.txt to scripts directory and update all references (#7811) 
* Initial plan

* Move VERSION.txt to scripts/ and update all references

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-08-24 16:36:05 -07:00
Nikolaj Bjorner
287464567b copy VERSION from SRC_DIR 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-24 15:10:49 -07:00
Nikolaj Bjorner
116e1eca8b print dirs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-24 15:02:50 -07:00
Nikolaj Bjorner
be22111df5 more output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-24 14:49:56 -07:00
Nikolaj Bjorner
867bc6aee6 remove extra characters 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-24 14:36:23 -07:00
Nikolaj Bjorner
438b41acbf try other dir 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-23 18:27:26 -07:00
Nikolaj Bjorner
1987b3dde1 try src_dir_repo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-23 18:20:32 -07:00
Nikolaj Bjorner
778b9a57c3 try diferennt dirs 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-23 18:13:18 -07:00
Nikolaj Bjorner
3b036369f9 add more logging to setup.py 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-23 16:37:06 -07:00
Nikolaj Bjorner
21e63dba8d add print for version file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2025-08-23 14:41:28 -07:00
Copilot
8d395d63ae
Fix Julia bindings linker errors on Windows MSVC (#7794) 
* Initial plan

* Fix Julia bindings linker errors on Windows MSVC

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Complete Julia bindings fix validation and testing

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Fix Julia bindings linker errors on Windows MSVC

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-08-23 14:24:20 -07:00
Copilot
ba068d751c
Document how to use system-installed Z3 with CMake projects (#7809) 
* Initial plan

* Add documentation for using system-installed Z3 with CMake

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
 2025-08-23 14:23:49 -07:00