mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 18:29:23 +00:00
Code Activity
19340 commits 46 branches 52 tags 178 MiB
Commit graph

19340 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
b84b4e7f9a fix attribute order 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 11:38:27 -07:00
Nikolaj Bjorner
49ba3bc12f address compiler warnings gcc-13 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 11:33:54 -07:00
Kirill A. Korinsky
cff1e9233f
Avoid broken stack at few places (#7353) 
* Avoid broken stack by degree_lit_num_lt

* Avoid broken stack by fix_dl_var_tactic

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 10:02:54 -07:00
Nikolaj Bjorner
6a68cc55bb #7353 - clear pointer when existing stack 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-26 09:59:56 -07:00
Zhang
c1454dc31c
Fix building with Windows SDK and Clang-CL (#7337) 
* Fix building with Windows SDK and Clang-CL

* Attempt to add Clang-CL to CI build configurations

* Fix typo

* Enable EHsc explicitly when using ClangCL due to it being default turned-off

* Override CMAKE_<LANG>_FLAGS instead due to Z3 resets the _INIT variants
 2024-08-15 13:08:38 -07:00
dependabot[bot]
0612a0ba17
Bump docker/build-push-action from 6.5.0 to 6.6.1 (#7338) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 6.5.0 to 6.6.1.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v6.5.0...v6.6.1)

---
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-08-14 22:09:44 +01:00
Nikolaj Bjorner
656545564d fix #7343 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-14 09:17:05 -07:00
Nikolaj Bjorner
ed17de56d2 fix #7343 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-14 08:51:24 -07:00
Lev Nachmanson
83f47bd84b wasm build problem 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-12 15:36:32 -10:00
Lev Nachmanson
bf34600f08 add release nodes and add the author reference in qfnra_tactic 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-12 08:49:55 -10:00
Lev Nachmanson
f2d35ddc5e more cleanup 2024-08-12 08:32:01 -10:00
Lev Nachmanson
8999e1a340 use standard name conventions and add file headers 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-12 08:29:06 -10:00
Lev Nachmanson
33f0256e20 cleanup 2024-08-11 12:45:36 -10:00
Lev Nachmanson
752c999e0a cleanup 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-11 12:45:36 -10:00
Lev Nachmanson
f81303f2f3 delete unused nlsat_symmetry_checker 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-11 12:45:36 -10:00
Lev Nachmanson
f7905a5d69 remove printouts 2024-08-11 12:45:36 -10:00
Lev Nachmanson
518a8b2bdb fix the build 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-11 12:45:36 -10:00
Lev Nachmanson
4b3a06a3c5 port hybridSMT 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-11 12:45:36 -10:00
Lev Nachmanson
1a5bddb4f0 port more from hybridSMT 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-11 12:45:36 -10:00
Lev Nachmanson
209366ba55 cleanup porting comments 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-11 12:45:36 -10:00
Lev Nachmanson
839594ac12 remove option look_for_0_witness 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-11 12:45:36 -10:00
Lev Nachmanson
0306eff692 port look for 0 witness 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-11 12:45:36 -10:00
Lev Nachmanson
a09e412cf0 cleaning up 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-11 12:45:36 -10:00
Lev Nachmanson
6ce0fcd3ef port sample cell projection 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-11 12:45:36 -10:00
Nikolaj Bjorner
3e518b9e8b fix #7331 2024-08-06 03:54:25 -07:00
Nikolaj Bjorner
26b8d634a3 add max conflict throttle to SAT based QFNIA tactic #7329 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-03 11:34:28 -07:00
Nikolaj Bjorner
52f8eb21fb #7255 #7328 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-03 09:39:19 -07:00
Nikolaj Bjorner
bc8fa67afc #7255 #7328 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-03 09:37:14 -07:00
Nikolaj Bjorner
d6040ee5ab do not copy artifacts from CI pipeline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-03 09:29:11 -07:00
Nikolaj Bjorner
51fcb10b2f shave some overhead from fingerprint hash function #7281 2024-08-02 20:04:50 -07:00
LiviaSun
7c30cbfe48
add scoped_vector invariants and unit tests (#7327) 
* add scoped vector unit test

* fix dlist tests

* add new scoped vector invariants

* remove all loop invariants
 2024-08-02 19:21:40 -07:00
LiviaSun
d2fc085b8c
update heap unit tests (#7324) 
* new heap invariants

* change ENSURE to SASSERT for unit test heap

* change SASSERT to VERIFY

* update heap tests

* update

* remove one invariant
 2024-08-02 18:29:50 -07:00
LiviaSun
fce4b36dad
add apply_permutation tests (#7322) 
* add permutation unit tests

* update test

* update

* Update permutation.cpp

fix macos build

* add apply_permutation tests

* update test

* Update permutation.cpp

* fix permutation tests

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-02 18:29:33 -07:00
Nikolaj Bjorner
ea9fa17f86 add static 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-02 11:38:03 -07:00
Nikolaj Bjorner
23e7dc0356 assert -> SASSERT 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-02 11:36:04 -07:00
LiviaSun
fe594618e6
fix dlist tests (#7323) 2024-08-01 16:56:54 -07:00
LiviaSun
6ba25b888b
add permutation unit tests (#7300) 
* add permutation unit tests

* update test

* update

* Update permutation.cpp

fix macos build

---------

Co-authored-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-01 12:56:26 -07:00
Philip Zucker
e7382d6ff9
Added "&lambda;" pretty printing to python (#7320) 2024-07-31 08:14:16 -07:00
Hari Govind V K
0c16d34eb0
fix #7292 (#7316) 2024-07-30 11:35:33 -07:00
Nikolaj Bjorner
5fcc50f606
Revert "add scoped vector unit test (#7307)" (#7317) 
This reverts commit 2ae3d87b21.
 2024-07-30 11:34:02 -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