mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 10:19:23 +00:00
Code Activity
10128 commits 46 branches 52 tags 178 MiB
Commit graph

10128 commits

This branch
This branch
All branches
Author SHA1 Message Date
nilsbecker
165b256d32 ensure equalities between terms bound to quantified variables are always logged 2018-11-25 20:34:25 +01:00
nilsbecker
1e4f524a22 Merge branch 'master' of https://github.com/Z3Prover/z3 2018-11-25 16:58:09 +01:00
Nikolaj Bjorner
aa723f1eee fix uninitialized variable 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-24 18:13:35 -08:00
Nikolaj Bjorner
074ed0d874 fix warnings 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-24 17:39:19 -08:00
Nikolaj Bjorner
32df9b1155 mac build errors 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-24 17:34:53 -08:00
Nikolaj Bjorner
96043216e5 fix unsound unfolding 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-24 17:25:56 -08:00
Nikolaj Bjorner
6ddbc9cd38 overhaul of regular expression membership solving. Use iterative deepening and propagation, coallesce intersections 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-24 15:26:39 -08:00
Nikolaj Bjorner
d61d9d4ce3 remove reject states 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-24 11:06:51 -08:00
Nikolaj Bjorner
33eb82c25a remove prefix2prefix, fix #1566 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-23 23:36:47 -08:00
Nikolaj Bjorner
069949a576 fix model construction for semantics of itos 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-23 22:30:13 -08:00
Nikolaj Bjorner
20a28af225 fix stoi/itos axiom replay 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-23 21:42:48 -08:00
Nikolaj Bjorner
d55af41955 constrain lengths 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-23 19:54:34 -08:00
Nikolaj Bjorner
88fb826a03 overhaul stoi and itos to fix #1957 and related 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-23 18:50:20 -08:00
Nikolaj Bjorner
801026937d fix #1846 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-23 13:49:09 -08:00
Nikolaj Bjorner
8d940f64b8 fix build regression 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-23 10:57:07 -08:00
Nikolaj Bjorner
f5455ce2ac fix exception handling for #1959 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-22 15:40:08 -08:00
Nikolaj Bjorner
f591e0948a fix #1841 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2018-11-22 15:28:33 -08:00
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