mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity
16747 commits 23 branches 48 tags 157 MiB
Commit graph

16747 commits

This branch
This branch
All branches
Author SHA1 Message Date
dependabot[bot]
c05c75c109
Bump docker/login-action from 1 to 2 (#6068) 2022-06-02 09:57:17 +01:00
dependabot[bot]
f54e8e55de
Bump docker/build-push-action from 2.7.0 to 3.0.0 (#6069) 2022-06-02 09:57:00 +01:00
dependabot[bot]
96e317620c
Bump actions/setup-node from 2 to 3 (#6067) 2022-06-02 09:56:41 +01:00
dependabot[bot]
05c1d6d5d1
Bump actions/upload-artifact from 2 to 3 (#6065) 2022-06-02 09:16:02 +01:00
dependabot[bot]
b8367247f5
Bump actions/checkout from 2 to 3 (#6066) 2022-06-02 09:14:08 +01:00
Nikolaj Bjorner
9190f22eb4 os 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-01 21:23:44 -07:00
Nikolaj Bjorner
6396cfd6e7 os 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-01 21:20:19 -07:00
Naveen
8384c321fc
chore: Set permissions for GitHub actions (#6063) 
Restrict the GitHub token permissions only to the required ones; this way, even if the attackers will succeed in compromising your workflow, they won’t be able to do much.

- Included permissions for the action. https://github.com/ossf/scorecard/blob/main/docs/checks.md#token-permissions

https://docs.github.com/en/actions/using-workflows/workflow-syntax-for-github-actions#permissions

https://docs.github.com/en/actions/using-jobs/assigning-permissions-to-jobs

[Keeping your GitHub Actions and workflows secure Part 1: Preventing pwn requests](https://securitylab.github.com/research/github-actions-preventing-pwn-requests/)

Signed-off-by: naveen <172697+naveensrinivasan@users.noreply.github.com>
 2022-06-01 20:02:45 -07:00
Naveen
b81b771055
chore: Included githubactions in the dependabot config (#6064) 
This should help with keeping the GitHub actions updated on new releases. This will also help with keeping it secure.

Dependabot helps in keeping the supply chain secure https://docs.github.com/en/code-security/dependabot

GitHub actions up to date https://docs.github.com/en/code-security/dependabot/working-with-dependabot/keeping-your-actions-up-to-date-with-dependabot

https://github.com/ossf/scorecard/blob/main/docs/checks.md#dependency-update-tool
Signed-off-by: naveen <172697+naveensrinivasan@users.noreply.github.com>
 2022-06-01 20:02:30 -07:00
Nikolaj Bjorner
9ed7fd9454 Update nightly.yaml for Azure Pipelines 2022-06-01 19:17:27 -07:00
Nikolaj Bjorner
aa8e89c5f3 try macos12 for arm64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-06-01 19:11:17 -07:00
Nikolaj Bjorner
a9d70fca1a fix #6061 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-31 19:09:10 -07:00
Nikolaj Bjorner
e9cff33feb fix #5068 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-30 11:24:58 -07:00
Nikolaj Bjorner
15c47808d6 #6059 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-30 11:03:50 -07:00
Nikolaj Bjorner
da3f31697b fix proof checking for bounds propagation 2022-05-30 10:18:16 -07:00
Nikolaj Bjorner
cb279fba2b fix sign for binary propagation hints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-29 10:32:05 -07:00
Nikolaj Bjorner
bffa7ff2f6 add hint verification, combine bounds/farkas into one rule 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-29 10:12:05 -07:00
Nikolaj Bjorner
36ad377a7d na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-29 09:21:43 -07:00
Nikolaj Bjorner
63b9c4bdf0 for AG 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 18:49:27 -07:00
Nikolaj Bjorner
9ec34d96ce comment out muslinux build 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 18:14:42 -07:00
Nikolaj Bjorner
6abea2de2c fix nightly, fix regression identified by Nuno 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 18:03:15 -07:00
Nikolaj Bjorner
b8532bec7e remove pragma from cpp file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 14:48:38 -07:00
Nikolaj Bjorner
ddc3445707 try to add back musllinux 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 14:47:39 -07:00
Nikolaj Bjorner
35db0ae58b workaround manylinux build failure (it is advertized as a compiler bug) 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 14:34:58 -07:00
Nikolaj Bjorner
d09d37cb10 wt$ 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 14:27:22 -07:00
Nikolaj Bjorner
6b4bc5bd38 remove broken matrix 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 14:26:00 -07:00
Nikolaj Bjorner
e9660016bc remove hardwired image name 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 14:21:23 -07:00
Nikolaj Bjorner
6ce03cd6f0 Update nightly.yaml for Azure Pipelines 2022-05-28 14:18:50 -07:00
Nikolaj Bjorner
0038817656 Update nightly.yaml for Azure Pipelines 2022-05-28 14:13:50 -07:00
Nikolaj Bjorner
48701826f1 indent 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 13:57:03 -07:00
Nikolaj Bjorner
4953b95baa cleanup pre-processor for z3_api.h 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 12:19:39 -07:00
Nikolaj Bjorner
8d980ea704 remove internal configuration 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 12:13:18 -07:00
Nikolaj Bjorner
dd46224a1d use structured proof hints 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-28 09:37:41 -07:00
Nikolaj Bjorner
7da9f12521 expose description of global parameters #6048 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-27 08:50:40 -04:00
Nikolaj Bjorner
de892ed9f2 fix #6054 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-26 15:51:57 -04:00
Nikolaj Bjorner
f77037e9a5 expand select/store when I/J are values #6053 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-25 20:23:43 -04:00
Nikolaj Bjorner
4d8e4b5bd3 fix #6052 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-25 17:21:01 -04:00
Nikolaj Bjorner
8c95dff33b cnf 2022-05-22 09:10:26 -04:00
Nikolaj Bjorner
c850259f89 rw 2022-05-22 07:54:27 -04:00
Nikolaj Bjorner
386c511f54 core opt 2022-05-21 10:27:37 -04:00
Nikolaj Bjorner
127af83c53 remove ad-hoc diagnostics 2022-05-21 10:27:37 -04:00
Nikolaj Bjorner
40fe472e95
nit 2022-05-18 13:23:33 -07:00
Nikolaj Bjorner
363b69f588 fix #6034 2022-05-16 16:44:13 -07:00
Nikolaj Bjorner
f6b2874d7c update to take effect of def_API for callback functions 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-16 10:30:54 -07:00
Nikolaj Bjorner
ca2497eecb na 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-15 12:00:41 -07:00
Nikolaj Bjorner
186a3c58e5 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-15 12:00:25 -07:00
Nikolaj Bjorner
1028c80851 update pretty printer for recursive function filtering 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-15 11:59:41 -07:00
Arie Gurfinkel
7f62fa2b66
Sparse matrix kernel (#6035) 
* Subtle bug in kernel computation

Coefficient was being passed by reference and, therefore, was
being changed indirectly.

In the process, updated the code to be more generic to avoid rational
computation in the middle of matrix manipulation.

* sparse_matrix: fixed handling of 0 in add_var() and add()

particularly in add_var(), without the fix the user is responsible for checking
coefficients for 0.
 2022-05-13 17:30:35 -07:00
Gleb Popov
6f7be77e2b
Buildsystem fixes for FreeBSD. (#6029) 
* Enable thread-local storage on FreeBSD.

* Pass -soname linker flag on FreeBSD.
 2022-05-12 10:54:57 -07:00
Nikolaj Bjorner
7497856ded add ignore int to new arithmetic solvers 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2022-05-11 15:14:22 -07:00