mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity
18751 commits 23 branches 48 tags 156 MiB
Commit graph

18751 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 187c2c6cae
Revert "add scoped vector unit test (#7307)" 
This reverts commit 2ae3d87b21.
 2024-07-30 11:33:36 -07:00
LiviaSun 2ae3d87b21
add scoped vector unit test (#7307) 
* add scoped vector unit test

* fix dlist tests

* add new scoped vector invariants
 2024-07-29 11:08:54 -07:00
David Seifert 2ce89e5f49
Gcc 15 two phase (#7313) 
* Fix `-Wclass-memaccess`

* Fix for GCC 15 two-phase lookup

* GCC 15 is more aggressive about checking dependent names:
  https://gcc.gnu.org/git/?p=gcc.git;a=commitdiff;h=r15-2117-g313afcfdabeab3

Bug: https://bugs.gentoo.org/936634
 2024-07-29 11:07:10 -07:00
Nikolaj Bjorner 25e683e4e1 fix finalize method 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-28 19:10:30 -07:00
Nikolaj Bjorner ac7014a68b expose public 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-29 03:18:20 +02:00
Nikolaj Bjorner f94500c3ca fix #7309 2024-07-28 13:18:08 +02:00
Nikolaj Bjorner 5f6bb3db3e fix #7311 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-27 08:26:47 +02:00
dependabot[bot] 1e6b13741c
Bump docker/build-push-action from 6.4.0 to 6.5.0 (#7304) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.4.0 to 6.5.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v6.4.0...v6.5.0)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2024-07-22 15:42:40 -07:00
Nikolaj Bjorner b535509cca remove crashing test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-22 08:43:22 -07:00
Nikolaj Bjorner 2013cd13b2
Update coverage.yml 
run code coverage on pull requests
 2024-07-21 21:08:53 -07:00
Nikolaj Bjorner 966c9a3764
Revert "new heap invariants (#7298)" (#7303) 
This reverts commit 80ac7b3438.
 2024-07-21 21:07:09 -07:00
LiviaSun 3d014f8b33
add new hashtable unit tests (#7297) 
* add new hashtable unit tests

* add copyright

* use VERIFY instead of assert
 2024-07-19 20:34:29 -07:00
LiviaSun 49dc1bb721
add new permutation class invariant (#7299) 
* new heap invariants

* change ENSURE to SASSERT for unit test heap

* change SASSERT to VERIFY

* new permutation invariant

* remove heap changes

* use bool_vector
 2024-07-19 19:27:23 -07:00
Nikolaj Bjorner 5003d41cdb
Revert "New invariant for dlist (#7294)" (#7301) 
This reverts commit cf4d0e74a5.
 2024-07-19 19:11:54 -07:00
LiviaSun 80ac7b3438
new heap invariants (#7298) 
* new heap invariants

* change ENSURE to SASSERT for unit test heap

* change SASSERT to VERIFY
 2024-07-19 14:03:21 -07:00
LiviaSun bc636d7ee0
new hashtable.h invariants (#7296) 
* add copyright for dlist unit test

* new hashtable invariants

* add copyright
 2024-07-19 14:01:42 -07:00
Nikolaj Bjorner 08b6338061 fix signature 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-18 10:19:57 -07:00
Nikolaj Bjorner 458d8b033a remove wsp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-18 10:11:15 -07:00
LiviaSun 9803e9ef6e
unit tests for dlist.h (#7293) 2024-07-18 10:08:41 -07:00
LiviaSun cf4d0e74a5
New invariant for dlist (#7294) 
* unit tests for dlist.h

* new invariant for dlist: should be circular. avoid infinite loop

* remove dlist test commit

* format

* format

* Update dlist.h

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-18 10:06:58 -07:00
dependabot[bot] 9073da4ee6
Bump docker/build-push-action from 6.3.0 to 6.4.0 (#7289) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.3.0 to 6.4.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v6.3.0...v6.4.0)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2024-07-15 16:54:27 -07:00
dependabot[bot] a2c3ce5c8b
Bump docker/build-push-action from 6.2.0 to 6.3.0 (#7280) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.2.0 to 6.3.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v6.2.0...v6.3.0)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2024-07-15 13:07:37 -07:00
LiviaSun b0069010f8
add new ema invariant (#7288) 2024-07-15 13:07:12 -07:00
Nikolaj Bjorner 374609bd46 kludge to address #7232, probably superseeded by planned revision to setup/pypi 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-07-08 16:54:09 -07:00
Nikolaj Bjorner af1f0e3184 fix #7268 2024-07-08 14:50:38 -07:00
Nikolaj Bjorner 6e069c1f41 remove macro distinction #7270 2024-07-08 13:56:34 -07:00
Lev Nachmanson 18b6087b72 trigger the build with a comment change 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-07-08 11:43:24 -07:00
Sergey Bronnikov 1da132005a
Fix a comment for Z3_solver_from_string (#7271) 
Z3_solver_from_string accepts a string buffer with solver
assertions, not a string buffer with filename.
 2024-07-02 07:09:33 -07:00
dependabot[bot] facc7d8de2
Bump docker/build-push-action from 6.1.0 to 6.2.0 (#7269) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.1.0 to 6.2.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v6.1.0...v6.2.0)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2024-07-01 15:43:36 -07:00
Nikolaj Bjorner 8de2544abb set clean shutdown for local search and re-enable local search when it parallelizes with PB solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-06-30 16:06:51 -07:00
dependabot[bot] b2b3bab246
Bump docker/build-push-action from 6.0.0 to 6.1.0 (#7265) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.0.0 to 6.1.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v6.0.0...v6.1.0)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  dependency-type: direct:production
  update-type: version-update:semver-minor
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2024-06-26 09:15:55 -07:00
Nikolaj Bjorner 8e482df62a fix #7264 2024-06-21 08:37:23 -07:00
Nikolaj Bjorner c137ef7fba disable publish and signing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-06-20 11:10:55 -07:00
Nikolaj Bjorner abea0b724c disable publish and signing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-06-20 09:43:26 -07:00
Nikolaj Bjorner b5c3a6a2e0 skip signing 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-06-19 18:28:07 -07:00
Nikolaj Bjorner 4ca59c51cb update to macOS-latest 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-06-19 17:25:56 -07:00
Nikolaj Bjorner 2654d80aaf revert nightly to 2_28 manylinux 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-06-19 16:19:48 -07:00
Nikolaj Bjorner 3bf2b3f741 fix #7260 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-06-19 15:37:20 -07:00
dependabot[bot] 223b65bd5a
Bump docker/build-push-action from 5.3.0 to 6.0.0 (#7257) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 5.3.0 to 6.0.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v5.3.0...v6.0.0)

---
updated-dependencies:
- dependency-name: docker/build-push-action
  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>
 2024-06-19 15:29:53 -07:00
dependabot[bot] 758d886fac
Bump braces from 3.0.2 to 3.0.3 in /src/api/js (#7261) 
Bumps [braces](https://github.com/micromatch/braces) from 3.0.2 to 3.0.3.
- [Changelog](https://github.com/micromatch/braces/blob/master/CHANGELOG.md)
- [Commits](https://github.com/micromatch/braces/compare/3.0.2...3.0.3)

---
updated-dependencies:
- dependency-name: braces
  dependency-type: indirect
...

Signed-off-by: dependabot[bot] <support@github.com>
Co-authored-by: dependabot[bot] <49699333+dependabot[bot]@users.noreply.github.com>
 2024-06-19 15:29:38 -07:00
Lev Nachmanson bf3615d4fb fix lemma logging in nlsat 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-06-17 13:14:31 -07:00
Lev Nachmanson e4b3df2189 remove unused column_info.h 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-06-17 12:58:16 -07:00
Nikolaj Bjorner c0b4d02ae2 update containers for Python, first steps to address #7232 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-06-17 08:06:21 -07:00
Nikolaj Bjorner ef86f5fcc2 add partial evaluation cases for algebraic data-types for recursive functions. 2024-06-16 16:07:16 -07:00
Nikolaj Bjorner 81ebd52f61 #7207 
the utility that computes case analysis is brittle when the body of a function contains ite expressions that are not relevant to recursive unfolding.
The fold-rec occurrences that get inserted to harness large case splits work against throttling case generation: they get treated as recursive functions that have to be guarded.
 2024-06-16 15:04:42 -07:00
Nikolaj Bjorner 972d35204c reshuffle priorities on multiplication allow non-determinism. 2024-06-15 10:47:10 -07:00
Nikolaj Bjorner 01e47bfe26 fix #7245 2024-06-15 02:29:32 -07:00
Nikolaj Bjorner a6b502779b fix #7252 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-06-13 17:52:17 -07:00
Nikolaj Bjorner 35c1cacf44 fix #7248 2024-06-12 14:26:35 -07:00
Nikolaj Bjorner b831a589e5 fixes to #7250 2024-06-12 08:50:24 -07:00