3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Commit graph

10107 commits

Author SHA1 Message Date
Nikolaj Bjorner
7bc3b4e381 swap order in equality for emptiness check to deal with rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-22 13:03:55 -08:00
Nikolaj Bjorner
ec36a9c495 fix user push/pop with ba constraints
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-22 12:40:23 -08:00
Nikolaj Bjorner
aeb4d1864d clean up suffix/prefix rewriting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-22 11:39:34 -08:00
Nikolaj Bjorner
498fa87993 seq rewriting fixes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-22 10:48:49 -08:00
Nikolaj Bjorner
7b2590c026 fix is-unit test in seq rewriter
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-21 17:08:33 -08:00
Nikolaj Bjorner
0c1408b30e fixing #1948
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-21 13:48:48 -08:00
Nikolaj Bjorner
8590876d18
Merge pull request #1960 from waywardmonkeys/improve-intra-doc-links
Improve intra-doc linking.
2018-11-21 09:18:16 -08:00
Bruce Mitchener
236f85d82b Improve intra-doc linking. 2018-11-21 19:13:02 +07:00
Nikolaj Bjorner
2cc654081c
Merge pull request #1955 from waywardmonkeys/Z3_bool_to_bool
Switch from using Z3_bool to using bool.
2018-11-20 20:29:28 -08:00
Nikolaj Bjorner
90070fda95 fix #1959
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-20 20:17:09 -08:00
Nikolaj Bjorner
c95dbb47a3 fix #1958
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-20 16:43:37 -08:00
Nikolaj Bjorner
37ef3cbeb2 add rc2 sample
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-20 14:32:01 -08:00
Nikolaj Bjorner
7016d94d59 fix #1956
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-20 11:30:44 -08:00
Nikolaj Bjorner
9615974e76 add macz3 status
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-20 10:30:00 -08:00
Nikolaj Bjorner
656cdc4635 Merge branch 'master' of https://github.com/z3prover/z3 2018-11-20 10:29:03 -08:00
Nikolaj Bjorner
5a94cece2e add macz3 status
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-20 10:29:00 -08:00
Lev Nachmanson
67ea2a2c88 test
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2018-11-20 09:52:43 -08:00
Nikolaj Bjorner
9aaeb15d1a
Merge pull request #1954 from waywardmonkeys/fix-broken-link-in-docs
Fix broken link. It is Z3_add_rec_def, not Z3_mk_rec_def.
2018-11-20 04:02:49 -08:00
Bruce Mitchener
b93ffe676b Fix broken link. It is Z3_add_rec_def, not Z3_mk_rec_def. 2018-11-20 11:34:32 +07:00
Bruce Mitchener
edf8ba44d1 Switch from using Z3_bool to using bool.
This is a continuation of the work started by using stdbool and
continued by switching from Z3_TRUE|FALSE to true|false.
2018-11-20 11:27:09 +07:00
Nikolaj Bjorner
a076e33037 tweaks to mk_nuget_release
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-19 15:35:49 -08:00
Nikolaj Bjorner
76d0a5a6ed tweaks to mk_nuget_release
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-19 15:35:42 -08:00
Nikolaj Bjorner
e83e9b02df increment version number to 4.8.4
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-19 15:17:55 -08:00
Nikolaj Bjorner
7f5d66c3c2 updated release notes
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-19 12:21:17 -08:00
Nikolaj Bjorner
7d0d7e6343 have replayer handle oom natively
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-19 10:59:12 -08:00
Nikolaj Bjorner
04d709dae1 build errors on shrink
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-19 09:42:10 -08:00
Nikolaj Bjorner
5a825d7ac3 true is true, false is not true, it is false
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-19 09:37:23 -08:00
Nikolaj Bjorner
f21162960e
Merge pull request #1951 from waywardmonkeys/remove-z3-true-false-mostly
Remove usages of Z3_TRUE / Z3_FALSE.
2018-11-19 09:31:50 -08:00
Bruce Mitchener
56bbed173e Remove usages of Z3_TRUE / Z3_FALSE.
Now that this is all using stdbool.h, we can just use true/false.

For now, we leave the aliases in place in z3_api.h.
2018-11-20 00:25:37 +07:00
Nikolaj Bjorner
8b2450aba7
Merge pull request #1949 from waywardmonkeys/fix-doc-precondition
Fix precondition in Z3_get_symbol_string doc comment.
2018-11-19 08:43:52 -08:00
Nikolaj Bjorner
3eb786838d Merge branch 'master' of https://github.com/z3prover/z3 2018-11-19 08:42:23 -08:00
Nikolaj Bjorner
5eefa9c34b fix combinator signatures
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-19 08:42:18 -08:00
Nikolaj Bjorner
ce49e036aa
Merge pull request #1950 from waywardmonkeys/improve-doc-linking
Improve intra-doc linking.
2018-11-19 08:27:39 -08:00
Bruce Mitchener
115256e353 Improve intra-doc linking. 2018-11-19 20:32:00 +07:00
Bruce Mitchener
e1388a838c Fix precondition in Z3_get_symbol_string doc comment. 2018-11-19 18:58:09 +07:00
Nikolaj Bjorner
b8ac3e6ce4 Merge branch 'master' of https://github.com/z3prover/z3 2018-11-19 00:48:40 -08:00
Nikolaj Bjorner
529e62e01e remove unsound rewrite
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-19 00:48:33 -08:00
Nikolaj Bjorner
127b585eaa
Merge pull request #1947 from waywardmonkeys/fix-from-file-docs
Correct Z3_(fixedpoint|optimize)_from_file param doc.
2018-11-18 22:09:42 -08:00
Bruce Mitchener
93835eab05 Correct Z3_(fixedpoint|optimize)_from_file param doc. 2018-11-19 13:04:07 +07:00
Nikolaj Bjorner
5188f4d82e update dist scripts
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-18 10:55:59 -08:00
Nikolaj Bjorner
e438de4f8a Merge branch 'master' of https://github.com/z3prover/z3 2018-11-18 10:48:50 -08:00
Nikolaj Bjorner
ddf6d48b3e update unix-dist
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-18 10:48:45 -08:00
Nikolaj Bjorner
102d23f780 Merge branch 'master' of https://github.com/z3prover/z3 2018-11-18 10:40:14 -08:00
Nikolaj Bjorner
a9e6d83c6e std::cout -> out
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-18 10:40:08 -08:00
Nikolaj Bjorner
6ef2557e2a investigate #1946
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-18 09:34:33 -08:00
Nikolaj Bjorner
fb1287155e fix windows build_dist setting
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-18 08:59:27 -08:00
Nikolaj Bjorner
d400929d9a fix #1945
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-18 08:56:30 -08:00
Nikolaj Bjorner
1603075189 add empty/full to java #1944
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-17 15:46:06 -08:00
Nikolaj Bjorner
141cd687ff disable validation in builds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-17 15:37:36 -08:00
Nikolaj Bjorner
d45b8a3ac8 fix debug build, add access to numerics from model
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2018-11-17 15:24:54 -08:00