mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-30 03:02:29 +00:00
Code Activity
10916 commits 49 branches 53 tags 180 MiB
Commit graph

10916 commits

This branch
This branch
All branches
Author SHA1 Message Date
Nikolaj Bjorner
115e6e9efe Update azure-pipeline.vs.yaml for Azure Pipelines 2019-06-04 00:46:09 +02:00
Nikolaj Bjorner
3297ab181e Update azure-pipeline.vs.yaml for Azure Pipelines 2019-06-04 00:45:18 +02:00
Nikolaj Bjorner
5ea5cf4937 Update azure-pipeline.vs.yaml for Azure Pipelines 2019-06-04 00:42:35 +02:00
Nikolaj Bjorner
35e2e6c82c Update azure-pipeline.vs.yaml for Azure Pipelines 2019-06-04 00:37:30 +02:00
Nikolaj Bjorner
5ae1de314d Update azure-pipeline.vs.yaml for Azure Pipelines 2019-06-04 00:11:16 +02:00
Nikolaj Bjorner
f2098dc863 vs pipeline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-03 15:08:03 -07:00
Nikolaj Bjorner
53514281d2 vs2017 pipeline 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-03 14:56:33 -07:00
Nikolaj Bjorner
d19eae1876 pipe v1 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-03 12:41:43 -07:00
Nikolaj Bjorner
11d7fca4d6 integrating another update by jfc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-03 08:15:11 -07:00
Nikolaj Bjorner
8cc92e0730 remove stale file 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-02 19:23:04 -07:00
Nikolaj Bjorner
1155a29c6e spelling 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-02 17:26:49 -07:00
Nikolaj Bjorner
51b75a132c signed char -> int, update mk_util to catch warnings on fptest, thanks to jfc 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-02 17:22:36 -07:00
Nikolaj Bjorner
6fdef691e5 fix #2316 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-02 16:37:38 -07:00
Nikolaj Bjorner
1d46d5c870 use signed char per porting issue for ARM/64 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-02 15:53:32 -07:00
Nikolaj Bjorner
cccd37101e fix #2314 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-06-01 20:34:58 -07:00
Nikolaj Bjorner
14923bad52
Merge pull request #2315 from waywardmonkeys/reduce-copies 
Use const& to reduce copies.
 2019-06-02 05:04:21 +02:00
Bruce Mitchener
a12de12515 Use const& to reduce copies. 2019-06-02 09:58:32 +07:00
Nikolaj Bjorner
62de187d02
Merge pull request #2311 from waywardmonkeys/fix-reorder-warning 
Fix -Wreorder warning.
 2019-06-02 02:57:24 +02:00
Nikolaj Bjorner
3c3e5d7f7d
Merge pull request #2313 from waywardmonkeys/fix-cppapi-comment-typo 
Fix C++ API comment typo.
 2019-06-02 02:56:52 +02:00
Nikolaj Bjorner
a6db02c6e3
Merge pull request #2312 from waywardmonkeys/fix-unused-variable-warning 
Fix some unused variable warnings.
 2019-06-02 02:56:32 +02:00
Bruce Mitchener
17a0d75436 Fix C++ API comment typo. 2019-06-01 15:57:56 +07:00
Bruce Mitchener
960b8566f5 Fix some unused variable warnings. 2019-06-01 15:45:17 +07:00
Bruce Mitchener
759811b308 Fix -Wreorder warning. 2019-06-01 15:44:21 +07:00
Nikolaj Bjorner
60e4cad7f1 increase minor version number 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-31 17:01:42 -07:00
Nikolaj Bjorner
01f6489892 fix #2310 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-31 16:22:49 -07:00
Nikolaj Bjorner
dd452e0ac1 eq 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-31 15:29:27 -07:00
Nikolaj Bjorner
e79542cc68 fix #2309 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-31 07:46:11 -07:00
Nikolaj Bjorner
f1dee935d0 remove UNREACHABLE 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 17:07:00 -07:00
Nikolaj Bjorner
f11cb77c3d merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 16:15:55 -07:00
Nikolaj Bjorner
8893913c98 remove internal referenes to set_activity 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 16:06:05 -07:00
Nikolaj Bjorner
fc4c162e31 add clause proof module, small improvements to bapa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 15:59:28 -07:00
Nikolaj Bjorner
f128398bf9 add clause proof module, small improvements to bapa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 15:57:19 -07:00
Nikolaj Bjorner
48fc3d752e add clause proof module, small improvements to bapa 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 15:49:19 -07:00
Nikolaj Bjorner
4d30639fd7 merge dotnetcore into dotnet 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-30 13:01:48 -07:00
Nikolaj Bjorner
6604aab1a2 remove dotnet as a build option 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-29 17:08:45 -07:00
Nikolaj Bjorner
30411b319a update build scripts 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-29 17:02:45 -07:00
Nikolaj Bjorner
25c93410b1 add #2298 to regression/example 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-29 07:24:42 -07:00
Nikolaj Bjorner
857dc0fcec
Merge pull request #2294 from AltGr/fix-ml-static-linking 
ml API + static linking: small fix on top of #2292
 2019-05-29 16:16:17 +02:00
Nikolaj Bjorner
8f36868285 fix #2300 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-27 09:35:55 -07:00
Nikolaj Bjorner
f99384c6a3 fix nightly regression from solve-eqs context solver addition 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-27 04:17:43 -07:00
Nikolaj Bjorner
2d0ff7d68a print literals more compactly 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-24 15:39:35 +02:00
Nikolaj Bjorner
8243139fb0 handle div 0 cases as it is uninterpreted #1683 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-24 07:00:56 +04:00
Nikolaj Bjorner
e49e5d7145 fix #2297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-24 06:55:06 +04:00
Louis Gesbert
5c0ad963c1 Fix z3 static link options 2019-05-23 09:49:32 +02:00
Nikolaj Bjorner
faf4ba8309 add check for contravariance to fix #2256 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-22 18:32:57 +04:00
Nikolaj Bjorner
082a0f4df4 add get_lstring per #2286 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-22 18:32:57 +04:00
Nikolaj Bjorner
b2845d888e add get_lstring per #2286 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2019-05-22 18:32:57 +04:00
Nikolaj Bjorner
112e13eeea
Merge pull request #2292 from AltGr/ocaml-static-linking 
Fix and enable OCaml static linking by default when --staticlib is specified
 2019-05-22 17:26:00 +04:00
Louis Gesbert
9bb0c882fa OCaml API build: provide static linking options by default 
when --staticlib is enabled, the linker will still choose to
dynamically link upon encountering `-lz3` when generating an
executable through OCaml.

The interaction between the underlying C linker and OCaml make it very
hard to choose the static version instead. The present patch works
around this issue by copying `libz3.a` to `libz3-static.a`, and using
`-lz3-static` instead: the static version is chosen since no dynamic
one is found.

One can get back to dynamically linking by compiling without
`--staticlib`, or switching back to `-lz3`, but will in the latter
case run into the same problem with specifying the option; if that
needs to be made easier, we could provide two versions of the `cm(x)a`
which differ only by their linking options.

One last solution would be to remove `lz3` altogether from the linking
options included in the cm(x)a, requiring either `-lz3` or
`-lz3-static` to be specified at link time. Simpler and most flexible,
but requires an update of all users that link with the Z3 ml api...
 2019-05-21 17:45:19 +02:00
Louis Gesbert
8d5466e781 OCaml / static: fix linking options 2019-05-21 16:09:18 +02:00