mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 19:22:28 +00:00
Code Activity
19045 commits 49 branches 53 tags 182 MiB
Commit graph

19045 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
11ed99089b remove restart 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-24 09:32:04 -07:00
Nikolaj Bjorner
b2bc51e9ac fix bug 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 16:44:44 -07:00
Nikolaj Bjorner
0b8177c7d6 generalize factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 16:23:37 -07:00
Nikolaj Bjorner
69dd247cfc re-add tabu override 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 09:25:34 -07:00
Nikolaj Bjorner
a2b8b724b2 fixes to semantics 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 09:20:11 -07:00
Nikolaj Bjorner
3884fc7b11 add factoring 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-23 05:05:10 -07:00
Nikolaj Bjorner
cfc4448be4 update sls_test 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-21 22:32:58 -07:00
Nikolaj Bjorner
80e7f6d355 disable tabu when using reset moves 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-21 22:28:50 -07:00
Nikolaj Bjorner
42289c2f44 disable fail restart 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-21 19:51:09 -07:00
Nikolaj Bjorner
988a46dbc4 fix division by 0 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-21 17:32:58 -07:00
Nikolaj Bjorner
f6dd6a38cd update 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-20 11:51:52 -07:00
Nikolaj Bjorner
8b281b625e updates 2024-08-19 16:04:28 -07:00
Nikolaj Bjorner
de8faa231f fixes to ite and other 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-16 16:48:12 -07:00
Nikolaj Bjorner
98f4b5103e refactor basic plugin and clause generation 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-15 14:04:03 -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
Nikolaj Bjorner
438389771d fix build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-14 16:20:24 -07:00
Nikolaj Bjorner
7d765ddb6b fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-14 15:55:30 -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
Nikolaj Bjorner
4978f5a9ac fixes 2024-08-13 21:38:38 -07:00
Nikolaj Bjorner
74c6eafde4 Update sls_test.cpp 2024-08-13 15:20:44 -07:00
Nikolaj Bjorner
afef727b88 bug fixes 2024-08-13 14:50:17 -07:00
Nikolaj Bjorner
920c207a27 fix typo 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-08-12 19:23:11 -07:00
Lev Nachmanson
83f47bd84b wasm build problem 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
 2024-08-12 15:36:32 -10:00
Nikolaj Bjorner
849385c6a1 bugfixes in sls-arith 2024-08-12 17:42:52 -07: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
8dac67d713 evolve sls arith 2024-08-06 15:07:29 -07: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