mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 06:39:02 +00:00
Code Activity
8029 commits 23 branches 48 tags 157 MiB
Commit graph

8029 commits

This branch
This branch
All branches
Author SHA1 Message Date
Miguel Neves bdce957ac8 Merge branch 'opt' of https://github.com/NikolajBjorner/z3 into opt 2017-10-12 15:34:56 -07:00
Miguel Neves 611a13e8b3 Changed lookahead backtrack. Parent lookahead re-use fix 2017-10-12 14:34:42 -07:00
Nikolaj Bjorner 8b280b1f64 Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-12 14:34:13 -07:00
Nikolaj Bjorner 8cf0c94e5f address some ASan leaks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 14:34:04 -07:00
Nikolaj Bjorner 6ecd77d91c Merge branch 'master' of https://github.com/z3prover/z3 2017-10-12 14:17:57 -07:00
Nikolaj Bjorner 3554554533 command to exit tests early 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 14:17:52 -07:00
Nikolaj Bjorner d338fab4f6 fix #1305 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 13:58:14 -07:00
Nikolaj Bjorner 4adf4d4ac2 micro opt 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 12:08:54 -07:00
Nikolaj Bjorner 11f1a81d7b disable failing unit tests 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 10:12:37 -07:00
Nikolaj Bjorner 5afef07f40 remove traces of old n-ary representation, add checks 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 08:37:49 -07:00
Nikolaj Bjorner 6a09040a8e Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-12 07:39:38 -07:00
Nikolaj Bjorner da2b876acb fix #1303 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-12 07:39:27 -07:00
Nikolaj Bjorner 99b232a4c5 fix lookahead with ba extension 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-11 17:30:21 -07:00
Nikolaj Bjorner 81ad69214c fixing lookahead/ba + parallel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-11 17:06:28 -07:00
Nikolaj Bjorner 79ceaa1d13 fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-11 13:17:57 -07:00
Nikolaj Bjorner 8384ee18e2 Merge pull request #1301 from delcypher/fix_some_unit_test_leaks 
[ASan] Fix some leaks reported in the small object allocator test
 2017-10-11 19:47:57 +01:00
Dan Liew a3b109cc14 [ASan] Fix some leaks reported in the small object allocator 
test.
 2017-10-11 19:40:16 +01:00
Nikolaj Bjorner c093e6d4b9 harden a few API methods against longjumps in set_error. Memory leak exposed in #1297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-11 09:53:02 -07:00
Nikolaj Bjorner 97f37613c2 parallel 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-11 07:50:04 -07:00
Nikolaj Bjorner d2395ad897 merge with Miguel's fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-10 16:47:07 -07:00
Nikolaj Bjorner 1a6f8c2fad working on parallel solver 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-10 16:35:05 -07:00
Miguel Neves 01897831fb Dynamic delta trigger decrease 2017-10-10 15:59:53 -07:00
Nikolaj Bjorner 09ea370ea3 update C-example that fails to not use longjumps. Issue #1297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-10 12:06:19 -07:00
Nikolaj Bjorner 8b32c15ac9 use clause structure for nary 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-10 11:49:31 -07:00
Nikolaj Bjorner 7f693186a0 trying to address leak reported in #1297 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-10 07:10:04 -07:00
Nikolaj Bjorner a0cd6e0fca adding outline for parallel tactic 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-09 16:47:23 -07:00
Nikolaj Bjorner cae414e575 fixes for #1296, removing COMPILE_TIME_ASSERT 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-09 13:59:44 -07:00
Christoph M. Wintersteiger e0db65bb1d Merge branch 'master' of https://github.com/Z3Prover/z3 2017-10-09 19:18:46 +01:00
Christoph M. Wintersteiger 800fa3d246 Added bv_sort_ac=true to asserted_formulas::m_rewriter 2017-10-09 19:18:41 +01:00
Christoph M. Wintersteiger 5819e38606 whitespace 2017-10-09 19:17:44 +01:00
Nikolaj Bjorner 42de274307 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-09 07:49:20 -07:00
Nikolaj Bjorner 79b2a4f605 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-09 07:22:02 -07:00
Nikolaj Bjorner f85c02600f remove verificaiton code 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 16:07:58 -07:00
Nikolaj Bjorner f359f23885 another fix for #1288 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 15:47:06 -07:00
Nikolaj Bjorner 10e4235b4c bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 14:35:31 -07:00
Nikolaj Bjorner 356835533a clean up debug output 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 10:47:15 -07:00
Nikolaj Bjorner d2ec927844 fix build break 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 12:34:08 +01:00
Nikolaj Bjorner 06d75a616f fix #1288, again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 11:40:17 +01:00
Nikolaj Bjorner 22fa108ffd fix #1288, again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 11:07:22 +01:00
Nikolaj Bjorner 1371caace2 fix #1287, again 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 11:05:57 +01:00
Nikolaj Bjorner 52217f0600 fix #1290 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 10:56:05 +01:00
Nikolaj Bjorner c72b3356c1 fix #1286 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 10:41:02 +01:00
Nikolaj Bjorner 6f7f957a26 likely fix for #1287 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 10:38:02 +01:00
Nikolaj Bjorner a5ecf87ab8 fix #1288 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-08 10:32:38 +01:00
Nikolaj Bjorner c1b243a8e3 merge 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 19:24:30 +01:00
Nikolaj Bjorner 6b88446ee8 bug fixes 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 19:02:06 +01:00
Nikolaj Bjorner deba7d4d6e use idom for checking dominator relationships 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 14:35:44 +01:00
Nikolaj Bjorner b898b07795 distinguish simplify_rec from simplify immediate argument 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 11:12:09 +01:00
Nikolaj Bjorner 7e4f532202 fix build by including mk_pp 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
 2017-10-07 00:37:44 +01:00
Nikolaj Bjorner bbab4153be Merge branch 'master' of https://github.com/z3prover/z3 2017-10-07 00:21:24 +01:00