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

9031 commits

Author SHA1 Message Date
Nuno Lopes 94d2a16282 fix bug with use-after-move 2019-06-13 16:01:11 +01:00
Nuno Lopes d1cbde3390 fix crash in 'test-z3 prime_generator' 2019-06-13 14:35:52 +01:00
Nuno Lopes 38eeaeae7a memory_allocator: allocate mutex in global init since allocate() is called from API functions before memory initialization 2019-06-13 12:02:28 +01:00
Nuno Lopes cf3e649462 fix crash on Mac due to different destruction order of globals
the mutex in memory_manager has to be destroyed after all mem deallocations happen
2019-06-13 11:22:18 +01:00
Nikolaj Bjorner 2bee9a062f merge more from csp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-12 20:24:37 -07:00
Nikolaj Bjorner e0d8cefde4 remove cooperate
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-12 20:15:46 -07:00
Nikolaj Bjorner 42ac3a5363 merge with csp
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-12 19:48:45 -07:00
Nikolaj Bjorner 9566d379d6 merge
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-12 19:44:56 -07:00
Nikolaj Bjorner 1ff08c45ce model
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-12 19:36:25 -07:00
Nikolaj Bjorner bd109c4522 fix memory leak when using prime_generator as non-static object
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-12 11:14:25 -07:00
Nikolaj Bjorner 5663aa0b16 double free
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-12 09:13:22 -07:00
Nikolaj Bjorner 8d3dfd36b2 initialize/finalize cooperate at top-level
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-12 02:37:24 -07:00
Nuno Lopes 04a2cce830 don't use thread-local storage if running a single thread 2019-06-12 09:59:19 +01:00
Nikolaj Bjorner 5c05b62025 deallocate mux, fix script
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-12 01:41:14 -07:00
Nikolaj Bjorner 921a574074 mutex allocation #2336
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-11 19:50:48 -07:00
Nikolaj Bjorner 71c38a08e5 add initialization
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-11 19:28:08 -07:00
Nikolaj Bjorner 583098b8b0 throttle som blowup by default factor of 10
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-11 17:11:54 -07:00
Lev Nachmanson 14ff768a63 limit the size of bit vectors
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
2019-06-11 16:40:54 -07:00
Nikolaj Bjorner 7bfb730fee fix traffic jam
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-10 17:45:55 -07:00
Audrey Dutcher 6fa85ad654 Allow building python wheels with binaries from a prebuilt release 2019-06-10 16:23:26 -07:00
Christoph M. Wintersteiger 998b0ff7f4
Fixed corner-case in fp.rem encoding. Fixes #2289. 2019-06-07 18:03:51 +01:00
Nikolaj Bjorner 7255edf216 remove new_sub
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-06 17:13:59 -07:00
Nikolaj Bjorner 44b0b0148b deal with warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-06 17:13:38 -07:00
Nikolaj Bjorner e731a44880
Merge pull request #2329 from Z3Prover/nomp
Nomp
2019-06-07 02:05:11 +02:00
Nikolaj Bjorner 82da3493ee fix printing of recursive defs
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-06 13:11:46 -07:00
Nikolaj Bjorner 71009a9d02 suspend limits during assert and macro expansion
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-06 11:07:57 -07:00
Nikolaj Bjorner 7c1e935bc2 rlimit mux
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 22:17:09 -07:00
Nikolaj Bjorner fdfb9e4fd5 Merge branch 'master' of https://github.com/z3prover/z3 2019-06-05 16:10:31 -07:00
Nikolaj Bjorner aabc54409c change printing directires
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 16:10:22 -07:00
Nikolaj Bjorner a8b02ddb93 fix #2323
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 13:43:45 -07:00
Nikolaj Bjorner 1ca3381390 fix #2319
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 09:42:19 -07:00
Nuno Lopes a53ff6f21c turn locks into no-ops when compiled with -DSINGLE_THREAD 2019-06-05 12:11:27 +01:00
Nuno Lopes 9b375150eb remove remaining _NO_OMP_ 2019-06-05 10:07:16 +01:00
Nuno Lopes 37882f5afa fix race condition in cooperate 2019-06-05 09:31:45 +01:00
Nikolaj Bjorner 7f74382863 capture i by value
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 09:06:18 +01:00
Nikolaj Bjorner 27971e3f68 exception behavior in C++11 threads?
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 09:06:17 +01:00
Nikolaj Bjorner 9f3089b098 try with std::vector and ptr_vectors
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 09:06:17 +01:00
Nikolaj Bjorner e4e60bff26 include thread in tactical
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 09:06:17 +01:00
Nikolaj Bjorner f5511b4174 missing include
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 09:06:17 +01:00
Nikolaj Bjorner 1f84381c4c pfor
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 09:06:17 +01:00
Nikolaj Bjorner 59330b3855 pfor
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 09:06:17 +01:00
Nikolaj Bjorner 9262908ebb mux
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-05 09:06:17 +01:00
Nikolaj Bjorner 2788f72bbb don't lose equalities over ite, #2317
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
2019-06-04 20:32:24 -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
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