mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-21 16:16:38 +00:00
Code Activity
19019 commits 23 branches 48 tags 157 MiB
Commit graph

19019 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner 182979771f disable verbose 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-21 10:41:31 -07:00
Jakob Rath 934b2ad5ef update target selection to what was intended 2024-03-21 13:53:26 +01:00
Jakob Rath 342db52558 fix 2024-03-21 12:03:52 +01:00
Jakob Rath acd05686e4 relevant level should be based on what's to appear in the lemma 2024-03-21 11:05:55 +01:00
Jakob Rath 7d1a57b6e9 remove commented code 2024-03-20 15:38:42 +01:00
Jakob Rath 7922ee3e82 debug output 2024-03-20 15:37:34 +01:00
Jakob Rath fd9c931168 skip entry for origin variable 2024-03-20 15:37:03 +01:00
Jakob Rath 23ca9d9fc5 select targets, try generic/specific version of projection 2024-03-20 15:26:33 +01:00
Jakob Rath de809932eb refactor, minor fixes 2024-03-20 14:33:30 +01:00
Jakob Rath ef6b5f82d1 relax level constraint 2024-03-20 13:39:16 +01:00
Jakob Rath 91a9feb5a8 warnings 2024-03-20 12:16:24 +01:00
Jakob Rath f47fbdd714 Move interval projection out of viable 2024-03-20 12:11:14 +01:00
Jakob Rath 5339a2f70f Don't access solver_interface directly 2024-03-20 10:16:40 +01:00
Jakob Rath a34bb99db3 Use variable from violated interval as origin 2024-03-20 10:15:25 +01:00
Jakob Rath 3a11350142 Move helper functions 2024-03-20 10:10:27 +01:00
Nikolaj Bjorner 6eeb022048 fix encoding for sdiv exposed by zQkAOXjEDwgm 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-19 16:00:09 -07:00
Nikolaj Bjorner ffe7b46e74 unsigned cast 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-19 15:02:42 -07:00
Jakob Rath f5eb457bee fix propagate_from_containing_slice dependency 2024-03-19 16:13:28 +01:00
Jakob Rath 489a1495d2 dep 2024-03-19 14:23:44 +01:00
Jakob Rath adc5313916 remove debug output 2024-03-19 10:11:06 +01:00
Jakob Rath 148eafaaf0 Merge remote-tracking branch 'origin/master' into poly 2024-03-19 09:50:24 +01:00
dependabot[bot] 1a7437144c
Bump docker/build-push-action from 5.2.0 to 5.3.0 (#7170) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 5.2.0 to 5.3.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v5.2.0...v5.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-03-18 15:25:58 -07:00
cctv130 18365907a2
Update util.h (#7169) 2024-03-17 20:29:27 -07:00
Nikolaj Bjorner b8a69987c3 fix #7165 2024-03-17 16:33:40 -07:00
Nikolaj Bjorner fb824bee54 inline unfolding if it is linear or constant. 2024-03-16 13:02:26 -07:00
Nikolaj Bjorner 3555b25317 Merge branch 'poly' of https://github.com/z3prover/z3 into poly 2024-03-15 08:55:16 -07:00
Nikolaj Bjorner e4cc6e29ca fix case when interval is full 2024-03-15 08:55:07 -07:00
Jakob Rath aa1285288e Fix integration of propagate_from_containing_slice 2024-03-15 15:08:12 +01:00
Jakob Rath dfb200a3c9 propagation from containing slice depends on concrete values 2024-03-15 12:31:31 +01:00
dependabot[bot] 6450a7a0b8
Bump docker/build-push-action from 5.1.0 to 5.2.0 (#7159) 
Bumps [docker/build-push-action](https://github.com/docker/build-push-action) from 5.1.0 to 5.2.0.
- [Release notes](https://github.com/docker/build-push-action/releases)
- [Commits](https://github.com/docker/build-push-action/compare/v5.1.0...v5.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-03-14 16:54:01 -07:00
Jakob Rath 5704e8d154
fix intblast is_bounded (#7163) 2024-03-14 08:48:38 -07:00
Jakob Rath 2102db2df8 Fix viable entry reduction (case new_lo == new_hi) 2024-03-14 15:09:21 +01:00
Jakob Rath f6c99585f3 fix warning 2024-03-14 15:08:00 +01:00
Nikolaj Bjorner 82dc254d0e Merge branch 'poly' of https://github.com/z3prover/z3 into poly 2024-03-13 16:20:54 -07:00
Nikolaj Bjorner c2f8dd9a02 use -> types 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-13 16:20:51 -07:00
Nikolaj Bjorner 1f0a6c051a update slice/offset claim structures to allow for equal variable. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-13 11:49:11 -07:00
Nikolaj Bjorner 1e9381c2f6 update slice/offset claim structures to allow for equal variable. 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-13 11:48:09 -07:00
Jakob Rath 5d1602b6c7 print validation failures 2024-03-13 14:12:10 +01:00
Jakob Rath 7da7e99ca2 try_umul_blast 2024-03-13 14:01:07 +01:00
Jakob Rath 8a16631fd1 fix intblast is_bounded 2024-03-13 12:37:37 +01:00
Jakob Rath d07d57c240 remove leftovers from earlier commit 2024-03-13 09:42:08 +01:00
Jakob Rath 22d80277ae signed_constraint == 2024-03-12 16:26:27 +01:00
Jakob Rath 35e3211ca8 display 2024-03-12 16:24:28 +01:00
Jakob Rath 450ed26440 implement 'is_full' case 2024-03-12 16:23:39 +01:00
Jakob Rath df85eeb581 viable explanation depends on assignment 2024-03-12 16:20:44 +01:00
Jakob Rath 58c14ba2f9 write validation in bv format too 2024-03-12 16:18:39 +01:00
Jakob Rath 37bf5fefca fix extract axiom 2024-03-12 13:47:23 +01:00
Nikolaj Bjorner 0b3bbc2972 #7158 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2024-03-11 18:19:43 -07:00
Jakob Rath 7311af699c fix 2024-03-11 15:02:55 +01:00
Jakob Rath d11c2b3265 Add ule_constraint simplification 2024-03-11 14:20:29 +01:00